OAI/NumberTheory/Ostmann/Arithmetic/MovingStatisticDecay.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventually_bulk_exp_margin line 12

   Source documentation

   Fixed constants are absorbed by a strict linear-exponent margin.

   theorem eventually_bulk_exp_margin (k : ℕ) (hk : 0 < k) (K a b : ℝ)
       (hK : 0 ≤ K) (hab : a < b) :
       ∀ᶠ L : ℝ in atTop, K * Real.exp (a * spectatorBulkCount k L) ≤
         Real.exp (b * spectatorBulkCount k L) := by
   …

   Mentions: OAI.Ostmann.spectatorBulkCount

2. theorem OAI.Ostmann.eventually_bulk_arithmetic_error line 27

   Source documentation

   The retained arithmetic error beats every fixed exponential in the bulk size.

   theorem eventually_bulk_arithmetic_error (k : ℕ) (T : ℝ) :
       ∀ᶠ L : ℝ in atTop, Real.exp (-Real.exp ((12 / 10000 : ℝ) * L)) ≤
         Real.exp (-T * spectatorBulkCount k L) := by
   …

   Mentions: OAI.Ostmann.spectatorBulkCount

3. theorem OAI.Ostmann.eventually_scaled_bulk_arithmetic_error line 43
4. theorem OAI.Ostmann.eventually_moving_statistic_decay line 63

   Source documentation

   This is the numerical bound occurring in the selected-prior theorem, including the root-frequency mass and all five arithmetic errors.

   theorem eventually_moving_statistic_decay (k : ℕ) (hk : 0 < k)
       (C K A badRate diagRate gain T : ℝ) (hC : 0 ≤ C) (hK : 0 ≤ K) (hA : 0 ≤ A)
       (hbad : A + badRate + diagRate < -T) (hgood : A - gain < -T) :
       ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
   …

   Mentions: OAI.Ostmann.spectatorBulkCount

5. theorem OAI.Ostmann.eventually_moving_statistic_decay_with_base line 109

   Source documentation

   Substitute the original bottom gap before applying the exponential margin.

   theorem eventually_moving_statistic_decay_with_base (k : ℕ) (hk : 0 < k)
       (r C K A badRate D ε gain T : ℝ)
       (hr : 0 ≤ r) (hC : 0 ≤ C) (hK : 0 ≤ K) (hA : 0 ≤ A)
       (hbad : A + r * badRate + (r * D + (Real.log 12 + 1) * r + ε) < -T)
       (hgood : A - gain < -T) :
       ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
   …

   Mentions: OAI.Ostmann.spectatorBulkCount