← Mathematical handbook

Unconditional attained transport duality for every positive multiplier

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.transport_primal_dual_attained {t : ℝ} (ht : 0 < t) : ∃ (D : ProbabilityTheory.Copula 2) (f : ↑unitInterval → ℝ), Continuous f ∧ (∀ (x : Fin 2 → ↑unitInterval), magnitudeCost t x ≤ f (x 0) + f (x 1)) ∧ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂D.toMeasure, magnitudeCost t x = f (x 0) + f (x 1)

No contact or optimizer assumption: both are constructed for every t>0.

def Papers.AnsariRockelSteinmassl2026RhoGamma.dualCosts (t : ℝ) : Set ℝ

Feasible symmetric continuous dual potentials, as in equation (33).

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.transport_strong_duality {t : ℝ} (ht : 0 < t) : IsLeast (dualCosts t) (transportValue t)

Remark 3.4: the primal supremum is the attained dual infimum.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.transportValue_eq_dual_infimum {t : ℝ} (ht : 0 < t) : transportValue t = sInf (dualCosts t)

Equality with the dual infimum, with no supplied certificate.