Approximate Kantorovich duality… to Strong Kantorovich duality for…

TheoremApproximate Kantorovich duality on compact spaces #

For probability measures on compact pseudometric spaces, a continuous nonnegative cost, and every ε > 0, there is a pair of continuous potentials satisfying the Kantorovich constraint whose value is within ε of the primal transport cost. Together with weak duality this closes the duality gap.

TauCeti.exists_continuous_forall_add_le_transportCost_le.{u, v} {X : Type u} {Y : Type v}
  [PseudoMetricSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
  [PseudoMetricSpace Y] [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y]
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c)
  (hc0 : ∀ (z : X × Y), 0 ≤ c z) {ε : ℝ} (hε : 0 < ε) :
  ∃ φ ψ,
    Continuous φ ∧
      Continuous ψ ∧
        (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧
          TauCeti.transportCost (fun z => ENNReal.ofReal (c z)) μ ν ≤
            ENNReal.ofReal (TauCeti.kantorovichDualValue μ ν φ ψ + ε)

Lean

Formalized in Tau Ceti as TauCeti.exists_continuous_forall_add_le_transportCost_le.

Sources

LeanTauCeti.exists_continuous_forall_add_le_transportCost_le

Used by 2

Used byKantorovich–Rubinstein duality · Strong Kantorovich duality for probability measures

TheoremThe Benamou–Brenier upper bound #

Let 1 ≤ p < ∞, and let π be an optimal coupling of a finite measure μ and a measure ν on E for the cost d(x, y) ^ p, at finite Wasserstein distance W_p (μ, ν). Then the displacement interpolation, the laws μₜ of (1 - t) • x + t • y under π, solves the continuity equation on (0, 1) with a velocity field of p-action at most W_p (μ, ν) ^ p: ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt ≤ W_p (μ, ν) ^ p.

TauCeti.exists_isContinuityEquation_map_smul_fst_add_smul_snd_of_isOptimalCoupling_le.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
  [FiniteDimensional ℝ E] [BorelSpace E] {μ ν : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure μ] {π : MeasureTheory.Measure (E × E)} {p : ENNReal} (hp : 1 ≤ p)
  (hp_top : p ≠ ⊤) (hopt : TauCeti.IsOptimalCoupling (fun z => edist z.1 z.2 ^ p.toReal) π μ ν)
  (hfin : TauCeti.wassersteinEDist p μ ν ≠ ⊤) :
  ∃ v,
    TauCeti.IsContinuityEquation
        (fun t => MeasureTheory.Measure.map (fun z => (1 - t) • z.1 + t • z.2) π) v 0 1 ∧
      ∫⁻ (t : ℝ) in Set.Ioo 0 1,
          ∫⁻ (w : E),
            ‖v t w‖ₑ ^ p.toReal ∂MeasureTheory.Measure.map (fun z => (1 - t) • z.1 + t • z.2) π ≤
        TauCeti.wassersteinEDist p μ ν ^ p.toReal

Lean

Formalized in Tau Ceti as TauCeti.exists_isContinuityEquation_map_smul_fst_add_smul_snd_of_isOptimalCoupling_le.

Sources

LeanTauCeti.exists_isContinuityEquation_map_smul_fst_add_smul_snd_of_isOptimalCoupling_le

Uses 1 · Used by 1

Proof usesJensen's inequality for the conditional expectation, as an inequality of lintegrals

Used byThe Benamou–Brenier formula

TheoremBounded-Lipschitz duality in supremum form #

A uniform bound R on the test functions corresponds to truncation of the ground distance at 2 * R, for finite measures of equal mass.

TauCeti.transportCost_truncated_dist_eq_iSup.{u} {X : Type u} [MeasurableSpace X]
  {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] {R : ℝ} [PolishSpace X] [BorelSpace X]
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hR : 0 ≤ R)
  (hmass : μ Set.univ = ν Set.univ) :
  TauCeti.transportCost (fun z => ENNReal.ofReal (min (dist z.1 z.2) (2 * R))) μ ν =
    ⨆ f,
      ⨆ (_ : LipschitzWith 1 f),
        ⨆ (_ : ∀ (x : X), ‖f x‖ ≤ R), ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν)

Lean

Formalized in Tau Ceti as TauCeti.transportCost_truncated_dist_eq_iSup.

Sources

LeanTauCeti.transportCost_truncated_dist_eq_iSup

Uses 1

