FinalHistoryCount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-depth cost of summing both frequency histories

theorem OAI.Ostmann.card_frequencyTree line 13
theorem OAI.Ostmann.frequency_history_pair_card_bound line 25

theorem OAI.Ostmann.eventual_history_pair_decay line 42

Source documentation

Double-exponential cancellation survives both full finite-depth frequency sums. The depth and the frequency exponent are fixed first.

theorem eventual_history_pair_decay (n : ℕ) (C z α c : ℝ)
    (hC : 0 ≤ C) (hz : 0 ≤ z) (hα : 0 < α) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ (m : ℝ) (S : Finset ℤ), 0 ≤ m → m ≤ z * L →
      (S.card : ℝ) ≤ Real.exp (C * m) →
      (Fintype.card (FrequencyTree S n) : ℝ) ^ 2 * Real.exp (-c * Real.exp (α * L)) ≤
        Real.exp (-(c / 2) * Real.exp (α * L)) := by
…

Mentions: OAI.Ostmann.FrequencyTree