OAI/NumberTheory/Ostmann/Arithmetic/MovingFullModulusScale.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The complete two-history modulus fits the published progression range

  1. def OAI.Ostmann.movingFullModulusExponent line 12
  2. theorem OAI.Ostmann.movingFullPairModulus_bound line 15
  3. theorem OAI.Ostmann.movingFullPairModulus_exp line 40
  4. theorem OAI.Ostmann.movingFullModulus_exponent_budget line 56
  5. theorem OAI.Ostmann.movingFullPairModulus_progression_range line 81