Kantorovich dual feasibility and weak duality

For an extended-real cost c : X × Y → EReal, a pair of real potentials φ and ψ is dual feasible when

φ x + ψ y ≤ c (x, y).

The comparison is made in EReal, so signed costs, negative potential values, and the value ∞ of a forbidden pair are all represented honestly. The dual value is the sum of the two marginal integrals. The weak-duality theorems and integral manipulations that need it require both potentials to be integrable. Integrability is not part of pointwise feasibility, since later c-transform arguments study feasibility before choosing marginals.

For nonnegative costs, weak duality says that the value of every integrable feasible pair is at most the cost of every coupling, and hence at most the primal transport cost. Neither the cost nor its integral needs to be finite or measurable.

Main definitions

• TauCeti.DualFeasible c φ ψ — the pointwise dual constraint;
• TauCeti.kantorovichDualValue μ ν φ ψ — the sum of the two marginal integrals.

Main statements

• TauCeti.dualFeasible_ofReal_iff — for a nonnegative real cost, feasibility for the associated extended cost is the plain real pointwise inequality;
• TauCeti.kantorovichDualValue_eq_integral — against any coupling the dual value is the integral of the split sum of the two potentials;
• TauCeti.DualFeasible.kantorovichDualValue_le_lintegral — weak duality against one coupling;
• TauCeti.DualFeasible.kantorovichDualValue_le_transportCost — weak duality against the primal infimum;
• TauCeti.DualFeasible.add_const_sub_const and TauCeti.kantorovichDualValue_add_const_sub_const — feasibility and value are unchanged by the usual opposite additive shifts when the marginals have equal finite mass.

References

• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §1.1.1, for the Kantorovich dual constraint and weak duality.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, 2009, Chapter 5.

This is Layer 2, item 1 of the optimal-transport roadmap.

def TauCeti.DualFeasible {X : Type u} {Y : Type v} (c : X × Y → EReal) (φ : X → ℝ) (ψ : Y → ℝ) : Prop

A pair of real-valued potentials is dual feasible for c when their split sum is bounded by the cost. The inequality is in EReal, retaining signed costs, negative potential values, and infinite costs.

Equations

• TauCeti.DualFeasible c φ ψ = ∀ (x : X) (y : Y), ↑(φ x) + ↑(ψ y) ≤ c (x, y)

@[simp]

theorem TauCeti.dualFeasible_iff {X : Type u} {Y : Type v} {φ : X → ℝ} {ψ : Y → ℝ} {c : X × Y → EReal} : DualFeasible c φ ψ ↔ ∀ (x : X) (y : Y), ↑(φ x) + ↑(ψ y) ≤ c (x, y)

The pointwise characterization of dual feasibility.

theorem TauCeti.dualFeasible_iff_ofReal_add_le {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ ↔ ∀ (x : X) (y : Y), ENNReal.ofReal (φ x + ψ y) ≤ c (x, y)

Dual feasibility in the equivalent extended-nonnegative form used by lintegral. Taking ENNReal.ofReal loses no information because the cost is nonnegative.

theorem TauCeti.DualFeasible.ofReal_add_le {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} (h : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (x : X) (y : Y) : ENNReal.ofReal (φ x + ψ y) ≤ c (x, y)

A dual-feasible pair satisfies the extended-nonnegative pointwise constraint.

theorem TauCeti.dualFeasible_ofReal_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} (hc : ∀ (z : X × Y), 0 ≤ c z) (φ : X → ℝ) (ψ : Y → ℝ) : DualFeasible (fun (z : X × Y) => ↑(ENNReal.ofReal (c z))) φ ψ ↔ ∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)

Dual feasibility for the extended cost attached to a nonnegative real cost is the plain real pointwise inequality. This is the bridge from a real linear-programming dual constraint to the canonical TauCeti.DualFeasible predicate.

