Entropic optimal transport and the static Schrödinger problem #
Two entropy-based transport problems share the coupling constraint of Kantorovich's problem.
- The static Schrödinger problem with reference measure
RonX × Yminimises the relative entropyklDiv π Rover the couplingsπofμandν. Its value isTauCeti.schroedingerValue R μ ν. - Entropically regularised transport at temperature
εaddsεtimes the relative entropy against the product of the marginals to the transport cost of a plan, and minimises∫⁻ c dπ + ε * klDiv π (μ.prod ν)over the same couplings. Its value isTauCeti.entropicTransportCost c ε μ ν.
The two are the same problem. For probability measures μ, ν, a cost that is finite
μ.prod ν-almost everywhere, and a positive temperature ε, let
Z = ∫ e^{-c/ε} d(μ ⊗ ν) be the partition function and R = Z⁻¹ e^{-c/ε} (μ ⊗ ν) the Gibbs
measure, which is Mathlib's tilted measure
(μ.prod ν).tilted fun z ↦ -((c z).toReal / ε). Then for every probability measure π on
X × Y
∫ c dπ + ε * klDiv π (μ ⊗ ν) = ε * klDiv π R - ε * log Z,
so the regularised value is ε times the Schrödinger value with reference R, shifted by the
free energy -ε log Z ≥ 0, and the two problems have the same optimal couplings.
Main definitions #
TauCeti.schroedingerValue R μ ν: the infimum ofklDiv π Rover the couplingsπofμandν.TauCeti.entropicTransportCost c ε μ ν: the infimum of∫⁻ z, c z ∂π + ε * klDiv π (μ.prod ν)over the couplingsπofμandν.
Main statements #
TauCeti.schroedingerValue_prod: with the product of the marginals as reference, the Schrödinger value is0, attained by the product coupling.TauCeti.IsCoupling.eq_of_klDiv_eq_schroedingerValue: a finite Schrödinger value has at most one minimizing coupling for a finite reference measure.TauCeti.exists_isCoupling_klDiv_eq_schroedingerValueandTauCeti.existsUnique_isCoupling_klDiv_eq_schroedingerValue: for a finite reference measure and a finite source measure, a finite Schrödinger value is attained, by exactly one coupling.TauCeti.IsCoupling.klDiv_eq_klDiv_add_klDiv_of_eq_withDensity: if a couplingπhas densityexp (φ(x) + ψ(y))againstR, every couplingγsatisfies the Pythagorean identityklDiv γ R = klDiv γ π + klDiv π R.TauCeti.IsCoupling.klDiv_eq_schroedingerValue_of_eq_withDensityandTauCeti.schroedingerValue_eq_ofReal_of_eq_withDensity: such a coupling is the Schrödinger minimizer, and the Schrödinger value is the dual value∫ φ dμ + ∫ ψ dνof its potentials, corrected by the masses ofRandμ.TauCeti.exists_ae_eq_add_const_of_withDensity_exp_eq: whenRdominatesμ.prod ν, the potentials are unique up to one additive constant.TauCeti.entropicTransportCost_zeroandTauCeti.transportCost_le_entropicTransportCost: at zero temperature the regularised value is the transport cost, which it always dominates.TauCeti.entropicTransportCost_le_lintegral_prod,TauCeti.entropicTransportCost_ne_top_of_lintegral_ne_topandTauCeti.entropicTransportCost_ne_top_of_ae_le: for probability measures the regularised value is at most the cost of the product coupling, so it is finite for a cost of finite integral againstμ ⊗ ν, in particular for a bounded cost.TauCeti.entropicTransportCost_const: for a constant cost the regularised value is the constant; when it is finite, withMathlib'sInformationTheory.klDiv_eq_zero_iff, the product coupling is then the unique optimal plan at positive temperature.TauCeti.lintegral_add_mul_klDiv_eq_mul_klDiv_tilted: the Gibbs identity above, plan by plan.TauCeti.entropicTransportCost_eq_mul_schroedingerValue_add: the same identity for the optimal values.TauCeti.lintegral_add_mul_klDiv_eq_entropicTransportCost_iff: a coupling is optimal for the regularised problem exactly when it is optimal for the Schrödinger problem with the Gibbs reference.TauCeti.IsCoupling.lintegral_add_mul_klDiv_eq_entropicTransportCost_of_eq_withDensityandTauCeti.entropicTransportCost_eq_ofReal_of_eq_withDensity: a coupling with densityexp ((φ(x) + ψ(y) - c(x, y)) / ε)againstμ.prod νis optimal for the regularised problem, whose value is then∫ φ dμ + ∫ ψ dν.
Implementation notes #
As for TauCeti.transportCost, both values are defined for arbitrary measures, with an
extended-nonnegative cost, as an iterated infimum over plans and proofs of TauCeti.IsCoupling,
so that an empty feasible set gives ∞. The temperature ε is a nonnegative real number; the
value at ε = 0 is the unregularised transport cost.
The Gibbs identity needs the cost to be finite μ.prod ν-almost everywhere, since otherwise the
Gibbs measure is not equivalent to μ.prod ν; a cost that is infinite on a set of positive
product measure constrains the support of every plan of finite entropy and is a separate,
degenerate regime. The identity holds for every probability measure π on X × Y, not only for
couplings, and in ℝ≥0∞ with no integrability hypothesis: when π is not absolutely continuous
with respect to μ.prod ν, or has infinite cost, both sides are ∞.
Existence of the Schrödinger minimizer holds in the same generality as its uniqueness: for a
finite source measure μ and a finite reference measure R, a finite Schrödinger value is
attained on arbitrary measurable spaces X and Y. No topology, separability, or normalization
of R to a probability measure is assumed. Together with uniqueness, the minimizing coupling is
then well defined whenever the Schrödinger value is finite.
The potentials φ and ψ are the dual side of the problem. A coupling whose density against
the reference factorises as exp (φ(x) + ψ(y)), with φ ∈ L¹(μ) and ψ ∈ L¹(ν), is the
minimizer: log (dπ/dR) then integrates to the same value ∫ φ dμ + ∫ ψ dν against every
coupling, which is the hypothesis of Csiszár's Pythagorean identity
TauCeti.klDiv_eq_klDiv_add_klDiv. This is the sufficiency half of the characterisation of the
Schrödinger minimizer by its density; the converse, that the minimizer has such a density, needs
further hypotheses and is not part of this file. For a reference measure with bounded log-density
against μ.prod ν it is proved in
TauCeti/MeasureTheory/OptimalTransport/Entropic/SchroedingerSystem.lean. The potentials are
measurable functions rather than almost everywhere defined ones, since the density is taken
against R and not against the marginals.
References #
- M. Nutz, Introduction to Entropic Optimal Transport, lecture notes, Columbia University, 2021, for the regularised problem, its Gibbs reference measure, and the reduction to minimising relative entropy, and Theorem 2.1 for the product form of the minimizer's density and the uniqueness of its potentials up to a constant.
- C. Léonard, A survey of the Schrödinger problem and some of its connections with optimal transport, Discrete Contin. Dyn. Syst. 34 (2014), for the static Schrödinger problem.
- I. Csiszár, I-divergence geometry of probability distributions and minimization problems, Ann. Probability 3 (1975), 146–158, Theorem 2.1, whose existence argument for entropy minimizers over convex sets closed in total variation is followed here, and for the Pythagorean identity of relative entropy.
The static Schrödinger problem #
The value of the static Schrödinger problem with reference measure R: the infimum of the
relative entropy klDiv π R over the couplings π of μ and ν. It is ∞ when μ and ν
have no coupling, or no coupling of finite relative entropy.
Instances For
The Schrödinger value as the infimum of the relative entropies of all feasible plans.
Every coupling bounds the Schrödinger value from above.
A bound valid on every coupling bounds the Schrödinger value from below.
The Schrödinger value is below a threshold exactly when some coupling is.
With the product of the marginals as reference, the Schrödinger value is 0: the product
coupling has zero relative entropy. By InformationTheory.klDiv_eq_zero_iff it is the only
coupling attaining this value.
Uniqueness of a finite-entropy Schrödinger minimizer. For a finite reference and finite
source measure, any two couplings attaining a finite Schrödinger value agree. This applies on
arbitrary measurable spaces; existence is
TauCeti.exists_isCoupling_klDiv_eq_schroedingerValue.
Existence of the Schrödinger minimizer. For a finite reference measure and a finite
source measure, a finite Schrödinger value is attained by a coupling. No topology, separability
or normalization is needed: the measurable spaces are arbitrary, and R need not be a
probability measure. Together with TauCeti.IsCoupling.eq_of_klDiv_eq_schroedingerValue, the
minimizer is unique; see TauCeti.existsUnique_isCoupling_klDiv_eq_schroedingerValue.
Existence and uniqueness of the Schrödinger minimizer. For a finite reference measure and a finite source measure, a finite Schrödinger value is attained by exactly one coupling.
Schrödinger potentials #
The 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.
The relative entropy of a coupling with density exp (φ(x) + ψ(y)) against R is the dual
value ∫ φ dμ + ∫ ψ dν of its potentials, corrected by the difference of the masses of R and
μ.
A product density certifies the Schrödinger minimizer. A coupling π of μ and ν
whose density against the finite reference R is exp (φ(x) + ψ(y)), for measurable
potentials φ ∈ L¹(μ) and ψ ∈ L¹(ν), attains the Schrödinger value. By
TauCeti.IsCoupling.eq_of_klDiv_eq_schroedingerValue it is the only coupling to do so.
The value of the Schrödinger problem from its potentials. If some coupling of μ and ν
has density exp (φ(x) + ψ(y)) against the finite reference R, for measurable potentials
φ ∈ L¹(μ) and ψ ∈ L¹(ν), then the Schrödinger value is the dual value
∫ φ dμ + ∫ ψ dν of the potentials, corrected by the difference of the masses of R and μ.
For probability measures μ and R the correction vanishes.
Uniqueness of the Schrödinger potentials. If a reference measure R dominates the
product of the nonzero marginals, two pairs of potentials that give the same density
exp (φ(x) + ψ(y)) against R differ by one additive constant, μ- and ν-almost everywhere:
φ = φ' + a and ψ = ψ' - a.
Entropically regularised transport #
The entropically regularised transport cost of μ and ν for the cost c at temperature
ε: the infimum of ∫⁻ z, c z ∂π + ε * klDiv π (μ.prod ν) over the couplings π of μ and
ν. It is ∞ when μ and ν have no coupling.
Instances For
The regularised transport cost as the infimum of the regularised costs of all feasible plans.
Every coupling bounds the regularised transport cost from above.
A bound valid on every coupling bounds the regularised transport cost from below.
The regularised transport cost is below a threshold exactly when some coupling is.
The regularised transport cost is monotone in the cost and in the temperature.
At zero temperature the regularised transport cost is the transport cost.
The regularised transport cost dominates the transport cost.
The regularised transport cost of two probability measures is at most the cost of their product
coupling, whose relative entropy against μ.prod ν vanishes.
For a cost of finite integral against μ.prod ν, the regularised transport cost of two
probability measures is finite, by the product-coupling bound.
For a cost bounded by B almost everywhere against μ.prod ν, the regularised transport
cost of two probability measures is finite, by the product-coupling bound.
For a constant cost a, the regularised transport cost of two probability measures is a,
attained by the product coupling. Since a coupling π pays a + ε * klDiv π (μ.prod ν), at
positive temperature and for finite a the product coupling is the only optimal plan, by
InformationTheory.klDiv_eq_zero_iff.
The Gibbs reformulation #
The 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 ∞.
The Gibbs reformulation of entropic transport. For probability measures μ and ν, a
cost c finite μ.prod ν-almost everywhere, and a positive temperature ε, the regularised
transport cost is ε times the value of the Schrödinger problem with the Gibbs reference
measure R = Z⁻¹ e^{-c/ε} (μ ⊗ ν), plus the free energy -ε log Z.
A coupling is optimal for the regularised transport problem at positive temperature exactly
when it is optimal for the Schrödinger problem with the Gibbs reference measure
R = Z⁻¹ e^{-c/ε} (μ ⊗ ν), for a cost finite μ.prod ν-almost everywhere.
Potentials of the regularised problem #
A Gibbs density certifies the entropic optimal plan. For probability measures μ and
ν, a cost c finite μ.prod ν-almost everywhere, and a positive temperature ε, a coupling
π whose density against μ.prod ν is exp ((φ(x) + ψ(y) - c(x, y)) / ε), for potentials
φ ∈ L¹(μ) and ψ ∈ L¹(ν), is optimal for the regularised transport problem.
The entropic transport cost from its potentials. For probability measures μ and ν,
a cost c finite μ.prod ν-almost everywhere, and a positive temperature ε, if some coupling
has density exp ((φ(x) + ψ(y) - c(x, y)) / ε) against μ.prod ν, for potentials
φ ∈ L¹(μ) and ψ ∈ L¹(ν), then the regularised transport cost is the dual value
∫ φ dμ + ∫ ψ dν of the potentials.