OAI/Geometry/RCD/Heat/HeatOsmoticNoiseRate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Explicit local osmotic decay for the actual RCD heat evolution

Only values and local gradient bounds of the logarithmic representatives are required. Their mixed chain rules and the energy inequality are proved from the original heat data.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_osmotic_noise_rate line 24