SmoothFamilyEnvelopes.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Elementary exponential envelopes for the non-low-zero errors

theorem OAI.Ostmann.exponential_split line 10
theorem OAI.Ostmann.log_height_bound line 17

theorem OAI.Ostmann.smooth_middle_zero_envelope line 34

Source documentation

The zeros with real part below one half.

theorem smooth_middle_zero_envelope (Cm Cz Q X : ℝ)
    (hm : 0 ≤ Cm) (hz : 0 ≤ Cz) (hQ : 1 ≤ Q) (hX : 0 < X) :
    (Real.exp ((1 / 2 : ℝ) * Real.log X) * Cm) *
      (Cz * Q ^ 2 * (Q ^ 5 + 1) * Real.log (Q * (Q ^ 5 + 2))) ≤
      X * ((16 * Cm * Cz) * Real.exp (8 * Real.log Q - Real.log X / 2)) := by
…

theorem OAI.Ostmann.smooth_high_zero_envelope line 62

Source documentation

The complete high-ordinate tail, including all its zeros.

theorem smooth_high_zero_envelope (Cm Cz Q X : ℝ)
    (hm : 0 ≤ Cm) (hz : 0 ≤ Cz) (hQ : 1 ≤ Q) (hX : 0 ≤ X) :
    (X * Cm) * (2 * (2 * (Cz * Q ^ 2) * (Real.log Q + 3)) ^ 2 *
      Real.exp (-4 * Real.log (1 + Q ^ 5))) ≤
      X * ((128 * Cm * Cz ^ 2) * Real.exp (-Real.log Q)) := by
…

theorem OAI.Ostmann.smooth_family_remainder_envelope line 94

Source documentation

The trivial-zero and shifted-contour remainders, summed over the family.

theorem smooth_family_remainder_envelope (Cm E Q X : ℝ) (N : ℕ)
    (hm : 0 ≤ Cm) (hE : 0 ≤ E) (hQ : 1 ≤ Q) (hX : 1 ≤ X)
    (hN : (N : ℝ) ≤ Q ^ 2) :
    (N : ℝ) * (Cm + E / Real.sqrt X * Real.log (2 * Q)) ≤
      X * ((Cm + 2 * E) * Real.exp (3 * Real.log Q - Real.log X / 2)) := by
…