BalancedEndpointRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A depth-independent exponential rate for the actual endpoint statistic

theorem OAI.Ostmann.eventual_balanced_endpoint_rate line 12

Source documentation

The number of top and compensation roles changes only the threshold. The exponential coefficient remains independent of their number.

theorem eventual_balanced_endpoint_rate (r : ℕ) (a c δ A : ℝ)
    (ha : 0 < a) (hc : 0 < c) (hδ : 0 < δ) :
    ∀ᶠ m : ℕ in atTop, ∀ (L Y X E : ℝ) (n : ℕ),
      L ≤ m → 0 < Y → Y ≤ Real.exp L → 0 ≤ X → n ≤ m + r →
      a * Real.sqrt X / Y ^ 3 ≤ E →
      Real.sqrt X * Real.exp (-(2 * A + 2 * Real.log 2 + 4) * m) ≤
        E * (c * (Real.exp (-A * m) * (1 / 2 : ℝ) ^ n * δ) ^ 2) := by
…