OAI/NumberTheory/EgyptianFractions/UniformDivisorMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DivisorMoment.eventually_uniform_divisor_moment_exp line 19

   Source documentation

   The complete uniform shifted divisor moment, with the upper cutoff parameterized exponentially. All three prime-factor classes are estimated unconditionally; the threshold depends only on the fixed D and r.

   theorem eventually_uniform_divisor_moment_exp (D r : ℝ)
       (hD : 1 ≤ D) (hr : 0 ≤ r) :
       ∀ᶠ S : ℝ in atTop, ∀ v Y : ℝ, ∀ N : ℕ,
         S / (2 * Real.log S) ≤ v → v ≤ D * S →
         Real.exp (v / 2) ≤ Y → Y ≤ Real.exp v →
         (N : ℝ) ≤ Real.exp (D * S) →
         (∑ h ∈ Finset.Icc 1 ⌊Y⌋₊,
           (truncatedDivisorCount (Real.exp v) (N + h) : ℝ) ^ r) ≤
           Y * Real.exp (S ^ (1 / 4 : ℝ)) := by
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.v, OAI.Problem337.truncatedDivisorCount

2. theorem OAI.Problem337.DivisorMoment.eventually_uniform_divisor_moment line 61

   Source documentation

   Uniform divisor moments with real cutoffs. The statement also covers a real interval length through its floor.

   theorem eventually_uniform_divisor_moment (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⌋₊,
           (truncatedDivisorCount X (N + h) : ℝ) ^ r) ≤
           Y * Real.exp (S ^ (1 / 4 : ℝ)) := by
   …

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