OAI/Geometry/RCD/Heat/HeatEntropyInterpolation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Regularized entropy along actual RCD heat interpolation

The gradient bounds used in differentiating the nonlinear pairing are provided by the proved bounded-data smoothing theorem.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_entropy_interpolation_derivative line 23
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_entropy_interpolation_monotone line 41