ReciprocalPhaseUniform.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.ReciprocalTerminalPowerBound line 11
Source documentation
The terminal estimate needed at one fixed differencing order.
```
def ReciprocalTerminalPowerBound (k : ℕ) (C U : ℝ) : Prop :=
…
```

theorem OAI.Problem337.reciprocal_phase_uniform_of_terminal line 25

Source documentation

For a bounded range of reciprocal-phase numerators, fixed-order terminal estimates give one positive power saving uniformly in the numerator and interval. All analytic hypotheses are confined to the explicit terminal estimate.

theorem reciprocal_phase_uniform_of_terminal
    (hterminal : ∀ k : ℕ, 4 ≤ k → ∃ C : ℝ, 0 ≤ C ∧
      ∀ᶠ U : ℝ in atTop, ReciprocalTerminalPowerBound k C U)
    (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.ReciprocalTerminalPowerBound, OAI.Problem337.differencingPhase