Proof usesThe theorem of Rockafellar and Rüschendorf

TheoremBounded-Lipschitz Kantorovich–Rubinstein duality with attainment #

The cost capped at 2 * R is the greatest difference of integrals of a 1-Lipschitz function bounded by R, for finite measures of equal mass. Both constraints are separate; this is the maximum-norm convention, not their sum.

TauCeti.isGreatest_ofReal_integral_sub_integral_boundedLipschitz.{u} {X : Type u}
  [MeasurableSpace X] {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] {R : ℝ} [PolishSpace X]
  [BorelSpace X] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hR : 0 ≤ R)
  (hmass : μ Set.univ = ν Set.univ) :
  IsGreatest
    {r |
      ∃ f,
        LipschitzWith 1 f ∧
          (∀ (x : X), ‖f x‖ ≤ R) ∧ ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν) = r}
    (TauCeti.transportCost (fun z => ENNReal.ofReal (min (dist z.1 z.2) (2 * R))) μ ν)

Lean

Formalized in Tau Ceti as TauCeti.isGreatest_ofReal_integral_sub_integral_boundedLipschitz.

Sources

LeanTauCeti.isGreatest_ofReal_integral_sub_integral_boundedLipschitz

Uses 1

Proof usesThe theorem of Rockafellar and Rüschendorf

TheoremCauchy–Schwarz for the pairing #

For an optimal coupling γ of two laws μ and ν of P₂(E) for the quadratic cost and ξ ∈ L²(μ; E), |∫ ⟪ξ x, y - x⟫ dγ| ≤ ‖ξ‖ W₂(μ, ν).

TauCeti.IsOptimalCoupling.abs_integral_inner_le.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [InnerProductSpace ℝ E]
  {γ : MeasureTheory.Measure (E × E)} [CompleteSpace E] {μ ν : TauCeti.WassersteinSpace 2 E}
  (hγ : TauCeti.IsOptimalCoupling (fun z => edist z.1 z.2 ^ 2) γ ↑↑μ ↑↑ν)
  (ξ : ↥(MeasureTheory.Lp E 2 ↑↑μ)) :
  |∫ (z : E × E), inner ℝ (↑↑ξ z.1) (z.2 - z.1) ∂γ| ≤ ‖ξ‖ * dist μ ν

Lean

Formalized in Tau Ceti as TauCeti.IsOptimalCoupling.abs_integral_inner_le.

Sources

LeanTauCeti.IsOptimalCoupling.abs_integral_inner_le

TheoremFinite multi-marginal Kantorovich duality #

For a nonempty finite family of finite spaces, the primal and dual problems have the same value and both attain it.

TauCeti.exists_cost_eq_finiteMultiDualValue.{u, v} {ι : Type u} {X : ι → Type v} [Fintype ι]
  [(i : ι) → Fintype (X i)] (c : ((i : ι) → X i) → ℝ) (μ : (i : ι) → PMF (X i)) [Nonempty ι] :
  ∃ π φ,
    (∀ (σ : TauCeti.FiniteMultiCoupling μ),
        TauCeti.FiniteMultiCoupling.cost c π ≤ TauCeti.FiniteMultiCoupling.cost c σ) ∧
      TauCeti.FiniteMultiDualFeasible c φ ∧
        TauCeti.FiniteMultiCoupling.cost c π = TauCeti.finiteMultiDualValue μ φ

Lean

Formalized in Tau Ceti as TauCeti.exists_cost_eq_finiteMultiDualValue.

Sources

LeanTauCeti.exists_cost_eq_finiteMultiDualValue

TheoremThe Fréchet–Hoeffding bound on a quadrant #

Every transport plan of two real laws gives the quadrant Iic a ×ˢ Ioi b mass at least cdf μ a - cdf ν b: the pairs with first coordinate at most a carry mass cdf μ a, and at most cdf ν b of it has second coordinate at most b.

TauCeti.ofReal_cdf_sub_le_measure {μ ν : MeasureTheory.Measure ℝ}
  [MeasureTheory.IsProbabilityMeasure μ] {π : MeasureTheory.Measure (ℝ × ℝ)}
  (hπ : TauCeti.IsCoupling π μ ν) (a b : ℝ) :
  ENNReal.ofReal (↑(ProbabilityTheory.cdf μ) a - ↑(ProbabilityTheory.cdf ν) b) ≤
    π (Set.Iic a ×ˢ Set.Ioi b)

Lean

