OAI/NumberTheory/DirichletL/Descent/FirstProfileUniform.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseMomentFirstProfileUniform.rooted line 13
  2. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.rooted_apply line 17
  3. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.rooted_support line 22
  4. def OAI.SevenEighths.InverseMomentFirstProfileUniform.translated line 28
  5. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.translated_apply line 31
  6. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.fourier_translated line 34
  7. def OAI.SevenEighths.InverseMomentFirstProfileUniform.normalization line 40
  8. def OAI.SevenEighths.InverseMomentFirstProfileUniform.density line 44
  9. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.density_formula line 50
  10. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.fourier_twist line 60
  11. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.density_norm line 68
  12. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.density_joint_measurable line 79
  13. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.normalization_bound line 92
  14. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.density_weighted_integrable line 112
  15. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.radial_common_box line 124
  16. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.translated_box line 156
  17. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.density_weighted_integral line 164
  18. def OAI.SevenEighths.InverseMomentFirstProfileUniform.profile line 187
  19. def OAI.SevenEighths.InverseMomentFirstProfileUniform.requiredOuterOrder line 195
  20. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.common_measure line 197
  21. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.balanced_exponential_identity line 253
  22. def OAI.SevenEighths.InverseMomentFirstProfileUniform.positiveSource line 267
  23. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.positiveSource_logSchwartz line 270
  24. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.balanced_profile_identity line 279
  25. theorem OAI.SevenEighths.InverseMomentFirstProfileUniform.first_profile_common_measure line 305