OAI/NumberTheory/Ostmann/Characters/DifferenceMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Means of nonnegative difference convolutions

Removing the zero difference can only decrease the sum. This supplies the mean bounds for the nonnegative quartet majorants in Section 6.

  1. def OAI.Ostmann.differenceMoment line 16
  2. theorem OAI.Ostmann.differenceMoment_nonneg line 19
  3. theorem OAI.Ostmann.sum_differenceMoment line 24
  4. theorem OAI.Ostmann.sum_units_differenceMoment_le line 35
  5. theorem OAI.Ostmann.mean_units_differenceMoment_le line 45