OAI/NumberTheory/EgyptianFractions/DescentDecay.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DescentDecay.eventually_exponent_bound line 11

   Source documentation

   The negative term in the density recurrence dominates the positive term.

   theorem eventually_exponent_bound (A c : ℝ) (hA : 0 ≤ A) (hc : 0 < c) :
       ∀ᶠ S : ℝ in atTop,
         A * S ^ (1 / 4 : ℝ) - c * S ^ (3 / 4 : ℝ) / Real.log S ≤
           -(S ^ (1 / 4 : ℝ)) := by
   …

2. theorem OAI.Problem337.DescentDecay.tendsto_density_envelope_zero line 44

   Source documentation

   The coarse density bound tends to zero, uniformly in its fixed constants.

   theorem tendsto_density_envelope_zero (A c K : ℝ)
       (hA : 0 ≤ A) (hc : 0 < c) (hK : 0 ≤ K) :
       Tendsto (fun S : ℝ => K * Real.log S *
         Real.exp (A * S ^ (1 / 4 : ℝ) - c * S ^ (3 / 4 : ℝ) / Real.log S))
         atTop (𝓝 0) := by
   …

3. theorem OAI.Problem337.DescentDecay.eventually_density_envelope_le_eighth line 75

   Source documentation

   In particular the exceptional density is eventually at most one eighth.

   theorem eventually_density_envelope_le_eighth (c K r : ℝ)
       (hc : 0 < c) (hK : 0 ≤ K) (hr : 0 ≤ r) :
       ∀ᶠ S : ℝ in atTop,
         K * Real.log S * Real.exp
           (2 * r * S ^ (1 / 4 : ℝ) - (c / 2) * S ^ (3 / 4 : ℝ) / Real.log S) ≤
             1 / 8 := by
   …

4. theorem OAI.Problem337.DescentDecay.eventually_descent_bound_le_eighth line 87

   Source documentation

   Uniform endgame for the unrolled recurrence with variable depth and scale.

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