aestronglyMeasurable_comp₂ — Mathlib

English

Let f ≥ 0 be a measurable function. The density-weighted strong measurability of g with respect to μ.withDensity f is equivalent to the strong measurability of (f)·g with respect to μ.

Русский

Пусть f ≥ 0 измерима. Тогда сильная измеримость g относительно μ.withDensity f эквивалентна сильной измеримости (f)·g относительно μ.

LaTeX

$$$ AEStronglyMeasurable\\, g \\; (μ.withDensity f) \\iff AEStronglyMeasurable\\, ((f) \\cdot g) \\; μ $$$

Lean4

theorem aestronglyMeasurable_comp₂ (L : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F} (hf : AEStronglyMeasurable f μ)
    (hg : AEStronglyMeasurable g μ) : AEStronglyMeasurable (fun x => L (f x) (g x)) μ :=
  L.continuous₂.comp_aestronglyMeasurable₂ hf hg

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