OAI/Analysis/RieszRectifiability/Foundations/JointFitBasePoints.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded base points for jointly fitting planes

A lower mass bound and a small integral joint-fit error produce a point close to both affine planes. Orthogonal projection of that point supplies base points on each plane with norm bounded by the ball radius plus the fitting tolerance.

  1. theorem OAI.RieszRectifiability.exists_small_norm_points_on_joint_fits line 22