OAI/NumberTheory/Ostmann/Tree/PairSpectrum.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.FiniteField.pairSpectrum line 12
  2. def OAI.Ostmann.FiniteField.pairWeight line 15
  3. def OAI.Ostmann.FiniteField.pairFourthMass line 18
  4. theorem OAI.Ostmann.FiniteField.characterTwist_norm line 21
  5. theorem OAI.Ostmann.FiniteField.characterTwist_l2Sq line 29
  6. theorem OAI.Ostmann.FiniteField.pairSpectrum_unit line 33
  7. theorem OAI.Ostmann.FiniteField.pairSpectrum_zero line 38
  8. theorem OAI.Ostmann.FiniteField.fourier_pairSpectrum line 45
  9. theorem OAI.Ostmann.FiniteField.pairWeight_nonneg line 53
  10. theorem OAI.Ostmann.FiniteField.pairWeight_mass line 56
  11. theorem OAI.Ostmann.FiniteField.norm_fourier_characterTwist_le line 61
  12. theorem OAI.Ostmann.FiniteField.pairWeight_le line 68
  13. theorem OAI.Ostmann.FiniteField.pairFourthMass_le line 75
  14. theorem OAI.Ostmann.FiniteField.pairFourthMass_eq_l2Sq line 86