Commit 2024-03-09 11:33 bf263ff8

View on Github →

feat: instantiate the continuous functional calculus (#10779) This adds instances of the continuous functional calculus for unital C⋆-algebras for normal, selfadjoint, and positive elements.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean

added theorem IsSelfAdjoint.continuousFunctionalCalculus_of_compactSpace_spectrum

added theorem IsSelfAdjoint.spectrumRestricts

added theorem IsSelfAdjoint.sq_spectrumRestricts

added theorem SpectrumRestricts.eq_zero_of_neg

added theorem SpectrumRestricts.isSelfAdjoint

added theorem SpectrumRestricts.nnreal_add

added theorem SpectrumRestricts.nnreal_iff_nnnorm

added theorem SpectrumRestricts.smul_of_nonneg

added theorem isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts

added theorem mem_unitary_of_spectrum_subset_circle

added theorem nonneg_iff_isSelfAdjoint_and_spectrumRestricts

added theorem spectrum_star_mul_self_nonneg

added theorem spectrum_subset_circle_of_mem_unitary

added theorem unitary_iff_isStarNormal_and_spectrum_subset_circle

Modified Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean

deleted theorem eq_algebraMap_of_spectrum_singleton

added theorem eq_algebraMap_of_spectrum_subset_singleton

deleted theorem eq_one_of_spectrum_eq_one

added theorem eq_one_of_spectrum_subset_one

deleted theorem eq_zero_of_spectrum_eq_zero

added theorem eq_zero_of_spectrum_subset_zero