Stability of the primal transport problem under varying marginals and costs #
A family of transport problems indexed by a filter is stable when its optimal values converge to
the optimal value of a limiting problem, and its optimal plans accumulate only on optimal plans of
that limiting problem. This file proves both, from two hypotheses that are stated explicitly rather
than packaged: a lower bound on the asymptotic cost of weakly convergent feasible families
(TauCeti.IsCostLiminfStable), and an upper bound produced by approximating each limiting plan
(TauCeti.HasRecoveryPlans).
The two hypotheses do exactly one job each, and neither implies the other.
TauCeti.IsCostLiminfStable is what makes the limiting value a lower bound: it says that along
any finer filter, a weakly convergent family of feasible plans cannot lose cost in the limit. It
holds for free when the limiting cost is lower semicontinuous and is dominated by the family
(TauCeti.isCostLiminfStable_of_le), which covers the fixed-cost problem where only the marginals
move.
TauCeti.HasRecoveryPlans is what makes the limiting value an upper bound: every plan of the
limiting problem must be reachable, asymptotically and in cost, by feasible plans of the moving
problems. It is a genuine assumption — for a fixed lower semicontinuous cost and weakly converging
marginals the optimal values can strictly drop in the limit: take c to be the indicator of the
off-diagonal of ℝ × ℝ, which is lower semicontinuous, μs n = δ (1 / (n + 1)) and νs n = δ 0;
every moving problem then has value 1, while the limiting problem has value 0. The recovery
family must converge weakly to the chosen limiting plan as well as satisfy the cost bound; this is
the recovery-coupling condition from the roadmap.
The two bounds are separated on purpose: TauCeti.transportCost_le_liminf_transportCost needs the
liminf hypothesis and compactness, TauCeti.limsup_transportCost_le_transportCost needs the
recovery hypothesis and nothing else, and only TauCeti.tendsto_transportCost needs both.
Compactness enters through TauCeti.exists_isCoupling_tendsto_of_isTightMeasureSet, proved in
TauCeti.MeasureTheory.OptimalTransport.Compactness: a family of plans whose (varying) marginals
are tight on a filter tail is relatively compact, and every weak limit along a finer filter is a
coupling of the limiting marginals. This is the "tightness of optimizer subsequences" step, and it
is what lets the arguments run along a filter rather than a sequence: passing to a subsequence is
replaced by passing to a finer filter.
Main statements #
TauCeti.IsCostLiminfStableandTauCeti.HasRecoveryPlans— the two stability hypotheses, withTauCeti.isCostLiminfStable_of_leandTauCeti.isCostLiminfStable_constsupplying the first one from lower semicontinuity;TauCeti.transportCost_le_liminf_transportCostandTauCeti.limsup_transportCost_le_transportCost— the two one-sided bounds on the optimal values;TauCeti.hasRecoveryPlans_of_limsup_le— the recovery hypothesis for a family with fixed marginals;TauCeti.tendsto_transportCost— convergence of the optimal values, withTauCeti.tendsto_transportCost_of_const_marginalsas a topology-free fixed-marginal criterion;TauCeti.isOptimalCoupling_of_tendstoandTauCeti.exists_isOptimalCoupling_tendsto— subsequential convergence of optimal plans to an optimal plan of the limiting problem;TauCeti.tendsto_transportCost_of_polishSpaceandTauCeti.exists_isOptimalCoupling_tendsto_of_polishSpace— the Polish sequential forms, where weak convergence supplies tightness and the stability theorems need no tightness hypothesis;TauCeti.transportCost_le_liminf_transportCost_of_lowerSemicontinuous— the fixed-cost corollary: on Polish spaces the optimal transport cost of a lower semicontinuous cost is weakly lower semicontinuous in the pair of marginals, withTauCeti.lowerSemicontinuous_transportCostits topological form onProbabilityMeasure X × ProbabilityMeasure Y.
References #
- C. Villani, Optimal Transport: Old and New, Springer 2009, Theorem 5.20 — stability of optimal transport: convergence of the optimal costs and of the optimal plans under weakly converging marginals and uniformly converging costs.
- F. Santambrogio, Optimal Transport for Applied Mathematicians, Springer 2015, Section 1.2 — the same statement obtained by the direct method from tightness and lower semicontinuity.
This is Layer 1, item 6 of the optimal-transport roadmap. Layer 10 is where these two hypotheses are packaged as the Γ-liminf, Γ-limsup and equicoercivity conditions of an abstract variational convergence; here they stay explicit.
The two stability hypotheses. Both are recorded as one-field structures so that they can be
consumed by name and produced by refine ⟨fun ... ↦ ?_⟩.
The asymptotic lower bound half of stability: along every filter l' refining l, a weakly
convergent family of plans that is eventually feasible for the moving marginals μs, νs costs at
least the limiting cost c of its limit, asymptotically. Quantifying over the refinements of l
is what makes the hypothesis usable after passing to a convergent subfamily, exactly as the
classical statement quantifies over subsequences.
- le_liminf {l' : Filter ι} (hne : l'.NeBot) (hle : l' ≤ l) {πs : ι → MeasureTheory.ProbabilityMeasure (X × Y)} {π : MeasureTheory.ProbabilityMeasure (X × Y)} (hπs : ∀ᶠ (i : ι) in l', IsCoupling ↑(πs i) ↑(μs i) ↑(νs i)) (hπ : Filter.Tendsto πs l' (nhds π)) : ∫⁻ (z : X × Y), c z ∂↑π ≤ Filter.liminf (fun (i : ι) => ∫⁻ (z : X × Y), cs i z ∂↑(πs i)) l'
The cost of a weak limit of feasible plans is at most the asymptotic cost of the family.
Instances For
The asymptotic upper bound half of stability: every plan of the limiting problem is recovered by a weakly convergent family of plans that is eventually feasible for the moving marginals and costs no more asymptotically.
- exists_recovery {π : MeasureTheory.ProbabilityMeasure (X × Y)} (hπ : IsCoupling ↑π ↑μ ↑ν) : ∃ (πs : ι → MeasureTheory.ProbabilityMeasure (X × Y)), (∀ᶠ (i : ι) in l, IsCoupling ↑(πs i) ↑(μs i) ↑(νs i)) ∧ Filter.Tendsto πs l (nhds π) ∧ Filter.limsup (fun (i : ι) => ∫⁻ (z : X × Y), cs i z ∂↑(πs i)) l ≤ ∫⁻ (z : X × Y), c z ∂↑π
Every coupling of the limiting marginals is recovered weakly and from above in cost.
Instances For
Liminf stability is preserved when the indexing filter is refined.
Recovery plans remain recovery plans when the indexing filter is refined.
Lower semicontinuity of the limiting cost, together with domination by the family, is the
standard source of TauCeti.IsCostLiminfStable. Only a compatible pseudometric and measurable
opens on the product are needed for the weak-topology lower semicontinuity of
TauCeti.lowerSemicontinuous_lintegral_probabilityMeasure.
A lower semicontinuous cost dominated by the family is liminf-stable. Weak lower
semicontinuity of π ↦ ∫⁻ c ∂π gives the inequality for the limiting cost itself, and eventual
domination c ≤ cs i upgrades it to the moving costs. The feasibility of the plans plays no role:
the bound holds for every weakly convergent family.
A fixed lower semicontinuous cost is liminf-stable. This is the case in which only the marginals move; it is the hypothesis under which the optimal transport cost is weakly lower semicontinuous in the marginals.
The lower bound on the optimal values: it is the half that consumes compactness.
The limiting optimal value is a lower bound. Under the liminf hypothesis and tail tightness
of the two marginal families, the optimal value of the limiting problem is at most the liminf of
the optimal values of the moving problems. Nearly optimal plans suffice, so no lower
semicontinuity of the moving costs is assumed.
The upper bound needs neither compactness nor a Hausdorff space of marginals.
The limiting optimal value is an upper bound. Under the recovery hypothesis, the limsup of
the optimal values of the moving problems is at most the optimal value of the limiting problem.
Neither compactness nor tightness is used: each coupling of the limiting marginals is tested
separately against its own recovery family.
Fixed marginals admit recovery plans as soon as the costs do. When the marginals are
eventually the limiting ones, a coupling of them is eventually feasible for the moving problems,
so it recovers itself and only the asymptotic cost inequality is left to check. This is the
regime in which nothing but the cost moves, for instance cs i = c + ε i • d with ε i → 0 and d
bounded.
Convergence of transport costs with fixed marginals. If the moving costs eventually
dominate the limiting cost, this supplies the liminf bound by monotonicity. A pointwise limsup
bound on the integral along every coupling supplies the reverse bound. No topology, tightness, or
lower semicontinuity is needed.
Both bounds together.
Convergence of the optimal values. With both stability hypotheses the optimal values of the
moving problems converge to the optimal value of the limiting problem, in ℝ≥0∞; no finiteness is
assumed anywhere, so the common value may be ∞.
A weak limit of optimal plans is optimal. If the plans πs i are eventually optimal for the
moving problems along a filter l' refining l and converge weakly to π, then π is an optimal
plan of the limiting problem, provided the moving optimal values have the required limsup upper
bound.
Subsequential convergence of optimal plans. A family of optimal plans of the moving problems
has a refinement along which the plans converge to an optimal plan of the limiting problem. The
theorem TauCeti.isOptimalCoupling_of_tendsto says that every such weak limit is optimal under the
explicit limsup upper bound on the moving optimal values.
The Polish specialisation. On a Polish space a weakly convergent sequence of probability measures is tight, by the converse half of Prokhorov's theorem applied to the compact set formed by the sequence and its limit; so the tightness hypotheses of the previous section are automatic there and the statements below carry none.
Convergence of the optimal values on Polish spaces, with no tightness hypothesis: weak convergence of the two marginal sequences supplies it.
Subsequential convergence of optimal plans on Polish spaces, with no tightness hypothesis.
The limsup upper bound on the moving optimal values is still assumed explicitly.
The optimal transport cost of a lower semicontinuous cost is weakly lower semicontinuous in the marginals. This is the fixed-cost corollary: the liminf hypothesis is automatic, so no stability assumption survives. The reverse inequality genuinely fails without a recovery hypothesis — the optimal value can drop in the limit — which is why only one bound is stated here.
The optimal transport cost of a lower semicontinuous cost is a lower semicontinuous function
of the pair of marginals, for the weak topology on ProbabilityMeasure X × ProbabilityMeasure Y.
This is the topological form of
TauCeti.transportCost_le_liminf_transportCost_of_lowerSemicontinuous.