OAI/NumberTheory/Jacobsthal/Renewal/FiniteAdmittedOccupation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.occupation line 20
2. instance OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.occupation_isSFinite line 23
3. theorem OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.restricted_occupation_at line 26
4. theorem OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.admitted_occupation_transform line 46
5. def OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.gapSquaredWeight line 51
6. theorem OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.gapSquaredWeight_measurable line 54
7. theorem OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.scaled_harmonic_weight line 58
8. theorem OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.scaled_ratio line 70
9. theorem OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.scaled_occupation line 81
10. theorem OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.admitted_tilted_occupation line 91
11. theorem OAI.Erdos970.NumberTheoryLean.OriginalHarmonicOccupation.scaled_occupation_arrival line 96
12. theorem OAI.Erdos970.NumberTheoryLean.FiniteAdmittedOccupation.occupation_eq_finite line 117
13. theorem OAI.Erdos970.NumberTheoryLean.FiniteAdmittedOccupation.occupation_integral_eq_finite line 130
14. theorem OAI.Erdos970.NumberTheoryLean.FiniteAdmittedOccupation.admitted_low_signed_error line 140
15. theorem OAI.Erdos970.NumberTheoryLean.FiniteAdmittedOccupation.low_occupation_integral_eq_source_sum line 173