OAI/NumberTheory/Jacobsthal/Analysis/ContinuousReference.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosContinuousBoundary.truncatedReference line 15
2. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_zero_of_index line 18
3. theorem OAI.Erdos970.ErdosContinuousBoundary.truncatedReference_stable line 26
4. def OAI.Erdos970.ErdosContinuousBoundary.referenceDepth line 36
5. theorem OAI.Erdos970.ErdosContinuousBoundary.referenceDepth_bounds line 38
6. def OAI.Erdos970.ErdosContinuousBoundary.boundaryReference line 47
7. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryReference_eq_truncated line 50
8. theorem OAI.Erdos970.ErdosContinuousBoundary.truncatedReference_continuous line 57
9. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryReference_continuous line 63