OAI/NumberTheory/Ostmann/Tree/Fourier.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.FiniteField.mean line 10
  2. def OAI.Ostmann.FiniteField.fourier line 12
  3. def OAI.Ostmann.FiniteField.l2Sq line 15
  4. instance OAI.Ostmann.FiniteField.characterFintype line 17
  5. def OAI.Ostmann.FiniteField.mixedCorrelation line 19
  6. def OAI.Ostmann.FiniteField.correlationBound line 22
  7. theorem OAI.Ostmann.FiniteField.fourier_zero line 25
  8. theorem OAI.Ostmann.FiniteField.fourier_apply line 28
  9. theorem OAI.Ostmann.FiniteField.mixedCorrelation_eq_fourier line 36
  10. theorem OAI.Ostmann.FiniteField.norm_mixedCorrelation_le line 40
  11. theorem OAI.Ostmann.FiniteField.l2Sq_nonneg line 46
  12. theorem OAI.Ostmann.FiniteField.fourier_inversion line 50