OAI/NumberTheory/DirichletL/Descent/WindowFourier.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseMoment.coordinateDensity line 13
  2. def OAI.SevenEighths.InverseMoment.coordinatePhase line 16
  3. theorem OAI.SevenEighths.InverseMoment.coordinate_fourier_inversion line 18
  4. theorem OAI.SevenEighths.InverseMoment.coordinate_density_weighted_integrable line 28
  5. theorem OAI.SevenEighths.InverseMoment.coordinate_density_weighted_integral line 35
  6. def OAI.SevenEighths.InverseMoment.pureProfileMode line 42
  7. theorem OAI.SevenEighths.InverseMoment.profileMode_coordinate_separation line 47
  8. theorem OAI.SevenEighths.InverseMoment.pureProfileMode_norm line 58
  9. def OAI.SevenEighths.InverseMoment.fullProfileDensity line 62
  10. def OAI.SevenEighths.InverseMoment.tripleHeight line 66
  11. def OAI.SevenEighths.InverseMoment.coordinateHeight line 69
  12. theorem OAI.SevenEighths.InverseMoment.fullProfileDensity_weighted_integrable line 71
  13. theorem OAI.SevenEighths.InverseMoment.fullProfileDensity_weighted_integral line 81
  14. theorem OAI.SevenEighths.InverseMoment.profile_integral_coordinate_absorption line 100
  15. def OAI.SevenEighths.InverseMoment.profileHeight line 120
  16. lemma OAI.SevenEighths.InverseMoment.logPhase_scaled_coordinate line 123
  17. theorem OAI.SevenEighths.InverseMoment.pureProfileMode_height line 129