Commit 2024-10-08 02:27 2e8a2b23

View on Github →

feat(Analysis/Convex): Birkhoff's theorem and doubly stochastic matrices (#16278)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Birkhoff.lean

added theorem doublyStochastic_eq_convexHull_permMatrix

added theorem exists_eq_sum_perm_of_mem_doublyStochastic

Created Mathlib/Data/Matrix/DoublyStochastic.lean

added theorem convex_doublyStochastic

added def doublyStochastic

added theorem exists_mem_doublyStochastic_eq_smul_iff

added theorem le_one_of_mem_doublyStochastic

added theorem mem_doublyStochastic

added theorem mem_doublyStochastic_iff_sum

added theorem mulVec_one_of_mem_doublyStochastic

added theorem nonneg_of_mem_doublyStochastic

added theorem one_vecMul_of_mem_doublyStochastic

added theorem permMatrix_mem_doublyStochastic

added theorem sum_col_of_mem_doublyStochastic

added theorem sum_row_of_mem_doublyStochastic