ASTIS mathematical exposition

A continuous transport cost attains its infimum

AutoSamplingTheory.TechnicalLemmas.Measure.OptimalContinuousCost.exists_optimal_coupling · theorem · Teaching coverage

Statement

For probability measures P,Q on complete second-countable metric Borel spaces E,F and any continuous nonnegative real cost c on E times F, there is an actual probability coupling gamma whose extended nonnegative integral of c equals the infimum over all couplings. The value may be infinite; neither a moment bound nor an optimizer is assumed.

\[\exists\gamma\in\Pi(P,Q),\qquad\int c\,d\gamma=\inf_{\rho\in\Pi(P,Q)}\int c\,d\rho.\]

All objects and hypotheses

E,F are complete second-countable metric spaces with their Borel sigma algebras.
P,Q are probability measures and c:E times F to nonnegative reals is continuous.
This is a generic expanded prerequisite to the optimal coupling chosen in Lemma6.2, not an additional hypothesis of that lemma.

Mathematical proof

1. Use a genuine nonempty coupling space

Package P and Q as probability measures. Their product is a coupling, so the space of probability couplings is nonempty.

\[P\otimes Q\in\Pi(P,Q).\]

Corresponding Lean step

Transport.isCoupling_prod and isProbabilityCoupling_iff_isCoupling_toMeasure.

2. Apply existing weak compactness and lower semicontinuity

The existing ASTIS compactness theorem makes the coupling space compact in the weak topology. Its continuous-cost lower semicontinuity theorem applies to the extended integral, without a bounded cost or finite moment restriction.

\[\Pi(P,Q)\text{ compact},\qquad\gamma\mapsto\int c\,d\gamma\text{ lower semicontinuous}.\]

Corresponding Lean step

isCompact_probabilityCouplingSet and lowerSemicontinuous_lintegral_continuous_nnreal.

3. Take the compact minimum

A lower-semicontinuous function into the ordered extended nonnegative reals attains a minimum on a nonempty compact set. Recover an actual raw measure gamma and its two marginals.

\[\int c\,d\gamma\le\int c\,d\rho\quad(\rho\in\Pi(P,Q)).\]

Corresponding Lean step

LowerSemicontinuousOn.exists_isMinOn supplies gamma and hmin.

4. Identify the original infimum over raw couplings

Every raw coupling is a probability because its first marginal is P. It therefore belongs to the compact probability-coupling set, so minimality gives the lower bound against every element in the transportCost infimum. Membership gives the reverse inequality.

\[\int c\,d\gamma=\operatorname{transportCost}(c,P,Q).\]

Corresponding Lean step

transportCost_eq_sInf, le_sInf and transportCost_le_lintegral_of_isCoupling.

Lean statement · exists_optimal_coupling

A genuine probability coupling attaining the extended integral infimum for a continuous NNReal cost.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem exists_optimal_coupling {E F : Type*}
    [MetricSpace E] [CompleteSpace E] [SecondCountableTopology E]
    [MeasurableSpace E] [BorelSpace E]
    [MetricSpace F] [CompleteSpace F] [SecondCountableTopology F]
    [MeasurableSpace F] [BorelSpace F]
    (μ : Measure E) (ν : Measure F) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (c : E × F → ℝ≥0) (hc : Continuous c) :
    ∃ γ : Measure (E × F), IsProbabilityMeasure γ ∧ Transport.IsCoupling γ μ ν ∧
      (∫⁻ z, (c z : ℝ≥0∞) ∂γ) = Transport.transportCost (fun z => (c z : ℝ≥0∞)) μ ν

Exact module and namespace context

Lean proof · exists_optimal_coupling

Compact minimum with explicit conversion between probability couplings and raw measure couplings.

theorem exists_optimal_coupling {E F : Type*}
    [MetricSpace E] [CompleteSpace E] [SecondCountableTopology E]
    [MeasurableSpace E] [BorelSpace E]
    [MetricSpace F] [CompleteSpace F] [SecondCountableTopology F]
    [MeasurableSpace F] [BorelSpace F]
    (μ : Measure E) (ν : Measure F) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (c : E × F → ℝ≥0) (hc : Continuous c) :
    ∃ γ : Measure (E × F), IsProbabilityMeasure γ ∧ Transport.IsCoupling γ μ ν ∧
      (∫⁻ z, (c z : ℝ≥0∞) ∂γ) = Transport.transportCost (fun z => (c z : ℝ≥0∞)) μ ν := by
  let P : ProbabilityMeasure E := ⟨μ,inferInstance⟩
  let Q : ProbabilityMeasure F := ⟨ν,inferInstance⟩
  have hn : (probabilityCouplingSet P Q).Nonempty := by
    refine ⟨⟨μ.prod ν,inferInstance⟩, ?_⟩
    exact isProbabilityCoupling_iff_isCoupling_toMeasure.mpr (Transport.isCoupling_prod μ ν)
  have hcompact := isCompact_probabilityCouplingSet P Q
  have hlsc := ContinuousCostWeakLowerSemicontinuity.lowerSemicontinuous_lintegral_continuous_nnreal c hc
  obtain ⟨γ,hγ,hmin⟩ := LowerSemicontinuousOn.exists_isMinOn hn hcompact (hlsc.lowerSemicontinuousOn _)
  have hγ' : Transport.IsCoupling (γ : Measure (E × F)) μ ν :=
    isProbabilityCoupling_iff_isCoupling_toMeasure.mp hγ
  refine ⟨γ,inferInstance,hγ',le_antisymm ?_ ?_⟩
  · rw [Transport.transportCost_eq_sInf]
    apply le_sInf
    rintro r ⟨ρ,hρ,rfl⟩
    let : IsProbabilityMeasure ρ := Transport.isProbabilityMeasure_of_isCoupling_left hρ
    let R : ProbabilityMeasure (E × F) := ⟨ρ,inferInstance⟩
    have hR : IsProbabilityCoupling R P Q := isProbabilityCoupling_iff_isCoupling_toMeasure.mpr hρ
    exact hmin hR
  · exact Transport.transportCost_le_lintegral_of_isCoupling _ μ ν γ hγ'

end AutoSamplingTheory.TechnicalLemmas.Measure.OptimalContinuousCost

Exact module and namespace context

Scope and omitted-condition boundaries

Actual infimum p-cost and bounded-displacement coupling certificate for Lemma6.2; no full Wp/Winfinity metric API, Gaussian reverse transport, Renyi/proxy-warmness, sampler construction, error/cost propagation or full-paper conclusion.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

LowerSemicontinuousOn.exists_isMinOn

Mathematical sources

Chen, Chewi, Lu and Zhang, SPHMC v1 Lemma 6.2 — Optimal-coupling existence expanded and actual truncation construction.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.