lintegral_fn_integral_sub_comp — Mathlib

English

Let f, g be γ → E; F: E → ℝ≥0∞; 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 → ℝ≥0∞; если f и g интегрируемы относительно композиции η∘κ, то линтегралы удовлетворяют соответствующему равенству.

LaTeX

$$$$ \\int^{-x} F\\left(\\int y\\,(f(y) - g(y))\\,d\\eta_x(y)\\right)\\,d\\kappa a = \\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 lintegral_fn_integral_sub_comp ⦃f g : γ → E⦄ (F : E → ℝ≥0∞) (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 lintegral_congr_ae ?_
  filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g
  simp [integral_sub h2f h2g]

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