OAI/Geometry/RCD/Heat/EntropyPowerRateContinuous.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Continuity of the dimensional entropy rate at zero distance as well

  1. def OAI.RegularPointCoordinates.sinhSlope line 12
  2. theorem OAI.RegularPointCoordinates.sinhSlope_zero line 14
  3. theorem OAI.RegularPointCoordinates.sinhSlope_of_ne_zero line 16
  4. theorem OAI.RegularPointCoordinates.continuous_sinhSlope line 19
  5. theorem OAI.RegularPointCoordinates.entropyPowerRate_formula line 31
  6. theorem OAI.RegularPointCoordinates.tendsto_entropyPowerRate line 39