Commit 2024-12-03 14:07 b7fbbb51

View on Github →

feat(LinearAlgebra/RootSystem/Finite): Coxeter weights are bounded above by 4 (#19343) This PR adds a version of the Cauchy-Schwarz inequality for positive semidefinite bilinear forms on modules over linearly ordered commutative rings, and applies it to restrict Coxeter weights for root systems.

Estimated changes

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

added theorem RootPairing.coxeterWeight_ne_four_of_linearIndependent

added theorem RootPairing.infinite_of_linearIndependent_coxeterWeight_four

deleted theorem RootPairing.infinite_of_linearly_independent_coxeterWeight_four

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.exists_int_eq_coxeterWeight

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

added theorem RootPairing.coxeterWeight_le_four

added theorem RootPairing.coxeterWeight_mem_set_of_isCrystallographic

added theorem RootPairing.four_smul_rootForm_sq_eq_coxeterWeight_smul

added theorem RootPairing.toPerfectPairing_apply_CoPolarization

added theorem RootPairing.toPerfectPairing_apply_apply_Polarization

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

deleted theorem RootPairing.rootForm_rootPositive

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

added theorem LinearMap.BilinForm.apply_mul_apply_le_of_forall_zero_le

added theorem LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent

added theorem LinearMap.BilinForm.apply_smul_sub_smul_sub_eq

added theorem LinearMap.BilinForm.apply_sq_le_of_symm

added theorem LinearMap.BilinForm.apply_sq_lt_iff_linearIndependent_of_symm

added theorem LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq