English
If F: X → ℝ → E is such that F x is ae-measurable and dominated, then the interval integral is continuous within a set.
Русский
Если F x измерима почти всюду и ограничена, то интеграл по интервалу непрерывен внутри множества.
LaTeX
$$$\\text{ContinuousWithinAt}\\bigl(\\lambda x, \\int t in a..b, F x t \\,dt\\bigr)\\, s\\, x_0$$$
Lean4
theorem continuousOn_primitive (h_int : IntegrableOn f (Icc a b) μ) :
ContinuousOn (fun x => ∫ t in Ioc a x, f t ∂μ) (Icc a b) :=
by
by_cases h : a ≤ b
· have : ∀ x ∈ Icc a b, ∫ t in Ioc a x, f t ∂μ = ∫ t in a..x, f t ∂μ :=
by
intro x x_in
simp_rw [integral_of_le x_in.1]
rw [continuousOn_congr this]
intro x₀ _
refine continuousWithinAt_primitive (measure_singleton x₀) ?_
simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, max_eq_right, h, min_self]
exact h_int.mono Ioc_subset_Icc_self le_rfl
· rw [Icc_eq_empty h]
exact continuousOn_empty _
