OAI/Geometry/RCD/Heat/ScaledHeatHamiltonJacobiFromCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weak Hamilton--Jacobi inequality for a prescribed heat limit

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_hamilton_jacobi_subsolution_of_compactness line 25