OAI/Geometry/RCD/Heat/HeatEntropyVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Boltzmann entropy differentiates along the actual exponential heat variation

  1. theorem OAI.RegularPointCoordinates.heat_exponential_entropy_hasDerivAt_zero line 15