OAI/Geometry/RCD/Metric/CompactFactorCenteredCompactness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Spatial compactness of the actual normalized entropic potentials

Endpoint scaling functions and interior times may vary along the sequence. Only the common support, noise range and interior-time margin enter the uniform Lipschitz bound. This is spatial compactness; no identification with a transport potential or time convergence is asserted here.

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.scaledCompactHeatPotential line 23
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_factor_centered_compactness line 28