measure_eq_top_of_setLIntegral_ne_top

English

Let f be a function on α with values in the extended nonnegative reals, and s a measurable set. If f is almost everywhere measurable with respect to μ restricted to s and the setwise L-integral over s is finite, then the subset of s where f takes the value ∞ has measure zero.

Русский

Пусть f : α → ℝ≥0∞ и s ⊆ α измеримо. Если f измеримо почти всюду относительно μ|s и интеграл по s конечен, то множество {x ∈ s | f(x) = ∞} имеет меру ноль.

LaTeX

$$$AEMeasurable\\ f\\ (\\mu\\restriction s) \\wedge \\int^{\\; -}_{x\\in s} f(x)\\,\\partial\\mu \\neq \\infty \\Rightarrow \\mu\\{x\\in s\\;|\\; f(x)=\\infty\\}=0$$$

Lean4

theorem measure_eq_top_of_setLIntegral_ne_top {f : α → ℝ≥0∞} {s : Set α} (hf : AEMeasurable f (μ.restrict s))
    (hμf : ∫⁻ x in s, f x ∂μ ≠ ∞) : μ ({x ∈ s | f x = ∞}) = 0 :=
  of_not_not fun h => hμf <| setLIntegral_eq_top_of_measure_eq_top_ne_zero hf h

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