OAI/Analysis/RieszRectifiability/Nets/FittedCellShadow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An affine fit places a lattice cell in a thin neighborhood of a plane. Contraction along one plane direction bounds the Hausdorff measure of the cell's image.

  1. theorem OAI.RieszRectifiability.fitted_cell_contracted_shadow_bound line 20
  2. theorem OAI.RieszRectifiability.projection_conditioned_cell_shadow_bound line 52