Formalized in Tau Ceti as TauCeti.ofReal_cdf_sub_le_measure.

Sources

LeanTauCeti.ofReal_cdf_sub_le_measure

TheoremThe generalised Bonnet–Myers theorem under `CD(K, N)`#

If M satisfies CD(K, N) with K > 0 and N ≥ 1, any two points of the support of the reference measure are at distance at most π √((N - 1) / K).

TauCeti.MetricMeasureSpace.CurvatureDimension.dist_le.{u_2} {X : Type u_2} [MetricSpace X]
  [MeasurableSpace X] [CompleteSpace X] [SecondCountableTopology X] [BorelSpace X]
  {M : TauCeti.MetricMeasureSpace X} {K N : ℝ} (h : M.CurvatureDimension K N) (hK : 0 < K)
  (hN : 1 ≤ N) {x y : X} (hx : x ∈ M.support) (hy : y ∈ M.support) :
  dist x y ≤ Real.pi * √((N - 1) / K)

Lean

Formalized in Tau Ceti as TauCeti.MetricMeasureSpace.CurvatureDimension.dist_le.

Sources

LeanTauCeti.MetricMeasureSpace.CurvatureDimension.dist_le

Used by 1

Used byThe Bonnet–Myers diameter bound under MCP(K, N)

TheoremThe Gibbs identity #

For probability measures μ and ν, a cost c finite μ.prod ν-almost everywhere, and a positive temperature ε, every probability measure π on X × Y satisfies ∫ c dπ + ε * klDiv π (μ ⊗ ν) = ε * klDiv π R - ε * log Z, where Z = ∫ e^{-c/ε} d(μ ⊗ ν) and R = Z⁻¹ e^{-c/ε} (μ ⊗ ν) is the Gibbs measure, written as the tilted measure (μ.prod ν).tilted fun z ↦ -((c z).toReal / ε). Both sides may be ∞.

TauCeti.lintegral_add_mul_klDiv_eq_mul_klDiv_tilted.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → ENNReal} {ε : NNReal}
  {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y}
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  [MeasureTheory.IsProbabilityMeasure π] (hc : AEMeasurable c (μ.prod ν))
  (hc_top : ∀ᵐ (z : X × Y) ∂μ.prod ν, c z ≠ ⊤) (hε : ε ≠ 0) :
  ∫⁻ (z : X × Y), c z ∂π + ↑ε * InformationTheory.klDiv π (μ.prod ν) =
    ↑ε * InformationTheory.klDiv π ((μ.prod ν).tilted fun z => -((c z).toReal / ↑ε)) +
      ↑ε * ENNReal.ofReal (-Real.log (∫ (z : X × Y), Real.exp (-((c z).toReal / ↑ε)) ∂μ.prod ν))

Lean

Formalized in Tau Ceti as TauCeti.lintegral_add_mul_klDiv_eq_mul_klDiv_tilted.

Sources

LeanTauCeti.lintegral_add_mul_klDiv_eq_mul_klDiv_tilted

TheoremKantorovich–Rubinstein duality #

For probability measures with finite first moments on a second-countable pseudometric space whose measurable structure is standard Borel and contains the open sets — in particular on a Polish metric space with its Borel σ-algebra — the 1-Wasserstein distance is the supremum of the differences of expectations of the 1-Lipschitz real functions.

TauCeti.wassersteinEDist_one_eq_iSup.{u} {X : Type u} [MeasurableSpace X]
  {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] [OpensMeasurableSpace X]
  [SecondCountableTopology X] [StandardBorelSpace X] [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] (hμ : TauCeti.HasFiniteMoment 1 μ)
  (hν : TauCeti.HasFiniteMoment 1 ν) :
  TauCeti.wassersteinEDist 1 μ ν =
    ⨆ f, ⨆ (_ : LipschitzWith 1 f), ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν)

Lean

Formalized in Tau Ceti as TauCeti.wassersteinEDist_one_eq_iSup.

Other forms

Kantorovich–Rubinstein duality on a compact space. Formalized in Tau Ceti as TauCeti.wassersteinEDist_one_eq_iSup_of_compactSpace.

TauCeti.wassersteinEDist_one_eq_iSup_of_compactSpace.{u} {X : Type u} [MeasurableSpace X]
  {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] [CompactSpace X] [OpensMeasurableSpace X]
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] :
  TauCeti.wassersteinEDist 1 μ ν =
    ⨆ f, ⨆ (_ : LipschitzWith 1 f), ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν)