theorem TauCeti.DualFeasible.mono_cost {X : Type u} {Y : Type v} {φ : X → ℝ} {ψ : Y → ℝ} {c c' : X × Y → EReal} (h : DualFeasible c φ ψ) (hcc' : c ≤ c') : DualFeasible c' φ ψ

Increasing the cost preserves dual feasibility.

@[simp]

theorem TauCeti.dualFeasible_zero {X : Type u} {Y : Type v} (c : X × Y → ENNReal) : DualFeasible (fun (z : X × Y) => ↑(c z)) (fun (x : X) => 0) fun (x : Y) => 0

The zero potentials are feasible for every nonnegative extended cost.

theorem TauCeti.DualFeasible.add_const_sub_const {X : Type u} {Y : Type v} {φ : X → ℝ} {ψ : Y → ℝ} {c : X × Y → EReal} (h : DualFeasible c φ ψ) (a : ℝ) : DualFeasible c (fun (x : X) => φ x + a) fun (y : Y) => ψ y - a

Adding a constant to the first potential and subtracting it from the second preserves dual feasibility.

noncomputable def TauCeti.kantorovichDualValue {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (φ : X → ℝ) (ψ : Y → ℝ) : ℝ

The value of a pair of Kantorovich potentials: the sum of its two marginal integrals. The weak-duality theorems require both potentials to be integrable.

Equations

• TauCeti.kantorovichDualValue μ ν φ ψ = ∫ (x : X), φ x ∂μ + ∫ (y : Y), ψ y ∂ν

theorem TauCeti.kantorovichDualValue_def {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (φ : X → ℝ) (ψ : Y → ℝ) : kantorovichDualValue μ ν φ ψ = ∫ (x : X), φ x ∂μ + ∫ (y : Y), ψ y ∂ν

The dual value is the sum of the two marginal integrals. The definition's body is not exposed, so this is the lemma downstream modules should rewrite with.

@[simp]

theorem TauCeti.kantorovichDualValue_zero {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} : (kantorovichDualValue μ ν (fun (x : X) => 0) fun (x : Y) => 0) = 0

The zero potentials have dual value zero.

theorem TauCeti.kantorovichDualValue_add {X : Type u} {Y : Type v} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {a : X → ℝ} {b : Y → ℝ} (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (ha : MeasureTheory.Integrable a μ) (hb : MeasureTheory.Integrable b ν) : (kantorovichDualValue μ ν (fun (x : X) => φ x + a x) fun (y : Y) => ψ y + b y) = kantorovichDualValue μ ν φ ψ + kantorovichDualValue μ ν a b

Adding integrable marginal terms to the potentials adds their dual value.

theorem TauCeti.kantorovichDualValue_sub {X : Type u} {Y : Type v} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {a : X → ℝ} {b : Y → ℝ} (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (ha : MeasureTheory.Integrable a μ) (hb : MeasureTheory.Integrable b ν) : (kantorovichDualValue μ ν (fun (x : X) => φ x - a x) fun (y : Y) => ψ y - b y) = kantorovichDualValue μ ν φ ψ - kantorovichDualValue μ ν a b

Subtracting integrable marginal terms from the potentials subtracts their dual value.

theorem TauCeti.kantorovichDualValue_add_const_sub_const {X : Type u} {Y : Type v} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure μ] (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hmass : μ Set.univ = ν Set.univ) (a : ℝ) : (kantorovichDualValue μ ν (fun (x : X) => φ x + a) fun (y : Y) => ψ y - a) = kantorovichDualValue μ ν φ ψ

Opposite additive shifts do not change the dual value when the first marginal is finite and the two marginals have the same mass.

theorem TauCeti.kantorovichDualValue_eq_integral {X : Type u} {Y : Type v} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) : kantorovichDualValue μ ν φ ψ = ∫ (z : X × Y), φ z.1 + ψ z.2 ∂π

Against any coupling of the two marginals, the dual value is the integral of the split sum (x, y) ↦ φ x + ψ y of the two potentials. This identity is what turns the dual value into a statement about a single plan; it underlies both weak duality and complementary slackness.

theorem TauCeti.DualFeasible.ofReal_kantorovichDualValue_le_lintegral {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hπ : IsCoupling π μ ν) : ENNReal.ofReal (kantorovichDualValue μ ν φ ψ) ≤ ∫⁻ (z : X × Y), c z ∂π

Weak duality against a fixed coupling, in extended-nonnegative form. The positive part of the dual value is bounded by the cost of every coupling.

theorem TauCeti.DualFeasible.kantorovichDualValue_le_lintegral {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hπ : IsCoupling π μ ν) : ↑(kantorovichDualValue μ ν φ ψ) ≤ ↑(∫⁻ (z : X × Y), c z ∂π)

Weak duality against a fixed coupling. The real dual value is at most the possibly infinite coupling cost, with both sides compared in EReal.

theorem TauCeti.DualFeasible.ofReal_kantorovichDualValue_le_transportCost {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) : ENNReal.ofReal (kantorovichDualValue μ ν φ ψ) ≤ transportCost c μ ν

Kantorovich weak duality, in extended-nonnegative form. The positive part of every integrable feasible dual value is at most the primal transport cost.

theorem TauCeti.DualFeasible.kantorovichDualValue_le_toReal_transportCost {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (hne : transportCost c μ ν ≠ ⊤) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) : kantorovichDualValue μ ν φ ψ ≤ (transportCost c μ ν).toReal

Kantorovich weak duality in finite real form. If the primal value is finite, every integrable feasible dual value is at most its real representative.

theorem TauCeti.DualFeasible.kantorovichDualValue_le_transportCost {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) : ↑(kantorovichDualValue μ ν φ ψ) ≤ ↑(transportCost c μ ν)

Kantorovich weak duality. Every integrable feasible dual value is at most the primal transport cost. The comparison in EReal remains meaningful when the primal value is ∞.