setLIntegral_eq_top_of_measure_eq_top_ne_zero

English

If f is a.e. measurable on s and μ({x ∈ s | f x = ∞}) ≠ 0, then the restricted lintegral over s equals ∞.

Русский

Если f измеримо почти на s и μ({x∈s: f(x)=∞}) ≠ 0, то интеграл на s бесконечен.

LaTeX

$$$$ \int⁻ x in s, f x ∂μ = ∞. $$$$

Lean4

theorem setLIntegral_eq_top_of_measure_eq_top_ne_zero {f : α → ℝ≥0∞} {s : Set α} (hf : AEMeasurable f (μ.restrict s))
    (hμf : μ ({x ∈ s | f x = ∞}) ≠ 0) : ∫⁻ x in s, f x ∂μ = ∞ :=
  lintegral_eq_top_of_measure_eq_top_ne_zero hf <|
    mt (eq_bot_mono <| by rw [← setOf_inter_eq_sep]; exact Measure.le_restrict_apply _ _) hμf

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