OAI/MeasureTheory/Falconer/Recursion/ParentBinFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PlanarFalconer.ParentDistanceBinLabel line 8
2. def OAI.PlanarFalconer.sourceParentBinLabels line 10
3. def OAI.PlanarFalconer.sourceParentBinIntegrand line 15
4. theorem OAI.PlanarFalconer.sourceParentRetainedF_bin_sum line 21
5. theorem OAI.PlanarFalconer.sourceParentBinLabels_spec line 39
6. theorem OAI.PlanarFalconer.sourceParentBinLabels_length line 47
7. theorem OAI.PlanarFalconer.sourceParentBinLabels_bin_lt line 55