OAI/NumberTheory/EgyptianFractions/DeterministicMeanDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.ResidueLevels.eventually_exp_absorb_real_scale line 11

   Source documentation

   The exponential absorption used in the deterministic second moment is uniform in every real prime-product scale in the standard interval.

   theorem eventually_exp_absorb_real_scale {a b c C : ℝ}
       (hab : a < b) (hc : 0 < c) (hC : 0 ≤ C) :
       ∀ᶠ S : ℝ in atTop, ∀ m : ℝ,
         S / (2 * Real.log S) ≤ m → m ≤ S / Real.log S →
         Real.exp (-b * m) + C * Real.exp (-c * S) ≤ Real.exp (-a * m) := by
   …

2. theorem OAI.Problem337.ResidueLevels.eventually_deterministic_mean_real_scale line 76

   Source documentation

   A diagonal term controlled by an exponential list cardinality and a uniform off-diagonal power saving give the precise deterministic mean rate. The threshold is independent of the list, cutoff, and real scale m.

   theorem eventually_deterministic_mean_real_scale {A δ : ℝ}
       (hA : 0 ≤ A) (hδ : 0 < δ) :
       ∀ᶠ S : ℝ in atTop, ∀ m N X : ℝ,
         S / (2 * Real.log S) ≤ m → m ≤ S / Real.log S →
         Real.exp (m * Real.log 2) ≤ N → 0 ≤ X →
         X / N + 2 * A * X * Real.exp (-(4 * δ * S / 5)) ≤
           X * Real.exp (-m / 100) := by
   …