OAI/MeasureTheory/Falconer/Recursion/SuffixRetainedPairs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.PositiveDistanceData.suffixRectangles line 11
2. def OAI.PlanarFalconer.PositiveDistanceData.suffixRetained line 14
3. abbrev OAI.PlanarFalconer.PositiveDistanceData.suffixData line 19
4. def OAI.PlanarFalconer.PositiveDistanceData.suffixFullDistance line 22
5. instance OAI.PlanarFalconer.PositiveDistanceData.suffixFullDistance_finite line 25
6. theorem OAI.PlanarFalconer.PositiveDistanceData.suffix_retained_spec line 30
7. theorem OAI.PlanarFalconer.PositiveDistanceData.cellPair_split_suffix line 41
8. theorem OAI.PlanarFalconer.PositiveDistanceData.pair_zero_of_no_witness line 55
9. theorem OAI.PlanarFalconer.PositiveDistanceData.pair_split_retained line 68
10. theorem OAI.PlanarFalconer.PositiveDistanceData.distance_split_retained line 82