feat(CStarAlgebra): for a monotone f on ℝ≥0, ‖cfc f a‖ = f ‖a‖

[dupuisf]

This PR shows various versions of the fact that if f : ℝ≥0 → ℝ≥0 is monotone on the spectrum of a, then ‖cfc f a‖ = f ‖a‖. We then apply this result to sqrt and rpow.

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.

---

[github-actions]

PR summary 94eccf7b61

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow	-1855
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic	1855
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.CStar (new file)	2251

---

Declarations diff

+ _root_.nnnorm_cfc_of_monotoneOn
+ _root_.nnnorm_cfcₙ_of_monotoneOn
+ monotone_nnrpow_const
+ nnnorm_nnrpow
+ nnnorm_rpow
+ nnnorm_sqrt
+ norm_nnrpow
+ norm_rpow
+ norm_sqrt

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[dupuisf]

I'm open to putting this lemma and the next somewhere else, I couldn't really think of a better place. Also, I don't think the extra import here is a big deal, but I could be convinced otherwise.