feat(Analysis/Normed/Algebra/SpectralNorm): extensions of absolute values

[tb65536]

Let L be a finite extension of a complete normed field K. Then there is a unique absolute value on L extending the absolute value on K. This PR gives a construction that works uniformly across the archimedean and non-archimedean cases (bypassing Gelfand-Mazur).

---

• depends on: feat(Analysis/Normed/Algebra/SpectralRadiusLimit): define the spectral radius limit lim ‖a ^ k‖ ^ (1 / k) #42607
• depends on: feat(Topology/Separation/Hausdorff): add tendsto_nhds_unique_of_forall #42986
• depends on: [Merged by Bors] - feat(Algebra/Group/Commute/Basic): an element commutes with its inverse #42987
• depends on: refactor(Analysis/Normed/Unbundled/SpectralNorm): extract, generalize, and golf uniqueness of power-multiplicative norms #43015
• depends on: feat(Analysis/Matrix/Normed): norm of block diagonal matrix #43016
• depends on: refactor(Analysis/Normed/Unbundled/SpectralNorm): extract, generalize, and golf algNormFromConst #43019

[github-actions]

PR summary 93f23f725c

Import changes exceeding 2%

%	File
+48.20%	Mathlib.Analysis.Subadditive

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Subadditive	1222	1811	+589 (+48.20%)
Mathlib.Analysis.Normed.Unbundled.SeminormFromConst	1813	1835	+22 (+1.21%)

Import changes for all files

Files	Import difference
4 files Mathlib.Analysis.Normed.Field.Dense Mathlib.Analysis.Normed.Field.Krasner Mathlib.Analysis.Normed.Unbundled.SpectralNorm Mathlib.NumberTheory.Padics.Complex	1
26 files Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.CStarAlgebra.CStarMatrix Mathlib.Analysis.CStarAlgebra.Commutative.PosPart Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.CStarAlgebra.Extreme Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.PositiveLinearMap Mathlib.Analysis.CStarAlgebra.Projection Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.Unitary.Connected Mathlib.Analysis.CStarAlgebra.Unitary.Span Mathlib.Analysis.InnerProductSpace.StandardSubspace Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.Normed.Algebra.GelfandFormula Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder Mathlib.MeasureTheory.Measure.ResolventTransform	2
Mathlib.Analysis.Normed.Unbundled.SeminormFromConst	22
Mathlib.Analysis.Subadditive	589
Mathlib.Analysis.Normed.Algebra.SpectralRadiusLimit (new file)	1817
Mathlib.Analysis.Normed.Unbundled.IsPowMulUnique (new file)	2284
Mathlib.Analysis.Normed.Algebra.SpectralNorm (new file)	2381

---

Declarations diff (regex)

