Unrestricted depth-three lower bound: reverse path recurrence

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

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

def Complexity.DepthThreeLowerBound.reverseEligible {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] (scope : I → Finset V) (violation : I → Bool) (R : Finset V) : Finset I

The eligible choices at a reverse reconstruction step.

Equations

• Complexity.DepthThreeLowerBound.reverseEligible scope violation R = {i : I | violation i = true ∧ Disjoint (scope i) R}

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_reverseEligible {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] (scope : I → Finset V) (violation : I → Bool) (R : Finset V) (i : I) : i ∈ reverseEligible scope violation R ↔ violation i = true ∧ Disjoint (scope i) R

def Complexity.DepthThreeLowerBound.reverseBlocks {V : Type uDepth1} (b : ℕ) (E : Finset V) : Finset (Finset V)

Coordinate blocks available to the reverse reconstruction.

Equations

• Complexity.DepthThreeLowerBound.reverseBlocks b E = {D ∈ E.powerset | b < D.card}

@[simp]

theorem Complexity.DepthThreeLowerBound.mem_reverseBlocks {V : Type uDepth1} (b : ℕ) (E D : Finset V) : D ∈ reverseBlocks b E ↔ D ⊆ E ∧ b < D.card

def Complexity.DepthThreeLowerBound.ReverseChoice {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] (b : ℕ) (scope : I → Finset V) (violation : I → Bool) (R : Finset V) (i : I) (D : Finset V) : Prop

A block and associated data selected during reverse reconstruction.

Equations

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

theorem Complexity.DepthThreeLowerBound.ReverseChoice.disjoint {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] {b : ℕ} {scope : I → Finset V} {violation : I → Bool} {R : Finset V} {i : I} {D : Finset V} (h : ReverseChoice b scope violation R i D) : Disjoint R D

theorem Complexity.DepthThreeLowerBound.ReverseChoice.eligible_card_pos {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] {b : ℕ} {scope : I → Finset V} {violation : I → Bool} {R : Finset V} {i : I} {D : Finset V} (h : ReverseChoice b scope violation R i D) : 0 < (reverseEligible scope violation R).card

noncomputable def Complexity.DepthThreeLowerBound.reverseChoiceWeight {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] (α : ℝ) (scope : I → Finset V) (violation : I → Bool) (R D : Finset V) : ℝ

The weight assigned to a reverse reconstruction choice.

Equations

• Complexity.DepthThreeLowerBound.reverseChoiceWeight α scope violation R D = α ^ D.card / ↑(Complexity.DepthThreeLowerBound.reverseEligible scope violation R).card

theorem Complexity.DepthThreeLowerBound.reverseChoiceWeight_nonneg {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] {α : ℝ} (hα : 0 ≤ α) (scope : I → Finset V) (violation : I → Bool) (R D : Finset V) : 0 ≤ reverseChoiceWeight α scope violation R D

def Complexity.DepthThreeLowerBound.reverseTheta (α : ℝ) (b k : ℕ) : ℝ

The scalar controlling a reverse reconstruction step.

Equations

• Complexity.DepthThreeLowerBound.reverseTheta α b k = ∑ l ∈ Finset.range (k + 1), if b < l then ↑(k.choose l) * α ^ l else 0

theorem Complexity.DepthThreeLowerBound.reverseTheta_nonneg {α : ℝ} (hα : 0 ≤ α) (b k : ℕ) : 0 ≤ reverseTheta α b k

def Complexity.DepthThreeLowerBound.reverseBlockMass {V : Type uDepth1} (α : ℝ) (b : ℕ) (E : Finset V) : ℝ

Total weight assigned to one reverse reconstruction block.

Equations

• Complexity.DepthThreeLowerBound.reverseBlockMass α b E = ∑ D ∈ Complexity.DepthThreeLowerBound.reverseBlocks b E, α ^ D.card

theorem Complexity.DepthThreeLowerBound.reverseBlockMass_nonneg {V : Type uDepth1} {α : ℝ} (hα : 0 ≤ α) (b : ℕ) (E : Finset V) : 0 ≤ reverseBlockMass α b E

theorem Complexity.DepthThreeLowerBound.reverseBlockMass_eq_theta {V : Type uDepth1} (α : ℝ) (b : ℕ) (E : Finset V) : reverseBlockMass α b E = reverseTheta α b E.card

theorem Complexity.DepthThreeLowerBound.reverseTheta_mono_width {α : ℝ} (hα : 0 ≤ α) (b : ℕ) {e k : ℕ} (hek : e ≤ k) : reverseTheta α b e ≤ reverseTheta α b k

theorem Complexity.DepthThreeLowerBound.reverseBlockMass_le_theta {V : Type uDepth1} {α : ℝ} (hα : 0 ≤ α) (b : ℕ) (E : Finset V) {k : ℕ} (hE : E.card ≤ k) : reverseBlockMass α b E ≤ reverseTheta α b k

noncomputable def Complexity.DepthThreeLowerBound.reverseOneStep {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] (α : ℝ) (b : ℕ) (scope : I → Finset V) (violation : I → Bool) (R : Finset V) : ℝ

Sum of the weighted one-step reverse choices.

Equations

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

theorem Complexity.DepthThreeLowerBound.sum_reverseBlockMass_le {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] {α : ℝ} (hα : 0 ≤ α) (b k : ℕ) (scope : I → Finset V) (hscope : ∀ (i : I), (scope i).card ≤ k) (violation : I → Bool) (R : Finset V) : ∑ i ∈ reverseEligible scope violation R, reverseBlockMass α b (scope i) ≤ ↑(reverseEligible scope violation R).card * reverseTheta α b k

theorem Complexity.DepthThreeLowerBound.reverseOneStep_le_theta {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] {α : ℝ} (hα : 0 ≤ α) (b k : ℕ) (scope : I → Finset V) (hscope : ∀ (i : I), (scope i).card ≤ k) (violation : I → Bool) (R : Finset V) : reverseOneStep α b scope violation R ≤ reverseTheta α b k

def Complexity.DepthThreeLowerBound.reverseTotal {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] (α : ℝ) (b : ℕ) (scope : I → Finset V) (violation : I → Bool) : ℕ → Finset V → ℝ

Total weight of reverse reconstructions of the specified length.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DepthThreeLowerBound.reverseTotal α b scope violation 0 x✝ = 1

@[simp]

theorem Complexity.DepthThreeLowerBound.reverseTotal_zero {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] (α : ℝ) (b : ℕ) (scope : I → Finset V) (violation : I → Bool) (R : Finset V) : reverseTotal α b scope violation 0 R = 1

theorem Complexity.DepthThreeLowerBound.reverseTotal_succ_of_nonempty {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] (α : ℝ) (b : ℕ) (scope : I → Finset V) (violation : I → Bool) (s : ℕ) (R : Finset V) (h : (reverseEligible scope violation R).Nonempty) : reverseTotal α b scope violation (s + 1) R = (∑ i ∈ reverseEligible scope violation R, ∑ D ∈ reverseBlocks b (scope i), α ^ D.card * reverseTotal α b scope violation s (R ∪ D)) / ↑(reverseEligible scope violation R).card

theorem Complexity.DepthThreeLowerBound.reverseTotal_succ_of_empty {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] (α : ℝ) (b : ℕ) (scope : I → Finset V) (violation : I → Bool) (s : ℕ) (R : Finset V) (h : reverseEligible scope violation R = ∅) : reverseTotal α b scope violation (s + 1) R = 0

theorem Complexity.DepthThreeLowerBound.reverseTotal_nonneg {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] {α : ℝ} (hα : 0 ≤ α) (b : ℕ) (scope : I → Finset V) (violation : I → Bool) (s : ℕ) (R : Finset V) : 0 ≤ reverseTotal α b scope violation s R

theorem Complexity.DepthThreeLowerBound.reverseTotal_le_theta_pow {V : Type uDepth1} {I : Type uDepth2} [instDecidableEqV : DecidableEq V] [Fintype I] {α : ℝ} (hα : 0 ≤ α) (b k : ℕ) (scope : I → Finset V) (hscope : ∀ (i : I), (scope i).card ≤ k) (violation : I → Bool) (s : ℕ) (R : Finset V) : reverseTotal α b scope violation s R ≤ reverseTheta α b k ^ s