OAI/NumberTheory/Ostmann/Arithmetic/ReducedFrequencyEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Reduced-frequency energy of a uniform set and its Ramanujan kernel

  1. def OAI.Ostmann.unitFrequencyEnergy line 11
  2. theorem OAI.Ostmann.unitFrequencyEnergy_nonneg line 16
  3. theorem OAI.Ostmann.unitFrequencyEnergy_kernel line 20
  4. theorem OAI.Ostmann.sum_reducedNumerators_eq_units line 48
  5. theorem OAI.Ostmann.intervalSetReducedEnergy_eq_unitFrequencyEnergy line 55