OAI/Geometry/RCD/Heat/BoundedHeatGram.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Sobolev energy densities for the actual bounded heat factors

The initial L2 function need not have compact support or be Lipschitz. The positive-time gradient bound and the existing Bochner estimate supply the Sobolev representative of its squared gradient.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_gram_of_gradient_bound line 24
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_gram line 53