OAI/NumberTheory/EgyptianFractions/IntermediateBandBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The final uniform intermediate-band budget for the actual canonical prime-factor class. All arithmetic, counting, and exponent estimates are proved here; no class-moment estimate remains as an assumption.

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

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