OAI/Geometry/RCD/Coordinates/ScalingDualPotential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Dual potentials from exact compact scaling normalization

The support of the second marginal is retained explicitly. Each row has zero maximal limiting slack on that support.

  1. theorem OAI.RegularPointCoordinates.scaling_dual_potential line 19