Transport costs bounded below by integrable marginal terms

An extended-real transport cost may take negative values, so it cannot be integrated directly by lintegral. If c : X × Y → EReal is bounded below by a split function a x + b y, with a and b integrable against the two marginals, subtracting that lower bound leaves a nonnegative residual. Its lintegral is well-defined, and adding back the two fixed marginal integrals gives the signed extended cost of a coupling.

This file packages the lower-bound hypothesis as TauCeti.IntegrableSplitLowerBound, defines the cost TauCeti.planCostBddBelow of an individual feasible plan, and defines its infimum TauCeti.transportCostBddBelow. The main theorem TauCeti.transportCostBddBelow_congr_lowerBound proves that the value is independent of the chosen split lower bound. The specialization TauCeti.transportCostBddBelow_coe_eq_transportCost recovers the nonnegative TauCeti.transportCost interface exactly. Finally, TauCeti.lowerSemicontinuous_planCostBddBelow proves the weak lower-semicontinuity bridge for the normalized cost of a coupling when the original cost is lower semicontinuous and the two split terms are upper semicontinuous.

The normalization avoids every indeterminate subtraction: the only extended integral is the lintegral of a nonnegative residual, and the quantities added afterwards are finite real numbers. In particular, a cost identically ∞ still has value ∞, while an empty feasible set also has value ∞.

References

• C. Villani, Optimal Transport: Old and New, Chapter 5, especially the convention of allowing costs bounded below by a sum of integrable marginal functions.

