Commit 2024-10-27 21:51 380f469e

View on Github →

feat: isometric continuous functional calculi (#17837)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

added theorem cfcHom_eq_of_isStarNormal

added theorem inr_comp_cfcₙHom_eq_cfcₙAux

Created Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean

added theorem IsGreatest.nnnorm_cfc

added theorem IsGreatest.nnnorm_cfc_nnreal

added theorem IsGreatest.nnnorm_cfcₙ

added theorem IsGreatest.nnnorm_cfcₙ_nnreal

added theorem IsGreatest.norm_cfc

added theorem IsGreatest.norm_cfcₙ

added theorem apply_le_nnnorm_cfc_nnreal

added theorem apply_le_nnnorm_cfcₙ_nnreal

added theorem isometry_cfcHom

added theorem isometry_cfcₙHom

added theorem nnnorm_apply_le_nnnorm_cfc

added theorem nnnorm_apply_le_nnnorm_cfcₙ

added theorem nnnorm_cfcHom

added theorem nnnorm_cfc_le

added theorem nnnorm_cfc_le_iff

added theorem nnnorm_cfc_nnreal_le

added theorem nnnorm_cfc_nnreal_le_iff

added theorem nnnorm_cfcₙHom

added theorem nnnorm_cfcₙ_le

added theorem nnnorm_cfcₙ_le_iff

added theorem nnnorm_cfcₙ_nnreal_le

added theorem nnnorm_cfcₙ_nnreal_le_iff

added theorem norm_apply_le_norm_cfc

added theorem norm_apply_le_norm_cfcₙ

added theorem norm_cfcHom

added theorem norm_cfc_le

added theorem norm_cfc_le_iff

added theorem norm_cfcₙHom

added theorem norm_cfcₙ_le

added theorem norm_cfcₙ_le_iff

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

added theorem spectrum.coe_le_norm_of_mem

added theorem spectrum.le_nnnorm_of_mem

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

added theorem Unitization.continuous_inr