OAI/NumberTheory/EgyptianFractions/ReciprocalPhaseCancellation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.reciprocal_interval_budget_eventually line 13

   Source documentation

   Ambient normalization converts a terminal forward-difference estimate on every shortened subinterval into cancellation on the original interval.

   theorem reciprocal_interval_budget_eventually (r : ℕ) (α C : ℝ)
       (hα : 0 < α) (hαsmall : α < (1 : ℝ) / 5) (hC : 0 ≤ C) :
       ∀ᶠ (U : ℝ) in atTop, ∀ (L R : ℤ), U ≤ (L : ℝ) → (R : ℝ) ≤ 2 * U →
         ∀ f : ℝ → ℝ,
         (∀ hs : List ℤ, hs.length = r →
           (∀ h ∈ hs, 0 < h ∧ h < (Nat.floor (U ^ α) : ℤ)) →
           ‖∑ n ∈ Finset.Icc L (R - hs.sum),
             differencingPhase (forwardDifference (hs.map (fun h : ℤ => (h : ℝ))) f n)‖ ≤
             C * U ^ ((4 : ℝ) / 5)) →
         ‖∑ n ∈ Finset.Icc L R, differencingPhase (f n)‖ ≤
           36 * U ^ (1 - α / (2 : ℝ) ^ r) := by
   …

   Mentions: OAI.Problem337.differencingPhase, OAI.Problem337.forwardDifference