+ AlgebraNorm.copy
+ AlgebraNorm.ringNorm
+ AlgebraNorm.toMulAlgebraNorm
+ Commute.spectralRadiusLim_add_le
+ Commute.spectralRadiusLim_mul_le
+ FiniteDimensional.spectralNorm'_eq
+ IsAlgebraic.spectralNorm'_eq
+ IsPowMul.unique
+ Matrix.linfty_opNNNorm_blockDiagonal
+ Matrix.linfty_opNorm_blockDiagonal
+ Matrix.spectralRadiusLim_blockMatrix
+ Matrix.spectralRadiusLim_conj
+ Matrix.spectralRadiusLim_conj_le
+ SpectralNorm
+ SpectralNorm.eq_zero_iff
+ SpectralNorm.ringNorm
+ SpectralNorm.space
+ Submultiplicative
+ absoluteValue
+ absoluteValue_algebraMap
+ algebraNormFromConst
+ coe_toOneHom
+ coe_toZeroHom
+ comap
+ enorm_neg_pow
+ eq_zero_of_spectralNorm'_eq_zero
+ exists_le_spectralRadiusLim
+ exists_spectralRadiusLim_le
+ extension
+ instance (f : AlgebraNorm K L) (x : L) : Algebra (f.copy x) L
+ instance (f : AlgebraNorm K L) (x : L) : FiniteDimensional K (f.copy x)
+ instance (f : AlgebraNorm K L) (x : L) : NormedAlgebra K (f.copy x)
+ instance (f : AlgebraNorm K L) (x : L) : NormedRing (f.copy x)
+ instance (f : SpectralNorm 𝕜 A) : FiniteDimensional 𝕜 f.space
+ instance (f : SpectralNorm 𝕜 A) : NormedAlgebra 𝕜 f.space
+ instance (f : SpectralNorm 𝕜 A) : NormedRing f.space
+ instance : (v.extension L).LiesOver v
+ instance : FunLike (SpectralNorm 𝕜 A) A ℝ
+ instance : NonnegHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance : OneHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance : SubadditiveHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance : SubmultiplicativeHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance : ZeroHomClass (SpectralNorm 𝕜 A) A ℝ
+ instance [NormOneClass 𝕜] : RingSeminormClass (SpectralNorm 𝕜 A) A ℝ
+ instance [NormOneClass 𝕜] : SeminormClass (SpectralNorm 𝕜 A) 𝕜 A
+ instance [SeminormedCommRing 𝕜] [NormOneClass 𝕜] [Field A] [Algebra 𝕜 A] :
+ isPowMul_spectralAlgNorm'
+ isPowMul_spectralNorm'
+ isPowMul_spectralRadiusLimNorm
+ lim
+ map_add_le_add
+ map_mul_le_mul
+ map_pow
+ map_smul_eq_mul
+ modify
+ modifyAux
+ modifyAux_add_le
+ modifyAux_map_smul_eq_mul
+ modifyAux_mul
+ modifyAux_mul_le
+ modifyAux_nonneg
+ modifyAux_one
+ modifyAux_pow
+ modifyAux_zero
+ modify_mul
+ nnnorm_neg_pow
+ norm_neg_pow
+ spectralAlgNorm'
+ spectralAlgNorm'_def
+ spectralAlgNorm'_extends
+ spectralAlgNorm'_one
+ spectralMulAlgNorm'
+ spectralNorm
+ spectralNorm'
+ spectralNorm'_add
+ spectralNorm'_algebraMap
+ spectralNorm'_eq_of_mem
+ spectralNorm'_eq_zero
+ spectralNorm'_extends
+ spectralNorm'_mul
+ spectralNorm'_neg
+ spectralNorm'_one
+ spectralNorm'_smul
+ spectralNorm'_zero
+ spectralNorm_le
+ spectralNorm_unique
+ spectralRadiusLim
+ spectralRadiusLimNorm_algebraMap
+ spectralRadiusLimNorm_apply
+ spectralRadiusLimNorm_def
+ spectralRadiusLimNorm_extends
+ spectralRadiusLimNorm_one
+ spectralRadiusLim_add_le
+ spectralRadiusLim_le_norm
+ spectralRadiusLim_le_norm_pow
+ spectralRadiusLim_mul_le
+ spectralRadiusLim_neg
+ spectralRadiusLim_nonneg
+ spectralRadiusLim_one
+ spectralRadiusLim_pow
+ spectralRadiusLim_pow_of_ne_zero
+ spectralRadiusLim_smul
+ spectralRadiusLim_zero
+ spectralRadius_eq_spectralRadiusLimit
+ tendsTo_modifyAux
+ tendsto_atBot
+ tendsto_lim
+ tendsto_nhds_unique_of_forall
+ tendsto_spectralRadiusLim
+ tendsto_spectralRadiusLim'
+ toAbsoluteValue
+ toAbsoluteValue_algebraMap
+ toRingNorm_apply
+ toRingSeminorm_apply
++ spectralRadiusLimNorm
- Subadditive

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

Computed after the build finishes.

---

No changes to strong technical debt.

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

Current number	Change	Type (weak)
4950	2	exposed public sections

Current commit 93f23f725c
Reference commit d7f2dbea7d

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Analysis/Normed/Algebra/SpectralRadiusLimit): define the spectral radius limit lim ‖a ^ k‖ ^ (1 / k) #42607
• feat(Topology/Separation/Hausdorff): add tendsto_nhds_unique_of_forall #42986
• [Merged by Bors] - feat(Algebra/Group/Commute/Basic): an element commutes with its inverse #42987
• refactor(Analysis/Normed/Unbundled/SpectralNorm): extract, generalize, and golf uniqueness of power-multiplicative norms #43015
• feat(Analysis/Matrix/Normed): norm of block diagonal matrix #43016
• refactor(Analysis/Normed/Unbundled/SpectralNorm): extract, generalize, and golf algNormFromConst #43019
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.