OAI/Geometry/RCD/Transport/RenyiPathVariation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Localized finite Rényi variations without finite reference volume

Only the restricted path family needs a positive lower density bound. This is suitable for the density-level and displacement truncations used on the noncompact RCD space.

  1. theorem OAI.RegularPointCoordinates.planInitialSecant_renyi_reweight_error_path line 20
  2. theorem OAI.RegularPointCoordinates.planInitialSecant_renyi_reweight_tendsto_path line 66