feat(Analysis/Normed/Algebra/SpectralNorm): define spectral norms and prove uniqueness

[tb65536]

This PR is the first step towards the construction of extensions of absolute values in #42985. The hard part of #42985 is the proof of multiplicativity of the extended norm. The proof involves applying a uniqueness theorem to the extended norm and a modification. This PR introduces the type SpectralNorm, develops the basic API, and proves the uniqueness theorem.

---

[github-actions]

PR summary b8bcbfd3ce

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Normed.Algebra.SpectralNorm (new file)	2153

---

Declarations diff (regex)

+ _root_.SpectralNorm
+ coe_toOneHom
+ coe_toZeroHom
+ comap
+ eq_zero_iff
+ instance (f : SpectralNorm 𝕜 A) : FiniteDimensional 𝕜 f.space
+ instance (f : SpectralNorm 𝕜 A) : NormedAlgebra 𝕜 f.space
+ instance (f : SpectralNorm 𝕜 A) : NormedRing f.space
+ instance : FunLike (SpectralNorm 𝕜 A) A ℝ
+ instance : NonnegHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance : OneHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance : ZeroHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance [CommSemiring A] [Algebra 𝕜 A] : SubadditiveHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance [CommSemiring A] [Algebra 𝕜 A] : SubmultiplicativeHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance [NormOneClass 𝕜] [Field A] [Algebra 𝕜 A] : RingNormClass (SpectralNorm 𝕜 A) A ℝ
+ map_add_le_add
+ map_mul_le_mul
+ map_pow
+ map_smul_eq_mul
+ ringNorm
+ space
+ spectralNorm_le
+ spectralNorm_unique
++ instance [NormOneClass 𝕜] [CommRing A] [Algebra 𝕜 A] :

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit b8bcbfd).

• +40 new declarations
• −0 removed declarations

+SpectralNorm
+SpectralNorm.casesOn
+SpectralNorm.coe_toOneHom
+SpectralNorm.coe_toZeroHom
+SpectralNorm.comap
+SpectralNorm.ctorIdx
+SpectralNorm.eq_zero_iff
+SpectralNorm.ext
+SpectralNorm.ext_iff
+SpectralNorm.instFunLikeReal
+SpectralNorm.instNonnegHomClassReal
+SpectralNorm.instOneHomClassReal
+SpectralNorm.instRingNormClassRealOfNormOneClass
+SpectralNorm.instRingSeminormClassRealOfNormOneClass
+SpectralNorm.instSeminormClassOfNormOneClass
+SpectralNorm.instSubadditiveHomClassReal
+SpectralNorm.instSubmultiplicativeHomClassReal
+SpectralNorm.instZeroHomClassReal
+SpectralNorm.map_add_le_add
+SpectralNorm.map_add_le_add'
+SpectralNorm.map_mul_le_mul
+SpectralNorm.map_mul_le_mul'
+SpectralNorm.map_pow
+SpectralNorm.map_pow'
+SpectralNorm.map_smul_eq_mul
+SpectralNorm.map_smul_eq_mul'
+SpectralNorm.map_zero'
+SpectralNorm.mk
+SpectralNorm.mk.inj
+SpectralNorm.mk.injEq
+SpectralNorm.mk.noConfusion
+SpectralNorm.mk.sizeOf_spec
+SpectralNorm.noConfusion
+SpectralNorm.noConfusionType
+SpectralNorm.nonneg'
+SpectralNorm.rec
+SpectralNorm.recOn
+SpectralNorm.spectralNorm_unique
+SpectralNorm.toOneHom
+SpectralNorm.toZeroHom

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
4939	1	exposed public sections

Current commit b8bcbfd3ce
Reference commit d77ef0741c

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).