The Schrödinger system for a bounded kernel

Let μ and ν be finite measures of equal mass on X and Y, and let g : X × Y → ℝ be a bounded measurable function. The Schrödinger system asks for potentials φ on X and ψ on Y such that exp (φ(x) + ψ(y) + g(x, y)) is the density, against μ.prod ν, of a coupling of μ and ν; that is,

φ x = -log ∫ exp (g (x, y) + ψ y) dν(y) and ψ y = -log ∫ exp (g (x, y) + φ x) dμ(x)

for μ-almost every x and ν-almost every y.

This file proves that the system has a solution by bounded measurable potentials (TauCeti.exists_isCoupling_withDensity_exp_add). The two equations are the two half-steps of the Sinkhorn iteration, and the solution is found as a fixed point of a full Sinkhorn sweep. If |g| ≤ M, a half-step contracts the oscillation sup (u - v) - inf (u - v) of the difference of two potentials by the factor 1 - exp (-4M). Indeed, the kernels at two points of X differ by at most the factor exp (2M), so after normalisation each of the two probability measures exp (g (x, y) + v y) dν(y) / ∫ exp (g (x, ·) + v) dν dominates exp (-4M) times the other, and the contraction then follows from the convexity of exp. Normalised to vanish at a base point, the iterates of the sweep therefore converge uniformly, at a geometric rate, to a fixed point up to an additive constant, and equality of the masses of μ and ν forces that constant to vanish.

The solution identifies the minimizers of the two entropic transport problems of TauCeti/MeasureTheory/OptimalTransport/Entropic/Basic.lean when the log-density of the reference measure is bounded.

• For a reference measure R with density exp g against μ.prod ν, the Schrödinger minimizer has density exp (φ(x) + ψ(y)) against R (TauCeti.IsCoupling.exists_eq_withDensity_exp_add_of_klDiv_eq_schroedingerValue).
• For a bounded measurable cost c and a positive temperature ε, the entropically regularised transport cost is attained by a coupling with density exp ((φ(x) + ψ(y) - c(x, y)) / ε) against μ.prod ν (TauCeti.exists_isCoupling_lintegral_add_mul_klDiv_eq_entropicTransportCost).

Boundedness of g is what makes the Sinkhorn sweep a contraction. The general theorem, for a reference measure equivalent to μ.prod ν that admits a coupling of finite relative entropy, needs a different argument and is not proved here.

Main statements

• TauCeti.exists_isCoupling_withDensity_exp_add: the Schrödinger system for a bounded measurable kernel has a solution by bounded measurable potentials.
• TauCeti.exists_isCoupling_withDensity_exp_add_of_eq_withDensity: the same system written against a reference measure R with density exp g against μ.prod ν.
• TauCeti.IsCoupling.exists_eq_withDensity_exp_add_of_klDiv_eq_schroedingerValue: the Schrödinger minimizer for a reference measure with bounded log-density against μ.prod ν has a product density.
• TauCeti.exists_isCoupling_lintegral_add_mul_klDiv_eq_entropicTransportCost: for a bounded cost the entropic optimal plan exists and has a Gibbs density with bounded potentials.

References

• R. Fortet, Résolution d'un système d'équations de M. Schrödinger, J. Math. Pures Appl. 19 (1940), 83–105, for the existence of solutions of the Schrödinger system for bounded kernels.
• J. M. Borwein, A. S. Lewis and R. D. Nussbaum, Entropy minimization, DAD problems, and doubly stochastic kernels, J. Funct. Anal. 123 (1994), 264–307, and Y. Chen, T. T. Georgiou and M. Pavon, Entropic and displacement interpolation: a computational approach using the Hilbert metric, SIAM J. Appl. Math. 76 (2016), 2375–2396, for the Sinkhorn iteration as a contraction for positive kernels bounded above and below.
• M. Nutz, Introduction to Entropic Optimal Transport, lecture notes, Columbia University, 2021, Theorem 2.1, for the product form of the density of the Schrödinger minimizer.

