Theorems · Theorem · functional analysis

CFC.sqrt_eq_real_sqrt

∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a : A),
  autoParam (0 ≤ a) CFC.sqrt_eq_real_sqrt._auto_1 → CFC.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⁺.

Defined in

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Cited by

2 results in Mathlib

Foundations

Depth 215 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PartialOrderNonUnitalRingTopologicalSpaceStarRingModuleSMulCommClassIsScalarTowerStarOrderedRingNonUnitalContinuousFunctionalCalculusNonnegSpectrumClassIsSemitopologicalRingT2Space