measurable_lintegral — Mathlib

English

If f is measurable and nonnegative, then the map μ ↦ ∫⁻ f dμ is measurable.

Русский

Если f измерима и неотрицательна, то отображение μ ↦ ∫ f dμ измеримо.

LaTeX

$$$\\text{Measurable } f \\rightarrow \\text{Measurable }(\\mu \\mapsto \\int⁻ f \\, d\\mu).$$$

Lean4

@[fun_prop]
theorem measurable_lintegral {f : α → ℝ≥0∞} (hf : Measurable f) : Measurable fun μ : Measure α => ∫⁻ x, f x ∂μ :=
  by
  simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]
  refine .iSup fun n => Finset.measurable_fun_sum _ fun i _ => ?_
  refine Measurable.const_mul ?_ _
  exact measurable_coe ((SimpleFunc.eapprox f n).measurableSet_preimage _)

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