OAI/Analysis/RieszRectifiability/Flatness/LocalPlaneDirectionComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Comparing nearby plane directions

Distances to affine planes control normal projections of differences. Directional projection bounds can then be composed through an intermediate linear subspace.

  1. theorem OAI.RieszRectifiability.normal_projection_bound_by_plane_distances line 19
  2. theorem OAI.RieszRectifiability.direction_normal_bound_of_local_plane_tube line 37
  3. theorem OAI.RieszRectifiability.compose_direction_normal_bounds line 69