DescentRecurrence.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.descent_recurrence_bound line 8

Source documentation

A finite iteration estimate for the exceptional-set recurrence. The factor A ^ (1 / (1 - α)) absorbs the geometric sum of exponents.

theorem descent_recurrence_bound
    (δ : ℕ → ℝ) (d : ℕ) (ε A α : ℝ)
    (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hA : 1 ≤ A)
    (hα0 : 0 < α) (hα1 : α < 1)
    (hδ0 : δ 0 = 0) (hδ : ∀ j ≤ d, 0 ≤ δ j)
    (hstep : ∀ j < d, δ (j + 1) ≤ ε + A * (δ j) ^ α) :
    δ d ≤ (d : ℝ) * A ^ (1 / (1 - α)) * ε ^ (α ^ d) := by
…

theorem OAI.Problem337.descent_recurrence_bound_backward line 75

Source documentation

The same estimate with the direction of indexing used by the backwards construction of good numerator sets.

theorem descent_recurrence_bound_backward
    (δ : ℕ → ℝ) (d : ℕ) (ε A α : ℝ)
    (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) (hA : 1 ≤ A)
    (hα0 : 0 < α) (hα1 : α < 1)
    (hδd : δ d = 0) (hδ : ∀ j ≤ d, 0 ≤ δ j)
    (hstep : ∀ j < d, δ j ≤ ε + A * (δ (j + 1)) ^ α) :
    δ 0 ≤ (d : ℝ) * A ^ (1 / (1 - α)) * ε ^ (α ^ d) := by
…

theorem OAI.Problem337.descent_recurrence_exp_bound line 92

Source documentation

Exponential form of the finite exceptional-density estimate.

theorem descent_recurrence_exp_bound
    (δ : ℕ → ℝ) (d : ℕ) (a b α : ℝ)
    (ha : 0 ≤ a) (hb : 0 ≤ b) (hα0 : 0 < α) (hα1 : α < 1)
    (hδd : δ d = 0) (hδ : ∀ j ≤ d, 0 ≤ δ j)
    (hstep : ∀ j < d,
      δ j ≤ Real.exp (-b) + Real.exp a * (δ (j + 1)) ^ α) :
    δ 0 ≤ (d : ℝ) * Real.exp (a / (1 - α) - b * α ^ d) := by
…