An infinite integral has positive infinite support

Stream: Is there code for X?

[Yaël Dillies]

Is there something like this somewhere? I can only find the other direction docs#lintegral_eq_top_of_measure_eq_top_pos

import measure_theory.integral.set_integral

open ennreal measure_theory
open_locale ennreal
variables {α : Type*} [measurable_space α] {μ : measure α} [is_finite_measure μ]
  {s : set α} {f : α → ℝ≥0∞}

lemma lintegral_eq_top (hf : ae_measurable f (μ.restrict s)) (hs : null_measurable_set s μ) :
  ∫⁻ x, f x ∂μ = ⊤ ↔ 0 < μ {x | f x = ⊤} :=
sorry

[Yaël Dillies]

Or maybe it's just not true?

[Yaël Dillies]

Oh yeah, of course it's not true :face_palm: Take $\frac 1 x$ over $[0, 1]$.