OAI/Analysis/RieszRectifiability/Flatness/PlaneMomentTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Transfer of squared plane-distance moments

A pointwise comparison of distances to two affine planes yields a comparison of their second moments on a ball. The additive distance error contributes its square times the ball mass, using local finiteness to justify integration.

  1. theorem OAI.RieszRectifiability.plane_distance_second_moment_transfer line 22
  2. theorem OAI.RieszRectifiability.plane_second_moment_bound_from_distance_transfer line 51