Measurability of sqrt over an algebra with an isometric CFC #
If A is a measurable non-unital normed ring with an isometric continuous functional calculus,
then the square root function sqrt : A → A is measurable.
theorem
CFC.measurable_sqrt
{A : Type u_1}
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace ℝ A]
[IsScalarTower ℝ A A]
[SMulCommClass ℝ A A]
[PartialOrder A]
[StarOrderedRing A]
[NonnegSpectrumClass ℝ A]
[NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
[CompleteSpace A]
[ContinuousStar A]
[OrderClosedTopology A]
[MeasurableSpace A]
[BorelSpace A]
: