Unrestricted depth-three lower bound: sparse thresholds

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

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

structure Complexity.DepthThreeLowerBound.SparseLevel : Type

The sunflower, occurrence, insertion, and accumulated thresholds at one level.

• r : ℕ

  The required sunflower cardinality.

• e : ℕ

  The literal-occurrence threshold.

• D : ℕ

  The insertion bound at this level.

• F : ℕ

  The sum of earlier insertion bounds.

noncomputable def Complexity.DepthThreeLowerBound.nextSparseLevel (ε : ℝ) (hε : 0 < ε) (i : ℕ) (previous : SparseLevel) : SparseLevel

Choose the next sparsification thresholds using the entropy bound.

Equations

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

def Complexity.DepthThreeLowerBound.sparseLevel (ε : ℝ) (hε : 0 < ε) : ℕ → SparseLevel

The recursively chosen sparsification thresholds at each clause size.

Equations

• Complexity.DepthThreeLowerBound.sparseLevel ε hε 0 = { r := 2, e := 0, D := 0, F := 0 }
• Complexity.DepthThreeLowerBound.sparseLevel ε hε 1 = { r := 2, e := 1, D := 4, F := 0 }
• Complexity.DepthThreeLowerBound.sparseLevel ε hε n.succ.succ = Complexity.DepthThreeLowerBound.nextSparseLevel ε hε (n + 1) (Complexity.DepthThreeLowerBound.sparseLevel ε hε (n + 1))

noncomputable def Complexity.DepthThreeLowerBound.sparseR (ε : ℝ) (hε : 0 < ε) (i : ℕ) : ℕ

The sunflower-size threshold at the given sparsification level.

Equations

• Complexity.DepthThreeLowerBound.sparseR ε hε i = (Complexity.DepthThreeLowerBound.sparseLevel ε hε i).r

noncomputable def Complexity.DepthThreeLowerBound.sparseE (ε : ℝ) (hε : 0 < ε) (i : ℕ) : ℕ

The literal-occurrence bound at the given sparsification level.

Equations

• Complexity.DepthThreeLowerBound.sparseE ε hε i = (Complexity.DepthThreeLowerBound.sparseLevel ε hε i).e

noncomputable def Complexity.DepthThreeLowerBound.sparseD (ε : ℝ) (hε : 0 < ε) (i : ℕ) : ℕ

The insertion bound at the given sparsification level.

Equations

• Complexity.DepthThreeLowerBound.sparseD ε hε i = (Complexity.DepthThreeLowerBound.sparseLevel ε hε i).D

noncomputable def Complexity.DepthThreeLowerBound.sparseF (ε : ℝ) (hε : 0 < ε) (i : ℕ) : ℕ

The sum of insertion bounds at earlier sparsification levels.

Equations

• Complexity.DepthThreeLowerBound.sparseF ε hε i = (Complexity.DepthThreeLowerBound.sparseLevel ε hε i).F

@[simp]

theorem Complexity.DepthThreeLowerBound.sparseE_zero (ε : ℝ) (hε : 0 < ε) : sparseE ε hε 0 = 0

@[simp]

theorem Complexity.DepthThreeLowerBound.sparseD_zero (ε : ℝ) (hε : 0 < ε) : sparseD ε hε 0 = 0

@[simp]

theorem Complexity.DepthThreeLowerBound.sparseF_zero (ε : ℝ) (hε : 0 < ε) : sparseF ε hε 0 = 0

@[simp]

theorem Complexity.DepthThreeLowerBound.sparseE_one (ε : ℝ) (hε : 0 < ε) : sparseE ε hε 1 = 1

@[simp]

theorem Complexity.DepthThreeLowerBound.sparseD_one (ε : ℝ) (hε : 0 < ε) : sparseD ε hε 1 = 4

@[simp]

theorem Complexity.DepthThreeLowerBound.sparseF_one (ε : ℝ) (hε : 0 < ε) : sparseF ε hε 1 = 0

theorem Complexity.DepthThreeLowerBound.sparseR_succ_succ (ε : ℝ) (hε : 0 < ε) (n : ℕ) : sparseR ε hε (n + 2) = Classical.choose ⋯

theorem Complexity.DepthThreeLowerBound.sparseF_succ_succ (ε : ℝ) (hε : 0 < ε) (n : ℕ) : sparseF ε hε (n + 2) = sparseF ε hε (n + 1) + sparseD ε hε (n + 1)

