integral_kernel_prod_right'' — Mathlib

English

Integrals with respect to kernels are linear in the integrand; a version of Fubini applies when swapping order of integration across product kernels.

Русский

Интегралы по ящикам ядер линейны по интегрантам; применяется версия Фубини для перестановки порядка интегрирования при произведении ядер.

LaTeX

$$$\\int (a f + b g) \\, d\\kappa = a\\int f \\, d\\kappa + b\\int g \\, d\\kappa$$$

Lean4

theorem integral_kernel_prod_right'' {f : β × γ → E} (hf : StronglyMeasurable f) :
    StronglyMeasurable fun x => ∫ y, f (x, y) ∂η (a, x) :=
  by
  change StronglyMeasurable ((fun x => ∫ y, (fun u : (α × β) × γ => f (u.1.2, u.2)) (x, y) ∂η x) ∘ fun x => (a, x))
  apply StronglyMeasurable.comp_measurable _ (measurable_prodMk_left (m := mα))
  · have :=
      MeasureTheory.StronglyMeasurable.integral_kernel_prod_right' (κ := η)
        (hf.comp_measurable (measurable_fst.snd.prodMk measurable_snd))
    simpa using this

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