Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.ReversePathWeights

Unrestricted depth-three lower bound: reverse path weights #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/ReversePathWeights.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

source
def Complexity.DepthThreeLowerBound.bernoulliWeight {V : Type uDepth1} [Fintype V] (p : ℝ) (R : Finset V) :
ℝ

The product Bernoulli weight of a selected coordinate set.

Equations
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.bernoulliWeight_nonneg {V : Type uDepth1} [Fintype V] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (R : Finset V) :
    0 ≤ bernoulliWeight p R
    source
    theorem Complexity.DepthThreeLowerBound.bernoulliWeight_pos {V : Type uDepth1} [Fintype V] {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (R : Finset V) :
    0 < bernoulliWeight p R
    source
    theorem Complexity.DepthThreeLowerBound.sum_bernoulliWeight {V : Type uDepth1} [Fintype V] (p : ℝ) :
    ∑ R : Finset V, bernoulliWeight p R = 1
    source
    theorem Complexity.DepthThreeLowerBound.bernoulliWeight_disjoint_balance {V : Type uDepth1} [Fintype V] [DecidableEq V] (p : ℝ) (R D : Finset V) (hRD : Disjoint R D) :
    bernoulliWeight p (R ∪ D) * (1 - p) ^ D.card = bernoulliWeight p R * p ^ D.card
    source
    theorem Complexity.DepthThreeLowerBound.bernoulliWeight_disjoint_union {V : Type uDepth1} [Fintype V] [DecidableEq V] {p : ℝ} (_hp0 : 0 < p) (hp1 : p < 1) (R D : Finset V) (hRD : Disjoint R D) :
    bernoulliWeight p (R ∪ D) * 2 ^ D.card = bernoulliWeight p R * (2 * p / (1 - p)) ^ D.card