Commit 2025-09-22 18:40 f914ea54

View on Github →

feat: range of the continuous functional calculus (#29561) This shows that the range of the continuous functional calculus is the elemental star algebra generated by the given element. In addition, we show that b commutes with cfc f a whenever it commutes with both a and star a. When a is selfadjoint, we can drop the latter hypothesis. Finally, we also show that the product of nonnegative elements is nonnegative if they commute.

Estimated changes

added theorem Commute.mul_nonneg
added theorem cfc_complex_eq_real
modified theorem cfc_nnreal_eq_real
added theorem cfc_real_eq_nnreal
added theorem cfcₙ_complex_eq_real
modified theorem cfcₙ_nnreal_eq_real
added theorem cfcₙ_real_eq_nnreal
added theorem range_cfc
added theorem range_cfcHom
added theorem range_cfc_nnreal
added theorem range_cfcₙ
added theorem range_cfcₙHom
added theorem range_cfcₙ_nnreal