feat(ContinuousFunctionalCalculus): cfc applied to products and pi types

[dupuisf]

This PR shows that cfc f ⟨a, b⟩ = ⟨cfc f a, cfc f b⟩ and cfc f (x : ∀ i, A i) = fun i => cfc f (x i) and likewise for the non-unital case. Specialized version for nnrpow, rpow and sqrt are also given.

---

[github-actions]

PR summary 09557472be

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Star.StarAlgHom	724	726	+2 (+0.28%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic	1857	1860	+3 (+0.16%)

Import changes for all files

Files	Import difference
7 files Mathlib.Algebra.Algebra.Spectrum.Quasispectrum Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.Subalgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.StarSubalgebra	1
Mathlib.Algebra.Star.StarAlgHom	2
9 files Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.PositiveLinearMap Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric	3
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi (new file)	1776

---

Declarations diff

+ _root_.Pi.evalNonUnitalStarAlgHom
+ _root_.Pi.evalStarAlgHom
+ cfc_map_pi
+ cfc_map_prod
+ cfcₙ_map_pi
+ cfcₙ_map_prod
+ nnrpow_map_pi
+ nnrpow_map_prod
+ rpow_map_pi
+ rpow_map_prod
+ sqrt_map_pi
+ sqrt_map_prod
++ for

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

[j-loreaux]

I find the mix of bound variables and free variables with the same name hard to parse.

Suggested change

	def _root_.Pi.evalNonUnitalStarAlgHom (R : Type*) (A : ι → Type*) (i : ι) [Monoid R]
	[∀ i, NonUnitalNonAssocSemiring (A i)] [∀ i, DistribMulAction R (A i)] [∀ i, Star (A i)] :
	(∀ i, A i) →⋆ₙₐ[R] A i :=
	{ Pi.evalMulHom A i, Pi.evalAddHom A i with
	def _root_.Pi.evalNonUnitalStarAlgHom (R : Type*) (A : ι → Type*) (j : ι) [Monoid R]
	[∀ i, NonUnitalNonAssocSemiring (A i)] [∀ i, DistribMulAction R (A i)] [∀ i, Star (A i)] :
	(∀ i, A i) →⋆ₙₐ[R] A j:=
	{ Pi.evalMulHom A j, Pi.evalAddHom A j with

[j-loreaux]

Suggested change

	def _root_.Pi.evalStarAlgHom (R : Type*) (A : ι → Type*) (i : ι) [CommSemiring R]
	[∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] [∀ i, Star (A i)] :
	(∀ i, A i) →⋆ₐ[R] A i :=
	{ Pi.evalNonUnitalStarAlgHom R A i, Pi.evalRingHom A i with
	def _root_.Pi.evalStarAlgHom (R : Type*) (A : ι → Type*) (j : ι) [CommSemiring R]
	[∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] [∀ i, Star (A i)] :
	(∀ i, A i) →⋆ₐ[R] A j :=
	{ Pi.evalNonUnitalStarAlgHom R A j, Pi.evalRingHom A j with

[j-loreaux]

I'm not sure why you're using anonymous constructor syntax ⟨a, b⟩ for Prod.mk a b when that already has the notation (a, b). It caused you to need a type ascription that would be unnecessary otherwise.

Suggested change

	`cfc f ⟨a, b⟩ = ⟨cfc f a, cfc f b⟩` (and likewise for the non-unital version)
	`cfc f (a, b) = (cfc f a, cfc f b)` (and likewise for the non-unital version)

[j-loreaux]

Suggested change

	(hab : pab ⟨a, b⟩ := by cfc_tac) (ha : pa a := by cfc_tac) (hb : pb b := by cfc_tac) :
	cfcₙ f (⟨a, b⟩ : A × B) = ⟨cfcₙ f a, cfcₙ f b⟩ := by
	by_cases hf₀ : f 0 = 0
	case pos =>
	ext
	case fst =>
	let φ := NonUnitalStarAlgHom.fst S A B
	exact φ.map_cfcₙ f ⟨a, b⟩ (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_fst hab ha
	case snd =>
	let φ := NonUnitalStarAlgHom.snd S A B
	exact φ.map_cfcₙ f ⟨a, b⟩ (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_snd hab hb
	(hab : pab (a, b) := by cfc_tac) (ha : pa a := by cfc_tac) (hb : pb b := by cfc_tac) :
	cfcₙ f (a, b) = (cfcₙ f a, cfcₙ f b) := by
	by_cases hf₀ : f 0 = 0
	case pos =>
	ext
	case fst =>
	let φ := NonUnitalStarAlgHom.fst S A B
	exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_fst hab ha
	case snd =>
	let φ := NonUnitalStarAlgHom.snd S A B
	exact φ.map_cfcₙ f (a, b) (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_snd hab hb

[j-loreaux]

Suggested change

	(hab : pab ⟨a, b⟩ := by cfc_tac) (ha : pa a := by cfc_tac) (hb : pb b := by cfc_tac) :
	cfc f (⟨a, b⟩ : A × B) = ⟨cfc f a, cfc f b⟩ := by
	ext
	case fst =>
	let φ := StarAlgHom.fst S A B
	exact φ.map_cfc f ⟨a, b⟩ (by rwa [Prod.spectrum_eq]) continuous_fst hab ha
	case snd =>
	let φ := StarAlgHom.snd S A B
	exact φ.map_cfc f ⟨a, b⟩ (by rwa [Prod.spectrum_eq]) continuous_snd hab hb
	(hab : pab (a, b) := by cfc_tac) (ha : pa a := by cfc_tac) (hb : pb b := by cfc_tac) :
	cfc f (a, b) = (cfc f a, cfc f b) := by
	ext
	case fst =>
	let φ := StarAlgHom.fst S A B
	exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_fst hab ha
	case snd =>
	let φ := StarAlgHom.snd S A B
	exact φ.map_cfc f (a, b) (by rwa [Prod.spectrum_eq]) continuous_snd hab hb

[j-loreaux]

You probably neeed to add [NonnegSpectrumClass ℝ _] to these to make it work. Please see the library note in the CStarAlgebra.ContinuousFunctionalCalculus.Note file.

I realize that the rest of this file may not yet be following those guidelines. I've been meaning to update it since I wrote them.

Essentially the point is: we'll never have a direct instance for ℝ≥0, it always goes through ℝ. Consequently, it's better for TC inference (in applications, not necessarily in the abstract cfc files), if the assumptions are for ℝ.

Suggested change

	[NonUnitalContinuousFunctionalCalculus ℝ≥0 B (0 ≤ ·)]
	[NonUnitalContinuousFunctionalCalculus ℝ≥0 (A × B) (0 ≤ ·)]
	variable {ι : Type*} {C : ι → Type*} [∀ i, PartialOrder (C i)] [∀ i, NonUnitalRing (C i)]
	[∀ i, TopologicalSpace (C i)] [∀ i, StarRing (C i)]
	[∀ i, Module ℝ (C i)] [∀ i, SMulCommClass ℝ (C i) (C i)] [∀ i, IsScalarTower ℝ (C i) (C i)]
	[∀ i, NonUnitalContinuousFunctionalCalculus ℝ≥0 (C i) (0 ≤ ·)]
	[NonUnitalContinuousFunctionalCalculus ℝ≥0 (∀ i, C i) (0 ≤ ·)]
	[NonUnitalContinuousFunctionalCalculus ℝ B (0 ≤ ·)]
	[NonUnitalContinuousFunctionalCalculus ℝ (A × B) (0 ≤ ·)]
	variable {ι : Type*} {C : ι → Type*} [∀ i, PartialOrder (C i)] [∀ i, NonUnitalRing (C i)]
	[∀ i, TopologicalSpace (C i)] [∀ i, StarRing (C i)]
	[∀ i, Module ℝ (C i)] [∀ i, SMulCommClass ℝ (C i) (C i)] [∀ i, IsScalarTower ℝ (C i) (C i)]
	[∀ i, NonUnitalContinuousFunctionalCalculus ℝ (C i) (0 ≤ ·)]
	[NonUnitalContinuousFunctionalCalculus ℝ (∀ i, C i) (0 ≤ ·)]

[j-loreaux]

Since these variable blocks cause big slowdowns with regard to elaboration (which we need to fix separately), can you just put them locally on the declaration (or in a mini section around each declaration)? Or if it makes more sense, group all the pi and all the prod results in this file in their own sections.

[j-loreaux]

I may have missed more ⟨a, b⟩ to (a, b) changes, I didn't check carefully.