OAI/NumberTheory/EgyptianFractions/SmallPrimeMoment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DivisorMoment.small_class_truncated_moment_bound line 15

   Source documentation

   Complete small-prime contribution, including the actual class, pointwise weight control, and exponential loss absorption.

   theorem small_class_truncated_moment_bound (D r : ℝ) (hD : 1 ≤ D) (hr : 0 ≤ r) :
       ∀ᶠ S : ℝ in atTop, ∀ X Y : ℝ, ∀ N : ℕ,
         S / (2 * Real.log S) ≤ Real.log X →
         Real.log X ≤ D * S → Real.sqrt X ≤ Y → Y ≤ X →
         (N : ℝ) ≤ Real.exp (D * S) →
         (∑ h ∈ Finset.Icc 1 ⌊Y⌋₊ with
             DivisorClasses.SmallClass (N + h) S (Real.log X) Y,
           (truncatedDivisorCount X (N + h) : ℝ) ^ r) ≤
           2 * Y * Real.exp (-Real.log X / 100) := by
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.DivisorClasses.SmallClass, OAI.Problem337.truncatedDivisorCount