OAI/NumberTheory/Ostmann/Arithmetic/FrozenFrequencyAverage.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The frequency/Page average on the fixed bulk residue representative

  1. theorem OAI.Ostmann.extend_eq_of_eq_off_range line 11
  2. def OAI.Ostmann.movingFrequencyCorePageAverage line 20
  3. theorem OAI.Ostmann.movingFrequencyPageAverage_core line 30
  4. theorem OAI.Ostmann.movingFrequencyCorePageAverage_bulk_residues line 46
  5. theorem OAI.Ostmann.movingFrequencyCorePageAverage_norm_le line 67