OAI/Geometry/RCD/Heat/HeatLocalBochnerMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual heat Bochner measures have vanishing local mass near a flat harmonic function

Both the regularizations and their sources are the original heat semigroup. The measures satisfy the full continuous compact Sobolev test identity; their singular parts are retained in the mass limit.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_local_bochner_mass line 24