Kantorovich duality for costs bounded below

For an extended-real cost bounded below by integrable marginal terms, subtracting those terms reduces both the primal and dual problems to the nonnegative cost regime. This file proves weak duality on arbitrary measurable spaces and strong duality on Polish spaces when the nonnegative residual is lower semicontinuous. In particular, this holds for lower semicontinuous costs with upper semicontinuous split lower bounds.

The supremum of the dual values is taken in EReal, without truncation at zero: the common value can be negative or infinite. Feasible potentials are real and integrable, and their constraint is stated directly as φ x + ψ y ≤ c (x, y). No dual attainment is asserted.

Main results

• TauCeti.dualFeasible_residual_iff: normalization of the signed dual constraint.
• TauCeti.kantorovichDualValue_le_transportCostBddBelow: weak duality for signed costs.
• TauCeti.isLUB_kantorovichDualValue_of_lowerSemicontinuous_residual_bddBelow: Polish strong duality for a lower semicontinuous residual.
• TauCeti.isLUB_kantorovichDualValue_of_lowerSemicontinuous_bddBelow: Polish strong duality.
• TauCeti.transportCostBddBelow_eq_sSup_kantorovichDualValue: its supremum formula.

References

• C. Villani, Optimal Transport: Old and New, Springer, 2009, Theorem 5.10.

@[simp]

theorem TauCeti.dualFeasible_residual_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {φ : X → ℝ} {ψ : Y → ℝ} (h : IntegrableSplitLowerBound c μ ν) : (DualFeasible (fun (z : X × Y) => ↑(h.residual z)) (fun (x : X) => φ x - h.fst x) fun (y : Y) => ψ y - h.snd y) ↔ DualFeasible c φ ψ

Subtracting a split lower bound from each potential identifies the signed dual constraint with dual feasibility for the nonnegative residual cost.

theorem TauCeti.kantorovichDualValue_le_planCostBddBelow {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {φ : X → ℝ} {ψ : Y → ℝ} (h : IntegrableSplitLowerBound c μ ν) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hf : DualFeasible c φ ψ) {π : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) : ↑(kantorovichDualValue μ ν φ ψ) ≤ planCostBddBelow π hπ h

Weak duality against a fixed coupling for an extended-real cost bounded below by integrable marginal terms.

theorem TauCeti.kantorovichDualValue_le_transportCostBddBelow {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {φ : X → ℝ} {ψ : Y → ℝ} (h : IntegrableSplitLowerBound c μ ν) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hf : DualFeasible c φ ψ) : ↑(kantorovichDualValue μ ν φ ψ) ≤ transportCostBddBelow c μ ν h

Weak duality for the signed primal infimum. No topological, probability, or finite-cost hypothesis is needed.

theorem TauCeti.isLUB_kantorovichDualValue_of_lowerSemicontinuous_residual_bddBelow {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [TopologicalSpace X] [PolishSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [BorelSpace Y] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h : IntegrableSplitLowerBound c μ ν) (hres : LowerSemicontinuous h.residual) : IsLUB {r : EReal | ∃ (φ : X → ℝ) (ψ : Y → ℝ), MeasureTheory.Integrable φ μ ∧ MeasureTheory.Integrable ψ ν ∧ DualFeasible c φ ψ ∧ ↑(kantorovichDualValue μ ν φ ψ) = r} (transportCostBddBelow c μ ν h)

Polish Kantorovich duality for costs bounded below. If the nonnegative residual of an integrable split lower bound is lower semicontinuous, the signed primal value is the least upper bound of the values of all integrable feasible real potentials. The value may be negative or ∞; no integrable split upper envelope or dual attainment is assumed.

theorem TauCeti.transportCostBddBelow_eq_sSup_kantorovichDualValue_of_lowerSemicontinuous_residual {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [TopologicalSpace X] [PolishSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [BorelSpace Y] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h : IntegrableSplitLowerBound c μ ν) (hres : LowerSemicontinuous h.residual) : transportCostBddBelow c μ ν h = sSup {r : EReal | ∃ (φ : X → ℝ) (ψ : Y → ℝ), MeasureTheory.Integrable φ μ ∧ MeasureTheory.Integrable ψ ν ∧ DualFeasible c φ ψ ∧ ↑(kantorovichDualValue μ ν φ ψ) = r}

The signed transport value is the supremum in EReal of all integrable feasible dual values on Polish spaces when the residual of an integrable split lower bound is lower semicontinuous.

theorem TauCeti.isLUB_kantorovichDualValue_of_lowerSemicontinuous_bddBelow {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [TopologicalSpace X] [PolishSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [BorelSpace Y] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h : IntegrableSplitLowerBound c μ ν) (hc : LowerSemicontinuous c) (ha : UpperSemicontinuous h.fst) (hb : UpperSemicontinuous h.snd) : IsLUB {r : EReal | ∃ (φ : X → ℝ) (ψ : Y → ℝ), MeasureTheory.Integrable φ μ ∧ MeasureTheory.Integrable ψ ν ∧ DualFeasible c φ ψ ∧ ↑(kantorovichDualValue μ ν φ ψ) = r} (transportCostBddBelow c μ ν h)

For a lower semicontinuous extended-real cost with an integrable upper semicontinuous split lower bound on Polish spaces, the signed primal value is the least upper bound of the values of all integrable feasible real potentials.

theorem TauCeti.transportCostBddBelow_eq_sSup_kantorovichDualValue {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [TopologicalSpace X] [PolishSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [BorelSpace Y] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (h : IntegrableSplitLowerBound c μ ν) (hc : LowerSemicontinuous c) (ha : UpperSemicontinuous h.fst) (hb : UpperSemicontinuous h.snd) : transportCostBddBelow c μ ν h = sSup {r : EReal | ∃ (φ : X → ℝ) (ψ : Y → ℝ), MeasureTheory.Integrable φ μ ∧ MeasureTheory.Integrable ψ ν ∧ DualFeasible c φ ψ ∧ ↑(kantorovichDualValue μ ν φ ψ) = r}

The signed transport value is the supremum in EReal of all integrable feasible dual values, for lower semicontinuous costs on Polish spaces with an integrable upper semicontinuous split lower bound.