OAI/Geometry/RCD/Transport/RenyiSingularReplacement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing singular mass strictly improves the Rényi integral

The replacement measure retains the original absolutely continuous part and adds a nonzero absolutely continuous measure. This handles possible singular parts of an entropy-maximizing midpoint before any density bound.

  1. theorem OAI.RegularPointCoordinates.integral_rpow_add_strict line 18
  2. theorem OAI.RegularPointCoordinates.renyi_singular_replacement_strict line 42