lintegral_fn_integral_sub — Mathlib

English

If f,g are integrable on the product kernel, the integral of f−g equals the integral of f minus the integral of g with respect to the iterated kernels.

Русский

Если f,g интегрируемы, то интеграл от f−g равен разности интегралов.

LaTeX

$$$\int x\,\int y\,(f-g)(x,y) dy dκ a = \int x\,\int y f(x,y) dy dη - \int x\,\int y g(x,y) dy dκ$$

Lean4

theorem lintegral_fn_integral_sub ⦃f g : β × γ → E⦄ (F : E → ℝ≥0∞) (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 lintegral_congr_ae ?_
  filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g
  simp [integral_sub h2f h2g]

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