OAI/Geometry/RCD/Transport/ShiftedEntropyBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-range shifted entropy and its affine upper bound

  1. theorem OAI.RegularPointCoordinates.shiftedEntropy_le_affine line 12
  2. theorem OAI.RegularPointCoordinates.shiftedEntropy_memLp line 23
  3. theorem OAI.RegularPointCoordinates.shiftedEntropy_weighted_integrable line 33