aestronglyMeasurable_integral_condExpKernel

English

If f is AEStronglyMeasurable, then the ω-average of ∫ f d condExpKernel μ m ω is AEStronglyMeasurable (nontriviality assumed).

Русский

Если f — AEStronglyMeasurable, то интеграл по ядру condExpKernel также AEStronglyMeasurable почти наверху по ω.

LaTeX

$$$\\text{AEStronglyMeasurable}(f)\\Rightarrow \\text{AEStronglyMeasurable}_{μ}(\\omega\\mapsto \\int y\\; f(y)\\; d condExpKernel(\\mu,m)(\\omega))$$$

Lean4

theorem aestronglyMeasurable_integral_condExpKernel [NormedSpace ℝ F] (hf : AEStronglyMeasurable f μ) :
    AEStronglyMeasurable[m] (fun ω => ∫ y, f y ∂condExpKernel μ m ω) μ :=
  by
  nontriviality Ω
  rw [condExpKernel_eq]
  have h :=
    aestronglyMeasurable_integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
      (hf.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
  rw [MeasurableSpace.comap_id] at h
  exact h.mono inf_le_left

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