OAI/NumberTheory/DirichletL/Inversion/SecondProfileUniform.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseSecondProfileUniform.rooted line 14
  2. theorem OAI.SevenEighths.InverseSecondProfileUniform.rooted_apply line 18
  3. theorem OAI.SevenEighths.InverseSecondProfileUniform.rooted_support line 23
  4. def OAI.SevenEighths.InverseSecondProfileUniform.translated line 29
  5. theorem OAI.SevenEighths.InverseSecondProfileUniform.translated_apply line 32
  6. theorem OAI.SevenEighths.InverseSecondProfileUniform.fourier_translated line 35
  7. def OAI.SevenEighths.InverseSecondProfileUniform.normalization line 41
  8. def OAI.SevenEighths.InverseSecondProfileUniform.density line 45
  9. theorem OAI.SevenEighths.InverseSecondProfileUniform.density_formula line 51
  10. theorem OAI.SevenEighths.InverseSecondProfileUniform.fourier_twist line 61
  11. theorem OAI.SevenEighths.InverseSecondProfileUniform.density_norm line 69
  12. theorem OAI.SevenEighths.InverseSecondProfileUniform.density_joint_measurable line 80
  13. theorem OAI.SevenEighths.InverseSecondProfileUniform.normalization_bound line 93
  14. theorem OAI.SevenEighths.InverseSecondProfileUniform.density_weighted_integrable line 113
  15. theorem OAI.SevenEighths.InverseSecondProfileUniform.radial_common_box line 125
  16. theorem OAI.SevenEighths.InverseSecondProfileUniform.translated_box line 157
  17. theorem OAI.SevenEighths.InverseSecondProfileUniform.density_weighted_integral line 165
  18. def OAI.SevenEighths.InverseSecondProfileUniform.profile line 188
  19. def OAI.SevenEighths.InverseSecondProfileUniform.requiredOuterOrder line 196
  20. theorem OAI.SevenEighths.InverseSecondProfileUniform.common_measure line 198
  21. theorem OAI.SevenEighths.InverseSecondProfileUniform.balanced_exponential_identity line 254
  22. def OAI.SevenEighths.InverseSecondProfileUniform.positiveSource line 268
  23. theorem OAI.SevenEighths.InverseSecondProfileUniform.positiveSource_logSchwartz line 271
  24. theorem OAI.SevenEighths.InverseSecondProfileUniform.balanced_profile_identity line 280
  25. theorem OAI.SevenEighths.InverseSecondProfileUniform.second_profile_common_measure line 306
  26. def OAI.SevenEighths.InverseSecondProfileUniform.densityTower line 348
  27. theorem OAI.SevenEighths.InverseSecondProfileUniform.densityTower_joint_measurable line 355
  28. theorem OAI.SevenEighths.InverseSecondProfileUniform.densityTower_norm line 370
  29. theorem OAI.SevenEighths.InverseSecondProfileUniform.densityTower_weighted_integrable line 380
  30. theorem OAI.SevenEighths.InverseSecondProfileUniform.tower_bound_from_inner line 393
  31. theorem OAI.SevenEighths.InverseSecondProfileUniform.second_profile_tower_uniform line 448
  32. theorem OAI.SevenEighths.InverseSecondProfileUniform.densityTower_fubini line 489
  33. theorem OAI.SevenEighths.InverseSecondProfileUniform.actual_child_height_weight_bound line 501
  34. theorem OAI.SevenEighths.InverseSecondProfileUniform.normalization_eta_log line 509
  35. theorem OAI.SevenEighths.InverseSecondProfileUniform.fresh_physical_profile line 515
  36. theorem OAI.SevenEighths.InverseSecondProfileUniform.retained_clipping_parameter line 556
  37. theorem OAI.SevenEighths.InverseSecondProfileUniform.first_second_tower_uniform line 568