Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.MomentBounds

Unrestricted depth-three lower bound: moment bounds #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/MomentBounds.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.UniformBitsUpTo {Ω : Type uDepth1} {Z : Type uDepth2} [Fintype Ω] [DecidableEq Z] (t : ℕ) (bits : Ω → Z → Bool) :
Prop

Every collection of at most the specified number of bits is uniform.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Complexity.DepthThreeLowerBound.sign_not (b : Bool) :
    (sign !b) = -sign b
    source
    theorem Complexity.DepthThreeLowerBound.abs_sign_mul_indicator_le_one (b c : Bool) :
    |sign b * indicator c| ≤ 1
    source
    def Complexity.DepthThreeLowerBound.flipCoordinate {A : Type uDepth3} [DecidableEq A] (a₀ : A) :
    (A → Bool) ≃ (A → Bool)

    Flip one coordinate of a Boolean assignment.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Complexity.DepthThreeLowerBound.uniform_product_zero_of_singleton {A : Type uDepth4} {I : Type uDepth5} [Fintype A] [DecidableEq A] [Fintype I] [DecidableEq I] (a : I → A) (w : I → ℝ) (i₀ : I) (hunique : ∀ (i : I), a i = a i₀ → i = i₀) :
      (finiteAvg fun (x : A → Bool) => ∏ i : I, sign (x (a i)) * w i) = 0
      source
      theorem Complexity.DepthThreeLowerBound.tuple_product_avg_zero {Ω : Type uDepth6} {Z : Type uDepth7} [Fintype Ω] [DecidableEq Z] {t : ℕ} (bits : Ω → Z → Bool) (hdist : UniformBitsUpTo t bits) (a : Fin t → Z) (w : Fin t → ℝ) (hns : ¬TupleNoSingleton a) :
      (finiteAvg fun (ω : Ω) => ∏ i : Fin t, sign (bits ω (a i)) * w i) = 0
      source
      theorem Complexity.DepthThreeLowerBound.sign_indicator_product_le_one {I : Type uDepth8} [Fintype I] (b c : I → Bool) :
      ∏ i : I, sign (b i) * indicator (c i) ≤ 1
      source
      theorem Complexity.DepthThreeLowerBound.even_moment_le {Ω : Type uDepth9} {Z : Type uDepth10} [Fintype Ω] [Nonempty Ω] [Fintype Z] [Nonempty Z] [DecidableEq Z] (h : ℕ) (bits : Ω → Z → Bool) (hdist : UniformBitsUpTo (2 * h) bits) (J : Z → Bool) :
      (finiteAvg fun (ω : Ω) => |∑ z : Z, sign (bits ω z) * indicator (J z)| ^ (2 * h)) ≤ ↑(Fintype.card Z) ^ h * ↑h ^ (2 * h)
      source
      theorem Complexity.DepthThreeLowerBound.even_moment_le_manuscript {Ω : Type uDepth11} {Z : Type uDepth12} [Fintype Ω] [Nonempty Ω] [Fintype Z] [Nonempty Z] [DecidableEq Z] (h : ℕ) (bits : Ω → Z → Bool) (hdist : UniformBitsUpTo (2 * h) bits) (J : Z → Bool) :
      (finiteAvg fun (ω : Ω) => |∑ z : Z, sign (bits ω z) * indicator (J z)| ^ (2 * h)) ≤ ↑(2 * h) ^ (2 * h) * ↑(Fintype.card Z) ^ h