English
The extreme points of the set of doubly stochastic matrices are exactly the permutation matrices.
Русский
Экстремальные точки множества двойственно стохастических матриц совпадают с перестановочными матрицами.
LaTeX
$$$\operatorname{extremePoints}_R\big(\text{doublyStochastic } R n\big) = \{\sigma.\text{permMatrix } R \mid \sigma : \operatorname{Perm}(n)\}$$$
Lean4
/-- The set of extreme points of the doubly stochastic matrices is the set of permutation matrices.
-/
theorem extremePoints_doublyStochastic :
Set.extremePoints R (doublyStochastic R n) = {σ.permMatrix R | σ : Equiv.Perm n} :=
by
refine subset_antisymm ?_ ?_
· rw [doublyStochastic_eq_convexHull_permMatrix]
exact extremePoints_convexHull_subset
rintro _ ⟨σ, rfl⟩
refine ⟨permMatrix_mem_doublyStochastic, fun x₁ hx₁ x₂ hx₂ hσ ↦ ?_⟩
suffices ∀ i j : n, x₁ i j = x₂ i j
by
obtain rfl : x₁ = x₂ := by simpa [← Matrix.ext_iff]
simp_all
intro i j
have h₁ : σ.permMatrix R i j ∈ openSegment R (x₁ i j) (x₂ i j) :=
image_openSegment _ (entryLinearMap R R i j).toAffineMap x₁ x₂ ▸ ⟨_, hσ, rfl⟩
by_contra! h
have h₂ : openSegment R (x₁ i j) (x₂ i j) ⊆ Set.Ioo 0 1 :=
by
rw [openSegment_eq_Ioo' h]
apply Set.Ioo_subset_Ioo <;> simp_all [nonneg_of_mem_doublyStochastic, le_one_of_mem_doublyStochastic]
specialize h₂ h₁
aesop