Kantorovich–Rubinstein duality, normalized at a basepoint. Formalized in Tau Ceti as TauCeti.wassersteinEDist_one_eq_iSup_apply_eq_zero.

TauCeti.wassersteinEDist_one_eq_iSup_apply_eq_zero.{u} {X : Type u} [MeasurableSpace X]
  {μ ν : MeasureTheory.Measure X} [PseudoMetricSpace X] [OpensMeasurableSpace X]
  [SecondCountableTopology X] [StandardBorelSpace X] [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] (hμ : TauCeti.HasFiniteMoment 1 μ)
  (hν : TauCeti.HasFiniteMoment 1 ν) (x₀ : X) :
  TauCeti.wassersteinEDist 1 μ ν =
    ⨆ f,
      ⨆ (_ : LipschitzWith 1 f),
        ⨆ (_ : f x₀ = 0), ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν)

Sources

LeanTauCeti.wassersteinEDist_one_eq_iSup · TauCeti.wassersteinEDist_one_eq_iSup_of_compactSpace · TauCeti.wassersteinEDist_one_eq_iSup_apply_eq_zero

Uses 2

Proof usesApproximate Kantorovich duality on compact spaces · Kantorovich–Rubinstein weak duality

TheoremKantorovich–Rubinstein weak duality #

The difference of the expectations of an integrable 1-Lipschitz real function under two measures is at most their 1-Wasserstein distance. No measurability of the ground distance and no finiteness of the measures is needed.

TauCeti.ofReal_integral_sub_integral_le_wassersteinEDist_one.{u} {X : Type u} [MeasurableSpace X]
  {μ ν : MeasureTheory.Measure X} [PseudoEMetricSpace X] {f : X → ℝ} (hf : LipschitzWith 1 f)
  (hμ : MeasureTheory.Integrable f μ) (hν : MeasureTheory.Integrable f ν) :
  ENNReal.ofReal (∫ (x : X), f x ∂μ - ∫ (x : X), f x ∂ν) ≤ TauCeti.wassersteinEDist 1 μ ν

Lean

Formalized in Tau Ceti as TauCeti.ofReal_integral_sub_integral_le_wassersteinEDist_one.

Sources

LeanTauCeti.ofReal_integral_sub_integral_le_wassersteinEDist_one

Used by 1

Used byKantorovich–Rubinstein duality

TheoremMarkov's inequality for the Wasserstein distance from a Dirac law #

For a probability measure μ and a radius r, the mass of μ outside the closed ball of radius r about x, multiplied by r, is at most W_p (δ_x, μ), for every exponent 1 ≤ p.

TauCeti.ofReal_mul_measure_compl_closedBall_le_wassersteinEDist.{u_1} {X : Type u_1} {p : ENNReal}
  [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X]
  [Fact (1 ≤ p)] (x : X) (μ : MeasureTheory.ProbabilityMeasure X) (r : ℝ) :
  ENNReal.ofReal r * ↑μ (Metric.closedBall x r)ᶜ ≤
    TauCeti.wassersteinEDist p (MeasureTheory.Measure.dirac x) ↑μ

Lean

Formalized in Tau Ceti as TauCeti.ofReal_mul_measure_compl_closedBall_le_wassersteinEDist.

Sources

LeanTauCeti.ofReal_mul_measure_compl_closedBall_le_wassersteinEDist

TheoremThe one-dimensional Kantorovich formula #

The Wasserstein distance at exponent one of two probability laws on ℝ is the area between their cumulative distribution functions.

TauCeti.wassersteinEDist_one_eq_lintegral_enorm_cdf_sub (μ ν : MeasureTheory.Measure ℝ)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] :
  TauCeti.wassersteinEDist 1 μ ν =
    ∫⁻ (s : ℝ), ‖↑(ProbabilityTheory.cdf μ) s - ↑(ProbabilityTheory.cdf ν) s‖ₑ

Lean

Formalized in Tau Ceti as TauCeti.wassersteinEDist_one_eq_lintegral_enorm_cdf_sub.

Sources

LeanTauCeti.wassersteinEDist_one_eq_lintegral_enorm_cdf_sub

TheoremPolish Kantorovich duality for costs bounded below #

If the nonnegative residual of an integrable split lower bound is lower semicontinuous, the signed primal value is the least upper bound of the values of all integrable feasible real potentials. The value may be negative or ∞; no integrable split upper envelope or dual attainment is assumed.

