Properties of rpow and sqrt over an algebra with an isometric CFC

This file collects results about CFC.rpow, CFC.nnrpow and CFC.sqrt that use facts that rely on an isometric continuous functional calculus.

Main theorems

• Various versions of ‖a ^ r‖ = ‖a‖ ^ r and ‖CFC.sqrt a‖ = sqrt ‖a‖.

Tags

continuous functional calculus, rpow, sqrt

theorem CFC.nnnorm_nnrpow {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) {r : NNReal} (hr : 0 < r) (ha : 0 ≤ a := by cfc_tac) : ‖a ^ r‖₊ = ‖a‖₊ ^ ↑r

theorem CFC.norm_nnrpow {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) {r : NNReal} (hr : 0 < r) (ha : 0 ≤ a := by cfc_tac) : ‖a ^ r‖ = ‖a‖ ^ ↑r

theorem CFC.nnnorm_sqrt {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : 0 ≤ a := by cfc_tac) : ‖sqrt a‖₊ = NNReal.sqrt ‖a‖₊

theorem CFC.norm_sqrt {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : 0 ≤ a := by cfc_tac) : ‖sqrt a‖ = √‖a‖

theorem CFC.continuousOn_sqrt {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [CompleteSpace A] : ContinuousOn sqrt {a : A | 0 ≤ a}

theorem CFC.continuousOn_nnrpow {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [CompleteSpace A] (r : NNReal) : ContinuousOn (fun (x : A) => x ^ r) {a : A | 0 ≤ a}

theorem CFC.nnnorm_rpow {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) {r : ℝ} (hr : 0 < r) (ha : 0 ≤ a := by cfc_tac) : ‖a ^ r‖₊ = ‖a‖₊ ^ r

theorem CFC.norm_rpow {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) {r : ℝ} (hr : 0 < r) (ha : 0 ≤ a := by cfc_tac) : ‖a ^ r‖ = ‖a‖ ^ r

theorem CFC.continuousOn_rpow {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [CompleteSpace A] (r : ℝ) : ContinuousOn (fun (x : A) => x ^ r) {a : A | IsStrictlyPositive a}

theorem CFC.norm_star_mul_mul_self_of_nonneg {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} (b : A) (ha : 0 ≤ a := by cfc_tac) : ‖star b * a * b‖ = ‖sqrt a * b‖ ^ 2

theorem CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} (b : A) (hb : IsSelfAdjoint b := by cfc_tac) (ha : 0 ≤ a := by cfc_tac) : ‖b * a * b‖ = ‖sqrt a * b‖ ^ 2

theorem CFC.norm_mul_mul_star_self_of_nonneg {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} (b : A) (ha : 0 ≤ a := by cfc_tac) : ‖b * a * star b‖ = ‖b * sqrt a‖ ^ 2

theorem CFC.IsSelfAdjoint.norm_mul_mul_self_of_nonneg' {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} (b : A) (hb : IsSelfAdjoint b := by cfc_tac) (ha : 0 ≤ a := by cfc_tac) : ‖b * a * b‖ = ‖b * sqrt a‖ ^ 2