OAI/NumberTheory/Ostmann/Quadratic/QuadraticFullCorrectionReindex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The literal frequency-first corrections are the bounded full sums

  1. theorem OAI.Ostmann.quadratic_weighted_filter_sum line 13
  2. theorem OAI.Ostmann.quadratic_full_low_reindex line 21
  3. theorem OAI.Ostmann.quadratic_full_high_reindex line 35
  4. theorem OAI.Ostmann.quadratic_full_middle_reindex line 51