OAI/Geometry/RCD/Heat/HeatBoundedLaplacian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Heat displacement of a function with bounded weak Laplacian

The semigroup derivative and conservation control its pairing with every nonnegative L¹ ∩ L² test. This is the input for short-time concentration of the constructed transition measures.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_bounded_laplacian_pairing line 25