OAI/Analysis/RieszRectifiability/Projections/AffineProjectionCloseness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Affine orthogonal projections are compared using their separation at a base point and the operator-norm difference of the projections onto their direction subspaces.

  1. theorem OAI.RieszRectifiability.affine_projection_pair_base_bound line 17
  2. theorem OAI.RieszRectifiability.affine_projection_pair_dist_bound line 28