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.

For a strictly positive K the minimiser is a diagonal scaling P i j = u i * K i j * v j of K by strictly positive factors. At a minimiser with positive entries the relative entropy is differentiable along every direction that preserves the marginals, and its derivative vanishes there; testing against the rectangle directions splits log (P i j) - log (K i j) into a function of the row plus a function of the column. 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.

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; strict positivity of K is needed only to identify the minimiser with a diagonal scaling of K. A kernel with zero entries constrains the support of a scaling and is not treated here.

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

Main results

• 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.pos_of_relEntropy_minOn: every such minimiser has strictly positive entries.
• 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.hasDerivAt_relEntropy_add_smul 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 positive minimiser.
• 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: the Pythagorean identity of the relative entropy at a diagonal 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.

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

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.

Equations

• P.HasMarginals a b = ((∀ (i : ι), ∑ j : κ, P i j = a i) ∧ ∀ (j : κ), ∑ i : ι, P i j = b j)

@[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

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.

Equations

• P.IsDiagonalScaling K u v = ∀ (i : ι) (j : κ), P i j = u i * K i j * v 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.

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.

Equations

• P.relEntropy K = ∑ i : ι, ∑ j : κ, (P i j * Real.log (P i j) - P i j * Real.log (K i j))

@[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.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.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 closed, every entry of such a matrix is at most ∑ i, a i, and the relative entropy is continuous, so the minimum is attained on a closed subset of a compact box.

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.

Rectangle perturbations

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.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 has no zero entry, for every matrix K: moving a sufficiently small positive amount of mass into a zero entry, taken from one entry of the same row and one entry of the same column, preserves the marginals and decreases the relative entropy.

There is no hypothesis on K: the argument below bounds the kernel contribution t * L, with L = log (K i j) - log (K i j') - log (K i' j) + log (K i' j'), by an arbitrary constant.

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.

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 {ι : 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 positive minimiser

theorem Matrix.hasDerivAt_relEntropy_add_smul {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (K P D : Matrix ι κ ℝ) (hP : ∀ (i : ι) (j : κ), P 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 no entry of P vanishes.

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.

The minimiser is a diagonal scaling

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.

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 {ι : 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.

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.