integral_fn_integral_sub_comp — Mathlib

English

Let f, g be γ → E; let F: E → E' be a map; if f and g are integrable with respect to (η ∘ₖ κ) a, then ∫x F(∫y (f(y) − g(y)) dηx(y)) dκa = ∫x F(∫y f(y) dηx(y) − ∫y g(y) dηx(y)) dκa.

Русский

Пусть f, g : γ → E; F: E → E'; если f и g интегрируемы относительно композиции η∘κ, то ∫x F(∫y (f(y) − g(y)) dηx(y)) dκa = ∫x F(∫y f(y) dηx(y) − ∫y g(y) dηx(y)) dκa.

LaTeX

$$$$ \\int x\, F\\left(\\int y\\,(f(y) - g(y))\,d\\eta_x(y)\\right)\\,d\\kappa a \n= \\int x\, F\\left(\\int y\\,f(y)\\,d\\eta_x(y) - \\int y\\,g(y)\\,d\\eta_x(y)\\right)\\,d\\kappa a $$$$

Lean4

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

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