Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

OptimalContinuousCost: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. A continuous transport cost attains its infimum
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.

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.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

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