BadEventDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A single prime saving dominates the short prohibited-word enumeration.

lemma OAI.TwoPointCorrelations.eventually_short_word_cost line 11

theorem OAI.TwoPointCorrelations.eventually_bad_event_decay line 37

Source documentation

The complete short-word cost may include pattern and endpoint choices, all reciprocal masses, and summation over lengths. No further saving is used beyond the single nondegenerate last-prime relation.

theorem eventually_bad_event_decay (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (s : ℕ) (H B cost total : ℝ),
      (s : ℝ) ≤ L ^ (1 / 10 : ℝ) → Real.exp (L ^ (199 / 200 : ℝ)) ≤ H →
      1 ≤ B → B ≤ Real.exp L →
      cost ≤ Real.exp (C * s * (Real.log L) ^ 2) →
      total ≤ cost * (H⁻¹ + (1 + Real.log B) / H) →
      total ≤ Real.exp (-(1 / 2 : ℝ) * L ^ (199 / 200 : ℝ)) := by
…