OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticGoodPatternRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Full equality-pattern and frequency sums in the good-matching estimate

  1. def OAI.Ostmann.goodPatternGain line 13

    Source documentation

    The signed gain can be chosen before the local quartet tolerance. This amount absorbs every original pattern and paired-frequency count.

    def goodPatternGain (n : ℕ) (Cprior Cfreq gain : ℝ) : ℝ :=
…
  2. theorem OAI.Ostmann.arithmetic_good_pattern_rate line 17