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.

Estimated changes