OAI/NumberTheory/Jacobsthal/Estimates/SourceReferenceRemainders.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.MovingGapHighRemoval.growing_gap_high_removal line 19
2. theorem OAI.Erdos970.NumberTheoryLean.LargeCutoffResidual.large_cutoff_relative_power line 44
3. theorem OAI.Erdos970.NumberTheoryLean.HighGapResidual.high_gap_residual_power line 117
4. theorem OAI.Erdos970.NumberTheoryLean.LowStateResidualBound.low_state_normalized_residual line 195
5. def OAI.Erdos970.NumberTheoryLean.HighResidualSum.highResidualAbsoluteSum line 280
6. theorem OAI.Erdos970.NumberTheoryLean.HighResidualSum.source_residual_crude line 284
7. theorem OAI.Erdos970.NumberTheoryLean.HighResidualSum.high_residual_sum_bound line 303
8. def OAI.Erdos970.NumberTheoryLean.SharpRetainedResidual.retainedResidualAbsoluteSum line 400
9. theorem OAI.Erdos970.NumberTheoryLean.SharpRetainedResidual.retained_residual_sum_bound line 403
10. theorem OAI.Erdos970.NumberTheoryLean.SharpGlobalResidual.actual_residual_partition line 494
11. theorem OAI.Erdos970.NumberTheoryLean.SharpGlobalResidual.sharp_source_residual_sum line 499
12. theorem OAI.Erdos970.NumberTheoryLean.SharpGlobalResidual.sharp_signed_residual line 543
13. theorem OAI.Erdos970.NumberTheoryLean.GlobalReferenceApproximation.global_reference_remainder line 562
14. theorem OAI.Erdos970.ErdosSourceReferenceMargin.root_source_remainder_tendsto line 590
15. theorem OAI.Erdos970.ErdosSourceReferenceMargin.root_anomaly_replacement_tendsto line 605