OAI/NumberTheory/EgyptianFractions/DivisorMomentFinalBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DivisorMomentFinalBudget.eventually_sqrt_cutoff_window line 10

   Source documentation

   The square-root cutoff in the harmonic-prefix estimate satisfies the uniform large-class parameter window.

   theorem eventually_sqrt_cutoff_window (D : ℝ) :
       ∀ᶠ S : ℝ in atTop, ∀ v Y : ℝ,
         S / (2 * Real.log S) ≤ v → v ≤ D * S →
         Real.exp (v / 2) ≤ Y → Y ≤ Real.exp v →
         0 ≤ v ∧ 2 ≤ Real.sqrt Y ∧ Real.log (Real.sqrt Y) ≤ D * S := by
   …

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

2. theorem OAI.Problem337.DivisorMomentFinalBudget.final_budget_of_large_majorant line 43

   Source documentation

   Final loss absorption with the large-class majorant supplied explicitly. This helper isolates the harmless square-root cutoff and finite-band count from the number-theoretic class estimates.

   theorem final_budget_of_large_majorant
       (D r C A B : ℝ) (hA : 0 ≤ A)
       (hlarge : ∀ᶠ S : ℝ in atTop, ∀ v Z : ℝ,
         S / (2 * Real.log S) ≤ v → v ≤ D * S → 2 ≤ Z →
         Real.log Z ≤ D * S →
         2 * Real.exp (r * (1 + Real.log ((D + 1) * S / v)) *
           v ^ (1 / 16 : ℝ) + C * Real.log (1 + Real.log Z)) ≤
         Real.exp (A * S ^ (1 / 16 : ℝ) * Real.log (Real.log S) +
           B * Real.log S)) :
       ∀ᶠ S : ℝ in atTop, ∀ v Y : ℝ,
         S / (2 * Real.log S) ≤ v → v ≤ D * S →
         Real.exp (v / 2) ≤ Y → Y ≤ Real.exp v →
   …

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

3. theorem OAI.Problem337.DivisorMomentFinalBudget.eventually_divisor_moment_final_budget line 70

   Source documentation

   Exact final numerical budget for the large, small, and dyadic intermediate classes. All growth estimates are unconditional and uniform in both windows.

   theorem eventually_divisor_moment_final_budget
       (D r C : ℝ) (hD : 1 ≤ D) (hr : 0 ≤ r) (hC : 0 ≤ C) :
       ∀ᶠ S : ℝ in atTop, ∀ v Y : ℝ,
         S / (2 * Real.log S) ≤ v → v ≤ D * S →
         Real.exp (v / 2) ≤ Y → Y ≤ Real.exp v →
         2 * Real.exp (r * (1 + Real.log ((D + 1) * S / v)) *
           v ^ (1 / 16 : ℝ) + C * Real.log (1 + Real.log (Real.sqrt Y))) +
           2 * Real.exp (-v / 100) + (6 / Real.log 2) * Real.log S ≤
         Real.exp (S ^ (1 / 4 : ℝ)) := by
   …

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

4. theorem OAI.Problem337.DivisorMomentFinalBudget.eventually_divisor_moment_weighted_budget line 86

   Source documentation

   The weighted form directly bounds the sum of the three class contributions.

   theorem eventually_divisor_moment_weighted_budget
       (D r C : ℝ) (hD : 1 ≤ D) (hr : 0 ≤ r) (hC : 0 ≤ C) :
       ∀ᶠ S : ℝ in atTop, ∀ v Y : ℝ,
         S / (2 * Real.log S) ≤ v → v ≤ D * S →
         Real.exp (v / 2) ≤ Y → Y ≤ Real.exp v →
         2 * Y * Real.exp (r * (1 + Real.log ((D + 1) * S / v)) *
           v ^ (1 / 16 : ℝ) + C * Real.log (1 + Real.log (Real.sqrt Y))) +
           2 * Y * Real.exp (-v / 100) +
           Y * ((6 / Real.log 2) * Real.log S) ≤
         Y * Real.exp (S ^ (1 / 4 : ℝ)) := by
   …

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