integral_integral_sub_comp — Mathlib

English

Analogous to the additivity results, with subtraction inside the inner integral.

Русский

Аналогично предыдущим результатам для разности внутри двойного интеграла.

LaTeX

$$$$ \\int x \\int y \\,(f(y) - g(y))\\,d\\eta_x(y)\\,d\\kappa a = \\int x \\int y \\! f(y)\\,d\\eta_x(y)\\,d\\kappa a - \\int x \\int y \\! g(y)\\,d\\eta_x(y)\\,d\\kappa a $$$$

Lean4

theorem integral_integral_sub_comp ⦃f g : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a)) (hg : Integrable g ((η ∘ₖ κ) a)) :
    ∫ x, ∫ y, f y - g y ∂η x ∂κ a = ∫ x, ∫ y, f y ∂η x ∂κ a - ∫ x, ∫ y, g y ∂η x ∂κ a :=
  (integral_fn_integral_sub_comp id hf hg).trans <| integral_sub hf.integral_comp hg.integral_comp

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