continuousOn_primitive_Icc — Mathlib

English

If the family f_i has summable norm on a compact interval, then the sum and the interval integral commute: ∑ ∫ f_i = ∫ tsum f_i.

Русский

Если сумма норм ограничений по компактному интервалу сходится, то сумма по интервалу и интеграл от суммы совпадают.

LaTeX

$$$\\text{HasSum}\\bigl(\\int_{a}^{b} f_i(t) \\,dt\\bigr) = \\int_{a}^{b} \\sum_i f_i(t) \\,dt$$$

Lean4

theorem continuousOn_primitive_Icc (h_int : IntegrableOn f (Icc a b) μ) :
    ContinuousOn (fun x => ∫ t in Icc a x, f t ∂μ) (Icc a b) :=
  by
  have aux : (fun x => ∫ t in Icc a x, f t ∂μ) = fun x => ∫ t in Ioc a x, f t ∂μ :=
    by
    ext x
    exact integral_Icc_eq_integral_Ioc
  rw [aux]
  exact continuousOn_primitive h_int

Похожие утверждения