Commit 2025-01-22 02:43 8d5e2c1a

feat(ContinuousFunctionalCalculus): ‖sqrt a‖ = sqrt ‖a‖ and ‖a ^ r‖ = ‖a‖^r for an isometric CFC (#20819) This PR shows that ‖sqrt a‖ = sqrt ‖a‖ and ‖a ^ r‖ = ‖a‖ ^ r when a is an element of an algebra that admits an isometric continuous functional calculus. We also rename the file Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow to Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic, in order to put the new results in a new file with heavier imports. I think the new folder makes sense, especially since we'll need to do something like that anyway soon for the operator monotonicity and convexity/concavity results that depend on integral representations.