OAI/Analysis/RieszRectifiability/Kernel/EuclideanCoordinateMoments.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Euclidean second moments from coordinate moments

The squared Euclidean norm is a finite sum of squared coordinates. This identity transfers coordinatewise integrability, integral formulas, and convergence of second moments to their Euclidean counterparts, including varying measures.

  1. theorem OAI.RieszRectifiability.integrable_euclidean_norm_sq_of_coordinates line 20
  2. theorem OAI.RieszRectifiability.integral_euclidean_norm_sq_eq_sum line 27
  3. theorem OAI.RieszRectifiability.euclidean_norm_sq_tendsto_zero_of_coordinates line 34