Facts about CFC.posPart and CFC.negPart involving norms

This file collects various facts about the positive and negative parts of elements of a C⋆-algebra that involve the norm.

Main results

• CFC.norm_eq_max_norm_posPart_negPart: states that ‖a‖ = max ‖a⁺‖ ‖a⁻‖
• CFC.norm_posPart_le and CFC.norm_negPart_le: state that ‖a⁺‖ ≤ ‖a‖ and ‖a⁻‖ ≤ ‖a‖ respectively.

@[simp]

theorem CStarAlgebra.norm_posPart_le {A : Type u_1} [NonUnitalNormedRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) : ‖a⁺‖ ≤ ‖a‖

@[simp]

theorem CStarAlgebra.norm_negPart_le {A : Type u_1} [NonUnitalNormedRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) : ‖a⁻‖ ≤ ‖a‖

theorem IsSelfAdjoint.norm_eq_max_norm_posPart_negPart {A : Type u_1} [NonUnitalNormedRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) : ‖a‖ = ‖a⁺‖ ⊔ ‖a⁻‖