mem_doublyStochastic_iff_sum — Mathlib

English

A matrix M is doubly stochastic iff it satisfies nonnegativity and both row and column sums equal 1, expressed via sums over indices.

Русский

Матрица M двойственно стохастична тогда и только тогда, когда выполняются неотрицательность и суммы по строкам и по столбцам равны 1, выраженные через суммы индексов.

LaTeX

$$$M\in doublyStochastic(R,n)\iff (\forall i,j, 0 \le M_{ij}) \land (\forall i, \sum_j M_{ij}=1) \land (\forall j, \sum_i M_{ij}=1).$$$

Lean4

theorem mem_doublyStochastic_iff_sum :
    M ∈ doublyStochastic R n ↔ (∀ i j, 0 ≤ M i j) ∧ (∀ i, ∑ j, M i j = 1) ∧ ∀ j, ∑ i, M i j = 1 := by
  simp [funext_iff, doublyStochastic, mulVec, vecMul, dotProduct]

Похожие утверждения