restrict — Mathlib

English

If f is AEStronglyMeasurable and the bound holds for all finite-measure sets, then f is integrable with μ.

Русский

Если f AEStronglyMeasurable и условие границы выполняется для всех множеств конечной меры, то f интегрируемо по μ.

LaTeX

$$$ (hf_meas: \\operatorname{AEStronglyMeasurable} f \\mu) \\; (hf: \\forall s, \\operatorname{MeasurableSet} s \\rightarrow \\mu s \\neq \\infty \\rightarrow \\int_{s} \\|f\\|_e \\partial\\mu \\le C) \\Rightarrow \\operatorname{Integrable} f \\mu$$

Lean4

/-- One should usually use `MeasureTheory.Integrable.integrableOn` instead. -/
theorem restrict (hf : Integrable f μ) {s : Set α} : Integrable f (μ.restrict s) :=
  hf.mono_measure Measure.restrict_le_self

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