English
Let the spaces X_i carry σ-finite measurable structures, and let s be a finite subset of indices. For a function f: ∏_i X_i → ℝ≥0∞ that is measurable, the marginal integral over s, viewed as a function of the whole argument x = (x_i)_i, is itself a measurable function. In particular, x ↦ ∫⋯∫⁻_s f ∂μ is measurable.
Русский
Пусть для индексов i задано семейство измеримых пространств X_i с σ-конечными мерами μ_i. Пусть s — конечный подмножество индексов. Пусть f: ∏_i X_i → ℝ≥0∞ измерима. Тогда маргинальное интегрирование по s, рассматриваемое как функция от полной кортежа x = (x_i)_i, также измеримо. То есть x ↦ ∫⋯∫⁻_s f ∂μ является измеримой функцией.
LaTeX
$$$\\text{Measurable}(f) \\Rightarrow \\text{Measurable}(\\mathrm{lmarginal}_{\\mu}(s,f))$$$
Lean4
theorem _root_.Measurable.lmarginal [∀ i, SigmaFinite (μ i)] (hf : Measurable f) : Measurable (∫⋯∫⁻_s, f ∂μ) :=
by
refine Measurable.lintegral_prod_right ?_
refine hf.comp ?_
rw [measurable_pi_iff]; intro i
by_cases hi : i ∈ s
· simpa [hi, updateFinset] using measurable_pi_iff.1 measurable_snd _
· simpa [hi, updateFinset] using measurable_pi_iff.1 measurable_fst _
