English
Let M be a matrix and s ≥ 0. There exists M' ∈ DS with M = s M' if and only if all entries of M are nonnegative and all row sums and column sums equal s.
Русский
Пусть M — матрица и s ≥ 0. Существует M' ∈ DS such that M = s M' тогда и только если все элементы M неотрицательны, и суммы по строкам и по столбцам равны s.
LaTeX
$$0 ≤ s ⇒ (∃ M' ∈ \mathrm{doublyStochastic}(R,n) , M = s \cdot M') ↔ (∀ i,j, M_{ij} ≥ 0) ∧ (∀ i, ∑_j M_{ij} = s) ∧ (∀ j, ∑_i M_{ij} = s)$$
Lean4
/-- A matrix is `s` times a doubly stochastic matrix iff all entries are nonnegative, and all row and
column sums are equal to `s`.
This lemma is useful for the proof of Birkhoff's theorem - in particular because it allows scaling
by nonnegative factors rather than positive ones only.
-/
theorem exists_mem_doublyStochastic_eq_smul_iff {M : Matrix n n R} {s : R} (hs : 0 ≤ s) :
(∃ M' ∈ doublyStochastic R n, M = s • M') ↔ (∀ i j, 0 ≤ M i j) ∧ (∀ i, ∑ j, M i j = s) ∧ (∀ j, ∑ i, M i j = s) := by
classical
constructor
case mp =>
rintro ⟨M', hM', rfl⟩
rw [mem_doublyStochastic_iff_sum] at hM'
simp only [smul_apply, smul_eq_mul, ← mul_sum]
exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
rcases eq_or_lt_of_le hs with rfl | hs
case inl =>
simp only [zero_smul, exists_and_right, and_imp]
intro h₁ h₂ _
refine ⟨⟨1, Submonoid.one_mem _⟩, ?_⟩
ext i j
specialize h₂ i
rw [sum_eq_zero_iff_of_nonneg (by simp [h₁ i])] at h₂
exact h₂ _ (by simp)
rintro ⟨hM₁, hM₂, hM₃⟩
exact ⟨s⁻¹ • M, by simp [mem_doublyStochastic_iff_sum, ← mul_sum, hs.ne', *]⟩
