OAI/Geometry/RCD/Metric/CanonicalBallMassLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed positive heat mass in every diffusive ball

Symmetry places the volume normalization at the fixed pole. Integration then cancels that volume exactly, without any boundary regularity.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_ball_mass_lower line 20