integral_norm_condExpKernel — Mathlib

English

If f is integrable with respect to μ, then a.e. ω, f is integrable with respect to condExpKernel μ m ω.

Русский

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

LaTeX

$$$\\text{Integrable}(f,μ) \\Rightarrow \\text{ae}_{μ}\\bigl(\\omega\\mapsto \\text{Integrable}(f, condExpKernel(μ,m)(\\omega))\\bigr)$$$

Lean4

theorem _root_.MeasureTheory.Integrable.integral_norm_condExpKernel (hf_int : Integrable f μ) :
    Integrable (fun ω => ∫ y, ‖f y‖ ∂condExpKernel μ m ω) μ :=
  by
  nontriviality Ω
  rw [condExpKernel_eq]
  convert
    Integrable.integral_norm_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
      (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ)) using
    1

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