OAI/NumberTheory/EgyptianFractions/DensityMomentBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.eventually_density_divisor_moment line 12

   Source documentation

   The unconditional uniform divisor moment in the density count notation.

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

   Mentions: OAI.Problem337.D, OAI.Problem337.densityDivisorCount

2. theorem OAI.Problem337.eventually_residue_level_moment line 24

   Source documentation

   All moments required by the canonical geometric density family hold unconditionally, simultaneously at each level and for every divisor of its auxiliary denominator. Only the stated size ranges remain as hypotheses.

   theorem eventually_residue_level_moment
       (DM η r : ℝ) (hDM : 1 < DM) (hη : 0 < η) (hηhalf : η ≤ 1 / 2)
       (hr : 0 ≤ r) :
       ∀ᶠ S : ℝ in atTop, ∀ C M : ℕ, 0 < C → 0 < M →
         (C : ℝ) ≤ Real.exp (8 * (DM + 2) * S) →
         (M : ℝ) ≤ Real.exp (DM * S) →
         ∀ j : ℕ, j < ResidueLevels.depth ((DM + 2) * S) (ResidueLevels.scale S) η →
         ∀ t : ℕ, t ∣ M →
         (∑ h ∈ Finset.Icc 1
             ⌊ResidueLevels.level ((DM + 2) * S) (ResidueLevels.scale S) η (j + 1)⌋₊,
           densityDivisorCount
             (ResidueLevels.level ((DM + 2) * S) (ResidueLevels.scale S) η j)
   …

   Mentions: OAI.Problem337.ResidueLevels.depth, OAI.Problem337.ResidueLevels.scale, OAI.Problem337.ResidueLevels.level, OAI.Problem337.densityDivisorCount