integral_kernel_compProd — Mathlib

English

Another instance of the left-sum compatibility: Kernel.sum κ ⊗ η equals Kernel.sum (i ↦ κ_i ⊗ η).

Русский

Ещё одно совместимое разложение слева: сумма κ_i ⊗ η.

LaTeX

$$$$ \\mathrm{Kernel.sum}\\ κ \\otimes_{\\kern-0.2em} η = \\mathrm{Kernel.sum}\\ i \\; (κ_i \\otimes_{\\kern-0.2em} η). $$$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd [NormedSpace ℝ E] ⦃f : β × γ → E⦄
    (hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) : AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂η (a, x)) (κ a) :=
  ⟨fun x => ∫ y, hf.mk f (x, y) ∂η (a, x), hf.stronglyMeasurable_mk.integral_kernel_prod_right'', by
    filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ hx using integral_congr_ae hx⟩

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