Commit 2024-08-28 00:04 f9ab5e7a
View on Github →feat(ContinuousFunctionalCalculus): Show that integration commutes with the CFC (#16013)
This PR shows that cfc (fun r => ∫ x, f x r ∂μ) a = ∫ x, cfc (f x) a ∂μ
under appropriate conditions.
The continuity condition given here is enough for most applications (I think) and reasonably easy to apply for the integral representations this is meant for, but I would be open to suggestions.