Unrestricted depth-three lower bound: uniform sparse bounds

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/UniformSparseBounds.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.sparseEnvelope (b M B d : ℝ) : ℝ

A common upper envelope for the sparse-family constants.

Equations

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

theorem Complexity.DepthThreeLowerBound.sparse_expression_le_envelope (b M B d m t : ℝ) (hb : 0 ≤ b) (hM : 0 ≤ M) (hB : 0 < B) (hd : 1 ≤ d) (hmlo : B * √d / 2 ≤ m) (hmhi : m ≤ 2 * B * √d) (htlo : d ^ (1 / 6) / 2 ≤ t) (hthi : t ≤ d ^ (1 / 6)) (htone : 1 ≤ t) : M * (1 + b * (Real.log (2 * m + 1) / Real.log 2)) / t + Real.log t / Real.log 2 / m ≤ sparseEnvelope b M B d

theorem Complexity.DepthThreeLowerBound.tendsto_sparseEnvelope (b M B : ℝ) : Filter.Tendsto (sparseEnvelope b M B) Filter.atTop (nhds 0)

theorem Complexity.DepthThreeLowerBound.uniform_sparse_condition (b M B : ℝ) (hb : 0 ≤ b) (hM : 0 ≤ M) (hB : 0 < B) : ∃ (D : ℕ), 1 ≤ D ∧ ∀ (d : ℝ), ↑D ≤ d → ∀ (m t : ℝ), B * √d / 2 ≤ m → m ≤ 2 * B * √d → d ^ (1 / 6) / 2 ≤ t → t ≤ d ^ (1 / 6) → 1 ≤ t → M * (1 + b * (Real.log (2 * m + 1) / Real.log 2)) / t + Real.log t / Real.log 2 / m ≤ 1 / 8

theorem Complexity.DepthThreeLowerBound.hard_slice_tail_bounds (μ m r t : ℝ) (hμ : 0 ≤ μ) (hmlo : μ / 2 ≤ m) (hmhi : m ≤ 2 * μ) (hr : 33 / 16 * μ ≤ r) (ht : 1 ≤ t) : 2 ^ (m - r) ≤ 2 ^ (-μ / 16) ∧ 2 ^ (-(m * t) / 8) ≤ 2 ^ (-μ / 16)

theorem Complexity.DepthThreeLowerBound.in_window_correlation_bound (μ m : ℝ) (hm : μ / 2 ≤ m) : 2 ^ (-m / 8) ≤ 2 ^ (-μ / 16)