feat: the Fuglede–Putnam–Rosenblum theorem for C⋆-algebras

[j-loreaux]

Let A be a C⋆-algebra, and let a b x : A. The Fuglede–Putnam–Rosenblum theorem states that if a and b are normal and x intertwines a and b (i.e., SemiconjBy x a b). Then x also intertwines star a and star b. Fuglede's original result was for a = b (i.e., if x commutes with a, then x also commutes with star a), and Putnam extended it to intertwining elements. Rosenblum later gave the elementary proof formalized here using Liouville's theorem.

A version of the Fuglede–Putnam theorem also holds for unbounded operators, but it necessitates a different proof technique and holds in different generality than the one given here.

---

[github-actions]

PR summary d194281a48

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.CStarAlgebra.Fuglede (new file)	2681

---

Declarations diff

+ IsStarNormal.commute_star_left
+ IsStarNormal.commute_star_right
+ SemiconjBy.smul_left
+ SemiconjBy.smul_left_iff
+ SemiconjBy.smul_left_iff₀
+ SemiconjBy.smul_right
+ SemiconjBy.smul_right_iff
+ SemiconjBy.smul_right_iff₀
+ SemiconjBy.star_right
+ SemiconjBy.star_right_of_unital
+ SemiconjBy.tsum_left
+ SemiconjBy.tsum_right
+ _root_.SemiconjBy.exp_neg_mul_mul_exp_eq_self
+ _root_.SemiconjBy.exp_right
+ differentiableAt_exp_smul_const
+ differentiable_exp_smul_const
+ expMulMulExp
+ expMulMulExp_const
+ expMulMulExp_eq_expUnitary_mul_expUnitary
+ fuglede_putnam_rosenblum
+ isStarNormal_iff_forall_exp_mul_exp_mem_unitary

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).