OAI/MeasureTheory/Falconer/Frostman/Capacity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PlanarFalconer.CapacityTree line 11
  2. def OAI.PlanarFalconer.CapacityTree.rootCapacity line 15
  3. def OAI.PlanarFalconer.CapacityTree.nonnegative line 19
  4. def OAI.PlanarFalconer.CapacityTree.effective line 24
  5. inductive OAI.PlanarFalconer.CutCost line 28
  6. theorem OAI.PlanarFalconer.effective_le_root line 35
  7. theorem OAI.PlanarFalconer.effective_le_cut line 40
  8. theorem OAI.PlanarFalconer.effective_cut line 47
  9. theorem OAI.PlanarFalconer.effective_is_minimum_cut line 59
  10. theorem OAI.PlanarFalconer.effective_nonnegative line 63
  11. theorem OAI.PlanarFalconer.split_four line 71
  12. inductive OAI.PlanarFalconer.Routes line 93
  13. theorem OAI.PlanarFalconer.routes_of_le_effective line 101
  14. theorem OAI.PlanarFalconer.routes_of_cut_lower_bound line 114