OAI/Geometry/RCD/Heat/ScaledHeatContinuousHamiltonJacobi.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The continuous representative satisfies the same Hamilton--Jacobi inequality

The Sobolev energy of the limiting function is bounded by twice its time derivative in the distributional sense. The tests retain their exact compact weak Laplacians, nonnegativity and common inner support.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_continuous_hamilton_jacobi_of_compactness line 27