structure TauCeti.IntegrableSplitLowerBound {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (c : X × Y → EReal) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : Type (max u v)

An integrable split lower bound for an extended-real cost c with marginals μ and ν.

The functions fst and snd provide the normalization fst x + snd y ≤ c (x, y). Their integrability makes their two marginal integrals finite, which is precisely what prevents an ∞ - ∞ ambiguity when the normalization is added back.

• fst : X → ℝ

  The part of the lower bound depending on the source variable.

• snd : Y → ℝ

  The part of the lower bound depending on the target variable.

• integrable_fst : MeasureTheory.Integrable self.fst μ

  The source part is integrable against the source marginal.

• integrable_snd : MeasureTheory.Integrable self.snd ν

  The target part is integrable against the target marginal.

• le_cost (x : X) (y : Y) : ↑(self.fst x + self.snd y) ≤ c (x, y)

  The two marginal terms together bound the cost from below.

theorem TauCeti.IntegrableSplitLowerBound.ext {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {h k : IntegrableSplitLowerBound c μ ν} (hfst : ∀ (x : X), h.fst x = k.fst x) (hsnd : ∀ (y : Y), h.snd y = k.snd y) : h = k

Two integrable split lower bounds are equal when their source and target parts agree pointwise.

theorem TauCeti.IntegrableSplitLowerBound.ext_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {h k : IntegrableSplitLowerBound c μ ν} : h = k ↔ (∀ (x : X), h.fst x = k.fst x) ∧ ∀ (y : Y), h.snd y = k.snd y

noncomputable def TauCeti.IntegrableSplitLowerBound.residual {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : IntegrableSplitLowerBound c μ ν) (z : X × Y) : ENNReal

The nonnegative residual left after subtracting an integrable split lower bound from a cost.

theorem TauCeti.IntegrableSplitLowerBound.residual_def {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : IntegrableSplitLowerBound c μ ν) (z : X × Y) : h.residual z = (c z - ↑(h.fst z.1 + h.snd z.2)).toENNReal

The characteristic formula for the residual of an integrable split lower bound.

@[simp]

theorem TauCeti.IntegrableSplitLowerBound.coe_residual_add {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : IntegrableSplitLowerBound c μ ν) (z : X × Y) : ↑(h.residual z) + (↑(h.fst z.1) + ↑(h.snd z.2)) = c z

The residual is the exact nonnegative part of the normalized cost: adding the split lower bound back in EReal recovers the original cost, including when that cost is ∞.

def TauCeti.IntegrableSplitLowerBound.ofNonneg {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} (hc : ∀ (z : X × Y), 0 ≤ c z) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : IntegrableSplitLowerBound c μ ν

Every nonnegative extended-real cost has the zero split lower bound.

theorem TauCeti.lowerSemicontinuous_residual {X : Type u} {Y : Type v} {c : X × Y → EReal} [TopologicalSpace X] [TopologicalSpace Y] (a : X → ℝ) (b : Y → ℝ) (hc : LowerSemicontinuous c) (ha : UpperSemicontinuous a) (hb : UpperSemicontinuous b) : LowerSemicontinuous fun (z : X × Y) => (c z - ↑(a z.1 + b z.2)).toENNReal

If c is lower semicontinuous and the real-valued split terms are upper semicontinuous, then their nonnegative extended-real residual is lower semicontinuous.

noncomputable def TauCeti.planCostBddBelow {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (π : MeasureTheory.Measure (X × Y)) (_hπ : IsCoupling π μ ν) (h : IntegrableSplitLowerBound c μ ν) : EReal

The signed cost of a coupling, normalized using an integrable split lower bound.

The coupling witness is part of the domain because the fixed marginal correction terms reconstruct the plan's cost only when π has marginals μ and ν; for an arbitrary measure, this expression can depend on the chosen lower bound.

theorem TauCeti.planCostBddBelow_def {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (π : MeasureTheory.Measure (X × Y)) (hπ : IsCoupling π μ ν) (h : IntegrableSplitLowerBound c μ ν) : planCostBddBelow π hπ h = ↑(∫⁻ (z : X × Y), h.residual z ∂π) + ↑(∫ (x : X), h.fst x ∂μ) + ↑(∫ (y : Y), h.snd y ∂ν)

The characteristic formula for the normalized signed cost of a coupling.

theorem TauCeti.lowerSemicontinuous_planCostBddBelow {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} [PseudoMetricSpace X] [PseudoMetricSpace Y] [OpensMeasurableSpace (X × Y)] {μp : MeasureTheory.ProbabilityMeasure X} {νp : MeasureTheory.ProbabilityMeasure Y} (h : IntegrableSplitLowerBound c ↑μp ↑νp) (hc : LowerSemicontinuous c) (ha : UpperSemicontinuous h.fst) (hb : UpperSemicontinuous h.snd) : LowerSemicontinuous fun (π : Coupling μp νp) => planCostBddBelow ↑↑π ⋯ h

If the cost is lower semicontinuous and both split terms are upper semicontinuous, its normalized signed cost is lower semicontinuous on the weak topology of couplings.

noncomputable def TauCeti.transportCostBddBelow {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (c : X × Y → EReal) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (h : IntegrableSplitLowerBound c μ ν) : EReal

The transport cost of μ and ν for an extended-real cost bounded below by integrable marginal terms.

For a lower bound h with components a and b, this is the infimum over couplings π of ↑(∫⁻ (c - a ⊕ b) dπ) + ∫ a dμ + ∫ b dν. The residual is nonnegative by h.le_cost, and the last two summands are finite real numbers. The value does not depend on h; see transportCostBddBelow_congr_lowerBound.

theorem TauCeti.transportCostBddBelow_def {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {h : IntegrableSplitLowerBound c μ ν} : transportCostBddBelow c μ ν h = ⨅ (π : MeasureTheory.Measure (X × Y)), ⨅ (hπ : IsCoupling π μ ν), planCostBddBelow π hπ h

The characteristic formula for the bounded-below signed transport cost.

theorem TauCeti.transportCostBddBelow_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) (h : IntegrableSplitLowerBound c μ ν) : transportCostBddBelow c μ ν h ≤ planCostBddBelow π hπ h

The signed transport cost is bounded above by the normalized cost of every feasible plan.

theorem TauCeti.le_transportCostBddBelow {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {d : EReal} (h : IntegrableSplitLowerBound c μ ν) (hd : ∀ (π : MeasureTheory.Measure (X × Y)) (hπ : IsCoupling π μ ν), d ≤ planCostBddBelow π hπ h) : d ≤ transportCostBddBelow c μ ν h

A lower bound valid for the normalized cost of every coupling bounds the signed transport cost from below.

theorem TauCeti.transportCostBddBelow_eq_transportCost_residual_add_integral_add_integral {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h : IntegrableSplitLowerBound c μ ν) : transportCostBddBelow c μ ν h = ↑(transportCost h.residual μ ν) + ↑(∫ (x : X), h.fst x ∂μ + ∫ (y : Y), h.snd y ∂ν)

Subtracting the split lower bound reduces the signed primal problem to the nonnegative transport problem. The marginal correction is finite even when the optimum is infinite or the feasible set is empty.

theorem TauCeti.planCostBddBelow_congr_lowerBound {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h k : IntegrableSplitLowerBound c μ ν) (hπ : IsCoupling π μ ν) : planCostBddBelow π hπ h = planCostBddBelow π hπ k

On a coupling, the signed plan cost is independent of the chosen split lower bound.

theorem TauCeti.transportCostBddBelow_congr_lowerBound {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (h k : IntegrableSplitLowerBound c μ ν) : transportCostBddBelow c μ ν h = transportCostBddBelow c μ ν k

The signed transport cost is independent of the chosen integrable split lower bound.

theorem TauCeti.transportCostBddBelow_coe_eq_transportCost {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (c : X × Y → ENNReal) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (h : IntegrableSplitLowerBound (fun (z : X × Y) => ↑(c z)) μ ν) : transportCostBddBelow (fun (z : X × Y) => ↑(c z)) μ ν h = ↑(transportCost c μ ν)

For a nonnegative ℝ≥0∞-valued cost, the bounded-below signed interface agrees exactly with the original nonnegative transport cost, for any valid split lower bound.