TauCeti.isLUB_kantorovichDualValue_of_lowerSemicontinuous_residual_bddBelow.{u, v} {X : Type u}
  {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {c : X × Y → EReal}
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [TopologicalSpace X] [PolishSpace X]
  [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [BorelSpace Y]
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  (h : TauCeti.IntegrableSplitLowerBound c μ ν) (hres : LowerSemicontinuous h.residual) :
  IsLUB
    {r |
      ∃ φ ψ,
        MeasureTheory.Integrable φ μ ∧
          MeasureTheory.Integrable ψ ν ∧
            TauCeti.DualFeasible c φ ψ ∧ ↑(TauCeti.kantorovichDualValue μ ν φ ψ) = r}
    (TauCeti.transportCostBddBelow c μ ν h)

Lean

Formalized in Tau Ceti as TauCeti.isLUB_kantorovichDualValue_of_lowerSemicontinuous_residual_bddBelow.

Sources

LeanTauCeti.isLUB_kantorovichDualValue_of_lowerSemicontinuous_residual_bddBelow

Uses 1

Proof usesStrong Kantorovich duality for probability measures

TheoremPratelli's theorem #

For an atomless finite source measure, a nonempty target type and a continuous cost c : X × Y → [0, ∞] on second-countable standard Borel spaces, for instance Polish spaces, the Monge and Kantorovich values agree, whether finite or not. The cost may be unbounded and take the value ∞, and the Monge infimum need not be attained.

TauCeti.mongeCost_eq_transportCost_of_continuous.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [SecondCountableTopology X] [MeasurableSpace X] [OpensMeasurableSpace X]
  [StandardBorelSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] [MeasurableSpace Y]
  [OpensMeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} {c : X × Y → ENNReal} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.NullSingletonClass μ] (hc : Continuous c) :
  TauCeti.mongeCost c μ ν = TauCeti.transportCost c μ ν

Lean

Formalized in Tau Ceti as TauCeti.mongeCost_eq_transportCost_of_continuous.

Sources

LeanTauCeti.mongeCost_eq_transportCost_of_continuous

Uses 1

Proof usesSierpiński's theorem

TheoremProkhorov's theorem for multi-couplings #

The multi-couplings of finitely many tight probability measures form a weakly compact set: it is tight, hence relatively compact, and closed.

TauCeti.isCompact_setOfPred_isMultiCoupling.{u_1, u_2} {ι : Type u_1} {X : ι → Type u_2}
  [(i : ι) → TopologicalSpace (X i)] [(i : ι) → MeasurableSpace (X i)] [Finite ι]
  [∀ (i : ι), OpensMeasurableSpace (X i)]
  [∀ (i : ι), T1Space (MeasureTheory.ProbabilityMeasure (X i))] [BorelSpace ((i : ι) → X i)]
  [T2Space ((i : ι) → X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)}
  (hμ : ∀ (i : ι), MeasureTheory.IsTightMeasureSet {↑(μ i)}) :
  IsCompact {π | TauCeti.Measure.IsMultiCoupling ↑π fun i => ↑(μ i)}

Lean

Formalized in Tau Ceti as TauCeti.isCompact_setOfPred_isMultiCoupling.

Sources

LeanTauCeti.isCompact_setOfPred_isMultiCoupling

TheoremThe Pythagorean identity of the Schrödinger problem #

Let π be a coupling of μ and ν whose density against the finite reference R is exp (φ(x) + ψ(y)), for measurable potentials φ ∈ L¹(μ) and ψ ∈ L¹(ν). Then every coupling γ of μ and ν satisfies klDiv γ R = klDiv γ π + klDiv π R.

TauCeti.IsCoupling.klDiv_eq_klDiv_add_klDiv_of_eq_withDensity.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {π R : MeasureTheory.Measure (X × Y)}
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {φ : X → ℝ} {ψ : Y → ℝ}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure R]
  {γ : MeasureTheory.Measure (X × Y)} (hγ : TauCeti.IsCoupling γ μ ν)
  (hπ : TauCeti.IsCoupling π μ ν)
  (hπR : π = R.withDensity fun z => ENNReal.ofReal (Real.exp (φ z.1 + ψ z.2))) (hφ : Measurable φ)
  (hψ : Measurable ψ) (hφi : MeasureTheory.Integrable φ μ) (hψi : MeasureTheory.Integrable ψ ν) :
  InformationTheory.klDiv γ R = InformationTheory.klDiv γ π + InformationTheory.klDiv π R

