OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternCostRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPattern_total_cost_le_exp line 13

   Source documentation

   All equality patterns and representative-prior losses contribute only a fixed-depth exponential in L when p times its prior is at most exp(C L).

   theorem movingPattern_total_cost_le_exp (n : ℕ) (C L : ℝ) (hC : 1 ≤ C) (hL : 1 ≤ L) :
       (2 : ℝ) ^ ((4 * n * 2 ^ n) ^ 2) *
           (max 2 (Real.exp (C * L))) ^ (4 * n * 2 ^ n) ≤
         Real.exp ((((4 * n * 2 ^ n) ^ 2 + 4 * n * 2 ^ n : ℕ) : ℝ) * C * L) := by
   …

2. theorem OAI.Ostmann.movingPattern_internal_error_rate line 36

   Source documentation

   The proved pattern count can be inserted into the actual internal-prime saving, together with the large pointwise spectator factor from (8.21).

   theorem movingPattern_internal_error_rate (n : ℕ) (C B c : ℝ)
       (hC : 1 ≤ C) (_hB : 0 ≤ B) (hc : 0 < c) :
       ∀ᶠ L : ℝ in atTop,
         ((2 : ℝ) ^ ((4 * n * 2 ^ n) ^ 2) *
           (max 2 (Real.exp (C * L))) ^ (4 * n * 2 ^ n)) *
           Real.exp (B * L ^ 2 + B * L * Real.exp ((1 / 1000 : ℝ) * L)) *
           Real.exp (-c * Real.exp ((1 / 100 : ℝ) * L)) ≤
         Real.exp (-Real.exp ((2 / 1000 : ℝ) * L)) := by
   …