English
A square matrix is doubly stochastic if all entries are nonnegative and both left and right multiplication by the all-ones vector yield the all-ones vector.
Русский
Квадратная матрица является двойственно стохастической, если все ее элементы неотрицательны и левая и правая умножения на вектор единиц дают вектор единиц.
LaTeX
$$$M\in M_{n\times n}(R)$ is doubly stochastic iff (∀ i,j, M_{ij} \ge 0) ∧ (M \mathbf{1} = \mathbf{1}) ∧ (\mathbf{1}^T M = \mathbf{1}^T),$$$
Lean4
/-- A square matrix is doubly stochastic iff all entries are nonnegative, and left or right
multiplication by the vector of all 1s gives the vector of all 1s.
-/
def doublyStochastic (R n : Type*) [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R] [IsOrderedRing R] :
Submonoid (Matrix n n R)
where
carrier := {M | (∀ i j, 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1}
mul_mem' {M N} hM
hN := by
refine ⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_, ?_⟩
next => rw [← mulVec_mulVec, hN.2.1, hM.2.1]
next => rw [← vecMul_vecMul, hM.2.2, hN.2.2]
one_mem' := by simp [zero_le_one_elem]
