aemeasurable_lintegral — Mathlib

English

If f is AEMeasurable with respect to m.join, then the map μ ↦ ∫ f a dμ is AEMeasurable with respect to m.

Русский

Если f является AEMeasurable относительно m.join, то μ ↦ ∫ f dμ является AEMeasurable относительно m.

LaTeX

$$$\\text{AEMeasurable } f\\ m.join \\rightarrow AEMeasurable (\\lambda \\mu. \\int⁻ a, f a \\partial\\mu)\\ m.$$$

Lean4

theorem aemeasurable_lintegral {m : Measure (Measure α)} {f : α → ℝ≥0∞} (h : AEMeasurable f m.join) :
    AEMeasurable (fun μ ↦ ∫⁻ a, f a ∂μ) m :=
  let ⟨g, hgm, hfg⟩ := h
  ⟨fun μ ↦ ∫⁻ a, g a ∂μ, measurable_lintegral hgm, (ae_ae_of_ae_join hfg).mono fun _ ↦ lintegral_congr_ae⟩

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