condKernel_ae — Mathlib

English

If f is integrable with respect to ρ, then almost surely a, f( a,·) is integrable with respect to ρ.condKernel a.

Русский

Если f интегрируема по мере ρ, то почти наверху, для почти всех a, функция ω ↦ f(a,ω) интегрируема по ρ.condKernel a.

LaTeX

$$$\\mathrm{Integrable}(f,\\rho) \\Rightarrow \\forall^\\mathrm{ae} a, \\mathrm{Integrable}(\\lambda \\omega. f(a,\\omega), \\rho.condKernel a)$$$

Lean4

theorem condKernel_ae {f : α × Ω → F} (hf_int : Integrable f ρ) :
    ∀ᵐ a ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a) :=
  by
  have hf_ae : AEStronglyMeasurable f ρ := hf_int.1
  rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int
  exact hf_int.1

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