theorem Complexity.DepthThreeLowerBound.sparseE_succ_succ (ε : ℝ) (hε : 0 < ε) (n : ℕ) : sparseE ε hε (n + 2) = (n + 1).factorial * (sparseR ε hε (n + 2) - 1) ^ (n + 1)

theorem Complexity.DepthThreeLowerBound.sparseD_succ_succ (ε : ℝ) (hε : 0 < ε) (n : ℕ) : sparseD ε hε (n + 2) = (sparseE ε hε (n + 2) + 1) * (2 + sparseF ε hε (n + 2))

theorem Complexity.DepthThreeLowerBound.sparseR_ge_two (ε : ℝ) (hε : 0 < ε) (i : ℕ) : 2 ≤ sparseR ε hε i

theorem Complexity.DepthThreeLowerBound.sparseF_eq_sum_Ico (ε : ℝ) (hε : 0 < ε) (i : ℕ) : sparseF ε hε i = ∑ v ∈ Finset.Ico 1 i, sparseD ε hε v

theorem Complexity.DepthThreeLowerBound.sparseE_succ (ε : ℝ) (hε : 0 < ε) (i : ℕ) (hi : 1 ≤ i) : sparseE ε hε (i + 1) = i.factorial * (sparseR ε hε (i + 1) - 1) ^ i

theorem Complexity.DepthThreeLowerBound.sparseD_eq (ε : ℝ) (hε : 0 < ε) (i : ℕ) (hi : 1 ≤ i) : sparseD ε hε i = (sparseE ε hε i + 1) * (2 + ∑ v ∈ Finset.Ico 1 i, sparseD ε hε v)

theorem Complexity.DepthThreeLowerBound.sparseE_pos (ε : ℝ) (hε : 0 < ε) (i : ℕ) (hi : 1 ≤ i) : 0 < sparseE ε hε i

theorem Complexity.DepthThreeLowerBound.sparseD_pos (ε : ℝ) (hε : 0 < ε) (i : ℕ) (hi : 1 ≤ i) : 0 < sparseD ε hε i

theorem Complexity.DepthThreeLowerBound.sparse_entropy_bound (ε : ℝ) (hε : 0 < ε) (i : ℕ) (hi : 2 ≤ i) : ↑(sparseF ε hε i) * binaryEntropy (1 / ↑(sparseR ε hε i)) ≤ ε

theorem Complexity.DepthThreeLowerBound.sparseNumerics (ε : ℝ) (hε : 0 < ε) (b : ℕ) : SparseNumerics (sparseR ε hε) (sparseE ε hε) (sparseD ε hε) b

noncomputable def Complexity.DepthThreeLowerBound.sparseM (ε : ℝ) (hε : 0 < ε) (b : ℕ) : ℕ

The resulting bound on sparse literal occurrences.

Equations

• Complexity.DepthThreeLowerBound.sparseM ε hε b = 2 + 2 * ∑ i ∈ Finset.Icc 1 b, Complexity.DepthThreeLowerBound.sparseE ε hε i

theorem Complexity.DepthThreeLowerBound.sparseM_eq (ε : ℝ) (hε : 0 < ε) (b : ℕ) : sparseM ε hε b = 2 + 2 * ∑ i ∈ Finset.Icc 1 b, sparseE ε hε i

theorem Complexity.DepthThreeLowerBound.sparseM_pos (ε : ℝ) (hε : 0 < ε) (b : ℕ) : 0 < sparseM ε hε b

theorem Complexity.DepthThreeLowerBound.sparse_tolerance_pos {b : ℕ} {η : ℝ} (hb : 1 ≤ b) (hη : 0 < η) : 0 < η / ↑b

theorem Complexity.DepthThreeLowerBound.exists_sparse_numerics (b : ℕ) (η : ℝ) (hb : 1 ≤ b) (hη : 0 < η) : ∃ (r : ℕ → ℕ) (e : ℕ → ℕ) (D : ℕ → ℕ) (F : ℕ → ℕ) (M : ℕ), SparseNumerics r e D b ∧ (∀ (i : ℕ), 2 ≤ r i) ∧ F 0 = 0 ∧ F 1 = 0 ∧ (∀ (i : ℕ), F i = ∑ v ∈ Finset.Ico 1 i, D v) ∧ (∀ (i : ℕ), 2 ≤ i → i ≤ b → ↑(F i) * binaryEntropy (1 / ↑(r i)) ≤ η / ↑b) ∧ M = 2 + 2 * ∑ i ∈ Finset.Icc 1 b, e i ∧ 0 < M