OscillatoryError.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Explicit modulus and frequency losses in the coefficient estimate

theorem OAI.JointDickman.oscillatory_error_bookkeeping line 12

Source documentation

A saving of 79 powers absorbs the modulus and frequency ranges in manuscript equation (1), leaving 50 powers.

theorem oscillatory_error_bookkeeping {B q K X a b M N ξ : ℝ}
    (hB : 1 ≤ B) (hq : q ≤ B ^ (15 : ℝ))
    (hK : 0 ≤ K) (hX : 0 < X) (hb : 0 ≤ b) (hab : a ≤ b)
    (hM : 0 ≤ M) (hN : 0 ≤ N) (hξ : |ξ| ≤ B ^ (14 : ℝ)) :
    q * (K * B ^ (-79 : ℝ) * (b * X) *
        (2 * M + (N + 2 * Real.pi * |ξ| * M) / X * (b * X - a * X))) ≤
      (K * b * (2 * M + (N + 2 * Real.pi * M) * (b - a))) * X * B ^ (-50 : ℝ) := by
…