Unrestricted depth-three lower bound: marker mixture

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

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

noncomputable def Complexity.DepthThreeLowerBound.markerSelected {I : Type u} [Fintype I] (c : ℕ) (π : Equiv.Perm (I ⊕ Fin c)) : Finset I

Determine which clause object is selected by a marker sample.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_markerSelected {I : Type u} [Fintype I] (c : ℕ) (π : Equiv.Perm (I ⊕ Fin c)) (i : I) : i ∈ markerSelected c π ↔ ∀ (m : Fin c), permutationRank π (Sum.inl i) < permutationRank π (Sum.inr m)

noncomputable def Complexity.DepthThreeLowerBound.markerSample {I : Type u} [Fintype I] [instDecidableEqI : DecidableEq I] {A : Type v} (C : I → A → Bool) (c : ℕ) (π : Equiv.Perm (I ⊕ Fin c)) (x : A) : Bool

Sample a marker from its permutation-based distribution.

Equations

• Complexity.DepthThreeLowerBound.markerSample C c π x = decide (∀ i ∈ Complexity.DepthThreeLowerBound.markerSelected c π, C i x = true)

@[simp]

theorem Complexity.DepthThreeLowerBound.markerSample_eq_true {I : Type u} [Fintype I] [instDecidableEqI : DecidableEq I] {A : Type v} (C : I → A → Bool) (c : ℕ) (π : Equiv.Perm (I ⊕ Fin c)) (x : A) : markerSample C c π x = true ↔ ∀ i ∈ markerSelected c π, C i x = true

def Complexity.DepthThreeLowerBound.markerBad {I : Type u} [Fintype I] {A : Type v} (C : I → A → Bool) (x : A) : Finset I

The event that a marker sample fails the prescribed selection condition.

Equations

• Complexity.DepthThreeLowerBound.markerBad C x = {i : I | C i x = false}

def Complexity.DepthThreeLowerBound.markerActive {I : Type u} [Fintype I] {A : Type v} (C : I → A → Bool) (x : A) (c : ℕ) : Finset (I ⊕ Fin c)

The event that the sampled marker is active.

Equations

• Complexity.DepthThreeLowerBound.markerActive C x c = (Complexity.DepthThreeLowerBound.markerBad C x).disjSum Finset.univ

def Complexity.DepthThreeLowerBound.markerObjects {I : Type u} (c : ℕ) : Finset (I ⊕ Fin c)

The objects indexed by the marker construction.

Equations

• Complexity.DepthThreeLowerBound.markerObjects c = ∅.disjSum Finset.univ

theorem Complexity.DepthThreeLowerBound.markerActive_nonempty {I : Type u} [Fintype I] {A : Type v} (C : I → A → Bool) (x : A) {c : ℕ} (hc : 0 < c) : (markerActive C x c).Nonempty

theorem Complexity.DepthThreeLowerBound.markerObjects_subset {I : Type u} [Fintype I] {A : Type v} (C : I → A → Bool) (x : A) (c : ℕ) : markerObjects c ⊆ markerActive C x c

theorem Complexity.DepthThreeLowerBound.markerSample_iff_first_marker {I : Type u} [Fintype I] [instDecidableEqI : DecidableEq I] {A : Type v} (C : I → A → Bool) (x : A) {c : ℕ} (hc : 0 < c) (π : Equiv.Perm (I ⊕ Fin c)) : markerSample C c π x = true ↔ ∃ s ∈ markerObjects c, IsFirst (markerActive C x c) π s

theorem Complexity.DepthThreeLowerBound.marker_mixture_ratio {I : Type u} [Fintype I] [instDecidableEqI : DecidableEq I] {A : Type v} (C : I → A → Bool) (x : A) {c : ℕ} (hc : 0 < c) : (finiteAvg fun (π : Equiv.Perm (I ⊕ Fin c)) => indicator (markerSample C c π x)) = ↑c / (↑c + ↑(markerBad C x).card)

theorem Complexity.DepthThreeLowerBound.markerSample_of_all_true {I : Type u} [Fintype I] [instDecidableEqI : DecidableEq I] {A : Type v} (C : I → A → Bool) (x : A) (c : ℕ) (π : Equiv.Perm (I ⊕ Fin c)) (hC : ∀ (i : I), C i x = true) : markerSample C c π x = true

theorem Complexity.DepthThreeLowerBound.markerSample_of_isEmpty {I : Type u} [Fintype I] [instDecidableEqI : DecidableEq I] {A : Type v} [IsEmpty I] (C : I → A → Bool) (x : A) (c : ℕ) (π : Equiv.Perm (I ⊕ Fin c)) : markerSample C c π x = true

theorem Complexity.DepthThreeLowerBound.marker_product_mixture_ratio {A : Type v} {H : Type uDepth1} [Fintype H] [DecidableEq H] {J : H → Type uDepth2} [(h : H) → Fintype (J h)] [(h : H) → DecidableEq (J h)] (C : (h : H) → J h → A → Bool) (c : H → ℕ) (hc : ∀ (h : H), 0 < c h) (x : A) : (finiteAvg fun (π : (h : H) → Equiv.Perm (J h ⊕ Fin (c h))) => ∏ h : H, indicator (markerSample (C h) (c h) (π h) x)) = ∏ h : H, ↑(c h) / (↑(c h) + ↑(markerBad (C h) x).card)