OAI/NumberTheory/DirichletL/Energy/AmplifiedChildWidth.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.ball_support line 32
  2. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.actual_ball_witness line 38
  3. def OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.geometry line 47
  4. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.geometry_pos line 49
  5. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.main_nominal_cap line 53
  6. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.error_volume_cap line 65
  7. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.error_nominal_cap line 80
  8. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.restored_nominal_eq line 98
  9. def OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.mainRadius line 109
  10. def OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.errorRadius line 115
  11. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.mainRadius_eq line 121
  12. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.errorRadius_eq line 130
  13. def OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.threshold line 139
  14. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.threshold_gt_one line 142
  15. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.main_child_width line 145
  16. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedChildWidth.error_child_width line 182