A continuous transport cost attains its infimum
AutoSamplingTheory.TechnicalLemmas.Measure.OptimalContinuousCost.exists_optimal_coupling · theorem · Teaching coverage
Mathematical 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.
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∞)) μ νProof roadmap
- 1Use 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.
- 2Apply 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.
- 3Take 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.
- 4Identify 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.
Full assumptions and notation
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.
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.
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.
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.
Corresponding Lean step
transportCost_eq_sInf, le_sInf and transportCost_le_lintegral_of_isCoupling.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · exists_optimal_coupling
Compact minimum with explicit conversion between probability couplings and raw measure couplings.
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∞)) μ ν := 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.OptimalContinuousCostSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Lemma6.2 invokes an optimal coupling for Euclidean p-distance cost. | Continuous nonnegative costs on complete second-countable metric Borel spaces, minimum possibly infinite. | generalization | Expanded optimizer prerequisite with one actual paper consumer; no assertion this generic statement is printed in the source. |
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.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: Generic two-space metric setting extends Euclidean source. — No vector structure or finite dimension; explicit generic expanded prerequisite.
- objects: Arbitrary continuous nonnegative costs and potentially infinite optimum extend finite p-distance application. — Arbitrary continuous NNReal cost; actual p-distance consumer is truncated_proxy.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.Measure.ProbabilityCouplingCompactness.isCompact_probabilityCouplingSetAutoSamplingTheory.TechnicalLemmas.Measure.ContinuousCostWeakLowerSemicontinuity.lowerSemicontinuous_lintegral_continuous_nnreal
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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.