OAI/Analysis/RieszRectifiability/Kernel/LeastSquaredExcess.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Least-squared approximation by affine planes

The squared excess minimizes the radius-normalized quadratic distance over affine planes of the prescribed dimension. Local finiteness ensures that these distance integrals exist on balls.

  1. def OAI.RieszRectifiability.IsAffineNPlane line 20
  2. def OAI.RieszRectifiability.quadraticPlaneError line 23
  3. def OAI.RieszRectifiability.squaredExcess line 27
  4. theorem OAI.RieszRectifiability.squared_infDist_integrableOn_ball line 31
  5. theorem OAI.RieszRectifiability.quadraticPlaneError_nonneg line 47
  6. theorem OAI.RieszRectifiability.squaredExcess_nonneg line 53
  7. theorem OAI.RieszRectifiability.squaredExcess_le_planeError line 59
  8. theorem OAI.RieszRectifiability.squaredExcess_div_sq_le line 69
  9. theorem OAI.RieszRectifiability.squaredExcess_ratio_tendsto_zero_of_planes line 81