Commit 2024-07-03 23:30 c52fabcd

View on Github →

feat(ContinuousFunctionalCalculus): add several lemmas involving the CFC and algebraMap (#14065) This PR adds several lemmas about the interaction between the (non-unital) CFC and algebraMap. Several lemmas require some sort of nontriviality statement for the CFC (i.e. the predicate can't be false everywhere), I just stated it as an hp : p 0 hypothesis in the lemma statements; it seems like the most convenient way in practice and probably the easiest to automate.

Estimated changes

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

Modified Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean

added theorem CFC.eq_algebraMap_of_spectrum_subset_singleton

added theorem CFC.eq_one_of_spectrum_subset_one

added theorem CFC.eq_zero_of_spectrum_subset_zero

added theorem CFC.spectrum_algebraMap_eq

added theorem CFC.spectrum_algebraMap_subset

added theorem CFC.spectrum_one_eq

added theorem CFC.spectrum_zero_eq

added theorem cfc_algebraMap

added theorem cfc_apply_one

added theorem cfc_apply_zero

deleted theorem eq_algebraMap_of_spectrum_subset_singleton

deleted theorem eq_one_of_spectrum_subset_one

deleted theorem eq_zero_of_spectrum_subset_zero

Modified Mathlib/Topology/ContinuousFunction/NonUnitalFunctionalCalculus.lean

added theorem CFC.eq_zero_of_quasispectrum_eq_zero

added theorem CFC.quasispectrum_zero_eq

added theorem cfcₙ_apply_zero

deleted theorem eq_zero_of_quasispectrum_eq_zero