feat(measure_theory): continuity of primitives (#7864)
From the sphere eversion project
This proves some continuity of interval integrals with respect to parameters and continuity of primitives of measurable functions. The statements are a bit abstract, but they allow to have:
```lean
example {f : ℝ → E} (h_int : integrable f) (a : ℝ) :
continuous (λ b, ∫ x in a .. b, f x ∂ volume) :=
h_int.continuous_primitive a
```
under the usual assumptions on `E`: `normed_group E`, `second_countable_topology E`, `normed_space ℝ E`
`complete_space E`, `measurable_space E`, `borel_space E`, say `E = ℝ` for instance. Of course global integrability is not needed, assuming integrability on all finite length intervals is enough:
```lean
example {f : ℝ → E} (h_int : ∀ a b : ℝ, interval_integrable f volume a b) (a : ℝ) :
continuous (λ b, ∫ x in a .. b, f x ∂ volume) :=
continuous_primitive h_int a
```
