OAI/Analysis/RieszRectifiability/Flatness/OpenPlaneBoxes.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Open projection boxes and coordinate-plane measures

Pulling back open boxes along continuous coordinates gives open subsets of the ambient space. Coordinate-plane measures satisfy upper growth bounds, which in turn imply finiteness on compact sets.

  1. def OAI.RieszRectifiability.coordinatePlaneMeasure line 21
  2. def OAI.RieszRectifiability.openProjectionBox line 24
  3. theorem OAI.RieszRectifiability.openProjectionBox_isOpen line 27
  4. theorem OAI.RieszRectifiability.coordinatePlaneMeasure_restrict_openBox line 31
  5. theorem OAI.RieszRectifiability.coordinatePlaneMeasure_upper_growth line 42
  6. theorem OAI.RieszRectifiability.GlobalUpperGrowth.finite_on_compacts line 66
  7. theorem OAI.RieszRectifiability.coordinatePlaneMeasure_finite_on_compacts line 72