OAI/Geometry/RCD/Heat/ScaledHeatAveragedHamiltonJacobi.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Differential Hamilton--Jacobi inequality for the actual time average

The continuous Sobolev average has its actual L2 derivative, and every nonnegative compact Lipschitz spatial test satisfies the differential energy inequality against this same derivative.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_averaged_hamilton_jacobi_of_compactness line 22