OAI/Geometry/RCD/Coordinates/NormalizedHeatEntropy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The entropy response of the normalized heat perturbation

  1. theorem OAI.RegularPointCoordinates.entropy_density_mul line 13
  2. theorem OAI.RegularPointCoordinates.exponentialTiltLp_integrable line 22
  3. theorem OAI.RegularPointCoordinates.integral_entropy_mul line 33
  4. theorem OAI.RegularPointCoordinates.heat_normalized_entropy_hasDerivAt_zero line 44