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_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.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)

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 : 0 ∉ spectrum NNReal 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₁ : 0 ∉ spectrum NNReal a) (hx : x ≠ 0) (ha₂ : 0 ≤ a := by cfc_tac) : (a ^ x) ^ y = a ^ (x * y)

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 : 0 ∉ spectrum NNReal 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 : 0 ∉ spectrum NNReal 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)

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 : 0 ∉ spectrum NNReal a) (hb : 0 ∉ spectrum NNReal 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_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 : 0 ∉ spectrum NNReal a) (hb : 0 ∉ spectrum NNReal b) (ha' : 0 ≤ a := by cfc_tac) (hb' : 0 ≤ b := by cfc_tac) : rpow (a, b) x = (a, b) ^ x

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 : ι), 0 ∉ spectrum NNReal (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 : ι), 0 ∉ spectrum NNReal (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

@[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_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 : 0 ∉ spectrum NNReal 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 : 0 ∉ spectrum NNReal 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)