OAI/MeasureTheory/Falconer/Angular/AngularStateSuccessor.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PlanarFalconer.AngularStateData.successorline 11 - theorem
OAI.PlanarFalconer.AngularStateData.successor_energyline 14 - theorem
OAI.PlanarFalconer.AngularStateData.children_lengthsline 19 - theorem
OAI.PlanarFalconer.AngularStateData.remaining_energy_eq_childline 29 - theorem
OAI.PlanarFalconer.AngularStateData.remaining_maximum_eq_childline 41 - theorem
OAI.PlanarFalconer.AngularStateData.retained_length_le_Nline 55