OAI/Geometry/RCD/Metric/InnerBallValueMoments.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local value convergence gives the actual normalized quadratic moments

  1. theorem OAI.RegularPointCoordinates.inner_ball_value_moment_tendsto line 14