OAI/Geometry/RCD/Metric/ScaledCompactHamiltonJacobi.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact viscous Hamilton--Jacobi equation at small-noise scale

Both the local weak source and the gradient square refer to the same scaled Sobolev representative of the actual logarithmic heat factor.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_factor_scaled_hamilton_jacobi line 21