OAI/NumberTheory/DirichletL/Moments/CommonRadiusSaving.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.common_saving_identity line 17
  2. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.common_saving_lower line 25
  3. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.main_saving_lower line 40
  4. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.error_penalty_le line 50
  5. def OAI.SevenEighths.CenteredMomentCommonRadiusSaving.errorLoss line 56
  6. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.error_penalty_refined line 59
  7. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.errorLoss_le line 74
  8. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.error_saving_refined line 78
  9. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.error_saving_lower line 92
  10. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.common_gain_width line 106
  11. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.saving_power_factor line 116
  12. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.main_radius_gain line 122
  13. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.error_radius_gain line 128
  14. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.canonical_saving_gates line 136
  15. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.actual_main_common_saving line 167
  16. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.actual_error_common_saving line 189
  17. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.actual_error_common_saving_refined line 218
  18. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.actual_main_common_factor line 247
  19. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.actual_error_common_factor line 267
  20. theorem OAI.SevenEighths.CenteredMomentCommonRadiusSaving.actual_common_radius_widths line 295