lintegral_eq_top_of_measure_eq_top_ne_zero

English

If f is a.e. measurable and μ({x | f x = ∞}) ≠ 0, then ∫ f dμ = ∞.

Русский

Если f измеримо почти везде и μ({x: f(x)=∞}) ≠ 0, то ∫ f dμ = ∞.

LaTeX

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

Lean4

theorem lintegral_eq_top_of_measure_eq_top_ne_zero {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hμf : μ {x | f x = ∞} ≠ 0) :
    ∫⁻ x, f x ∂μ = ∞ :=
  eq_top_iff.mpr <|
    calc
      ∞ = ∞ * μ {x | ∞ ≤ f x} := by simp [hμf]
      _ ≤ ∫⁻ x, f x ∂μ := mul_meas_ge_le_lintegral₀ hf ∞

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