integral_fn_integral_add — Mathlib

English

For f,g: β×γ→E integrable, and F:E→ ENNReal, the lintegral of F applied to f−g equals the lintegral of F applied to f and g separately with the subtraction inside.

Русский

Для f,g: β×γ→E интегрируемых и F:E→NNReal, линтерегральная формула для F(f−g) равна линтерегральной форме для F(f)−F(g).

LaTeX

$$$\int⁻ f(z) d(κ ⊗ η)a = \int⁻ F(f(x,y) - g(x,y)) dκ a$$$

Lean4

theorem integral_fn_integral_add ⦃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_add h2f h2g]

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