InitialRepeatedErrorRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The initial gap absorbs the exact repeated-prime error

theorem OAI.Ostmann.eventual_initial_repeated_error line 11

Source documentation

The L^(2m) factor is precisely the contribution of the two copies of all broad positions. Cell normalizers remain in the exponent A*m.

theorem eventual_initial_repeated_error (r : ℕ) (z K A B Bs B₀ : ℝ)
    (hz : 1 ≤ z) (hBs : 2 * (A + B + 2 * Real.log 4 + B₀ + 3) ≤ Bs) :
    ∀ᶠ m : ℕ in atTop, ∀ L C H Δ : ℝ,
      0 < L → (m : ℝ) ≤ z * L → 0 ≤ C →
      C * L ^ (2 * m) ≤ Real.exp (A * m) → H ≤ B * m →
      (Bs + 8 * Real.log z) * m ≤ Δ →
      K * C * ((2 * (m + r) : ℕ) : ℝ) ^ (2 * (m + r)) * Real.exp (H - Δ / 2) ≤
        Real.exp (-(B₀ + 1) * m) := by
…