OAI/NumberTheory/Jacobsthal/Estimates/FundamentalBlockEstimate.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.product_upper_estimate line 17
2. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.correction_upper_estimate line 35
3. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.exp_sub_one_le_self_mul_exp line 66
4. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.global_relative_error line 72
5. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.baseError line 112
6. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.baseError_nonneg line 114
7. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.baseError_add line 116
8. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.sum_scheduled_error_le line 123
9. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.six_baseError_le_exp line 136
10. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.scheduled_global_error_le_exp line 162
11. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.blockEuler line 183
12. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.blockUpperDensity line 186
13. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.blockOverflowDensity line 190
14. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.actual_local_density_inputs line 194
15. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.actualUpperDensity line 223
16. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.actualLowerDensity line 228
17. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.actual_global_density_error line 231
18. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.actualUpperCoefficient line 264
19. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.actualUpperCoefficient_support line 268
20. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.levelSubsets line 283
21. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.coefficient_remainder_level_bound line 286
22. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.additive_bounds_of_relative line 299
23. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.finite_fundamental_lemma line 306
24. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.levelDivisors line 353
25. def OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.integerRemainder line 356
26. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.remainder_sum_eq_divisors line 360
27. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.finite_fundamental_integer_level line 392
28. theorem OAI.Erdos970.NumberTheoryLean.FundamentalBlockEstimate.fundamental_integer_parameter line 407