OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternGiantErrorRate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPattern_giant_error_rate line 12

   Source documentation

   The upper prime cutoff costs one factor per internal class. Even at the full permitted small-prime scale, the two giant errors remain negligible.

   theorem movingPattern_giant_error_rate (n : ℕ) (C : ℝ) (hC : 1 ≤ C) :
       ∀ᶠ L : ℝ in atTop, ∀ c : ℕ, c ≤ 4 * n * 2 ^ n → ∀ E U : ℝ,
         0 ≤ E → E ≤ Real.exp (C * L) → 0 ≤ U → U ≤ Real.exp (Real.exp ((12 / 1000 : ℝ) * L)) →
         ((2 : ℝ) ^ c * E ^ (4 * n * 2 ^ n - c) * U ^ c) *
           (Real.exp (-Real.exp ((125 / 10000 : ℝ) * L)) +
             Real.exp (-Real.exp ((1225 / 100000 : ℝ) * L))) ≤
           Real.exp (-Real.exp ((2 / 1000 : ℝ) * L)) := by
   …