OAI/Geometry/RCD/Transport/RenyiDualScore.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A bounded dual approximation for the finite Rényi entropy

The logarithmic tests are clipped at finite levels. Their nonnegative scores have an integrable bound independent of the clipping level. This is the scalar ingredient of the semicontinuity used in the entropy minimizing midpoint construction of Rajala, arXiv:1202.6514, Lemma 2.4.

  1. def OAI.RegularPointCoordinates.renyiDualScore line 19
  2. theorem OAI.RegularPointCoordinates.renyiDualScore_nonneg line 22
  3. theorem OAI.RegularPointCoordinates.renyiDualScore_log line 27
  4. theorem OAI.RegularPointCoordinates.rpow_le_renyiDualScore line 39
  5. theorem OAI.RegularPointCoordinates.renyiDualScore_logTest_bound line 51
  6. theorem OAI.RegularPointCoordinates.renyiDualScore_logTest_tendsto line 81