OAI/Analysis/RieszRectifiability/Projections/NonemptyAffineProjectionIncrement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Increments of affine projections

Affine projection increments are projections onto the direction subspace. Consequently, operator-norm bounds for two direction projections control the difference of increments.

  1. theorem OAI.RieszRectifiability.nonemptyAffineProjection_sub line 19
  2. theorem OAI.RieszRectifiability.nonemptyAffineProjection_increment_difference_le line 27