OAI/Geometry/RCD/Coordinates/NormalizedUniformL2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform almost-everywhere convergence gives normalized L2 convergence

The measures may vary and their masses need not be bounded away from zero. Only positivity and finiteness of each normalizing mass are used.

  1. theorem OAI.RegularPointCoordinates.normalized_sq_mean_tendsto_zero line 17