OAI/Analysis/RieszRectifiability/Flatness/AffineAnchorBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An affine map controlled at a base point and its basis anchors is controlled at every affine combination by the sum of the absolute coordinates. The operator norm of the basis-coordinate map bounds that sum in terms of the dimension and the ambient norm on the subspace.

  1. theorem OAI.RieszRectifiability.affine_map_norm_bound_from_anchors line 19
  2. def OAI.RieszRectifiability.basisCoordinateNorm line 44
  3. theorem OAI.RieszRectifiability.basisCoordinateNorm_nonneg line 49
  4. theorem OAI.RieszRectifiability.basis_coordinate_l1_bound line 55