Unrestricted depth-three lower bound: restriction probability

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

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

def Complexity.DepthThreeLowerBound.liveSet {V : Type uDepth1} [instFintypeV : Fintype V] (σ : Restriction V) : Finset V

The finite set of coordinates left live by a restriction.

Equations

• Complexity.DepthThreeLowerBound.liveSet σ = {v : V | σ v = none}

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_liveSet {V : Type uDepth1} [instFintypeV : Fintype V] (σ : Restriction V) (v : V) : v ∈ liveSet σ ↔ σ v = none

def Complexity.DepthThreeLowerBound.maskRestriction {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (T : Finset V) (y : Cube V) : Restriction V

Build a restriction from a live-coordinate mask and fixed bits.

Equations

• Complexity.DepthThreeLowerBound.maskRestriction T y v = if v ∈ T then none else some (y v)

@[simp]

theorem Complexity.DepthThreeLowerBound.maskRestriction_live {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (T : Finset V) (y : Cube V) (v : V) (hv : v ∈ T) : maskRestriction T y v = none

@[simp]

theorem Complexity.DepthThreeLowerBound.maskRestriction_fixed {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (T : Finset V) (y : Cube V) (v : V) (hv : v ∉ T) : maskRestriction T y v = some (y v)

@[simp]

theorem Complexity.DepthThreeLowerBound.liveSet_maskRestriction {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (T : Finset V) (y : Cube V) : liveSet (maskRestriction T y) = T

@[simp]

theorem Complexity.DepthThreeLowerBound.fill_maskRestriction {V : Type uDepth1} [instDecidableEqV : DecidableEq V] (T : Finset V) (y : Cube V) : (fill (maskRestriction T y) fun (v : Live (maskRestriction T y)) => y ↑v) = y

@[simp]

theorem Complexity.DepthThreeLowerBound.maskRestriction_fill {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (σ : Restriction V) (z : Cube (Live σ)) : maskRestriction (liveSet σ) (fill σ z) = σ

def Complexity.DepthThreeLowerBound.restrictionCoordinates {V : Type uDepth1} [instFintypeV : Fintype V] (s : (σ : Restriction V) × Cube (Live σ)) : Finset V × Cube V

Decompose a restriction into its mask and fixed assignments.

Equations

• Complexity.DepthThreeLowerBound.restrictionCoordinates s = (Complexity.DepthThreeLowerBound.liveSet s.fst, Complexity.DepthThreeLowerBound.fill s.fst s.snd)

theorem Complexity.DepthThreeLowerBound.restrictionCoordinates_injective {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] : Function.Injective restrictionCoordinates

theorem Complexity.DepthThreeLowerBound.restrictionCoordinates_surjective {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] : Function.Surjective restrictionCoordinates

noncomputable def Complexity.DepthThreeLowerBound.restrictionCoordinatesEquiv {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] : (σ : Restriction V) × Cube (Live σ) ≃ Finset V × Cube V

Identify restrictions with their masks and fixed-coordinate assignments.

Equations

• Complexity.DepthThreeLowerBound.restrictionCoordinatesEquiv = Equiv.ofBijective Complexity.DepthThreeLowerBound.restrictionCoordinates ⋯

@[simp]

theorem Complexity.DepthThreeLowerBound.restrictionCoordinatesEquiv_apply {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (s : (σ : Restriction V) × Cube (Live σ)) : restrictionCoordinatesEquiv s = (liveSet s.fst, fill s.fst s.snd)

@[simp]

theorem Complexity.DepthThreeLowerBound.card_live_maskRestriction {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (T : Finset V) (y : Cube V) : Fintype.card (Live (maskRestriction T y)) = T.card

theorem Complexity.DepthThreeLowerBound.restrictionWeight_maskRestriction {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (p : ℝ) (T : Finset V) (y : Cube V) : restrictionWeight p (maskRestriction T y) = p ^ T.card * ((1 - p) / 2) ^ (Fintype.card V - T.card)

theorem Complexity.DepthThreeLowerBound.restriction_mask_joint_weight {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (p : ℝ) (T : Finset V) (y : Cube V) : restrictionWeight p (maskRestriction T y) * (↑(Fintype.card (Cube (Live (maskRestriction T y)))))⁻¹ = bernoulliWeight p T * (↑(Fintype.card (Cube V)))⁻¹

theorem Complexity.DepthThreeLowerBound.restriction_fill_joint_weight {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (p : ℝ) (σ : Restriction V) (z : Cube (Live σ)) : restrictionWeight p σ * (↑(Fintype.card (Cube (Live σ))))⁻¹ = bernoulliWeight p (liveSet σ) * (↑(Fintype.card (Cube V)))⁻¹

theorem Complexity.DepthThreeLowerBound.restrictionAvg_fill_coupling {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (p : ℝ) (F : Restriction V → Cube V → ℝ) : (restrictionAvg p fun (σ : Restriction V) => finiteAvg fun (z : Cube (Live σ)) => F σ (fill σ z)) = ∑ T : Finset V, bernoulliWeight p T * finiteAvg fun (y : Cube V) => F (maskRestriction T y) y

theorem Complexity.DepthThreeLowerBound.restrictionAvg_fill_reweight {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (p : ℝ) (F : Restriction V → Cube V → ℝ) : (restrictionAvg p fun (σ : Restriction V) => finiteAvg fun (z : Cube (Live σ)) => F σ (fill σ z)) = finiteAvg fun (y : Cube V) => ∑ T : Finset V, bernoulliWeight p T * F (maskRestriction T y) y

theorem Complexity.DepthThreeLowerBound.restrictionAvg_fill {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (p : ℝ) (F : Cube V → ℝ) : (restrictionAvg p fun (σ : Restriction V) => finiteAvg fun (z : Cube (Live σ)) => F (fill σ z)) = finiteAvg F

theorem Complexity.DepthThreeLowerBound.restrictionAvg_mask_sampler {V : Type uDepth1} [instFintypeV : Fintype V] [instDecidableEqV : DecidableEq V] (p : ℝ) (F : Restriction V → ℝ) : restrictionAvg p F = ∑ T : Finset V, bernoulliWeight p T * finiteAvg fun (y : Cube V) => F (maskRestriction T y)