l2_opNorm_le_one_of_mem_doublyStochastic

English

If M is a doubly stochastic matrix, then its L2 operator norm is at most 1.

Русский

Если матрица M двойственно стохастическая, то её норма оператора по L2 не превосходит 1.

LaTeX

$$$M \in \text{doublyStochastic } R n \;\Rightarrow\; \|M\|_{2} \le 1$$$

Lean4

theorem l2_opNorm_le_one_of_mem_doublyStochastic {M : Matrix n n ℝ} (hM : M ∈ doublyStochastic ℝ n) : ‖M‖ ≤ 1 :=
  by
  rw [← SetLike.mem_coe, doublyStochastic_eq_convexHull_permMatrix] at hM
  have ⟨_, ⟨σ, rfl⟩, hσ⟩ := convexOn_univ_norm.exists_ge_of_mem_convexHull (by simp) hM
  exact hσ.trans (permMatrix_l2_opNorm_le _)

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