OAI/Analysis/RieszRectifiability/Flatness/AssembledAffineHeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Assembling affine height coordinates

Coordinatewise continuous linear maps assemble into a Euclidean-valued map. Their affine extensions give an ambient vector-valued affine map, whose Lipschitz constant is bounded by the operator norm of its linear part.

  1. def OAI.RieszRectifiability.assembleCoordinateLinear line 21
  2. theorem OAI.RieszRectifiability.assembleCoordinateLinear_apply line 26
  3. theorem OAI.RieszRectifiability.exists_ambient_vector_affine line 29
  4. theorem OAI.RieszRectifiability.vectorAffine_lipschitz line 42