OAI/NumberTheory/Jacobsthal/Analysis/PaperContinuousCorrection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosCorrectionLimit.paperStart line 19
2. theorem OAI.Erdos970.ErdosCorrectionLimit.paper_start_eventually line 26
3. theorem OAI.Erdos970.ErdosCorrectionLimit.paper_normalized_correction_tendsto line 43
4. theorem OAI.Erdos970.ErdosCorrectionLimit.paper_continuous_correction_tendsto line 59
5. theorem OAI.Erdos970.ErdosCorrectionLimit.paper_z_continuous_correction_tendsto line 74