OAI/Geometry/RCD/Transport/RenyiSemicontinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Weak upper semicontinuity of the finite-volume Rényi integral

The dual formula includes measures with singular parts. The logarithmic test is sent to positive infinity on the singular support and clipped on its complement, so that no absolute continuity of a weak limit is assumed.

  1. theorem OAI.RegularPointCoordinates.renyiDualValue_nonneg line 19
  2. theorem OAI.RegularPointCoordinates.renyiDual_ne_top line 27
  3. theorem OAI.RegularPointCoordinates.renyiDual_le_measurable line 30
  4. theorem OAI.RegularPointCoordinates.renyiDual_eq_power line 42
  5. theorem OAI.RegularPointCoordinates.upperSemicontinuous_renyiPower line 99