feat: refactor and expand lemmas about integration and continuous functional calculus (#26041)

- [x] depends on: #26040 
- [x] depends on: #26045 
- [x] depends on: #26050  
- [x] depends on: #26079 
- [x] depends on: #26058 



Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>

Author: ADedecker