RankinExponentialBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An explicit numerical margin in the high-weight Rankin parameter

theorem OAI.Ostmann.rankin_exponential_bound line 12

Source documentation

The large negative Rankin exponent dominates with ample margin once the stated logarithmic and positive-error bounds hold.

theorem rankin_exponential_bound (T u K E : ℝ) (b : ℕ)
    (hT : 1 < T) (hu : 1 < u) (hK : 0 ≤ K)
    (hlog : Real.log u ≤ Real.log T / 100000)
    (hb : K / (400 * Real.log u) - 1 ≤ b)
    (hE : Real.log u + Real.log T / 4 + E ≤ K) :
    u * ((T ^ (1 / 4 : ℝ)) ^ b)⁻¹ * Real.exp E ≤ Real.exp (-20 * K) := by
…