integral_integral_sub — Mathlib

English

A variant form of integral subtraction for product kernels with respect to iterated measures.

Русский

Вариант формы вычитания интеграла для произведённых ядер.

LaTeX

$$$\int f - g = \int f - \int g$$$

Lean4

theorem integral_integral_sub ⦃f g : β × γ → E⦄ (hf : Integrable f ((κ ⊗ₖ η) a)) (hg : Integrable g ((κ ⊗ₖ η) a)) :
    ∫ x, ∫ y, f (x, y) - g (x, y) ∂η (a, x) ∂κ a =
      ∫ x, ∫ y, f (x, y) ∂η (a, x) ∂κ a - ∫ x, ∫ y, g (x, y) ∂η (a, x) ∂κ a :=
  (Kernel.integral_fn_integral_sub id hf hg).trans <| integral_sub hf.integral_compProd hg.integral_compProd

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