OAI/NumberTheory/Ostmann/Preliminaries/FiniteMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Removing the constant Fourier mode

Centering a finite-field function removes exactly its zero frequency. The energy splits into the centered energy and the squared mean.

  1. def OAI.Ostmann.fieldMean line 16
  2. def OAI.Ostmann.fieldCentered line 19
  3. theorem OAI.Ostmann.fieldCentered_fourier line 22
  4. theorem OAI.Ostmann.fieldCentered_fourier_zero line 29
  5. theorem OAI.Ostmann.fieldCentered_energy_identity line 33
  6. theorem OAI.Ostmann.fieldCentered_energy_le line 52