theorem TauCeti.exists_isCoupling_withDensity_exp_add {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {g : X × Y → ℝ} {M : ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμν : μ Set.univ = ν Set.univ) (hg : Measurable g) (hgM : ∀ (z : X × Y), |g z| ≤ M) : ∃ (φ : X → ℝ) (ψ : Y → ℝ) (C : ℝ), Measurable φ ∧ Measurable ψ ∧ (∀ (x : X), |φ x| ≤ C) ∧ (∀ (y : Y), |ψ y| ≤ C) ∧ IsCoupling ((μ.prod ν).withDensity fun (z : X × Y) => ENNReal.ofReal (Real.exp (φ z.1 + ψ z.2 + g z))) μ ν

The Schrödinger system for a bounded kernel. Let μ be a finite measure, ν a measure of the same mass, and g a bounded measurable function on X × Y. Then there are bounded measurable potentials φ and ψ such that exp (φ(x) + ψ(y) + g(x, y)) is the density, against μ.prod ν, of a coupling of μ and ν.

theorem TauCeti.exists_isCoupling_withDensity_exp_add_of_eq_withDensity {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {g : X × Y → ℝ} {M : ℝ} [MeasureTheory.IsFiniteMeasure μ] {R : MeasureTheory.Measure (X × Y)} (hμν : μ Set.univ = ν Set.univ) (hg : Measurable g) (hgM : ∀ (z : X × Y), |g z| ≤ M) (hR : R = (μ.prod ν).withDensity fun (z : X × Y) => ENNReal.ofReal (Real.exp (g z))) : ∃ (φ : X → ℝ) (ψ : Y → ℝ) (C : ℝ), Measurable φ ∧ Measurable ψ ∧ (∀ (x : X), |φ x| ≤ C) ∧ (∀ (y : Y), |ψ y| ≤ C) ∧ IsCoupling (R.withDensity fun (z : X × Y) => ENNReal.ofReal (Real.exp (φ z.1 + ψ z.2))) μ ν

The Schrödinger system against a reference measure with bounded log-density. Let μ be a finite measure, ν a measure of the same mass, and let the reference measure R have density exp g against μ.prod ν, for a bounded measurable g. Then there are bounded measurable potentials φ and ψ such that exp (φ(x) + ψ(y)) is the density, against R, of a coupling of μ and ν.

theorem TauCeti.IsCoupling.exists_eq_withDensity_exp_add_of_klDiv_eq_schroedingerValue {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {g : X × Y → ℝ} {M : ℝ} [MeasureTheory.IsFiniteMeasure μ] {π R : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) (hg : Measurable g) (hgM : ∀ (z : X × Y), |g z| ≤ M) (hR : R = (μ.prod ν).withDensity fun (z : X × Y) => ENNReal.ofReal (Real.exp (g z))) (hπR : InformationTheory.klDiv π R = schroedingerValue R μ ν) : ∃ (φ : X → ℝ) (ψ : Y → ℝ) (C : ℝ), Measurable φ ∧ Measurable ψ ∧ (∀ (x : X), |φ x| ≤ C) ∧ (∀ (y : Y), |ψ y| ≤ C) ∧ π = R.withDensity fun (z : X × Y) => ENNReal.ofReal (Real.exp (φ z.1 + ψ z.2))

The Schrödinger minimizer has a product density. Let the reference measure R have density exp g against μ.prod ν, for a bounded measurable g, and let μ be finite. Then a coupling of μ and ν attaining the Schrödinger value has density exp (φ(x) + ψ(y)) against R, for bounded measurable potentials φ and ψ. Such a coupling exists whenever μ and ν have equal mass, by TauCeti.exists_isCoupling_withDensity_exp_add and TauCeti.IsCoupling.klDiv_eq_schroedingerValue_of_eq_withDensity.

theorem TauCeti.exists_isCoupling_lintegral_add_mul_klDiv_eq_entropicTransportCost {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {c : X × Y → ENNReal} (hc : Measurable c) {B : NNReal} (hcB : ∀ (z : X × Y), c z ≤ ↑B) {ε : NNReal} (hε : ε ≠ 0) : ∃ (π : MeasureTheory.Measure (X × Y)), IsCoupling π μ ν ∧ ∫⁻ (z : X × Y), c z ∂π + ↑ε * InformationTheory.klDiv π (μ.prod ν) = entropicTransportCost c ε μ ν ∧ ∃ (φ : X → ℝ) (ψ : Y → ℝ) (C : ℝ), Measurable φ ∧ Measurable ψ ∧ (∀ (x : X), |φ x| ≤ C) ∧ (∀ (y : Y), |ψ y| ≤ C) ∧ π = (μ.prod ν).withDensity fun (z : X × Y) => ENNReal.ofReal (Real.exp ((φ z.1 + ψ z.2 - (c z).toReal) / ↑ε))

The entropic optimal plan for a bounded cost. For probability measures μ and ν, a bounded measurable cost c and a positive temperature ε, the regularised transport cost TauCeti.entropicTransportCost c ε μ ν is attained by a coupling whose density against μ.prod ν is exp ((φ(x) + ψ(y) - c(x, y)) / ε), for bounded measurable potentials φ and ψ.