OAI/NumberTheory/Jacobsthal/Partitions/ActualCoordinateBlocks.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosVarianceEffective.intervalK line 12
2. def OAI.Erdos970.ErdosVarianceEffective.intervalM0 line 15
3. theorem OAI.Erdos970.ErdosVarianceEffective.intervalK_lt line 18
4. theorem OAI.Erdos970.ErdosVarianceEffective.interval_numerator_dvd line 21
5. theorem OAI.Erdos970.ErdosVarianceEffective.intervalM0_identity line 31
6. theorem OAI.Erdos970.ErdosVarianceEffective.intervalM0_modEq line 36
7. theorem OAI.Erdos970.ErdosVarianceEffective.intervalM0_bounds line 42
8. theorem OAI.Erdos970.ErdosVarianceEffective.intervalM0_unique line 58
9. theorem OAI.Erdos970.ErdosLargeHeightBlocks.actual_m0_block_interval line 91
10. theorem OAI.Erdos970.ErdosLargeHeightBlocks.actual_large_height_blocks line 102