integral_fn_integral_sub — Mathlib

English

If f,g are integrable on the product kernel, then the integral of F applied to f+g equals the sum of the integrals with F applied to each, i.e., an additivity property of the integral over sums.

Русский

Если f,g интегрируемы, то интеграл от F(f+g) равен интегралу от F(f) плюс интеграл от F(g).

LaTeX

$$$\\int x\, F\\bigl(\\int y\\,(f+g)(x,y) dη(a,x)\\bigr) dκ a = \\int x\\, F\\bigl(\\int y f(x,y) dη(a,x)\\bigr) dκ a + \\int x\\, F\\bigl(\\int y g(x,y) dη(a,x)\\bigr) dκ a$$$

Lean4

theorem integral_fn_integral_sub ⦃f g : β × γ → E⦄ (F : E → E') (hf : Integrable f ((κ ⊗ₖ η) a))
    (hg : Integrable g ((κ ⊗ₖ η) a)) :
    ∫ x, F (∫ y, f (x, y) - g (x, y) ∂η (a, x)) ∂κ a =
      ∫ x, F (∫ y, f (x, y) ∂η (a, x) - ∫ y, g (x, y) ∂η (a, x)) ∂κ a :=
  by
  refine integral_congr_ae ?_
  filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
  simp [integral_sub h2f h2g]

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