Lean

Formalized in Tau Ceti as TauCeti.IsCoupling.klDiv_eq_klDiv_add_klDiv_of_eq_withDensity.

Sources

LeanTauCeti.IsCoupling.klDiv_eq_klDiv_add_klDiv_of_eq_withDensity

Uses 1

Proof usesCsiszár's Pythagorean identity

TheoremRockafellar's theorem #

A cyclically monotone set lies in the graph of the subdifferential of a Legendre–Fenchel conjugate g⋆, hence of a convex function that is lower semicontinuous for every topology compatible with the pairing, and is never ⊥ as soon as the set is nonempty (TauCeti.apply_ne_bot_of_mem_subdifferential).

TauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_subset_subdifferential.{u_1, u_2}
  {E : Type u_1} {F : Type u_2} [AddCommGroup E] [_root_.Module ℝ E] [AddCommMonoid F]
  [_root_.Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {Γ : Set (E × F)}
  (hΓ : TauCeti.IsCyclicallyMonotone (TauCeti.pairingCost B) Γ) :
  ∃ g, Γ ⊆ {p | p.2 ∈ TauCeti.subdifferential B (TauCeti.fenchelConjugate B.flip g) p.1}

Lean

Formalized in Tau Ceti as TauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_subset_subdifferential.

Other forms

Rockafellar's theorem for the quadratic cost. Formalized in Tau Ceti as TauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_innerₗ_subset_subdifferential.

TauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_innerₗ_subset_subdifferential.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set (E × E)}
  (hS : TauCeti.IsCyclicallyMonotone (fun p => ‖p.1 - p.2‖ ^ 2 / 2) S) :
  ∃ g,
    S ⊆ {p | p.2 ∈ TauCeti.subdifferential (innerₗ E) (TauCeti.fenchelConjugate (innerₗ E) g) p.1}

Sources

LeanTauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_subset_subdifferential · TauCeti.IsCyclicallyMonotone.exists_fenchelConjugate_innerₗ_subset_subdifferential

Uses 2 · Used by 2

Proof usesThe Fenchel–Young inequality · The theorem of Rockafellar and Rüschendorf

Used byBrenier's theorem · The Knott–Smith optimality criterion

TheoremThe Schachermayer--Teichmann theorem #

For a finite-valued lower semicontinuous cost on a product of Polish spaces, a coupling of finite cost between two probability measures is optimal if and only if it is concentrated on a measurable c-cyclically monotone set.

The finite-cost hypothesis is used only for the forward implication: when every coupling has infinite cost, every coupling is optimal.

TauCeti.IsCoupling.isOptimalCoupling_iff_exists_isCyclicallyMonotone.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [PolishSpace X] [BorelSpace X]
  [MeasurableSpace Y] [TopologicalSpace Y] [PolishSpace Y] [BorelSpace Y]
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} {π : MeasureTheory.Measure (X × Y)}
  (hπ : TauCeti.IsCoupling π μ ν) (hc : LowerSemicontinuous c) (hctop : ∀ (z : X × Y), c z ≠ ⊤)
  (hfin : ∫⁻ (z : X × Y), c z ∂π ≠ ⊤) :
  TauCeti.IsOptimalCoupling c π μ ν ↔
    ∃ S, MeasurableSet S ∧ TauCeti.IsCyclicallyMonotone c S ∧ π Sᶜ = 0

Lean

Formalized in Tau Ceti as TauCeti.IsCoupling.isOptimalCoupling_iff_exists_isCyclicallyMonotone.

Sources

LeanTauCeti.IsCoupling.isOptimalCoupling_iff_exists_isCyclicallyMonotone

Uses 2

Proof usesLusin's universal-measurability theorem · Strong Kantorovich duality for probability measures

TheoremStrong Kantorovich duality for probability measures #

Strong Kantorovich duality for probability measures, read as an equality between the primal value and the supremum of the dual values over the continuous potentials.

