OAI/NumberTheory/Jacobsthal/Estimates/PairedBlockContraction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.PairedBlockContraction.moment_add_constant line 15
2. theorem OAI.Erdos970.NumberTheoryLean.PairedBlockContraction.actual_block_contraction line 23
3. theorem OAI.Erdos970.NumberTheoryLean.PairedBlockContraction.paired_survival_geometric line 65
4. theorem OAI.Erdos970.NumberTheoryLean.PairedBlockContraction.paired_survival_tendsto_zero line 103