lintegral_prod_right' — Mathlib

English

If f is AEMeasurable on μ×ν, then x ↦ ∫ f(x,y) dν is AEMeasurable with respect to μ.

Русский

Если f измеримо почти всюду на μ×ν, то ∫ f(x,y) dν по y является AEMeasurable по μ.

LaTeX

$$AEMeasurable f (μ × ν) → AEMeasurable (fun x => ∫ f(x,y) dν) μ$$

Lean4

@[fun_prop, measurability]
theorem lintegral_prod_right' [SFinite ν] {f : α × β → ℝ≥0∞} (hf : AEMeasurable f (μ.prod ν)) :
    AEMeasurable (fun x ↦ ∫⁻ y, f (x, y) ∂ν) μ :=
  by
  obtain ⟨g, hg, hfg⟩ := hf
  refine ⟨fun x ↦ ∫⁻ y, g (x, y) ∂ν, by fun_prop, ?_⟩
  exact (ae_ae_of_ae_prod hfg).mono fun x hfg' ↦ lintegral_congr_ae hfg'

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