OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticPatternErrorRate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.pairedFrequencyTree_card line 11
2. theorem OAI.Ostmann.movingPattern_frequency_error_rate line 15
3. theorem OAI.Ostmann.movingPattern_three_errors_rate line 60

   Source documentation

   All three errors in the original-prior norm bound fit the final common scale after the exact equality-pattern and two-history sums.

   theorem movingPattern_three_errors_rate (n k : ℕ) (hk : 0 < k)
       (Cprior Cfreq : ℝ) (hCprior : 1 ≤ Cprior) (hCfreq : 0 ≤ Cfreq) :
       ∀ᶠ L : ℝ in atTop, ∀ S : Finset ℤ,
         (S.card : ℝ) ≤ Real.exp (Cfreq * spectatorBulkCount k L) →
         ((2 : ℝ) ^ ((4 * n * 2 ^ n) ^ 2) *
           (max 2 (Real.exp (Cprior * L))) ^ (4 * n * 2 ^ n)) *
           (Fintype.card (FrequencyTree (S × S) n) : ℝ) *
             (Real.exp (-Real.exp ((125 / 100000 : ℝ) * L)) +
               2 * Real.exp (-Real.exp ((2 / 1000 : ℝ) * L))) ≤
           3 * Real.exp (-Real.exp ((12 / 10000 : ℝ) * L)) := by
   …

   Mentions: OAI.Ostmann.spectatorBulkCount, OAI.Ostmann.FrequencyTree

4. theorem OAI.Ostmann.movingPattern_four_errors_rate line 81

   Source documentation

   The internal-prime comparison contributes one further error of the same scale. All four errors survive both finite sums with a common saving.

   theorem movingPattern_four_errors_rate (n k : ℕ) (hk : 0 < k)
       (Cprior Cfreq : ℝ) (hCprior : 1 ≤ Cprior) (hCfreq : 0 ≤ Cfreq) :
       ∀ᶠ L : ℝ in atTop, ∀ S : Finset ℤ,
         (S.card : ℝ) ≤ Real.exp (Cfreq * spectatorBulkCount k L) →
         ((2 : ℝ) ^ ((4 * n * 2 ^ n) ^ 2) *
           (max 2 (Real.exp (Cprior * L))) ^ (4 * n * 2 ^ n)) *
           (Fintype.card (FrequencyTree (S × S) n) : ℝ) *
             (Real.exp (-Real.exp ((125 / 100000 : ℝ) * L)) +
               3 * Real.exp (-Real.exp ((2 / 1000 : ℝ) * L))) ≤
           4 * Real.exp (-Real.exp ((12 / 10000 : ℝ) * L)) := by
   …

   Mentions: OAI.Ostmann.spectatorBulkCount, OAI.Ostmann.FrequencyTree

5. theorem OAI.Ostmann.movingPattern_five_errors_rate line 100

   Source documentation

   The literal giant comparison adds one further error to the two bulk and one internal comparison errors. All five survive the exact finite sums.

   theorem movingPattern_five_errors_rate (n k : ℕ) (hk : 0 < k)
       (Cprior Cfreq : ℝ) (hCprior : 1 ≤ Cprior) (hCfreq : 0 ≤ Cfreq) :
       ∀ᶠ L : ℝ in atTop, ∀ S : Finset ℤ,
         (S.card : ℝ) ≤ Real.exp (Cfreq * spectatorBulkCount k L) →
         ((2 : ℝ) ^ ((4 * n * 2 ^ n) ^ 2) *
           (max 2 (Real.exp (Cprior * L))) ^ (4 * n * 2 ^ n)) *
           (Fintype.card (FrequencyTree (S × S) n) : ℝ) *
             (Real.exp (-Real.exp ((125 / 100000 : ℝ) * L)) +
               4 * Real.exp (-Real.exp ((2 / 1000 : ℝ) * L))) ≤
           5 * Real.exp (-Real.exp ((12 / 10000 : ℝ) * L)) := by
   …

   Mentions: OAI.Ostmann.spectatorBulkCount, OAI.Ostmann.FrequencyTree