OAI/Geometry/RCD/Heat/BoundedHeatVelocityHessian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact velocity-minus-osmotic decomposition for the heat Hessian term

The local logarithms and all their Gram representatives are constructed. The identity retains the actual product density and the physical scale.

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