ae_integrable_condKernel_iff — Mathlib

English

For AES-trongly measurable f, the a.e. integrability of sections and the integrability of the norm are equivalent to integrability of f.

Русский

Для AES-сильносмеримой f almost everywhere интегрируемость секций и интегрируемость нормы эквивалентны интегрируемости f.

LaTeX

$$$\\mathrm{AEStronglyMeasurable}(f,\\rho) \\Rightarrow (\\forall^\\mathrm{ae} a, \\mathrm{Integrable}(f(a,\\cdot), \\rho.condKernel a)) \\land \\mathrm{Integrable}\\left(a \\mapsto \\int_\\omega \\|f(a,\\omega)\\| \\, d\\rho.condKernel a\\right)\\rho.fst \\iff \\mathrm{Integrable}(f,\\rho)$$$

Lean4

theorem ae_integrable_condKernel_iff {f : α × Ω → F} (hf : AEStronglyMeasurable f ρ) :
    (∀ᵐ a ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)) ∧
        Integrable (fun a ↦ ∫ ω, ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
      Integrable f ρ :=
  by
  rw [← ρ.disintegrate ρ.condKernel] at hf
  conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
  rw [Measure.integrable_compProd_iff hf]

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