InitialEndpointRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform exponential rate in the positive endpoint lower bound

theorem OAI.Ostmann.eventual_endpoint_statistic_rate line 13

Source documentation

The number of cell roles affects only the cutoff, not the final rate.

theorem eventual_endpoint_statistic_rate (r : ℕ) (c δ γ A B : ℝ)
    (hc : 0 < c) (hδ : 0 < δ) (hγ : 0 < γ) (hA : 0 ≤ A) (hB : 0 ≤ B) :
    ∀ᶠ m : ℕ in atTop, ∀ (L u K : ℝ), L ≤ 2 * m → 0 < K →
      Real.exp (-A * L) ≤ u → K ≤ Real.exp (B * L) →
      Real.exp (-(2 * (A + 3 * B) - 2 * Real.log δ + 1) * m) ≤
        u / K * (c * (δ ^ (m + 1) / K) ^ 2 * γ ^ (2 * r)) := by
…