Commit 2025-03-30 03:51 e45f6a28

View on Github →

feat(CStarAlgebra): define positive maps and show their continuity (#23210) This PR defines positive maps and shows that a positive map between non-unital C*-algebras is continuous.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

added theorem LinearMapClass.map_smul_of_tower

Created Mathlib/Algebra/Order/Module/PositiveLinearMap.lean

added theorem PositiveLinearMap.map_smul_of_tower

added def PositiveLinearMap.mk₀

added structure PositiveLinearMap

added def PositiveLinearMapClass.toPositiveLinearMap

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

added theorem selfAdjoint.isSelfAdjoint

Created Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean

added theorem PositiveLinearMap.apply_le_of_isSelfAdjoint

added theorem PositiveLinearMap.exists_norm_apply_le

added theorem PositiveLinearMap.norm_apply_le_of_nonneg

added theorem map_isSelfAdjoint

Modified Mathlib/Analysis/CStarAlgebra/SpecialFunctions/PosPart.lean

added theorem CStarAlgebra.exists_sum_four_nonneg

Modified Mathlib/Analysis/Complex/Basic.lean

added theorem imaginaryPart.norm_le

added theorem realPart.norm_le

Modified Mathlib/Data/Complex/Basic.lean

added theorem Complex.I_pow_eq_pow_mod

added theorem Complex.I_pow_three