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 ℝ ℝ.

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

noncomputable def CFC.nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {a : A} {y : NNReal} : CFC.nnrpow a y = a ^ y

@[simp]

theorem CFC.nnrpow_nonneg {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {a : A} {x : NNReal} : 0 ≤ a ^ x

theorem CFC.nnrpow_def {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {a : A} : a ^ 0 = 0

theorem CFC.nnrpow_one {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ 1 = a

theorem CFC.nnrpow_two {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ 2 = a * a

theorem CFC.nnrpow_three {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {x : NNReal} : 0 ^ x = 0

@[simp]

theorem CFC.nnrpow_nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a : A} {x y : NNReal} : (a ^ x) ^ y = a ^ (x * y)

theorem CFC.nnrpow_nnrpow_inv {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal 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] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal 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] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal 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

noncomputable def CFC.sqrt {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {a : A} : 0 ≤ CFC.sqrt a

theorem CFC.sqrt_eq_nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {a : A} : CFC.sqrt a = a ^ (1 / 2)

@[simp]

theorem CFC.sqrt_zero {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] : CFC.sqrt 0 = 0

@[simp]

theorem CFC.nnrpow_sqrt {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a : A} {x : NNReal} : CFC.sqrt a ^ x = a ^ (x / 2)

theorem CFC.nnrpow_sqrt_two {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] (a : A) (ha : 0 ≤ a := by cfc_tac) : CFC.sqrt a ^ 2 = a

theorem CFC.sqrt_mul_sqrt_self {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] (a : A) (ha : 0 ≤ a := by cfc_tac) : CFC.sqrt a * CFC.sqrt a = a

@[simp]

theorem CFC.sqrt_nnrpow {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a : A} {x : NNReal} : CFC.sqrt (a ^ x) = a ^ (x / 2)

theorem CFC.sqrt_nnrpow_two {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] (a : A) (ha : 0 ≤ a := by cfc_tac) : CFC.sqrt (a ^ 2) = a

theorem CFC.sqrt_mul_self {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] (a : A) (ha : 0 ≤ a := by cfc_tac) : CFC.sqrt (a * a) = a

theorem CFC.mul_self_eq {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a b : A} (h : CFC.sqrt a = b) (ha : 0 ≤ a := by cfc_tac) : b * b = a

theorem CFC.sqrt_unique {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a b : A} (h : b * b = a) (hb : 0 ≤ b := by cfc_tac) : CFC.sqrt a = b

theorem CFC.sqrt_eq_iff {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : CFC.sqrt a = b ↔ b * b = a

theorem CFC.sqrt_eq_zero_iff {A : Type u_1} [PartialOrder A] [NonUnitalNormedRing A] [StarRing A] [Module NNReal A] [SMulCommClass NNReal A A] [IsScalarTower NNReal A A] [NonUnitalContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] (a : A) (ha : 0 ≤ a := by cfc_tac) : CFC.sqrt a = 0 ↔ a = 0

noncomputable def CFC.rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {a : A} {y : ℝ} : CFC.rpow a y = a ^ y

@[simp]

theorem CFC.rpow_nonneg {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {a : A} {y : ℝ} : 0 ≤ a ^ y

theorem CFC.rpow_def {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {a : A} {y : ℝ} : a ^ y = cfc (fun (x : NNReal) => x ^ y) a

theorem CFC.rpow_one {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ 1 = a

@[simp]

theorem CFC.one_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {x : ℝ} : 1 ^ x = 1

theorem CFC.rpow_zero {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] (a : A) (ha : 0 ≤ a := by cfc_tac) : a ^ 0 = 1

theorem CFC.zero_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {x : ℝ} (hx : x ≠ 0) : CFC.rpow 0 x = 0

theorem CFC.rpow_natCast {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] {x : NNReal} {y : ℝ} : (algebraMap NNReal A) x ^ y = (algebraMap NNReal A) (x ^ y)

theorem CFC.rpow_add {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueContinuousFunctionalCalculus NNReal 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] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueContinuousFunctionalCalculus NNReal 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] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ 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] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x] (a : A) : a ^ (-1) = cfc (fun (x : NNReal) => x⁻¹) a

theorem CFC.rpow_neg {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueContinuousFunctionalCalculus NNReal A] (a : Aˣ) (x : ℝ) (ha' : 0 ≤ ↑a := by cfc_tac) : ↑a ^ (-x) = ↑a⁻¹ ^ x

theorem CFC.rpow_intCast {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] (a : Aˣ) (n : ℤ) (ha : 0 ≤ ↑a := by cfc_tac) : ↑a ^ ↑n = ↑(a ^ n)

theorem CFC.nnrpow_eq_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a : A} {x : NNReal} (hx : 0 < x) : a ^ x = a ^ ↑x

theorem CFC.sqrt_eq_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a : A} : CFC.sqrt a = a ^ (1 / 2)

theorem CFC.sqrt_eq_cfc {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a : A} : CFC.sqrt a = cfc (⇑NNReal.sqrt) a

theorem CFC.sqrt_sq {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] (a : A) (ha : 0 ≤ a := by cfc_tac) : CFC.sqrt (a ^ 2) = a

theorem CFC.sq_sqrt {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] (a : A) (ha : 0 ≤ a := by cfc_tac) : CFC.sqrt a ^ 2 = a

@[simp]

theorem CFC.sqrt_algebraMap {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {r : NNReal} : CFC.sqrt ((algebraMap NNReal A) r) = (algebraMap NNReal A) (NNReal.sqrt r)

@[simp]

theorem CFC.sqrt_one {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] : CFC.sqrt 1 = 1

theorem CFC.sqrt_rpow {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] [UniqueContinuousFunctionalCalculus NNReal A] {a : A} {x : ℝ} (h : 0 ∉ spectrum NNReal a) (hx : x ≠ 0) : CFC.sqrt (a ^ x) = a ^ (x / 2)

theorem CFC.rpow_sqrt {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] [UniqueContinuousFunctionalCalculus NNReal A] (a : A) (x : ℝ) (h : 0 ∉ spectrum NNReal a) (ha : 0 ≤ a := by cfc_tac) : CFC.sqrt a ^ x = a ^ (x / 2)

theorem CFC.sqrt_rpow_nnreal {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] {a : A} {x : NNReal} : CFC.sqrt (a ^ ↑x) = a ^ (↑x / 2)

theorem CFC.rpow_sqrt_nnreal {A : Type u_1} [PartialOrder A] [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [ContinuousFunctionalCalculus NNReal fun (a : A) => 0 ≤ a] [UniqueNonUnitalContinuousFunctionalCalculus NNReal A] [UniqueContinuousFunctionalCalculus NNReal A] {a : A} {x : NNReal} (ha : 0 ≤ a := by cfc_tac) : CFC.sqrt a ^ ↑x = a ^ (↑x / 2)