OAI/Geometry/RCD/Heat/EntropyPowerBarrier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The explicit entropy-power barrier and its initial rate

  1. def OAI.RegularPointCoordinates.entropyPowerChord line 10
  2. def OAI.RegularPointCoordinates.entropyPowerChordDerivative line 13
  3. def OAI.RegularPointCoordinates.entropyPowerRate line 16
  4. theorem OAI.RegularPointCoordinates.entropyPowerChord_zero line 19
  5. theorem OAI.RegularPointCoordinates.hasDerivAt_entropyPowerChord_zero line 25
  6. theorem OAI.RegularPointCoordinates.entropyPowerRate_eq line 38