Unrestricted depth-three lower bound: finite probability

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

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

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.Restriction (V : Type uDepth1) : Type uDepth1

A partial Boolean assignment; none denotes a live variable.

Equations

• Complexity.DepthThreeLowerBound.Restriction V = (V → Option Bool)

@[reducible, inline]

abbrev Complexity.DepthThreeLowerBound.Live {V : Type uDepth2} (σ : Restriction V) : Type uDepth2

Variables left unfixed by a restriction.

Equations

• Complexity.DepthThreeLowerBound.Live σ = { v : V // σ v = none }

def Complexity.DepthThreeLowerBound.fill {V : Type uDepth3} (σ : Restriction V) (z : Cube (Live σ)) : Cube V

Extend an assignment on live variables by the fixed coordinates.

Equations

• Complexity.DepthThreeLowerBound.fill σ z v = if h : σ v = none then z ⟨v, h⟩ else (σ v).getD false

@[simp]

theorem Complexity.DepthThreeLowerBound.fill_live {V : Type uDepth4} (σ : Restriction V) (z : Cube (Live σ)) (v : Live σ) : fill σ z ↑v = z v

@[simp]

theorem Complexity.DepthThreeLowerBound.fill_fixed {V : Type uDepth5} (σ : Restriction V) (z : Cube (Live σ)) (v : V) (b : Bool) (h : σ v = some b) : fill σ z v = b

noncomputable def Complexity.DepthThreeLowerBound.finiteAvg {Ω : Type uDepth6} [Fintype Ω] (f : Ω → ℝ) : ℝ

Uniform average over a finite type, with value zero on the empty type.

Equations

• Complexity.DepthThreeLowerBound.finiteAvg f = (↑(Fintype.card Ω))⁻¹ * ∑ ω : Ω, f ω

theorem Complexity.DepthThreeLowerBound.finiteAvg_congr {Ω : Type uDepth7} [Fintype Ω] {f g : Ω → ℝ} (h : ∀ (ω : Ω), f ω = g ω) : finiteAvg f = finiteAvg g

@[simp]

theorem Complexity.DepthThreeLowerBound.finiteAvg_zero {Ω : Type uDepth7} [Fintype Ω] : (finiteAvg fun (x : Ω) => 0) = 0

theorem Complexity.DepthThreeLowerBound.finiteAvg_add {Ω : Type uDepth7} [Fintype Ω] (f g : Ω → ℝ) : (finiteAvg fun (ω : Ω) => f ω + g ω) = finiteAvg f + finiteAvg g

theorem Complexity.DepthThreeLowerBound.finiteAvg_sub {Ω : Type uDepth7} [Fintype Ω] (f g : Ω → ℝ) : (finiteAvg fun (ω : Ω) => f ω - g ω) = finiteAvg f - finiteAvg g

theorem Complexity.DepthThreeLowerBound.finiteAvg_const_mul {Ω : Type uDepth7} [Fintype Ω] (c : ℝ) (f : Ω → ℝ) : (finiteAvg fun (ω : Ω) => c * f ω) = c * finiteAvg f

theorem Complexity.DepthThreeLowerBound.finiteAvg_mul_const {Ω : Type uDepth7} [Fintype Ω] (f : Ω → ℝ) (c : ℝ) : (finiteAvg fun (ω : Ω) => f ω * c) = finiteAvg f * c

theorem Complexity.DepthThreeLowerBound.finiteAvg_sum {Ω : Type uDepth7} [Fintype Ω] {ι : Type uDepth9} (s : Finset ι) (f : ι → Ω → ℝ) : (finiteAvg fun (ω : Ω) => ∑ i ∈ s, f i ω) = ∑ i ∈ s, finiteAvg (f i)

theorem Complexity.DepthThreeLowerBound.finiteAvg_nonneg {Ω : Type uDepth7} [Fintype Ω] {f : Ω → ℝ} (h : ∀ (ω : Ω), 0 ≤ f ω) : 0 ≤ finiteAvg f

theorem Complexity.DepthThreeLowerBound.finiteAvg_mono {Ω : Type uDepth7} [Fintype Ω] {f g : Ω → ℝ} (h : ∀ (ω : Ω), f ω ≤ g ω) : finiteAvg f ≤ finiteAvg g

theorem Complexity.DepthThreeLowerBound.finiteAvg_abs_le {Ω : Type uDepth7} [Fintype Ω] (f : Ω → ℝ) : |finiteAvg f| ≤ finiteAvg fun (ω : Ω) => |f ω|

@[simp]

theorem Complexity.DepthThreeLowerBound.finiteAvg_const {Ω : Type uDepth7} [Fintype Ω] [Nonempty Ω] (c : ℝ) : (finiteAvg fun (x : Ω) => c) = c

theorem Complexity.DepthThreeLowerBound.finiteAvg_equiv {Ω : Type uDepth7} {Λ : Type uDepth8} [Fintype Ω] [Fintype Λ] (e : Ω ≃ Λ) (f : Λ → ℝ) : (finiteAvg fun (ω : Ω) => f (e ω)) = finiteAvg f

theorem Complexity.DepthThreeLowerBound.finiteAvg_comm {Ω : Type uDepth7} {Λ : Type uDepth8} [Fintype Ω] [Fintype Λ] (f : Ω → Λ → ℝ) : (finiteAvg fun (ω : Ω) => finiteAvg (f ω)) = finiteAvg fun (l : Λ) => finiteAvg fun (ω : Ω) => f ω l

theorem Complexity.DepthThreeLowerBound.finiteAvg_product {Ω : Type uDepth7} {Λ : Type uDepth8} [Fintype Ω] [Fintype Λ] (f : Ω × Λ → ℝ) : finiteAvg f = finiteAvg fun (ω : Ω) => finiteAvg fun (l : Λ) => f (ω, l)

theorem Complexity.DepthThreeLowerBound.finiteAvg_pi_prod {ι : Type uDepth10} [Fintype ι] {κ : ι → Type uDepth21} [(i : ι) → Fintype (κ i)] (f : (i : ι) → κ i → ℝ) : (finiteAvg fun (x : (i : ι) → κ i) => ∏ i : ι, f i (x i)) = ∏ i : ι, finiteAvg (f i)

noncomputable def Complexity.DepthThreeLowerBound.restrictionCoordinateWeight (p : ℝ) : Option Bool → ℝ

Weight a live coordinate by p and each fixed bit by (1 - p) / 2.

Equations

• Complexity.DepthThreeLowerBound.restrictionCoordinateWeight p none = p
• Complexity.DepthThreeLowerBound.restrictionCoordinateWeight p (some val) = (1 - p) / 2

noncomputable def Complexity.DepthThreeLowerBound.restrictionWeight {V : Type uDepth11} [Fintype V] (p : ℝ) (σ : Restriction V) : ℝ

Product weight of an independently sampled random restriction.

Equations

• Complexity.DepthThreeLowerBound.restrictionWeight p σ = ∏ v : V, Complexity.DepthThreeLowerBound.restrictionCoordinateWeight p (σ v)

noncomputable def Complexity.DepthThreeLowerBound.restrictionAvg {V : Type uDepth12} [Fintype V] (p : ℝ) (F : Restriction V → ℝ) : ℝ

Expectation with respect to the product distribution of restrictions.

Equations

• Complexity.DepthThreeLowerBound.restrictionAvg p F = ∑ σ : Complexity.DepthThreeLowerBound.Restriction V, Complexity.DepthThreeLowerBound.restrictionWeight p σ * F σ

theorem Complexity.DepthThreeLowerBound.restrictionCoordinateWeight_sum (p : ℝ) : ∑ a : Option Bool, restrictionCoordinateWeight p a = 1

theorem Complexity.DepthThreeLowerBound.restrictionCoordinateWeight_nonneg {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (a : Option Bool) : 0 ≤ restrictionCoordinateWeight p a

theorem Complexity.DepthThreeLowerBound.restrictionWeight_nonneg {V : Type uDepth13} [Fintype V] {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (σ : Restriction V) : 0 ≤ restrictionWeight p σ

@[simp]

theorem Complexity.DepthThreeLowerBound.restrictionWeight_sum {V : Type uDepth14} [Fintype V] (p : ℝ) : ∑ σ : Restriction V, restrictionWeight p σ = 1

@[simp]

theorem Complexity.DepthThreeLowerBound.restrictionAvg_const {V : Type uDepth15} [Fintype V] (p c : ℝ) : (restrictionAvg p fun (x : Restriction V) => c) = c

theorem Complexity.DepthThreeLowerBound.restrictionAvg_nonneg {V : Type uDepth16} [Fintype V] {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) {F : Restriction V → ℝ} (hF : ∀ (σ : Restriction V), 0 ≤ F σ) : 0 ≤ restrictionAvg p F

theorem Complexity.DepthThreeLowerBound.restrictionAvg_mono {V : Type uDepth17} [Fintype V] {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) {F G : Restriction V → ℝ} (h : ∀ (σ : Restriction V), F σ ≤ G σ) : restrictionAvg p F ≤ restrictionAvg p G

theorem Complexity.DepthThreeLowerBound.restrictionAvg_add {V : Type uDepth18} [Fintype V] (p : ℝ) (F G : Restriction V → ℝ) : (restrictionAvg p fun (σ : Restriction V) => F σ + G σ) = restrictionAvg p F + restrictionAvg p G

theorem Complexity.DepthThreeLowerBound.restrictionAvg_const_mul {V : Type uDepth19} [Fintype V] (p c : ℝ) (F : Restriction V → ℝ) : (restrictionAvg p fun (σ : Restriction V) => c * F σ) = c * restrictionAvg p F

theorem Complexity.DepthThreeLowerBound.restrictionAvg_abs_le {V : Type uDepth20} [Fintype V] {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (F : Restriction V → ℝ) : |restrictionAvg p F| ≤ restrictionAvg p fun (σ : Restriction V) => |F σ|