OAI/NumberTheory/DirichletL/Inversion/AmbientProfileTower.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.InverseAmbientProfileTower.frequencyTwist_fourier_joint_stronglyMeasurable line 14
  2. theorem OAI.SevenEighths.InverseAmbientProfileTower.logSource_fourier_joint_stronglyMeasurable line 25
  3. theorem OAI.SevenEighths.InverseAmbientProfileTower.twistedTriple_joint_stronglyMeasurable line 32
  4. abbrev OAI.SevenEighths.InverseAmbientProfileTower.Ambient line 46
  5. def OAI.SevenEighths.InverseAmbientProfileTower.ambientWeight line 48
  6. theorem OAI.SevenEighths.InverseAmbientProfileTower.ambientWeight_eq_pow line 52
  7. theorem OAI.SevenEighths.InverseAmbientProfileTower.ambientWeight_one_le line 56
  8. theorem OAI.SevenEighths.InverseAmbientProfileTower.ambientWeight_add line 66
  9. def OAI.SevenEighths.InverseAmbientProfileTower.inheritedLeft line 70
  10. def OAI.SevenEighths.InverseAmbientProfileTower.inheritedRight line 73
  11. theorem OAI.SevenEighths.InverseAmbientProfileTower.one_add_norm_add_le line 76
  12. theorem OAI.SevenEighths.InverseAmbientProfileTower.coordinate_factor_le line 83
  13. theorem OAI.SevenEighths.InverseAmbientProfileTower.inheritedLeft_bound line 92
  14. theorem OAI.SevenEighths.InverseAmbientProfileTower.inheritedRight_bound line 108
  15. theorem OAI.SevenEighths.InverseAmbientProfileTower.inherited_pair_weight_bound line 115
  16. theorem OAI.SevenEighths.InverseAmbientProfileTower.ambientWeight_continuous line 128
  17. theorem OAI.SevenEighths.InverseAmbientProfileTower.inheritedLeft_continuous line 133
  18. theorem OAI.SevenEighths.InverseAmbientProfileTower.inheritedRight_continuous line 136
  19. theorem OAI.SevenEighths.InverseAmbientProfileTower.inheritedParameter_measurable line 139
  20. theorem OAI.SevenEighths.InverseAmbientProfileTower.conditional_tower_integrable line 145
  21. theorem OAI.SevenEighths.InverseAmbientProfileTower.conditional_tower_bound line 196
  22. theorem OAI.SevenEighths.InverseAmbientProfileTower.integrable_density_test line 230
  23. theorem OAI.SevenEighths.InverseAmbientProfileTower.density_test_fubini line 242
  24. def OAI.SevenEighths.InverseAmbientProfileTower.twistedFullDensity line 251
  25. theorem OAI.SevenEighths.InverseAmbientProfileTower.fullProfileDensity_continuous line 257
  26. theorem OAI.SevenEighths.InverseAmbientProfileTower.twistedFullDensity_joint_stronglyMeasurable line 263
  27. theorem OAI.SevenEighths.InverseAmbientProfileTower.fullProfileDensity_weighted_integrable line 276
  28. theorem OAI.SevenEighths.InverseAmbientProfileTower.fullProfileDensity_weighted_integral line 286
  29. def OAI.SevenEighths.InverseAmbientProfileTower.towerMomentOrder line 305
  30. theorem OAI.SevenEighths.InverseAmbientProfileTower.twistedFullDensity_moment line 307
  31. def OAI.SevenEighths.InverseAmbientProfileTower.towerDensity line 330
  32. theorem OAI.SevenEighths.InverseAmbientProfileTower.towerDensity_joint_stronglyMeasurable line 338
  33. theorem OAI.SevenEighths.InverseAmbientProfileTower.towerDensity_weighted line 349
  34. theorem OAI.SevenEighths.InverseAmbientProfileTower.towerDensity_fubini line 381
  35. theorem OAI.SevenEighths.InverseAmbientProfileTower.first_inherited_left_eq line 393
  36. theorem OAI.SevenEighths.InverseAmbientProfileTower.first_inherited_right_eq line 398
  37. theorem OAI.SevenEighths.InverseAmbientProfileTower.second_inherited_left_eq line 403
  38. theorem OAI.SevenEighths.InverseAmbientProfileTower.second_inherited_right_eq line 408
  39. theorem OAI.SevenEighths.InverseAmbientProfileTower.twistedFullDensity_uniform_separation line 413
  40. theorem OAI.SevenEighths.InverseAmbientProfileTower.fullProfile_tower_uniform line 448
  41. def OAI.SevenEighths.InverseAmbientProfileTower.twistedPositiveSource line 505
  42. theorem OAI.SevenEighths.InverseAmbientProfileTower.first_second_profile_tower line 508