The entropy minimiser with prescribed marginals and the Sinkhorn–Knopp theorem

Let ι and κ be finite types, let a : ι → ℝ and b : κ → ℝ be the row and the column sums, and let S be the set of the nonnegative matrices P : ι × κ → ℝ whose row sums are a and whose column sums are b. Against a fixed matrix K : ι × κ → ℝ, the relative entropy of P attains a minimum on S as soon as S is nonempty, and for strictly positive marginals of equal total mass every minimiser has strictly positive entries.

On a convex set of nonnegative matrices, a minimiser of the relative entropy has the largest support (Csiszár's support property), which gives the positivity above. For a nonnegative K the minimiser among the matrices vanishing wherever K does is a diagonal scaling P i j = u i * K i j * v j of K by strictly positive factors, as soon as some competitor has the zero pattern of K. At such a minimiser the relative entropy is differentiable along every direction that preserves the marginals and vanishes off the support of P, and its derivative vanishes there; a matrix orthogonal to all these directions is a function of the row plus a function of the column on that support, and this splits log (P i j) - log (K i j). A strictly positive K is the case without zero entries. Conversely, Gibbs' inequality and the Pythagorean identity relEntropy Q K = relEntropy Q P + relEntropy P K show that every such scaling with marginals a and b is the minimiser. This gives the Sinkhorn–Knopp theorem for a strictly positive kernel: strictly positive marginals of equal total mass are the row and column sums of a diagonal scaling of K, the scaled matrix is unique, and its factors are unique up to one common scalar.

The same decomposition of the relative entropy through a diagonal scaling computes the duality gap of the Lagrangian dual objective Matrix.relEntropyDual of the minimisation: every dual value is at most every primal value, and at the logarithms of the factors of the minimiser the two agree.

Nothing here uses the ordinal structure of the row and column types: the results are stated for arbitrary finite ι and κ, and the diagonal scaling of a kernel between two enumerated finite sets is the specialisation of Matrix.IsDiagonalScaling to Fin n and Fin m.

The relative entropy Matrix.relEntropy P K below is the formula ∑ i, ∑ j, (P i j * log (P i j) - P i j * log (K i j)); for a nonnegative P and a strictly positive K it is the relative entropy of P against K. Existence and positivity of the minimiser hold for every K; nonnegativity of K and a competitor with its zero pattern are needed only to identify the minimiser with a diagonal scaling of K. The resulting scaling criterion for a kernel with zero entries is in TauCeti.Data.Matrix.Scaling.Support.

Matrix.IsDiagonalScaling P K u v records the shape of the minimiser: P i j = u i * K i j * v j for row factors u and column factors v, that is a diagonal scaling of K.

The marginals here are arbitrary vectors of equal total mass, not probability distributions, and the matrices are real: this is the setting of a diagonal scaling of a kernel, where the scaled matrix has total mass ∑ i, a i and is compared against the real kernel K. A probability-valued plan with PMF marginals is TauCeti.TransportMatrix.

Main definitions

• Matrix.HasMarginals P a b: the row sums of P are a and its column sums are b.
• Matrix.IsDiagonalScaling P K u v: P i j = u i * K i j * v j for all i and j.
• Matrix.relEntropy P K: the sum over i, j of P i j * (log (P i j) - log (K i j)).
• Matrix.relEntropyDual K a b f g: the dual objective of the entropy minimisation with marginals a and b against K, at the potentials f and g.

Main results

• Matrix.isCompact_setOf_nonneg_hasMarginals: the nonnegative matrices with row sums a and column sums b form a compact set.
• Matrix.hasMarginals_mul_mul_inv: the product coupling a i * (b j * (∑ k, a k)⁻¹) has row sums a and column sums b when these have the same nonzero total mass.
• Matrix.exists_relEntropy_minOn: a minimiser of Matrix.relEntropy against K among the nonnegative matrices with row sums a and column sums b exists, as soon as there is one such matrix.
• Matrix.exists_relEntropy_minOn_of_pos: the same, for strictly positive marginals a and b of equal total mass.
• Matrix.convex_setOf_nonneg_hasMarginals: these matrices form a convex set.
• Matrix.pos_of_isMinOn_relEntropy: a minimiser of the relative entropy over a convex set is positive wherever some nonnegative member of the set is.
• Matrix.pos_of_relEntropy_minOn: every minimiser with strictly positive marginals has strictly positive entries; Matrix.pos_of_relEntropy_minOn_support is the version among the matrices vanishing wherever K does.
• Matrix.HasMarginals.add_vecMulVec_of_sum_eq_zero: the row and column sums of a matrix are preserved by an outer product of a row weight and a column weight, each of total sum 0.
• Matrix.relEntropy_nonneg and Matrix.relEntropy_eq_zero_iff: Gibbs' inequality for matrices of equal total mass, with its equality case; Matrix.relEntropy_nonneg_of_nonneg allows a reference with zero entries, on which the other matrix vanishes.
• Matrix.hasDerivAt_relEntropy_add_smul, Matrix.sum_sum_mul_log_sub_log_eq_zero_of_relEntropy_minOn_support and Matrix.sum_sum_mul_log_sub_log_eq_zero_of_relEntropy_minOn: the derivative of the relative entropy along a direction, and the first-order condition at a minimiser on its own support and at a positive minimiser.
• Matrix.exists_forall_mem_eq_add_iff: on a set s of cells, a matrix is f i + g j exactly when it is orthogonal to every matrix vanishing off s with zero row and column sums.
• Matrix.exists_isDiagonalScaling_of_relEntropy_minOn_support: for a nonnegative K, if some competitor has the zero pattern of K, the minimiser among the matrices vanishing wherever K does is a diagonal scaling of K by strictly positive factors.
• Matrix.exists_isDiagonalScaling_of_relEntropy_minOn: for a strictly positive K, every minimiser is a diagonal scaling of K by strictly positive factors; Matrix.relEntropy_minOn_iff_exists_isDiagonalScaling is the resulting characterisation.
• Matrix.IsDiagonalScaling.relEntropy_eq_relEntropy_add_sum_sum_mul and Matrix.IsDiagonalScaling.relEntropy_eq_relEntropy_add: the decomposition of the relative entropy against K through a diagonal scaling of K, and the resulting Pythagorean identity.
• Matrix.IsDiagonalScaling.relEntropy_sub_relEntropyDual: the duality gap at the potentials of a diagonal scaling R of K is the relative entropy against R plus the mass excess of R.
• Matrix.relEntropyDual_le_relEntropy and Matrix.IsDiagonalScaling.relEntropyDual_eq_relEntropy: weak duality, and strong duality with attainment at the Sinkhorn–Knopp scaling.
• Matrix.exists_sinkhorn_scaling: the Sinkhorn–Knopp theorem for a strictly positive kernel.
• Matrix.IsDiagonalScaling.eq_of_hasMarginals and Matrix.IsDiagonalScaling.exists_eq_rescale_factors: the scaled matrix is unique, and its factors are unique up to a common scalar.
• Matrix.IsDiagonalScaling.apply_le_exp_hilbertProjectiveDist_mul: two diagonal scalings of a strictly positive kernel with the same row sums agree entrywise up to the factor exp d, where d is the Hilbert projective distance between their column factors.

References

• R. Sinkhorn and P. Knopp, Concerning nonnegative matrices and doubly stochastic matrices, Pacific J. Math. 21 (1967), 343--348.
• I. Csiszár, I-divergence geometry of probability distributions and minimization problems, Ann. Probab. 3 (1975), 146--158, for the Pythagorean identity of the relative entropy and the support of a relative-entropy minimiser.
• G. Peyré and M. Cuturi, Computational Optimal Transport, Found. Trends Mach. Learn. 11 (2019), Proposition 4.3, for the characterisation of the entropic minimiser as a diagonal scaling, and Section 4.4, for the dual of the entropic problem.

Marginals and diagonal scalings

def Matrix.HasMarginals {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (P : Matrix ι κ ℝ) (a : ι → ℝ) (b : κ → ℝ) : Prop

P has row sums a and column sums b, that is (∑ j, P i j) = a i and (∑ i, P i j) = b j for all i and j.

This is the two sum equalities only. The nonnegativity of a matrix with these marginals is a separate hypothesis, as it is in the results below.

@[simp]

theorem Matrix.hasMarginals_def {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (P : Matrix ι κ ℝ) (a : ι → ℝ) (b : κ → ℝ) : P.HasMarginals a b ↔ (∀ (i : ι), ∑ j : κ, P i j = a i) ∧ ∀ (j : κ), ∑ i : ι, P i j = b j

theorem Matrix.HasMarginals.apply_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P : Matrix ι κ ℝ} {a : ι → ℝ} {b : κ → ℝ} (hP : P.HasMarginals a b) (h0 : ∀ (i : ι) (j : κ), 0 ≤ P i j) (i : ι) (j : κ) : P i j ≤ a i ∧ P i j ≤ b j

Every entry of a nonnegative matrix is at most its row sum and its column sum.

theorem Matrix.HasMarginals.sum_eq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P : Matrix ι κ ℝ} {a : ι → ℝ} {b : κ → ℝ} (hP : P.HasMarginals a b) : ∑ i : ι, a i = ∑ j : κ, b j

The row sums and the column sums of a matrix have the same total.

def Matrix.IsDiagonalScaling {ι : Type u_1} {κ : Type u_2} (P K : Matrix ι κ ℝ) (u : ι → ℝ) (v : κ → ℝ) : Prop

P is the diagonal scaling of K by the row factors u and the column factors v, that is P i j = u i * K i j * v j for all i and j.

@[simp]

theorem Matrix.isDiagonalScaling_def {ι : Type u_1} {κ : Type u_2} (P K : Matrix ι κ ℝ) (u : ι → ℝ) (v : κ → ℝ) : P.IsDiagonalScaling K u v ↔ ∀ (i : ι) (j : κ), P i j = u i * K i j * v j

theorem Matrix.IsDiagonalScaling.hasMarginals {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P K : Matrix ι κ ℝ} {u : ι → ℝ} {v : κ → ℝ} (h : P.IsDiagonalScaling K u v) (a : ι → ℝ) (b : κ → ℝ) (ha : ∀ (i : ι), ∑ j : κ, u i * K i j * v j = a i) (hb : ∀ (j : κ), ∑ i : ι, u i * K i j * v j = b j) : P.HasMarginals a b

The row and column sums of a diagonal scaling are the row and column sums of its factors, so the stated sums of u i * K i j * v j over the columns and over the rows transfer through IsDiagonalScaling to HasMarginals P a b.

theorem Matrix.IsDiagonalScaling.rescale_factors {ι : Type u_1} {κ : Type u_2} {P K : Matrix ι κ ℝ} {u : ι → ℝ} {v : κ → ℝ} (h : P.IsDiagonalScaling K u v) {r : ℝ} (hr : r ≠ 0) : P.IsDiagonalScaling K (fun (i : ι) => r * u i) fun (j : κ) => r⁻¹ * v j

A diagonal scaling is not unique: rescaling the row factors by r and the column factors by r ⁻¹, for a nonzero r, leaves the scaled matrix P unchanged.

theorem Matrix.IsDiagonalScaling.pos {ι : Type u_1} {κ : Type u_2} {P K : Matrix ι κ ℝ} {u : ι → ℝ} {v : κ → ℝ} (h : P.IsDiagonalScaling K u v) (hK : ∀ (i : ι) (j : κ), 0 < K i j) (hu : ∀ (i : ι), 0 < u i) (hv : ∀ (j : κ), 0 < v j) (i : ι) (j : κ) : 0 < P i j

A diagonal scaling of a strictly positive K by strictly positive factors is strictly positive.

theorem Matrix.IsDiagonalScaling.transpose {ι : Type u_1} {κ : Type u_2} {P K : Matrix ι κ ℝ} {u : ι → ℝ} {v : κ → ℝ} (h : P.IsDiagonalScaling K u v) : P.transpose.IsDiagonalScaling K.transpose v u

Transposing a diagonal scaling exchanges the roles of the row and the column factors: if P is the diagonal scaling of K by u and v, then Pᵀ is the diagonal scaling of Kᵀ by v and u.

The relative entropy of a matrix against a kernel

noncomputable def Matrix.relEntropy {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (P K : Matrix ι κ ℝ) : ℝ

Matrix.relEntropy P K is the real number ∑ i, ∑ j, (P i j * Real.log (P i j) - P i j * Real.log (K i j)), with the convention 0 * log 0 = 0.

The formula is defined for arbitrary real matrices P and K. For a nonnegative P and a strictly positive K it is the relative entropy of P against K; the nonnegativity of P and the strict positivity of K are hypotheses of the results that use this interpretation, not part of the definition.

Writing A = ∑ i j, P i j and B = ∑ i j, K i j, for a nonnegative P of positive total mass and a strictly positive K it is A times the relative entropy of the probability distributions P i j / A and K i j / B, up to the additive constant A * (log A - log B). Two matrices of equal total mass that differ by that constant are compared the same way by an optimisation against K.

@[simp]

theorem Matrix.relEntropy_def {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (P K : Matrix ι κ ℝ) : P.relEntropy K = ∑ i : ι, ∑ j : κ, (P i j * Real.log (P i j) - P i j * Real.log (K i j))

theorem Matrix.relEntropy_self {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (P : Matrix ι κ ℝ) : P.relEntropy P = 0

The relative entropy of a matrix against itself vanishes.

theorem Matrix.continuous_relEntropy {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K : Matrix ι κ ℝ) : Continuous fun (x : Matrix ι κ ℝ) => x.relEntropy K

The relative entropy against a fixed matrix is continuous in the matrix it is applied to.

A minimiser of the relative entropy

theorem Matrix.isCompact_setOf_nonneg_hasMarginals {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : ι → ℝ) (b : κ → ℝ) : IsCompact {P : Matrix ι κ ℝ | (∀ (i : ι) (j : κ), 0 ≤ P i j) ∧ P.HasMarginals a b}

The nonnegative matrices with row sums a and column sums b form a compact set.

The set is closed, and every entry of such a matrix is at most ∑ i, a i, so it is a closed subset of a compact box.

theorem Matrix.exists_relEntropy_minOn {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K : Matrix ι κ ℝ) (a : ι → ℝ) (b : κ → ℝ) (hfeas : ∃ (P : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ P i j) ∧ P.HasMarginals a b) : ∃ (P : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ P i j) ∧ P.HasMarginals a b ∧ ∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → P.relEntropy K ≤ Q.relEntropy K

The relative entropy against K attains a minimum on the nonnegative matrices with row sums a and column sums b, as soon as there is one such matrix.

The set of these matrices is compact by Matrix.isCompact_setOf_nonneg_hasMarginals, and the relative entropy is continuous.

theorem Matrix.hasMarginals_mul_mul_inv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {a : ι → ℝ} {b : κ → ℝ} (hmass : ∑ i : ι, a i = ∑ j : κ, b j) (hA : ∑ i : ι, a i ≠ 0) : HasMarginals (fun (i : ι) (j : κ) => a i * (b j * (∑ k : ι, a k)⁻¹)) a b

For row sums a and column sums b of the same nonzero total mass A = ∑ i, a i, the product coupling a i * (b j * A⁻¹) has row sums a and column sums b.

theorem Matrix.exists_relEntropy_minOn_of_nonneg {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K : Matrix ι κ ℝ) (a : ι → ℝ) (b : κ → ℝ) (ha : ∀ (i : ι), 0 ≤ a i) (hb : ∀ (j : κ), 0 ≤ b j) (hmass : ∑ i : ι, a i = ∑ j : κ, b j) : ∃ (P : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ P i j) ∧ P.HasMarginals a b ∧ ∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → P.relEntropy K ≤ Q.relEntropy K

The relative entropy against K attains a minimum on the nonnegative matrices with row sums a and column sums b whenever a and b are nonnegative and of equal total mass.

Such a matrix is always available: the product coupling P i j = a i * b j / ∑ k, a k has the prescribed marginals when the total mass is positive, and when the total mass is zero both marginals vanish identically, so the zero matrix has them.

theorem Matrix.exists_relEntropy_minOn_of_pos {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K : Matrix ι κ ℝ) (a : ι → ℝ) (b : κ → ℝ) (ha : ∀ (i : ι), 0 < a i) (hb : ∀ (j : κ), 0 < b j) (hmass : ∑ i : ι, a i = ∑ j : κ, b j) : ∃ (P : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ P i j) ∧ P.HasMarginals a b ∧ ∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → P.relEntropy K ≤ Q.relEntropy K

For strictly positive marginals a and b of equal total mass, the relative entropy against K attains a minimum on the nonnegative matrices with row sums a and column sums b.

This is the case of nonnegative marginals of exists_relEntropy_minOn_of_nonneg; it is stated separately because strictly positive marginals are the setting of Matrix.exists_isDiagonalScaling_of_relEntropy_minOn, which identifies the minimiser with a diagonal scaling of K.

Linearity of the marginal constraints

theorem Matrix.HasMarginals.add {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P Q : Matrix ι κ ℝ} {a a' : ι → ℝ} {b b' : κ → ℝ} (hP : P.HasMarginals a b) (hQ : Q.HasMarginals a' b') : (P + Q).HasMarginals (a + a') (b + b')

The row and column sums of a sum of two matrices are the sums of their row and column sums.

theorem Matrix.HasMarginals.smul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P : Matrix ι κ ℝ} {a : ι → ℝ} {b : κ → ℝ} (hP : P.HasMarginals a b) (t : ℝ) : (t • P).HasMarginals (t • a) (t • b)

The row and column sums of a scalar multiple of a matrix are the same multiple of its row and column sums.

theorem Matrix.HasMarginals.sum_sum_mul_add {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {Q : Matrix ι κ ℝ} {a : ι → ℝ} {b : κ → ℝ} (hQ : Q.HasMarginals a b) (f : ι → ℝ) (g : κ → ℝ) : ∑ i : ι, ∑ j : κ, Q i j * (f i + g j) = ∑ i : ι, a i * f i + ∑ j : κ, b j * g j

Summed against a matrix with row sums a and column sums b, a function f i + g j of the row plus a function of the column gives ∑ i, a i * f i + ∑ j, b j * g j: only the marginals of the matrix enter.

theorem Matrix.HasMarginals.add_vecMulVec_of_sum_eq_zero {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : ι → ℝ) (b : κ → ℝ) (P : Matrix ι κ ℝ) (hP : P.HasMarginals a b) (r : ι → ℝ) (c : κ → ℝ) (hr : ∑ x : ι, r x = 0) (hc : ∑ y : κ, c y = 0) (t : ℝ) : (P + vecMulVec (fun (x : ι) => t * r x) c).HasMarginals a b

Adding the outer product Matrix.vecMulVec (t * r) c of a row weight r and a column weight c, both of total sum 0, preserves the row sums and the column sums: the row of x gains t * r x * (∑ y, c y) and the column of y gains t * (∑ x, r x) * c y, and both are zero.

theorem Matrix.exists_hasMarginals_abs_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [Nonempty ι] [Nonempty κ] {h : ι → ℝ} {k : κ → ℝ} (hhk : ∑ i : ι, h i = ∑ j : κ, k j) {δ : ℝ} (hh : ∀ (i : ι), |h i| ≤ δ) (hk : ∀ (j : κ), |k j| ≤ δ) : ∃ (D : Matrix ι κ ℝ), D.HasMarginals h k ∧ ∀ (i : ι) (j : κ), |D i j| ≤ 3 * δ

Row sums h and column sums k of the same total, with entries bounded by δ, are the marginals of a matrix with entries bounded by 3 * δ, independently of the sizes of ι and κ: the matrix h i / card κ + k j / card ι - (∑ i, h i) / (card ι * card κ).

This is how a perturbation of the marginals of a strictly positive plan is followed by a perturbation of the plan that stays nonnegative.

The minimiser has the largest support

theorem Matrix.convex_setOf_nonneg_hasMarginals {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : ι → ℝ) (b : κ → ℝ) : Convex ℝ {P : Matrix ι κ ℝ | (∀ (i : ι) (j : κ), 0 ≤ P i j) ∧ P.HasMarginals a b}

The nonnegative matrices with row sums a and column sums b form a convex set.

theorem Matrix.pos_of_isMinOn_relEntropy {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {K : Matrix ι κ ℝ} {C : Set (Matrix ι κ ℝ)} (hC : Convex ℝ C) {P Q : Matrix ι κ ℝ} (hP0 : ∀ (i : ι) (j : κ), 0 ≤ P i j) (hQ0 : ∀ (i : ι) (j : κ), 0 ≤ Q i j) (hPC : P ∈ C) (hmin : IsMinOn (fun (x : Matrix ι κ ℝ) => x.relEntropy K) C P) (hQC : Q ∈ C) {i : ι} {j : κ} (hQ : 0 < Q i j) : 0 < P i j

A minimiser P of the relative entropy against K over a convex set C of matrices has the largest support among the nonnegative members of C: if P and some Q ∈ C are nonnegative, then every entry at which Q is positive is a positive entry of P. There is no hypothesis on K.

theorem Matrix.pos_of_relEntropy_minOn {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K : Matrix ι κ ℝ) (a : ι → ℝ) (b : κ → ℝ) (ha : ∀ (i : ι), 0 < a i) (hb : ∀ (j : κ), 0 < b j) {P : Matrix ι κ ℝ} (hP : ∀ (i : ι) (j : κ), 0 ≤ P i j) (hPa : P.HasMarginals a b) (hmin : ∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → P.relEntropy K ≤ Q.relEntropy K) (i : ι) (j : κ) : 0 < P i j

A minimiser of the relative entropy against K among the nonnegative matrices with strictly positive row sums a and column sums b has no zero entry, for every matrix K: the product coupling a i * b j / ∑ k, a k is a strictly positive competitor, so this is the case of Matrix.pos_of_isMinOn_relEntropy for the convex set of these matrices.

theorem Matrix.pos_of_relEntropy_minOn_support {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {K : Matrix ι κ ℝ} {a : ι → ℝ} {b : κ → ℝ} {P Q : Matrix ι κ ℝ} (hP : ∀ (i : ι) (j : κ), 0 ≤ P i j) (hPa : P.HasMarginals a b) (hPK : ∀ (i : ι) (j : κ), K i j = 0 → P i j = 0) (hmin : ∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → (∀ (i : ι) (j : κ), K i j = 0 → Q i j = 0) → P.relEntropy K ≤ Q.relEntropy K) (hQ : ∀ (i : ι) (j : κ), 0 ≤ Q i j) (hQa : Q.HasMarginals a b) (hQK : ∀ (i : ι) (j : κ), K i j = 0 → Q i j = 0) {i : ι} {j : κ} (hQij : 0 < Q i j) : 0 < P i j

A minimiser of the relative entropy against K among the nonnegative matrices with row sums a and column sums b that vanish wherever K does is positive at every entry where some such matrix is positive.

theorem Matrix.HasMarginals.sum_sum_eq {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {Q : Matrix ι κ ℝ} {a : ι → ℝ} {b : κ → ℝ} (hQ : Q.HasMarginals a b) : ∑ i : ι, ∑ j : κ, Q i j = ∑ i : ι, a i

The total mass of a matrix with row sums a is ∑ i, a i.

theorem Matrix.HasMarginals.nonempty_of_col_sum_ne_zero {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {Q : Matrix ι κ ℝ} {a : ι → ℝ} {b : κ → ℝ} (hQ : Q.HasMarginals a b) {j : κ} (hj : b j ≠ 0) : Nonempty ι

A matrix with a nonzero column sum has a row.

theorem Matrix.HasMarginals.nonempty_of_row_sum_ne_zero {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {Q : Matrix ι κ ℝ} {a : ι → ℝ} {b : κ → ℝ} (hQ : Q.HasMarginals a b) {i : ι} (hi : a i ≠ 0) : Nonempty κ

A matrix with a nonzero row sum has a column.

Gibbs' inequality

theorem Matrix.sum_sum_sq_sqrt_sub_sqrt_le_relEntropy {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P Q : Matrix ι κ ℝ} (hQ : ∀ (i : ι) (j : κ), 0 ≤ Q i j) (hP : ∀ (i : ι) (j : κ), 0 < P i j) (hmass : ∑ i : ι, ∑ j : κ, Q i j = ∑ i : ι, ∑ j : κ, P i j) : ∑ i : ι, ∑ j : κ, (√(Q i j) - √(P i j)) ^ 2 ≤ Q.relEntropy P

Gibbs' inequality in its quantitative form: the relative entropy of a nonnegative matrix Q against a strictly positive matrix P of the same total mass dominates the squared Hellinger distance ∑ i, ∑ j, (√(Q i j) - √(P i j)) ^ 2.

theorem Matrix.relEntropy_nonneg_of_nonneg {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P Q : Matrix ι κ ℝ} (hQ : ∀ (i : ι) (j : κ), 0 ≤ Q i j) (hP : ∀ (i : ι) (j : κ), 0 ≤ P i j) (hQP : ∀ (i : ι) (j : κ), P i j = 0 → Q i j = 0) (hmass : ∑ i : ι, ∑ j : κ, Q i j = ∑ i : ι, ∑ j : κ, P i j) : 0 ≤ Q.relEntropy P

Gibbs' inequality against a reference with zero entries: the relative entropy of a nonnegative matrix Q against a nonnegative matrix P of the same total mass is nonnegative, provided Q vanishes wherever P does.

theorem Matrix.relEntropy_nonneg {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P Q : Matrix ι κ ℝ} (hQ : ∀ (i : ι) (j : κ), 0 ≤ Q i j) (hP : ∀ (i : ι) (j : κ), 0 < P i j) (hmass : ∑ i : ι, ∑ j : κ, Q i j = ∑ i : ι, ∑ j : κ, P i j) : 0 ≤ Q.relEntropy P

Gibbs' inequality: the relative entropy of a nonnegative matrix Q against a strictly positive matrix P of the same total mass is nonnegative.

theorem Matrix.relEntropy_eq_zero_iff {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P Q : Matrix ι κ ℝ} (hQ : ∀ (i : ι) (j : κ), 0 ≤ Q i j) (hP : ∀ (i : ι) (j : κ), 0 < P i j) (hmass : ∑ i : ι, ∑ j : κ, Q i j = ∑ i : ι, ∑ j : κ, P i j) : Q.relEntropy P = 0 ↔ Q = P

The equality case of Gibbs' inequality: the relative entropy of a nonnegative matrix Q against a strictly positive matrix P of the same total mass vanishes exactly when Q = P.

The first-order condition at a minimiser

theorem Matrix.hasDerivAt_relEntropy_add_smul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K P D : Matrix ι κ ℝ) (hDP : ∀ (i : ι) (j : κ), P i j = 0 → D i j = 0) : HasDerivAt (fun (t : ℝ) => (P + t • D).relEntropy K) (∑ i : ι, ∑ j : κ, D i j * (Real.log (P i j) + 1 - Real.log (K i j))) 0

The relative entropy against K of the matrix P + t • D has derivative ∑ i, ∑ j, D i j * (log (P i j) + 1 - log (K i j)) in t at t = 0, as soon as D vanishes wherever P does.

theorem Matrix.sum_sum_mul_log_sub_log_eq_zero_of_relEntropy_minOn_support {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K : Matrix ι κ ℝ) {a : ι → ℝ} {b : κ → ℝ} {P D : Matrix ι κ ℝ} (hP : ∀ (i : ι) (j : κ), 0 ≤ P i j) (hPa : P.HasMarginals a b) (hmin : ∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → (∀ (i : ι) (j : κ), P i j = 0 → Q i j = 0) → P.relEntropy K ≤ Q.relEntropy K) (hD : D.HasMarginals 0 0) (hDP : ∀ (i : ι) (j : κ), P i j = 0 → D i j = 0) : ∑ i : ι, ∑ j : κ, D i j * (Real.log (P i j) - Real.log (K i j)) = 0

The first-order condition at a minimiser on its own support: if P minimises the relative entropy against K among the nonnegative matrices with row sums a and column sums b that vanish wherever P does, then the matrix log (P i j) - log (K i j) is orthogonal to every direction D whose row and column sums vanish and which vanishes wherever P does.

theorem Matrix.sum_sum_mul_log_sub_log_eq_zero_of_relEntropy_minOn {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K : Matrix ι κ ℝ) {a : ι → ℝ} {b : κ → ℝ} {P D : Matrix ι κ ℝ} (hP : ∀ (i : ι) (j : κ), 0 < P i j) (hPa : P.HasMarginals a b) (hmin : ∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → P.relEntropy K ≤ Q.relEntropy K) (hD : D.HasMarginals 0 0) : ∑ i : ι, ∑ j : κ, D i j * (Real.log (P i j) - Real.log (K i j)) = 0

The first-order condition at a minimiser with positive entries: if P minimises the relative entropy against K among the nonnegative matrices with row sums a and column sums b, and every entry of P is positive, then the matrix log (P i j) - log (K i j) is orthogonal to every direction D whose row and column sums vanish.

Matrices orthogonal to the zero-marginal directions on a support

theorem Matrix.exists_forall_mem_eq_add_iff {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (H : Matrix ι κ ℝ) (s : Set (ι × κ)) : (∃ (f : ι → ℝ) (g : κ → ℝ), ∀ (i : ι) (j : κ), (i, j) ∈ s → H i j = f i + g j) ↔ ∀ (D : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), (i, j) ∉ s → D i j = 0) → D.HasMarginals 0 0 → ∑ i : ι, ∑ j : κ, D i j * H i j = 0

On a set s of cells, a matrix H is the sum f i + g j of a function of the row and a function of the column exactly when ∑ i, ∑ j, D i j * H i j = 0 for every matrix D that vanishes off s and has zero row and column sums.

The minimiser is a diagonal scaling

theorem Matrix.exists_isDiagonalScaling_of_relEntropy_minOn_support {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {K : Matrix ι κ ℝ} (hK : ∀ (i : ι) (j : κ), 0 ≤ K i j) {a : ι → ℝ} {b : κ → ℝ} {P Q : Matrix ι κ ℝ} (hP : ∀ (i : ι) (j : κ), 0 ≤ P i j) (hPa : P.HasMarginals a b) (hPK : ∀ (i : ι) (j : κ), K i j = 0 → P i j = 0) (hmin : ∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → (∀ (i : ι) (j : κ), K i j = 0 → Q i j = 0) → P.relEntropy K ≤ Q.relEntropy K) (hQ : ∀ (i : ι) (j : κ), 0 ≤ Q i j) (hQa : Q.HasMarginals a b) (hQK : ∀ (i : ι) (j : κ), Q i j = 0 ↔ K i j = 0) : ∃ (u : ι → ℝ) (v : κ → ℝ), (∀ (i : ι), 0 < u i) ∧ (∀ (j : κ), 0 < v j) ∧ P.IsDiagonalScaling K u v

If some nonnegative matrix with row sums a and column sums b has the zero pattern of the nonnegative kernel K, then every minimiser of the relative entropy against K among the nonnegative matrices with these row and column sums that vanish wherever K does is a diagonal scaling of K by strictly positive row and column factors.

theorem Matrix.exists_isDiagonalScaling_of_relEntropy_minOn {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {K : Matrix ι κ ℝ} (hK : ∀ (i : ι) (j : κ), 0 < K i j) {a : ι → ℝ} {b : κ → ℝ} (ha : ∀ (i : ι), 0 < a i) (hb : ∀ (j : κ), 0 < b j) {P : Matrix ι κ ℝ} (hP : ∀ (i : ι) (j : κ), 0 ≤ P i j) (hPa : P.HasMarginals a b) (hmin : ∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → P.relEntropy K ≤ Q.relEntropy K) : ∃ (u : ι → ℝ) (v : κ → ℝ), (∀ (i : ι), 0 < u i) ∧ (∀ (j : κ), 0 < v j) ∧ P.IsDiagonalScaling K u v

For a strictly positive kernel K and strictly positive marginals a and b, every minimiser P of the relative entropy against K among the nonnegative matrices with row sums a and column sums b is a diagonal scaling of K by strictly positive row and column factors.

This is the case of Matrix.exists_isDiagonalScaling_of_relEntropy_minOn_support in which K has no zero entry: P itself has no zero entry by Matrix.pos_of_relEntropy_minOn.

theorem Matrix.exists_sinkhorn_scaling {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {K : Matrix ι κ ℝ} (hK : ∀ (i : ι) (j : κ), 0 < K i j) {a : ι → ℝ} {b : κ → ℝ} (ha : ∀ (i : ι), 0 < a i) (hb : ∀ (j : κ), 0 < b j) (hmass : ∑ i : ι, a i = ∑ j : κ, b j) : ∃ (u : ι → ℝ) (v : κ → ℝ), (∀ (i : ι), 0 < u i) ∧ (∀ (j : κ), 0 < v j) ∧ (∀ (i : ι), ∑ j : κ, u i * K i j * v j = a i) ∧ ∀ (j : κ), ∑ i : ι, u i * K i j * v j = b j

The Sinkhorn–Knopp theorem for a strictly positive kernel: a strictly positive matrix K and strictly positive row sums a and column sums b of equal total mass admit strictly positive row factors u and column factors v such that the diagonal scaling u i * K i j * v j has row sums a and column sums b.

The scaled matrix is the minimiser of the relative entropy against K with these marginals.

theorem Matrix.IsDiagonalScaling.relEntropy_eq_relEntropy_add_sum_sum_mul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {R K : Matrix ι κ ℝ} {u : ι → ℝ} {v : κ → ℝ} (h : R.IsDiagonalScaling K u v) (hK : ∀ (i : ι) (j : κ), K i j ≠ 0) (hu : ∀ (i : ι), u i ≠ 0) (hv : ∀ (j : κ), v j ≠ 0) (Q : Matrix ι κ ℝ) : Q.relEntropy K = Q.relEntropy R + ∑ i : ι, ∑ j : κ, Q i j * (Real.log (u i) + Real.log (v j))

Against a diagonal scaling R of K whose kernel and factors have no zero entries, the relative entropy of every matrix Q against K is its relative entropy against R plus its sum against the potentials log (u i) + log (v j).

theorem Matrix.IsDiagonalScaling.relEntropy_eq_relEntropy_add {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P K : Matrix ι κ ℝ} {u : ι → ℝ} {v : κ → ℝ} (h : P.IsDiagonalScaling K u v) (hK : ∀ (i : ι) (j : κ), K i j ≠ 0) (hu : ∀ (i : ι), u i ≠ 0) (hv : ∀ (j : κ), v j ≠ 0) {a : ι → ℝ} {b : κ → ℝ} (hP : P.HasMarginals a b) {Q : Matrix ι κ ℝ} (hQ : Q.HasMarginals a b) : Q.relEntropy K = Q.relEntropy P + P.relEntropy K

The Pythagorean identity of the relative entropy at a diagonal scaling: if K and the scaling factors have no zero entries, then for every matrix Q with the row and column sums of P, relEntropy Q K = relEntropy Q P + relEntropy P K.

theorem Matrix.IsDiagonalScaling.relEntropy_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P K : Matrix ι κ ℝ} {u : ι → ℝ} {v : κ → ℝ} (h : P.IsDiagonalScaling K u v) (hK : ∀ (i : ι) (j : κ), 0 < K i j) (hu : ∀ (i : ι), 0 < u i) (hv : ∀ (j : κ), 0 < v j) {a : ι → ℝ} {b : κ → ℝ} (hP : P.HasMarginals a b) {Q : Matrix ι κ ℝ} (hQ0 : ∀ (i : ι) (j : κ), 0 ≤ Q i j) (hQ : Q.HasMarginals a b) : P.relEntropy K ≤ Q.relEntropy K

A diagonal scaling of a strictly positive K by strictly positive factors minimises the relative entropy against K among the nonnegative matrices with its row and column sums.

Duality

noncomputable def Matrix.relEntropyDual {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K : Matrix ι κ ℝ) (a : ι → ℝ) (b : κ → ℝ) (f : ι → ℝ) (g : κ → ℝ) : ℝ

The dual objective of the minimisation of Matrix.relEntropy · K over the nonnegative matrices with row sums a and column sums b, at the row potentials f and the column potentials g: ∑ i, a i * f i + ∑ j, b j * g j + ∑ i, a i - ∑ i, ∑ j, exp (f i) * K i j * exp (g j).

This is the Lagrangian dual of the minimisation, with the potentials shifted by one so that the optimal potentials of a diagonal scaling u i * K i j * v j are log u and log v. It is at most every primal value (Matrix.relEntropyDual_le_relEntropy), with equality at the minimiser (Matrix.IsDiagonalScaling.relEntropyDual_eq_relEntropy).

theorem Matrix.relEntropyDual_def {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K : Matrix ι κ ℝ) (a : ι → ℝ) (b : κ → ℝ) (f : ι → ℝ) (g : κ → ℝ) : K.relEntropyDual a b f g = ∑ i : ι, a i * f i + ∑ j : κ, b j * g j + ∑ i : ι, a i - ∑ i : ι, ∑ j : κ, Real.exp (f i) * K i j * Real.exp (g j)

The defining formula of the dual objective.

theorem Matrix.IsDiagonalScaling.relEntropy_sub_relEntropyDual {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {R K : Matrix ι κ ℝ} {u : ι → ℝ} {v : κ → ℝ} (hR : R.IsDiagonalScaling K u v) (hK : ∀ (i : ι) (j : κ), K i j ≠ 0) (hu : ∀ (i : ι), 0 < u i) (hv : ∀ (j : κ), 0 < v j) {a : ι → ℝ} {b : κ → ℝ} {Q : Matrix ι κ ℝ} (hQ : Q.HasMarginals a b) : (Q.relEntropy K - K.relEntropyDual a b (fun (i : ι) => Real.log (u i)) fun (j : κ) => Real.log (v j)) = Q.relEntropy R + ∑ i : ι, ∑ j : κ, R i j - ∑ i : ι, a i

The duality gap at a diagonal scaling: if R is the diagonal scaling of a kernel K with no zero entries by strictly positive factors u and v, then for every Q with row sums a and column sums b, the gap between relEntropy Q K and the dual objective at the potentials log u and log v is relEntropy Q R plus the excess ∑ i, ∑ j, R i j - ∑ i, a i of the mass of R over that of Q.

theorem Matrix.relEntropyDual_le_relEntropy {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {K : Matrix ι κ ℝ} (hK : ∀ (i : ι) (j : κ), 0 < K i j) {a : ι → ℝ} {b : κ → ℝ} {Q : Matrix ι κ ℝ} (hQ0 : ∀ (i : ι) (j : κ), 0 ≤ Q i j) (hQ : Q.HasMarginals a b) (f : ι → ℝ) (g : κ → ℝ) : K.relEntropyDual a b f g ≤ Q.relEntropy K

Weak duality for the entropy minimisation: against a strictly positive K, the dual objective at any potentials f and g is at most the relative entropy of every nonnegative Q with row sums a and column sums b.

theorem Matrix.IsDiagonalScaling.relEntropyDual_eq_relEntropy {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P K : Matrix ι κ ℝ} {u : ι → ℝ} {v : κ → ℝ} (hP : P.IsDiagonalScaling K u v) (hu : ∀ (i : ι), 0 < u i) (hv : ∀ (j : κ), 0 < v j) {a : ι → ℝ} {b : κ → ℝ} (hPm : P.HasMarginals a b) : (K.relEntropyDual a b (fun (i : ι) => Real.log (u i)) fun (j : κ) => Real.log (v j)) = P.relEntropy K

Strong duality for the entropy minimisation: if P is the diagonal scaling of a kernel K by strictly positive factors u and v, with row sums a and column sums b, the dual objective at the potentials log u and log v is relEntropy P K. No entry of K need be nonzero: P vanishes where K does. With Matrix.relEntropyDual_le_relEntropy, for a strictly positive K these potentials maximise the dual objective, and its maximum is the minimum of the relative entropy.

theorem Matrix.relEntropy_minOn_iff_exists_isDiagonalScaling {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {K : Matrix ι κ ℝ} (hK : ∀ (i : ι) (j : κ), 0 < K i j) {a : ι → ℝ} {b : κ → ℝ} (ha : ∀ (i : ι), 0 < a i) (hb : ∀ (j : κ), 0 < b j) {P : Matrix ι κ ℝ} (hP : ∀ (i : ι) (j : κ), 0 ≤ P i j) (hPa : P.HasMarginals a b) : (∀ (Q : Matrix ι κ ℝ), (∀ (i : ι) (j : κ), 0 ≤ Q i j) → Q.HasMarginals a b → P.relEntropy K ≤ Q.relEntropy K) ↔ ∃ (u : ι → ℝ) (v : κ → ℝ), (∀ (i : ι), 0 < u i) ∧ (∀ (j : κ), 0 < v j) ∧ P.IsDiagonalScaling K u v

For a strictly positive kernel K and strictly positive marginals a and b, a nonnegative matrix with row sums a and column sums b minimises the relative entropy against K among all such matrices exactly when it is a diagonal scaling of K by strictly positive factors.

theorem Matrix.IsDiagonalScaling.eq_of_hasMarginals {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {P P' K : Matrix ι κ ℝ} {u u' : ι → ℝ} {v v' : κ → ℝ} (h : P.IsDiagonalScaling K u v) (h' : P'.IsDiagonalScaling K u' v') (hK : ∀ (i : ι) (j : κ), 0 < K i j) (hu : ∀ (i : ι), 0 < u i) (hv : ∀ (j : κ), 0 < v j) (hu' : ∀ (i : ι), 0 < u' i) (hv' : ∀ (j : κ), 0 < v' j) {a : ι → ℝ} {b : κ → ℝ} (hP : P.HasMarginals a b) (hP' : P'.HasMarginals a b) : P = P'

Two diagonal scalings of a strictly positive K by strictly positive factors that have the same row and column sums are equal: the scaled matrix of the Sinkhorn–Knopp theorem is unique.

theorem Matrix.IsDiagonalScaling.exists_eq_rescale_factors {ι : Type u_1} {κ : Type u_2} [Nonempty ι] [Nonempty κ] {P K : Matrix ι κ ℝ} {u u' : ι → ℝ} {v v' : κ → ℝ} (h : P.IsDiagonalScaling K u v) (h' : P.IsDiagonalScaling K u' v') (hK : ∀ (i : ι) (j : κ), K i j ≠ 0) (hu' : ∀ (i : ι), u' i ≠ 0) (hv' : ∀ (j : κ), v' j ≠ 0) : ∃ (r : ℝ), r ≠ 0 ∧ (∀ (i : ι), u i = r * u' i) ∧ ∀ (j : κ), v j = r⁻¹ * v' j

Up to a common scalar, the factors of a diagonal scaling of a kernel with no zero entry are unique: if P is the diagonal scaling of K both by u, v and by u', v', with nonzero u' and v', then u = r * u' and v = r⁻¹ * v' for a nonzero scalar r. This is the converse of Matrix.IsDiagonalScaling.rescale_factors.

Comparison of diagonal scalings with the same row sums

theorem Matrix.IsDiagonalScaling.apply_le_exp_hilbertProjectiveDist_mul {ι : Type u_1} {κ : Type u_2} [Fintype κ] {P Q K : Matrix ι κ ℝ} {u u' : ι → ℝ} {v v' : κ → ℝ} (hP : P.IsDiagonalScaling K u v) (hQ : Q.IsDiagonalScaling K u' v') {i : ι} (hK : ∀ (j : κ), 0 < K i j) (hu : 0 ≤ u i) (hv : ∀ (j : κ), 0 < v j) (hv' : ∀ (j : κ), 0 < v' j) (hrow : ∑ j : κ, P i j = ∑ j : κ, Q i j) (j : κ) : P i j ≤ Real.exp (TauCeti.hilbertProjectiveDist v v') * Q i j

Two diagonal scalings whose kernel is strictly positive in row i, with the same i-th row sum, agree on that row up to the factor exp d, where d is the Hilbert projective distance between their column factors: if P is the diagonal scaling of K by u and v > 0, with u i ≥ 0, and Q that by u' and v' > 0, then P i j ≤ exp (hilbertProjectiveDist v v') * Q i j.