integral_condDistrib — Mathlib

English

If f is AEStronglyMeasurable on μ and condDistrib Y X μ is used, then the map a ↦ ∫ f(a, y) d condDistrib(Y,X,μ)(a) is AEStronglyMeasurable on μ.map X.

Русский

Пусть f сильно измеримо в форме AES на μ; тогда функция a ↦ ∫ f(a, y) d condDistrib(Y,X,μ)(a) измерима относительно μ.map X.

LaTeX

$$$$\\text{AEStronglyMeasurable}(f, μ) \\implies \\text{AEStronglyMeasurable}(a \\mapsto \\int f(a,y) \\partial \\mathrm{condDistrib}(Y,X,μ)(a)\\, dy, μ.map X).$$$$

Lean4

theorem _root_.MeasureTheory.StronglyMeasurable.integral_condDistrib (hf : StronglyMeasurable f) :
    StronglyMeasurable (fun x ↦ ∫ y, f (x, y) ∂condDistrib Y X μ x) := by rw [condDistrib];
  exact hf.integral_kernel_prod_right'

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