TauCeti.toReal_transportCost_eq_sSup.{u, v} {X : Type u} {Y : Type v} [PseudoMetricSpace X]
  [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [PseudoMetricSpace Y]
  [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) :
  (TauCeti.transportCost (fun z => ENNReal.ofReal (c z)) μ ν).toReal =
    sSup
      {r |
        ∃ φ ψ,
          Continuous φ ∧
            Continuous ψ ∧
              (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧ TauCeti.kantorovichDualValue μ ν φ ψ = r}

Lean

Formalized in Tau Ceti as TauCeti.toReal_transportCost_eq_sSup.

Other forms

Strong Kantorovich duality against the integrable dual class. Formalized in Tau Ceti as TauCeti.isLUB_kantorovichDualValue_integrable.

TauCeti.isLUB_kantorovichDualValue_integrable.{u, v} {X : Type u} {Y : Type v} [PseudoMetricSpace X]
  [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [PseudoMetricSpace Y]
  [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) :
  IsLUB
    {r |
      ∃ φ ψ,
        MeasureTheory.Integrable φ μ ∧
          MeasureTheory.Integrable ψ ν ∧
            (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧ TauCeti.kantorovichDualValue μ ν φ ψ = r}
    (TauCeti.transportCost (fun z => ENNReal.ofReal (c z)) μ ν).toReal

Strong Kantorovich duality for lower-semicontinuous costs on compact metrizable spaces. Formalized in Tau Ceti as TauCeti.isLUB_ofReal_kantorovichDualValue_continuous_of_lowerSemicontinuous.

TauCeti.isLUB_ofReal_kantorovichDualValue_continuous_of_lowerSemicontinuous.{u, v} {X : Type u}
  {Y : Type v} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y]
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} [TopologicalSpace.MetrizableSpace X]
  [CompactSpace X] [BorelSpace X] [TopologicalSpace.MetrizableSpace Y] [CompactSpace Y]
  [BorelSpace Y] (hc : LowerSemicontinuous c) :
  IsLUB
    {r |
      ∃ φ ψ,
        Continuous φ ∧
          Continuous ψ ∧
            TauCeti.DualFeasible (fun z => ↑(c z)) φ ψ ∧
              ENNReal.ofReal (TauCeti.kantorovichDualValue μ ν φ ψ) = r}
    (TauCeti.transportCost c μ ν)

Strong Kantorovich duality for nonnegative lower-semicontinuous costs on Polish spaces. Formalized in Tau Ceti as TauCeti.isLUB_ofReal_kantorovichDualValue_integrable_of_lowerSemicontinuous.

TauCeti.isLUB_ofReal_kantorovichDualValue_integrable_of_lowerSemicontinuous.{u, v} {X : Type u}
  {Y : Type v} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y]
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} [PolishSpace X] [BorelSpace X]
  [PolishSpace Y] [BorelSpace Y] (hc : LowerSemicontinuous c) :
  IsLUB
    {r |
      ∃ φ ψ,
        MeasureTheory.Integrable φ μ ∧
          MeasureTheory.Integrable ψ ν ∧
            TauCeti.DualFeasible (fun z => ↑(c z)) φ ψ ∧
              ENNReal.ofReal (TauCeti.kantorovichDualValue μ ν φ ψ) = r}
    (TauCeti.transportCost c μ ν)

Strong Kantorovich duality for probability measures, read in ℝ≥0∞. Formalized in Tau Ceti as TauCeti.transportCost_eq_ofReal_sSup.

