integrable_compProd_snd_iff — Mathlib

English

Variant of the previous theorem using F as identity, yielding the same additivity of inner integrals.

Русский

Вариант предыдущей теоремы с F как тождественной функцией даёт ту же аддитивность вложенных интегралов.

LaTeX

$$$$ \\int x \\int y (f(y) + g(y)) dη_x(y) dκ a = \\int x \\int y f(y) dη_x(y) dκ a + \\int x \\int y g(y) dη_x(y) dκ a $$$$

Lean4

theorem integrable_compProd_snd_iff [SFinite μ] [IsSFiniteKernel κ] (hf : AEStronglyMeasurable f (κ ∘ₘ μ)) :
    Integrable (fun p ↦ f p.2) (μ ⊗ₘ κ) ↔ Integrable f (κ ∘ₘ μ) :=
  by
  rw [← Measure.snd_compProd, Measure.snd, integrable_map_measure _ measurable_snd.aemeasurable, Function.comp_def]
  rwa [← Measure.snd, Measure.snd_compProd]

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