Matrix scaling to doubly stochastic form

TheoremCsima–Datta: sufficiency of total support#✓fully proved

A symmetric nonnegative matrix with total support has a positive vector d with diag(d) A diag(d) doubly stochastic.

theorem exists_symmetric_balancing_of_hasTotalSupport {A : Matrix (Fin n) (Fin n) ℝ}
    (hsymm : A.IsSymm) (hA : ∀ i j, 0 ≤ A i j) (hts : HasTotalSupport A) :
    ∃ d : Fin n → ℝ, (∀ i, 0 < d i) ∧
      (fun i j => d i * A i j * d j) ∈ doublyStochastic ℝ (Fin n)

Sources

• Csima & Datta (1972); Sinkhorn & Knopp (1967).

Uses 1 · Used by 1

Statement usesTotal support of a square matrix

Used byCsima–Datta theorem

TheoremCsima–Datta theorem#✓fully proved

For 0 < n, a symmetric nonnegative matrix has a positive vector d with diag(d) A diag(d) doubly stochastic if and only if it has total support.

theorem exists_symmetric_balancing_iff_hasTotalSupport (hn : 0 < n)
    {A : Matrix (Fin n) (Fin n) ℝ} (hsymm : A.IsSymm) (hA : ∀ i j, 0 ≤ A i j) :
    (∃ d : Fin n → ℝ, (∀ i, 0 < d i) ∧
      (fun i j => d i * A i j * d j) ∈ doublyStochastic ℝ (Fin n)) ↔ HasTotalSupport A

Uses 3

Statement usesTotal support of a square matrix

Proof usesCsima–Datta: sufficiency of total support · Necessity of total support

TheoremSinkhorn's scaling theorem#✓fully proved

Let \(n \ge 1\) and let \(A\) be a real \(n \times n\) matrix all of whose entries are strictly positive. Then there are vectors \(r, c \in \mathbb{R}^n\) with strictly positive entries such that the matrix with entries \(r_i A_{ij} c_j\) is doubly stochastic, that is, its entries are nonnegative and each of its rows and each of its columns sums to \(1\).

theorem sinkhorn_scaling {n : ℕ} (hn : 0 < n)
    (A : Matrix (Fin n) (Fin n) ℝ)
    (hA : ∀ i j, 0 < A i j) :
    ∃ (r c : Fin n → ℝ), (∀ i, 0 < r i) ∧ (∀ j, 0 < c j) ∧
      (fun i j => r i * A i j * c j) ∈ doublyStochastic ℝ (Fin n)

Sources

• R. Sinkhorn, Ann. Math. Statist. 35 (1964), 876-879, DOI 10.1214/aoms/1177703591.

Used by 1

Used bySymmetric matrix balancing

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.