Commit 2021-06-13 17:23 2f40f351

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:

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:

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