OAI/NumberTheory/EgyptianFractions/DivisorClassAssembly.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DivisorClasses.eventually_class_budget_assembly line 16

   Source documentation

   Once the three arithmetic class estimates are supplied, the exact uniform moment budget follows. The prime-prefix cover and every numerical loss are discharged here, including the case of an empty intermediate range.

   theorem eventually_class_budget_assembly (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 →
         ∀ (H : Finset ℕ) (n : ℕ → ℕ) (w : ℕ → ℝ),
         (∀ i ∈ H, 0 ≤ w i) →
         (∑ i ∈ H with LargeClass (n i) v Y, w i) ≤
           2 * Y * Real.exp (r * (1 + Real.log ((D + 1) * S / v)) *
             v ^ (1 / 16 : ℝ) + C * Real.log (1 + Real.log (Real.sqrt Y))) →
         (∑ i ∈ H with SmallClass (n i) S v Y, w i) ≤
           2 * Y * Real.exp (-v / 100) →
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.v, OAI.Problem337.DivisorClasses.LargeClass, OAI.Problem337.DivisorClasses.SmallClass