OAI/Geometry/RCD/Coordinates/RegularizedEntropyFirstVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional first variation for the actual regularized log direction

  1. theorem OAI.RegularPointCoordinates.regularized_entropy_power_first_variation line 15