OAI/Analysis/RieszRectifiability/Flatness/AffineTubeCover.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Covering tubes around affine planes

Affine orthogonal projection is distance nonincreasing. Combining this estimate with Euclidean ball nets gives finite covers of bounded tubes, with a cardinality estimate in the dimension of the plane.

  1. theorem OAI.RieszRectifiability.affine_projection_difference line 21
  2. theorem OAI.RieszRectifiability.affine_projection_dist_le line 29
  3. theorem OAI.RieszRectifiability.exists_affine_tube_ball_cover line 35