OAI/MeasureTheory/Falconer/Estimates/RegularizationLabels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarFalconer.CellPath line 10
  2. def OAI.PlanarFalconer.labeledChildren line 12
  3. def OAI.PlanarFalconer.extendLabel line 17
  4. def OAI.PlanarFalconer.upwardLabels line 21
  5. theorem OAI.PlanarFalconer.take_eq_of_take_eq line 26
  6. theorem OAI.PlanarFalconer.labeledChildren_eq line 31
  7. theorem OAI.PlanarFalconer.labeledChildren_nonempty line 37
  8. theorem OAI.PlanarFalconer.extendLabel_old line 43
  9. theorem OAI.PlanarFalconer.extendLabel_local line 47
  10. theorem OAI.PlanarFalconer.upwardLabels_old line 55
  11. theorem OAI.PlanarFalconer.upwardLabels_local line 62
  12. theorem OAI.PlanarFalconer.final_labeledChildren_eq line 72
  13. theorem OAI.PlanarFalconer.final_child_count_bin line 88
  14. theorem OAI.PlanarFalconer.final_child_count_bounds line 99