convex_doublyStochastic — Mathlib

English

The set of doubly stochastic matrices is convex: if X and Y are in DS and α ∈ [0,1], then αX + (1−α)Y ∈ DS.

Русский

Множество двоустойчивых матриц выпукло: если X и Y ∈ DS и α ∈ [0,1], то αX + (1−α)Y ∈ DS.

LaTeX

$$$X,Y \in \mathrm{doublyStochastic}(R,n) \land \alpha \in [0,1] \Rightarrow \alpha X + (1-\alpha)Y \in \mathrm{doublyStochastic}(R,n)$$$

Lean4

/-- The set of doubly stochastic matrices is convex. -/
theorem convex_doublyStochastic : Convex R (doublyStochastic R n : Set (Matrix n n R)) :=
  by
  intro x hx y hy a b ha hb h
  simp only [SetLike.mem_coe, mem_doublyStochastic_iff_sum] at hx hy ⊢
  simp [add_nonneg, ha, hb, mul_nonneg, hx, hy, sum_add_distrib, ← mul_sum, h]

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