Commit 2025-01-21 01:50 94352f57

View on Github →

feat: show IsGreatest (spectrum ℝ≥0 a) ‖a‖₊ for IsometricContinuousFunctionalCalculus (#20882) This also contains other similar results, and uses it to prove ‖cfc f a‖₊ = f ‖a‖₊ for 0 ≤ a, and monotone f : ℝ≥0 → ℝ≥0.

Estimated changes

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

added theorem IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum

added theorem IsometricContinuousFunctionalCalculus.isGreatest_norm_spectrum

added theorem IsometricContinuousFunctionalCalculus.isGreatest_spectrum

added theorem IsometricContinuousFunctionalCalculus.nnnorm_spectrum_le

added theorem IsometricContinuousFunctionalCalculus.norm_spectrum_le

added theorem IsometricContinuousFunctionalCalculus.spectrum_le

added theorem MonotoneOn.nnnorm_cfc

added theorem MonotoneOn.nnnorm_cfcₙ

added theorem NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum

added theorem NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_norm_quasispectrum

added theorem NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum

added theorem NonUnitalIsometricContinuousFunctionalCalculus.nnnorm_quasispectrum_le

added theorem NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le

added theorem NonUnitalIsometricContinuousFunctionalCalculus.quasispectrum_le