OAI/Analysis/RieszRectifiability/Flatness/AmbientAffineHeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ambient extensions of affine plane heights

The adjoint of a linear isometric embedding extends an affine height from plane coordinates to the ambient space. Its operator norms give a Lipschitz bound, and the pullback identity transfers almost-everywhere affine agreement to the coordinate plane measure.

  1. def OAI.RieszRectifiability.ambientAffineHeight line 22
  2. theorem OAI.RieszRectifiability.ambientAffineHeight_lipschitz line 26
  3. theorem OAI.RieszRectifiability.ambientAffineHeight_pullback line 40
  4. theorem OAI.RieszRectifiability.height_ae_eq_ambient_affine line 47