OAI/NumberTheory/Jacobsthal/Estimates/ReferenceSourceDecomposition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.ActualBoundaryDomain.BoundaryDomain line 19
2. theorem OAI.Erdos970.NumberTheoryLean.ActualBoundaryDomain.child_boundary_domain line 23
3. theorem OAI.Erdos970.NumberTheoryLean.ActualBoundaryDomain.boundary_domain_preserved line 54
4. theorem OAI.Erdos970.NumberTheoryLean.ActualBoundaryDomain.source_boundary_domain line 65
5. theorem OAI.Erdos970.NumberTheoryLean.ActualBoundaryDomain.boundary_gap_ge_two line 92
6. def OAI.Erdos970.NumberTheoryLean.UniformBoundaryCorrection.boundaryCorrection line 109
7. theorem OAI.Erdos970.NumberTheoryLean.UniformBoundaryCorrection.uniform_boundary_correction line 113
8. theorem OAI.Erdos970.NumberTheoryLean.UniformBoundaryCorrection.uniform_boundary_correction_div line 137
9. def OAI.Erdos970.NumberTheoryLean.ReferenceSourceDecomposition.sourceReference line 164
10. def OAI.Erdos970.NumberTheoryLean.ReferenceSourceDecomposition.residualCorrection line 167
11. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourceDecomposition.suffix_highPrimes line 170
12. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourceDecomposition.uncapped_cutoff_gt_two line 184
13. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourceDecomposition.forest_insertion_eq_corrections line 193
14. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourceDecomposition.actual_reference_decomposition line 212
15. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourceDecomposition.actual_reference_value line 220