OAI/MeasureTheory/Falconer/Angular/AngularStateData.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PlanarFalconer.AngularStateData line 10
  2. def OAI.PlanarFalconer.AngularStateData.profile line 29
  3. def OAI.PlanarFalconer.AngularStateData.retainedList line 31
  4. def OAI.PlanarFalconer.AngularStateData.cellEnergy line 34
  5. def OAI.PlanarFalconer.AngularStateData.energy line 45
  6. def OAI.PlanarFalconer.AngularStateData.childEnergy line 49
  7. def OAI.PlanarFalconer.AngularStateData.children line 54
  8. def OAI.PlanarFalconer.AngularStateData.childMaximum line 57
  9. theorem OAI.PlanarFalconer.AngularStateData.child_budget line 62
  10. theorem OAI.PlanarFalconer.AngularStateData.cellEnergy_finite line 68
  11. theorem OAI.PlanarFalconer.AngularStateData.childMaximum_nonneg line 82
  12. theorem OAI.PlanarFalconer.AngularStateData.childMaximum_empty line 86
  13. theorem OAI.PlanarFalconer.AngularStateData.childMaximum_attained line 91