OAI/NumberTheory/Ostmann/QuadraticCenter/NumericCommonCenterMargins.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds line 10
2. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.Z_pos line 24
3. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.rpow_large line 26
4. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.J_one_le line 30
5. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.descFactorial_half line 34
6. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.cutoff_bounds line 49
7. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.cutoff_power_ten line 57
8. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.incidence_gap line 64
9. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.height_spacing line 90
10. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.momentScale_large line 93
11. theorem OAI.Ostmann.QuadraticCenter.CommonCenterElementaryBounds.lower_moment_negligible line 102