OAI/NumberTheory/Ostmann/Arithmetic/MovingArithmeticSumRate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The original arithmetic error after summing all equality patterns

  1. theorem OAI.Ostmann.movingInternalArithmeticError_nonneg line 13
  2. theorem OAI.Ostmann.movingInternalArithmeticError_card line 25
  3. theorem OAI.Ostmann.movingInternalArithmeticError_mono_card line 31
  4. theorem OAI.Ostmann.moving_arithmetic_pattern_sum_rate line 43

    Source documentation

    A fixed-depth pattern sum retains any prescribed ordinary exponential saving in the bulk count, and all arithmetic comparison errors stay negligible. The antecedent is the explicit per-pattern bound proved for the original harmonic prime laws, not a new analytic input.

    theorem moving_arithmetic_pattern_sum_rate (n k : ℕ) (hk : 0 < k)
    (C D E Cprior B G : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hE : 0 ≤ E)
    (hCprior : 1 ≤ Cprior) (hB : 0 ≤ B) :
    let J := 4 * n * 2 ^ n
…