Commit 2026-08-23 19:23 5b1c3618

View on Github →

refactor: redefine spectralRadius in terms of quasispectrum (#42753)

Estimated changes

Modified Mathlib/Algebra/Algebra/Spectrum/Basic.lean

Modified Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

modified theorem isQuasiregular_zero

added theorem quasispectrum.of_subsingleton

added theorem quasispectrum.zero_eq

added theorem quasispectrum.zero_eq_nonunits

Modified Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

Modified Mathlib/Analysis/CStarAlgebra/Hom.lean

Modified Mathlib/Analysis/CStarAlgebra/Spectrum.lean

Modified Mathlib/Analysis/InnerProductSpace/Rayleigh.lean

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Modified Mathlib/Analysis/Matrix/Spectrum.lean

modified theorem Matrix.spectralRadius_transpose

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

added theorem QuasispectrumRestricts.spectralRadius_eq

added theorem Unitization.spectralRadius_inr

added theorem exists_nnnorm_quasispectrum_eq_spectralRadius

added theorem quasispectrum.isBounded

added theorem quasispectrum.isClosed

modified theorem quasispectrum.isCompact

modified theorem quasispectrum.isCompact_nnreal

added theorem quasispectrum.norm_le_norm_of_mem

added theorem spectralRadius_eq_of_unital

added theorem spectralRadius_le_nnnorm

added theorem spectralRadius_lt_of_forall_quasispectrum_lt

modified theorem spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty

deleted theorem spectrum.spectralRadius_le_nnnorm

modified theorem spectrum.spectralRadius_lt_of_forall_lt_of_nonempty

Modified Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

added theorem WithLp.unitization_ofLp_one

added theorem WithLp.unitization_toLp_one