OAI/Analysis/RieszRectifiability/Foundations/PlanarPullbackMeasure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Pullback along the adjoint of an isometric embedding transports a measure supported on its range to Euclidean coordinates, preserving ball masses and upper growth bounds.

  1. def OAI.RieszRectifiability.planarPullbackMeasure line 19
  2. theorem OAI.RieszRectifiability.planarPullbackMeasure_recover line 22
  3. theorem OAI.RieszRectifiability.planarPullbackMeasure_ball line 36
  4. theorem OAI.RieszRectifiability.planarPullbackMeasure_growth line 51
  5. theorem OAI.RieszRectifiability.globalGrowth_finite_on_compacts line 59
  6. theorem OAI.RieszRectifiability.planarPullbackMeasure_support_iff line 65
  7. theorem OAI.RieszRectifiability.planarPullbackMeasure_lower line 71
  8. theorem OAI.RieszRectifiability.planarPullbackMeasure_ne_zero line 81