OAI/Geometry/RCD/Transport/RenyiDualIntegral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dual scores and the absolutely continuous density

The singular part of a finite measure is retained explicitly. In particular the tangent inequality does not assume absolute continuity.

  1. theorem OAI.RegularPointCoordinates.integral_renyiDualScore_logTest_tendsto line 18
  2. theorem OAI.RegularPointCoordinates.renyiDualValue_decomposition line 37
  3. theorem OAI.RegularPointCoordinates.renyiPower_le_dualValue line 84
  4. theorem OAI.RegularPointCoordinates.renyiPower_le_dual line 115