Real powers defined via the continuous functional calculus

This file defines real powers via the continuous functional calculus (CFC) and builds its API. This allows one to take real powers of matrices, operators, elements of a C⋆-algebra, etc. The square root is also defined via the non-unital CFC.

Main declarations

• CFC.nnrpow: the ℝ≥0 power function based on the non-unital CFC, i.e. cfcₙ NNReal.rpow composed with (↑) : ℝ≥0 → ℝ.
• CFC.sqrt: the square root function based on the non-unital CFC, i.e. cfcₙ NNReal.sqrt
• CFC.rpow: the real power function based on the unital CFC, i.e. cfc NNReal.rpow

Implementation notes

We define two separate versions CFC.nnrpow and CFC.rpow due to what happens at 0. Since NNReal.rpow 0 0 = 1, this means that this function does not map zero to zero when the exponent is zero, and hence CFC.nnrpow a 0 = 0 whereas CFC.rpow a 0 = 1. Note that the non-unital version only makes sense for nonnegative exponents, and hence we define it such that the exponent is in ℝ≥0.

Notation

• We define a Pow A ℝ instance for CFC.rpow, i.e a ^ y with A an operator and y : ℝ works as expected. Likewise, we define a Pow A ℝ≥0 instance for CFC.nnrpow. Note that these are low-priority instances, in order to avoid overriding instances such as Pow ℝ ℝ, Pow (A × B) ℝ or Pow (∀ i, A i) ℝ.

TODO

• Relate these to the log and exp functions
• Lemmas about how these functions interact with commuting a and b.
• Prove the order properties (operator monotonicity and concavity/convexity)

@[reducible, inline]

noncomputable abbrev NNReal.nnrpow (a b : NNReal) : NNReal

Taking a nonnegative power of a nonnegative number. This is defined as a standalone definition in order to speed up automation such as cfc_cont_tac.

Equations

• a.nnrpow b = a ^ ↑b

@[simp]

theorem NNReal.nnrpow_def (a b : NNReal) : a.nnrpow b = a ^ ↑b

theorem NNReal.continuous_nnrpow_const (y : NNReal) : Continuous fun (x : NNReal) => x.nnrpow y

theorem NNReal.monotone_nnrpow_const (y : NNReal) : Monotone fun (x : NNReal) => x.nnrpow y

noncomputable def CFC.nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (y : NNReal) : A

Real powers of operators, based on the non-unital continuous functional calculus.

Equations

• CFC.nnrpow a y = cfcₙ (fun (x : NNReal) => x.nnrpow y) a

@[instance 100]

noncomputable instance CFC.instPowNNReal {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] : Pow A NNReal

Enable a ^ y notation for CFC.nnrpow. This is a low-priority instance to make sure it does not take priority over other instances when they are available.

Equations

• CFC.instPowNNReal = { pow := fun (a : A) (y : NNReal) => CFC.nnrpow a y }

@[simp]

theorem CFC.nnrpow_eq_pow {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} {y : NNReal} : nnrpow a y = a ^ y

@[simp]

theorem CFC.nnrpow_nonneg {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} {x : NNReal} : 0 ≤ a ^ x

theorem CFC.nnrpow_def {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} {y : NNReal} : a ^ y = cfcₙ (fun (x : NNReal) => x.nnrpow y) a

theorem CFC.nnrpow_eq_cfcₙ_real {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] (a : A) (y : NNReal) (ha : 0 ≤ a := by cfc_tac) : a ^ y = cfcₙ (fun (x : ℝ) => x ^ ↑y) a

theorem CFC.nnrpow_add {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} {x y : NNReal} (hx : 0 < x) (hy : 0 < y) : a ^ (x + y) = a ^ x * a ^ y

@[simp]

theorem CFC.nnrpow_zero {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} : a ^ 0 = 0

theorem CFC.nnrpow_one {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ 1 = a

theorem CFC.nnrpow_two {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ 2 = a * a

theorem CFC.nnrpow_three {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ 3 = a * a * a

@[simp]

theorem CFC.zero_nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {x : NNReal} : 0 ^ x = 0

@[simp]

theorem CFC.nnrpow_nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} {x y : NNReal} : (a ^ x) ^ y = a ^ (x * y)

theorem CFC.nnrpow_nnrpow_inv {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) {x : NNReal} (hx : x ≠ 0) (ha : 0 ≤ a := by cfc_tac) : (a ^ x) ^ x⁻¹ = a

theorem CFC.nnrpow_inv_nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) {x : NNReal} (hx : x ≠ 0) (ha : 0 ≤ a := by cfc_tac) : (a ^ x⁻¹) ^ x = a

theorem CFC.nnrpow_inv_eq {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a b : A) {x : NNReal} (hx : x ≠ 0) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : a ^ x⁻¹ = b ↔ b ^ x = a

theorem CFC.nnrpow_map_prod {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {B : Type u_2} [PartialOrder B] [NonUnitalRing B] [TopologicalSpace B] [StarRing B] [Module ℝ B] [SMulCommClass ℝ B B] [IsScalarTower ℝ B B] [NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint] [NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsTopologicalRing B] [T2Space B] [NonnegSpectrumClass ℝ B] [NonnegSpectrumClass ℝ (A × B)] [StarOrderedRing B] {a : A} {b : B} {x : NNReal} (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : nnrpow (a, b) x = (a ^ x, b ^ x)

theorem CFC.nnrpow_eq_nnrpow_prod {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {B : Type u_2} [PartialOrder B] [NonUnitalRing B] [TopologicalSpace B] [StarRing B] [Module ℝ B] [SMulCommClass ℝ B B] [IsScalarTower ℝ B B] [NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint] [NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsTopologicalRing B] [T2Space B] [NonnegSpectrumClass ℝ B] [NonnegSpectrumClass ℝ (A × B)] [StarOrderedRing B] {a : A} {b : B} {x : NNReal} (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : nnrpow (a, b) x = (a, b) ^ x

theorem CFC.nnrpow_map_pi {ι : Type u_2} {C : ι → Type u_3} [(i : ι) → PartialOrder (C i)] [(i : ι) → NonUnitalRing (C i)] [(i : ι) → TopologicalSpace (C i)] [(i : ι) → StarRing (C i)] [∀ (i : ι), StarOrderedRing (C i)] [StarOrderedRing ((i : ι) → C i)] [(i : ι) → Module ℝ (C i)] [∀ (i : ι), SMulCommClass ℝ (C i) (C i)] [∀ (i : ι), IsScalarTower ℝ (C i) (C i)] [∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint] [NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint] [∀ (i : ι), IsTopologicalRing (C i)] [∀ (i : ι), T2Space (C i)] [NonnegSpectrumClass ℝ ((i : ι) → C i)] [∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : NNReal} (hc : ∀ (i : ι), 0 ≤ c i := by cfc_tac) : nnrpow c x = fun (i : ι) => c i ^ x

theorem CFC.nnrpow_eq_nnrpow_pi {ι : Type u_2} {C : ι → Type u_3} [(i : ι) → PartialOrder (C i)] [(i : ι) → NonUnitalRing (C i)] [(i : ι) → TopologicalSpace (C i)] [(i : ι) → StarRing (C i)] [∀ (i : ι), StarOrderedRing (C i)] [StarOrderedRing ((i : ι) → C i)] [(i : ι) → Module ℝ (C i)] [∀ (i : ι), SMulCommClass ℝ (C i) (C i)] [∀ (i : ι), IsScalarTower ℝ (C i) (C i)] [∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint] [NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint] [∀ (i : ι), IsTopologicalRing (C i)] [∀ (i : ι), T2Space (C i)] [NonnegSpectrumClass ℝ ((i : ι) → C i)] [∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : NNReal} (hc : ∀ (i : ι), 0 ≤ c i := by cfc_tac) : nnrpow c x = c ^ x

noncomputable def CFC.sqrt {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) : A

Square roots of operators, based on the non-unital continuous functional calculus.

Equations

• CFC.sqrt a = cfcₙ (⇑NNReal.sqrt) a

@[simp]

theorem CFC.sqrt_nonneg {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) : 0 ≤ sqrt a

theorem CFC.sqrt_eq_nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) : sqrt a = a ^ (1 / 2)

@[simp]

theorem CFC.sqrt_zero {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] : sqrt 0 = 0

@[simp]

theorem CFC.nnrpow_sqrt {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} {x : NNReal} : sqrt a ^ x = a ^ (x / 2)

theorem CFC.nnrpow_sqrt_two {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt a ^ 2 = a

theorem CFC.sqrt_mul_sqrt_self {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt a * sqrt a = a

@[simp]

theorem CFC.sqrt_nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} {x : NNReal} : sqrt (a ^ x) = a ^ (x / 2)

theorem CFC.sqrt_nnrpow_two {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt (a ^ 2) = a

theorem CFC.sqrt_mul_self {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt (a * a) = a

theorem CFC.mul_self_eq {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A} (h : sqrt a = b) (ha : 0 ≤ a := by cfc_tac) : b * b = a

theorem CFC.sqrt_unique {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A} (h : b * b = a) (hb : 0 ≤ b := by cfc_tac) : sqrt a = b

theorem CFC.sqrt_eq_iff {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : sqrt a = b ↔ b * b = a

theorem CFC.sqrt_eq_zero_iff {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt a = 0 ↔ a = 0

theorem CFC.mul_self_eq_mul_self_iff {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : a * a = b * b ↔ a = b

theorem CFC.sqrt_eq_real_sqrt {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt a = cfcₙ Real.sqrt a

Note that the hypothesis 0 ≤ a is necessary because the continuous functional calculi over ℝ≥0 (for the left-hand side) and ℝ (for the right-hand side) use different predicates (i.e., (0 ≤ ·) versus IsSelfAdjoint). Consequently, if a is selfadjoint but not nonnegative, then the left-hand side is zero, but the right-hand side is (provably equal to) CFC.sqrt a⁺.

theorem CFC.sqrt_map_prod {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {B : Type u_2} [PartialOrder B] [NonUnitalRing B] [TopologicalSpace B] [StarRing B] [Module ℝ B] [SMulCommClass ℝ B B] [IsScalarTower ℝ B B] [StarOrderedRing B] [NonUnitalContinuousFunctionalCalculus ℝ B IsSelfAdjoint] [NonUnitalContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsTopologicalRing B] [T2Space B] [NonnegSpectrumClass ℝ B] [NonnegSpectrumClass ℝ (A × B)] {a : A} {b : B} (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : sqrt (a, b) = (sqrt a, sqrt b)

theorem CFC.sqrt_map_pi {ι : Type u_2} {C : ι → Type u_3} [(i : ι) → PartialOrder (C i)] [(i : ι) → NonUnitalRing (C i)] [(i : ι) → TopologicalSpace (C i)] [(i : ι) → StarRing (C i)] [∀ (i : ι), StarOrderedRing (C i)] [StarOrderedRing ((i : ι) → C i)] [(i : ι) → Module ℝ (C i)] [∀ (i : ι), SMulCommClass ℝ (C i) (C i)] [∀ (i : ι), IsScalarTower ℝ (C i) (C i)] [∀ (i : ι), NonUnitalContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint] [NonUnitalContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint] [∀ (i : ι), IsTopologicalRing (C i)] [∀ (i : ι), T2Space (C i)] [NonnegSpectrumClass ℝ ((i : ι) → C i)] [∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} (hc : ∀ (i : ι), 0 ≤ c i := by cfc_tac) : sqrt c = fun (i : ι) => sqrt (c i)

theorem CStarAlgebra.nonneg_TFAE {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : [0 ≤ a, a = CFC.sqrt a * CFC.sqrt a, ∃ (b : A), 0 ≤ b ∧ a = b * b, ∃ (b : A), IsSelfAdjoint b ∧ a = b * b, ∃ (b : A), a = star b * b, ∃ (b : A), a = b * star b, IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE

For an element a in a C⋆-algebra, TFAE:

• 0 ≤ a
• a = sqrt a * sqrt a
• a = b * b for some nonnegative b
• a = b * b for some self-adjoint b
• a = star b * b for some b
• a = b * star b for some b
• a is self-adjoint and has nonnegative spectrum

theorem CStarAlgebra.nonneg_iff_eq_sqrt_mul_sqrt {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : 0 ≤ a ↔ a = CFC.sqrt a * CFC.sqrt a

theorem CStarAlgebra.nonneg_iff_exists_nonneg_and_eq_mul_self {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : 0 ≤ a ↔ ∃ (b : A), 0 ≤ b ∧ a = b * b

theorem CStarAlgebra.nonneg_iff_exists_isSelfAdjoint_and_eq_mul_self {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : 0 ≤ a ↔ ∃ (b : A), IsSelfAdjoint b ∧ a = b * b

theorem CStarAlgebra.nonneg_iff_eq_star_mul_self {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : 0 ≤ a ↔ ∃ (b : A), a = star b * b

theorem CStarAlgebra.nonneg_iff_eq_mul_star_self {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : 0 ≤ a ↔ ∃ (b : A), a = b * star b

noncomputable def CFC.rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (y : ℝ) : A

Real powers of operators, based on the unital continuous functional calculus.

Equations

• CFC.rpow a y = cfc (fun (x : NNReal) => x ^ y) a

@[instance 100]

noncomputable instance CFC.instPowReal {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] : Pow A ℝ

Enable a ^ y notation for CFC.rpow. This is a low-priority instance to make sure it does not take priority over other instances when they are available (such as Pow ℝ ℝ).

Equations

• CFC.instPowReal = { pow := fun (a : A) (y : ℝ) => CFC.rpow a y }

@[simp]

theorem CFC.rpow_eq_pow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} {y : ℝ} : rpow a y = a ^ y

@[simp]

theorem CFC.rpow_nonneg {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} {y : ℝ} : 0 ≤ a ^ y

theorem CFC.rpow_def {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} {y : ℝ} : a ^ y = cfc (fun (x : NNReal) => x ^ y) a

theorem CFC.rpow_one {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ 1 = a

@[simp]

theorem CFC.one_rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {x : ℝ} : 1 ^ x = 1

theorem CFC.rpow_zero {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ 0 = 1

theorem CFC.zero_rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {x : ℝ} (hx : x ≠ 0) : rpow 0 x = 0

theorem CFC.rpow_natCast {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (n : ℕ) (ha : 0 ≤ a := by cfc_tac) : a ^ ↑n = a ^ n

@[simp]

theorem CFC.rpow_algebraMap {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {x : NNReal} {y : ℝ} : (algebraMap NNReal A) x ^ y = (algebraMap NNReal A) (x ^ y)

theorem CFC.rpow_add {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} {x y : ℝ} (ha : IsUnit a) : a ^ (x + y) = a ^ x * a ^ y

theorem CFC.rpow_rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (x y : ℝ) (ha₁ : IsUnit a) (hx : x ≠ 0) (ha₂ : 0 ≤ a := by cfc_tac) : (a ^ x) ^ y = a ^ (x * y)

theorem CFC.rpow_rpow_inv {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (x : ℝ) (ha₁ : IsUnit a) (hx : x ≠ 0) (ha₂ : 0 ≤ a := by cfc_tac) : (a ^ x) ^ x⁻¹ = a

theorem CFC.rpow_inv_rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (x : ℝ) (ha₁ : IsUnit a) (hx : x ≠ 0) (ha₂ : 0 ≤ a := by cfc_tac) : (a ^ x⁻¹) ^ x = a

theorem CFC.rpow_rpow_of_exponent_nonneg {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (ha₂ : 0 ≤ a := by cfc_tac) : (a ^ x) ^ y = a ^ (x * y)

theorem CFC.rpow_mul_rpow_neg {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} (x : ℝ) (ha : IsUnit a) (ha' : 0 ≤ a := by cfc_tac) : a ^ x * a ^ (-x) = 1

theorem CFC.rpow_neg_mul_rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} (x : ℝ) (ha : IsUnit a) (ha' : 0 ≤ a := by cfc_tac) : a ^ (-x) * a ^ x = 1

theorem CFC.rpow_neg_one_eq_inv {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : Aˣ) (ha : 0 ≤ ↑a := by cfc_tac) : ↑a ^ (-1) = ↑a⁻¹

theorem CFC.rpow_neg_one_eq_cfc_inv {A : Type u_2} [PartialOrder A] [NormedRing A] [StarRing A] [StarOrderedRing A] [NormedAlgebra ℝ A] [NonnegSpectrumClass ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) : a ^ (-1) = cfc (fun (x : NNReal) => x⁻¹) a

theorem CFC.rpow_neg {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : Aˣ) (x : ℝ) (ha' : 0 ≤ ↑a := by cfc_tac) : ↑a ^ (-x) = ↑a⁻¹ ^ x

theorem CFC.rpow_intCast {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : Aˣ) (n : ℤ) (ha : 0 ≤ ↑a := by cfc_tac) : ↑a ^ ↑n = ↑(a ^ n)

noncomputable def Units.cfcRpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : Aˣ) (x : ℝ) (ha : 0 ≤ ↑a := by cfc_tac) : Aˣ

a ^ x bundled as an element of Aˣ for a : Aˣ.

Equations

• a.cfcRpow x ha = { val := ↑a ^ x, inv := ↑a ^ (-x), val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem Units.val_inv_cfcRpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : Aˣ) (x : ℝ) (ha : 0 ≤ ↑a := by cfc_tac) : ↑(a.cfcRpow x ha)⁻¹ = ↑a ^ (-x)

@[simp]

theorem Units.val_cfcRpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : Aˣ) (x : ℝ) (ha : 0 ≤ ↑a := by cfc_tac) : ↑(a.cfcRpow x ha) = ↑a ^ x

theorem IsUnit.cfcRpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} (ha : IsUnit a) (x : ℝ) (ha_nonneg : 0 ≤ a := by cfc_tac) : IsUnit (a ^ x)

theorem CFC.spectrum_rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (x : ℝ) (h : ContinuousOn (fun (x_1 : NNReal) => x_1 ^ x) (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : spectrum NNReal (a ^ x) = (fun (x_1 : NNReal) => x_1 ^ x) '' spectrum NNReal a

theorem CFC.isUnit_rpow_iff {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (y : ℝ) (hy : y ≠ 0) (ha : 0 ≤ a := by cfc_tac) : IsUnit (a ^ y) ↔ IsUnit a

theorem CFC.rpow_map_prod {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {B : Type u_2} [PartialOrder B] [Ring B] [StarRing B] [TopologicalSpace B] [StarOrderedRing B] [Algebra ℝ B] [ContinuousFunctionalCalculus ℝ B IsSelfAdjoint] [ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsTopologicalRing B] [T2Space B] [StarOrderedRing (A × B)] [NonnegSpectrumClass ℝ B] [NonnegSpectrumClass ℝ (A × B)] {a : A} {b : B} {x : ℝ} (ha : IsUnit a) (hb : IsUnit b) (ha' : 0 ≤ a := by cfc_tac) (hb' : 0 ≤ b := by cfc_tac) : rpow (a, b) x = (a ^ x, b ^ x)

theorem CFC.rpow_eq_rpow_prod {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {B : Type u_2} [PartialOrder B] [Ring B] [StarRing B] [TopologicalSpace B] [StarOrderedRing B] [Algebra ℝ B] [ContinuousFunctionalCalculus ℝ B IsSelfAdjoint] [ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsTopologicalRing B] [T2Space B] [StarOrderedRing (A × B)] [NonnegSpectrumClass ℝ B] [NonnegSpectrumClass ℝ (A × B)] {a : A} {b : B} {x : ℝ} (ha : IsUnit a) (hb : IsUnit b) (ha' : 0 ≤ a := by cfc_tac) (hb' : 0 ≤ b := by cfc_tac) : rpow (a, b) x = (a, b) ^ x

@[deprecated CFC.rpow_eq_rpow_prod (since := "2025-05-13")]

theorem CFC.rpow_eq_rpow_rpod {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {B : Type u_2} [PartialOrder B] [Ring B] [StarRing B] [TopologicalSpace B] [StarOrderedRing B] [Algebra ℝ B] [ContinuousFunctionalCalculus ℝ B IsSelfAdjoint] [ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint] [IsTopologicalRing B] [T2Space B] [StarOrderedRing (A × B)] [NonnegSpectrumClass ℝ B] [NonnegSpectrumClass ℝ (A × B)] {a : A} {b : B} {x : ℝ} (ha : IsUnit a) (hb : IsUnit b) (ha' : 0 ≤ a := by cfc_tac) (hb' : 0 ≤ b := by cfc_tac) : rpow (a, b) x = (a, b) ^ x

Alias of CFC.rpow_eq_rpow_prod.

theorem CFC.rpow_map_pi {ι : Type u_2} {C : ι → Type u_3} [(i : ι) → PartialOrder (C i)] [(i : ι) → Ring (C i)] [(i : ι) → StarRing (C i)] [(i : ι) → TopologicalSpace (C i)] [∀ (i : ι), StarOrderedRing (C i)] [StarOrderedRing ((i : ι) → C i)] [(i : ι) → Algebra ℝ (C i)] [∀ (i : ι), ContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint] [ContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint] [∀ (i : ι), IsTopologicalRing (C i)] [∀ (i : ι), T2Space (C i)] [NonnegSpectrumClass ℝ ((i : ι) → C i)] [∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : ℝ} (hc : ∀ (i : ι), IsUnit (c i)) (hc' : ∀ (i : ι), 0 ≤ c i := by cfc_tac) : rpow c x = fun (i : ι) => c i ^ x

theorem CFC.rpow_eq_rpow_pi {ι : Type u_2} {C : ι → Type u_3} [(i : ι) → PartialOrder (C i)] [(i : ι) → Ring (C i)] [(i : ι) → StarRing (C i)] [(i : ι) → TopologicalSpace (C i)] [∀ (i : ι), StarOrderedRing (C i)] [StarOrderedRing ((i : ι) → C i)] [(i : ι) → Algebra ℝ (C i)] [∀ (i : ι), ContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint] [ContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint] [∀ (i : ι), IsTopologicalRing (C i)] [∀ (i : ι), T2Space (C i)] [NonnegSpectrumClass ℝ ((i : ι) → C i)] [∀ (i : ι), NonnegSpectrumClass ℝ (C i)] {c : (i : ι) → C i} {x : ℝ} (hc : ∀ (i : ι), IsUnit (c i)) (hc' : ∀ (i : ι), 0 ≤ c i := by cfc_tac) : rpow c x = c ^ x

theorem CFC.nnrpow_eq_rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} {x : NNReal} (hx : 0 < x) : a ^ x = a ^ ↑x

theorem CFC.sqrt_eq_rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : sqrt a = a ^ (1 / 2)

theorem CFC.sqrt_eq_cfc {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : sqrt a = cfc (⇑NNReal.sqrt) a

theorem CFC.sqrt_sq {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt (a ^ 2) = a

theorem CFC.sq_sqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt a ^ 2 = a

theorem CFC.sq_eq_sq_iff {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : a ^ 2 = b ^ 2 ↔ a = b

@[simp]

theorem CFC.sqrt_algebraMap {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {r : NNReal} : sqrt ((algebraMap NNReal A) r) = (algebraMap NNReal A) (NNReal.sqrt r)

@[simp]

theorem CFC.sqrt_one {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] : sqrt 1 = 1

theorem CFC.sqrt_eq_one_iff {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt a = 1 ↔ a = 1

theorem CFC.sqrt_eq_one_iff' {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [Nontrivial A] (a : A) : sqrt a = 1 ↔ a = 1

theorem CFC.sqrt_rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} {x : ℝ} (h : IsUnit a) (hx : x ≠ 0) : sqrt (a ^ x) = a ^ (x / 2)

theorem CFC.rpow_sqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (x : ℝ) (h : IsUnit a) (ha : 0 ≤ a := by cfc_tac) : sqrt a ^ x = a ^ (x / 2)

theorem CFC.sqrt_rpow_nnreal {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} {x : NNReal} : sqrt (a ^ ↑x) = a ^ (↑x / 2)

theorem CFC.rpow_sqrt_nnreal {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} {x : NNReal} (ha : 0 ≤ a := by cfc_tac) : sqrt a ^ ↑x = a ^ (↑x / 2)

theorem CFC.isUnit_nnrpow_iff {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (y : NNReal) (hy : y ≠ 0) (ha : 0 ≤ a := by cfc_tac) : IsUnit (a ^ y) ↔ IsUnit a

theorem IsUnit.cfcNNRpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (y : NNReal) (ha_unit : IsUnit a) (hy : y ≠ 0) (ha : 0 ≤ a := by cfc_tac) : IsUnit (a ^ y)

theorem CFC.isUnit_sqrt_iff {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) : IsUnit (sqrt a) ↔ IsUnit a

theorem IsUnit.cfcSqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha_unit : IsUnit a) (ha : 0 ≤ a := by cfc_tac) : IsUnit (CFC.sqrt a)

theorem IsStrictlyPositive.nnrpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} {y : NNReal} (ha : IsStrictlyPositive a) (hy : y ≠ 0) : IsStrictlyPositive (a ^ y)

theorem IsStrictlyPositive.sqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} (ha : IsStrictlyPositive a) : IsStrictlyPositive (CFC.sqrt a)

theorem IsStrictlyPositive.rpow {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {a : A} {y : ℝ} (ha : IsStrictlyPositive a) : IsStrictlyPositive (a ^ y)

theorem CStarAlgebra.isStrictlyPositive_TFAE {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : [IsStrictlyPositive a, IsStrictlyPositive (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a, IsUnit (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a, ∃ (b : A), IsStrictlyPositive b ∧ a = b * b, ∃ (b : A), IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b, ∃ (b : A), IsUnit b ∧ a = star b * b, ∃ (b : A), IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a, IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE

For an element a in a C⋆-algebra, TFAE:

1. a is strictly positive,
2. sqrt a is strictly positive and a = sqrt a * sqrt a,
3. sqrt a is invertible and a = sqrt a * sqrt a,
4. a = b * b for some strictly positive b,
5. a = b * b for some self-adjoint and invertible b,
6. a = star b * b for some invertible b,
7. a = b * star b for some invertible b,
8. 0 ≤ a and a is invertible,
9. a is self-adjoint and has positive spectrum.

theorem CStarAlgebra.isStrictlyPositive_iff_isStrictlyPositive_sqrt_and_eq_sqrt_mul_sqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : IsStrictlyPositive a ↔ IsStrictlyPositive (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a

theorem CStarAlgebra.isStrictlyPositive_iff_isUnit_sqrt_and_eq_sqrt_mul_sqrt {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : IsStrictlyPositive a ↔ IsUnit (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a

theorem CStarAlgebra.isStrictlyPositive_iff_exists_isStrictlyPositive_and_eq_mul_self {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : IsStrictlyPositive a ↔ ∃ (b : A), IsStrictlyPositive b ∧ a = b * b

theorem CStarAlgebra.isStrictlyPositive_iff_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : IsStrictlyPositive a ↔ ∃ (b : A), IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b

theorem CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : IsStrictlyPositive a ↔ ∃ (b : A), IsUnit b ∧ a = star b * b

theorem CStarAlgebra.isStrictlyPositive_iff_eq_mul_star_self {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : IsStrictlyPositive a ↔ ∃ (b : A), IsUnit b ∧ a = b * star b

theorem CStarAlgebra.isStrictlyPositive_iff_isSelfAdjoint_and_spectrum_pos {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a : A} : IsStrictlyPositive a ↔ IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x