compProd_mk_left — Mathlib

English

Analogous to the previous, Kernel.sum η i composed with κ equals Kernel.sum (i ↦ κ ⊗ η_i).

Русский

Аналогично: сумма η_i по i превращается в κ ⊗ η_i.

LaTeX

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

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.compProd_mk_left {δ : Type*} [TopologicalSpace δ] {f : β × γ → δ}
    (hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) : ∀ᵐ x ∂κ a, AEStronglyMeasurable (fun y => f (x, y)) (η (a, x)) := by
  filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with x hx using
    ⟨fun y => hf.mk f (x, y), hf.stronglyMeasurable_mk.comp_measurable measurable_prodMk_left, hx⟩

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