[Merged by Bors] - feat: define CFC.abs, the absolute value in a C⋆-algebra

[j-loreaux]

---

[github-actions]

PR summary 7e091d1f76

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (new file)	2240

---

Declarations diff

+ Commute.star_left
+ Commute.star_right
+ _root_.Commute.cfcAbs_cfcAbs
+ _root_.Commute.cfcAbs_left
+ _root_.Commute.cfcAbs_mul_eq
+ _root_.Commute.cfcAbs_right
+ _root_.cfc_comp_norm
+ _root_.cfcₙ_comp_norm
+ _root_.cfcₙ_norm_nonneg
+ _root_.cfcₙ_norm_sq_nonneg
+ abs
+ abs_add_self
+ abs_algebraMap
+ abs_algebraMap_nnreal
+ abs_eq_cfc_norm
+ abs_eq_cfcₙ_coe_norm
+ abs_eq_cfcₙ_norm
+ abs_eq_zero_iff
+ abs_intCast
+ abs_mul_abs
+ abs_mul_self
+ abs_natCast
+ abs_neg
+ abs_nnrpow
+ abs_nnrpow_two
+ abs_nnrpow_two_mul
+ abs_nonneg
+ abs_ofNat
+ abs_of_nonneg
+ abs_of_nonpos
+ abs_one
+ abs_smul
+ abs_smul_nonneg
+ abs_sq
+ abs_star
+ abs_sub_self
+ abs_zero
+ cfcAbs_cfcAbs
+ commute_abs_self
+ norm_abs
+ posPart_add_negPart
+ quasispectrum_abs
+ spectrum_abs

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

[themathqueen]

How about also adding that abs a commutes with a for IsSelfAdjoint a?

Also, maybe that the spectrum of abs a is equal to the absolute value of the spectrum of a for IsSelfAdjoint a?

[j-loreaux]

@dupuisf see my response above. Come to think of it though, I do wonder the following. Which do think is better for (almost) the entire file: CFC.***abs*** or _root_.***cfcAbs***?

[dupuisf]

I wasn't aware that this namespacing trick works, but I think it still looks strange... I would vote for Commute.cfcAbs_foobar and so on.

[dupuisf]

Looks good, thanks!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build
• Post-Build Step