continuous_primitive — Mathlib

English

If f_i are integrable and the dominating condition holds, then the integral interchange with tsum is valid: HasSum (∫ f_i) = ∫ tsum f_i.

Русский

Если f_i интегрируемы и соблюдается ограничение, то обмен интеграла и суммирования допустим: HasSum(∫ f_i) = ∫ tsum f_i.

LaTeX

$$$\\text{HasSum}\\left(\\lambda i, \\int f_i\\right) = \\int \\left(\\sum_i f_i\\right)$$$

Lean4

nonrec theorem _root_.MeasureTheory.Integrable.continuous_primitive (h_int : Integrable f μ) (a : ℝ) :
    Continuous fun b => ∫ x in a..b, f x ∂μ :=
  continuous_primitive (fun _ _ => h_int.intervalIntegrable) a

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