OAI/Analysis/RieszRectifiability/Flatness/JointPlaneGoodSet.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous approximation by two affine planes

The joint squared-distance error defines a good set close to both planes. Its continuity gives local integrability, and an integral error bound yields a lower mass estimate for the good set by controlling the complementary bad set.

  1. def OAI.RieszRectifiability.jointPlaneFitError line 21
  2. def OAI.RieszRectifiability.jointPlaneGoodSet line 25
  3. theorem OAI.RieszRectifiability.jointPlaneFitError_continuous line 29
  4. theorem OAI.RieszRectifiability.jointPlaneFitError_integrableOn_ball line 34
  5. theorem OAI.RieszRectifiability.jointPlaneGoodSet_distance_bounds line 41
  6. theorem OAI.RieszRectifiability.jointPlaneGoodSet_mass_lower line 52