OAI/NumberTheory/DirichletL/Moments/AmplifiedRetainedRadius.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.ballProfile_support_upper line 18
  2. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.ballProfile_radius_le line 26
  3. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.gaussEnergy_radius_le line 35
  4. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.sourceGaussEnergy_radius_le line 47
  5. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.childEnergy_radius_le line 52
  6. lemma OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.exponent_max line 66
  7. lemma OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.rpow_exponent_max line 74
  8. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.main_radius_identity line 80
  9. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.error_radius_identity line 85
  10. lemma OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.envelope_exponent line 96
  11. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.main_exponent_envelope line 103
  12. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.error_exponent_envelope line 107
  13. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.eventually_support_reserve line 115
  14. lemma OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.doubled_radius_le line 121
  15. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.unamplified_radius_identity line 131
  16. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.dyadic_to_common_ball line 136
  17. def OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.mainCommonRadius line 150
  18. def OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.errorCommonRadius line 153
  19. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.main_energy_common line 156
  20. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.child_energy_common line 168
  21. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.errorCommonRadius_six line 180
  22. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.retained_nominal_upper line 187
  23. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.actual_retained_radii line 197
  24. theorem OAI.SevenEighths.CenteredMomentAmplifiedRetainedRadius.eventually_original_amplification_common line 220