SmoothMeanDecayRates.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Numerical decay for the remaining terms of the smooth explicit formula

theorem OAI.Ostmann.eventual_conductor_exponential_decay line 10

Source documentation

The conductor grows more slowly than log X = exp L.

theorem eventual_conductor_exponential_decay (a b C D : ℝ)
    (ha : 0 < a) (hb : 0 ≤ b) :
    ∀ᶠ L : ℝ in atTop, ∀ q : ℝ, 0 ≤ q →
      q ≤ a * L * Real.exp ((9 / 10 : ℝ) * L) →
      C * Real.exp (b * q - Real.exp L / 2) ≤ Real.exp (-D * L) := by
…

theorem OAI.Ostmann.eventual_conductor_negative_decay line 44

Source documentation

The high-zero tail decays when log Q is at least L².

theorem eventual_conductor_negative_decay (C D : ℝ) :
    ∀ᶠ L : ℝ in atTop, ∀ q : ℝ, L ^ 2 ≤ q →
      C * Real.exp (-q) ≤ Real.exp (-D * L) := by
…