OAI/NumberTheory/EgyptianFractions/ReciprocalPhase.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.reciprocal_phase_local_power_saving line 12

   Source documentation

   Uniform local power cancellation for reciprocal phases, with no analytic hypotheses beyond the indicated numerator range.

   theorem reciprocal_phase_local_power_saving (B : ℝ) (hB : 4 ≤ B) :
       ∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧
         ∀ᶠ U : ℝ in atTop, ∀ (Z : ℝ) (L R : ℤ),
           U ^ (4 : ℕ) ≤ |Z| → |Z| ≤ U ^ B →
           U ≤ (L : ℝ) → (R : ℝ) ≤ 2 * U →
           ‖∑ n ∈ Finset.Icc L R, differencingPhase (Z / (n : ℝ))‖ ≤
             A * U ^ (1 - δ) := by
   …

   Mentions: OAI.Problem337.differencingPhase