TauCeti.transportCost_eq_ofReal_sSup.{u, v} {X : Type u} {Y : Type v} [PseudoMetricSpace X]
  [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [PseudoMetricSpace Y]
  [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) :
  TauCeti.transportCost (fun z => ENNReal.ofReal (c z)) μ ν =
    ENNReal.ofReal
      (sSup
        {r |
          ∃ φ ψ,
            Continuous φ ∧
              Continuous ψ ∧
                (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧
                  TauCeti.kantorovichDualValue μ ν φ ψ = r})

Strong Kantorovich duality on compact pseudometrizable spaces. Formalized in Tau Ceti as TauCeti.isLUB_kantorovichDualValue_continuous.

TauCeti.isLUB_kantorovichDualValue_continuous.{u, v} {X : Type u} {Y : Type v} [PseudoMetricSpace X]
  [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [PseudoMetricSpace Y]
  [CompactSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z) :
  IsLUB
    {r |
      ∃ φ ψ,
        Continuous φ ∧
          Continuous ψ ∧
            (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧ TauCeti.kantorovichDualValue μ ν φ ψ = r}
    (TauCeti.transportCost (fun z => ENNReal.ofReal (c z)) μ ν).toReal

Strong Kantorovich duality with dual attainment on Polish spaces. Formalized in Tau Ceti as TauCeti.isGreatest_kantorovichDualValue_integrable.

TauCeti.isGreatest_kantorovichDualValue_integrable.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y]
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [PolishSpace X]
  [BorelSpace X] [PolishSpace Y] [BorelSpace Y] [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] (hc : Continuous c) (hc0 : ∀ (z : X × Y), 0 ≤ c z)
  (hcb : BddAbove (Set.range c)) :
  IsGreatest
    {r |
      ∃ φ ψ,
        MeasureTheory.Integrable φ μ ∧
          MeasureTheory.Integrable ψ ν ∧
            (∀ (x : X) (y : Y), φ x + ψ y ≤ c (x, y)) ∧ TauCeti.kantorovichDualValue μ ν φ ψ = r}
    (TauCeti.transportCost (fun z => ENNReal.ofReal (c z)) μ ν).toReal

Sources

LeanTauCeti.toReal_transportCost_eq_sSup · TauCeti.isLUB_kantorovichDualValue_integrable · TauCeti.isLUB_ofReal_kantorovichDualValue_continuous_of_lowerSemicontinuous · TauCeti.isLUB_ofReal_kantorovichDualValue_integrable_of_lowerSemicontinuous · TauCeti.transportCost_eq_ofReal_sSup · TauCeti.isLUB_kantorovichDualValue_continuous · TauCeti.isGreatest_kantorovichDualValue_integrable

Uses 2 · Used by 2

Proof usesApproximate Kantorovich duality on compact spaces · The theorem of Rockafellar and Rüschendorf

Used byPolish Kantorovich duality for costs bounded below · The Schachermayer--Teichmann theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Approximate Kantorovich duality… to Strong Kantorovich duality for…

TheoremApproximate Kantorovich duality on compact spaces#

Lean

Sources

TheoremThe Benamou–Brenier upper bound#

Lean

Sources

TheoremBounded-Lipschitz duality in supremum form#

Lean

Sources

TheoremBounded-Lipschitz Kantorovich–Rubinstein duality with attainment#

Lean

Sources

TheoremCauchy–Schwarz for the pairing#

Lean

Sources

TheoremFinite multi-marginal Kantorovich duality#

Lean

Sources

TheoremThe Fréchet–Hoeffding bound on a quadrant#

Lean

Sources

TheoremThe generalised Bonnet–Myers theorem under CD(K, N)#

Lean

Sources

TheoremThe Gibbs identity#

Lean

Sources

TheoremKantorovich–Rubinstein duality#

Lean

Other forms

Sources

TheoremKantorovich–Rubinstein weak duality#

Lean

Sources

TheoremMarkov's inequality for the Wasserstein distance from a Dirac law#

Lean

Sources

TheoremThe one-dimensional Kantorovich formula#

Lean

Sources

TheoremPolish Kantorovich duality for costs bounded below#

Lean

Sources

TheoremPratelli's theorem#

Lean

Sources

TheoremProkhorov's theorem for multi-couplings#

Lean

Sources

TheoremThe Pythagorean identity of the Schrödinger problem#

Lean

Sources

TheoremRockafellar's theorem#

Lean

Other forms

Sources

TheoremThe Schachermayer--Teichmann theorem#

Lean

Sources

TheoremStrong Kantorovich duality for probability measures#

Lean

Other forms

Sources

TheoremApproximate Kantorovich duality on compact spaces #

TheoremThe Benamou–Brenier upper bound #

TheoremBounded-Lipschitz duality in supremum form #

TheoremBounded-Lipschitz Kantorovich–Rubinstein duality with attainment #

TheoremCauchy–Schwarz for the pairing #

TheoremFinite multi-marginal Kantorovich duality #

TheoremThe Fréchet–Hoeffding bound on a quadrant #

TheoremThe generalised Bonnet–Myers theorem under `CD(K, N)`#

TheoremThe Gibbs identity #

TheoremKantorovich–Rubinstein duality #

TheoremKantorovich–Rubinstein weak duality #

TheoremMarkov's inequality for the Wasserstein distance from a Dirac law #

TheoremThe one-dimensional Kantorovich formula #

TheoremPolish Kantorovich duality for costs bounded below #

TheoremPratelli's theorem #

TheoremProkhorov's theorem for multi-couplings #

TheoremThe Pythagorean identity of the Schrödinger problem #

TheoremRockafellar's theorem #

TheoremThe Schachermayer--Teichmann theorem #

TheoremStrong Kantorovich duality for probability measures #