OAI/NumberTheory/DirichletL/Moments/AmplifiedChildWidth.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.modulus_pos line 28
2. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.span_pos line 30
3. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.canonical_modulus_log line 33
4. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.radical_error_log_bound line 55
5. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.common_nominal_identity line 90
6. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.common_nominal_le line 95
7. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.shortened_log line 102
8. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.main_nominal_bound line 112
9. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.error_nominal_bound line 132
10. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.physical_radial_budget line 156
11. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.physical_declared_budget line 189
12. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.physical_whole_budget line 208
13. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.original_coefficient_fixed_mask line 231
14. def OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.presentationFactor line 239
15. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.presentationFactor_pos line 242
16. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.presentationFactor_log line 245
17. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.first_fixed_log_le line 259
18. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.exists_fixed_width_threshold line 265
19. def OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.fixedWidthThreshold line 284
20. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.fixedWidthThreshold_spec line 287
21. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.main_nominal_fixed line 308
22. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.error_nominal_fixed line 314
23. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.main_declared_width line 326
24. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.error_declared_width line 345
25. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.main_whole_width line 372
26. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.error_whole_width line 393
27. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.main_declared_width_drop line 422
28. theorem OAI.SevenEighths.CenteredMomentAmplifiedChildWidth.error_declared_width_drop line 442