OAI/MeasureTheory/Falconer/Graphs/ParentRetainedEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.sourceParentDistanceF line 10
2. def OAI.PlanarFalconer.sourceParentDiscardedF line 16
3. def OAI.PlanarFalconer.sourceParentRetainedF line 23
4. theorem OAI.PlanarFalconer.sourceAngularShellMeasure_ae_nonzero line 30
5. theorem OAI.PlanarFalconer.sourceParentF_partition line 39
6. theorem OAI.PlanarFalconer.sourceParentRetainedF_measurable line 56
7. theorem OAI.PlanarFalconer.sourceParentDistanceF_measurable line 66
8. theorem OAI.PlanarFalconer.parent_retained_energy_error_le line 75