OAI/NumberTheory/EgyptianFractions/DescentDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DescentDecay.eventually_density_le_eighth line 13

   Source documentation

   Complete analytic endgame for backwards exceptional densities. The residue and moment arguments must supply the displayed recurrence and depth bound.

   theorem eventually_density_le_eighth (c K r α : ℝ)
       (hc : 0 < c) (hK : 0 ≤ K) (hr : 0 ≤ r)
       (hα0 : 0 < α) (hα1 : α < 1) (hαr : 1 / (1 - α) ≤ r) :
       ∀ᶠ S : ℝ in atTop, ∀ (m : ℝ) (d : ℕ) (δ : ℕ → ℝ),
         S / (2 * Real.log S) ≤ m → (d : ℝ) ≤ K * Real.log S →
         S ^ (-1 / 4 : ℝ) ≤ α ^ d →
         δ d = 0 → (∀ j ≤ d, 0 ≤ δ j) →
         (∀ j < d, δ j ≤ Real.exp (-(c * m)) +
           Real.exp (2 * S ^ (1 / 4 : ℝ)) * (δ (j + 1)) ^ α) →
         δ 0 ≤ 1 / 8 := by
   …