OAI/Analysis/RieszRectifiability/Rigidity/PlanarReflectionlessSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reflectionless measures supported on a plane

Compactly supported plane tests extend to ambient tests, allowing the isometric pullback of a plane-supported measure to inherit reflectionlessness. Upper and lower growth bounds then give full support in the intrinsic coordinates. Recovering the ambient measure identifies its support with the entire isometric plane.

  1. theorem OAI.RieszRectifiability.planarPullbackMeasure_reflectionless line 24
  2. theorem OAI.RieszRectifiability.planar_full_support_of_reflectionless line 80