ae finite function of convergent integral

Stream: Is there code for X?

[Alex Kontorovich]

Lemma: If a function taking values in ennreal has finite integral, then it is finite almost everywhere. Is this in mathlib somewhere? (I wrote out most of the proof -- see below -- before thinking to ask here... But I couldn't figure out how to say: now g is a simple function, so its integral is the measure of s times its value, which is infinite. But maybe there's a better way of doing this?...) Thanks!

import measure_theory.integral.lebesgue

open_locale big_operators

lemma ae_not_top_of_has_finite_integral {α : Type*} {m : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal}
  (h : ∫⁻ (a : α), f a ∂μ < ⊤) :
  ∀ᵐ (a : α) ∂μ,  f a < ⊤  :=
begin
  rw measure_theory.ae_iff,
  set s := {a : α | ¬ f a < ⊤},
  by_contra hs,
  have μ_pos : μ s > 0 := zero_lt_iff.mpr hs,
  let g : α → ennreal := λ a, if a∈s then 1 else 0,
  have : g ≤ f,
  { intros a,
    by_cases ha : a ∈ s,
    { have : ¬ f a < ⊤ := ha,
      rw not_lt_top_iff at this,
      rw this,
      simp, },
    { have : g a = 0,
      { simp only [ite_eq_right_iff, set.mem_set_of_eq, not_lt_top_iff, one_ne_zero],
        have : ¬ ¬ f a < ⊤ := ha,
        push_neg at this,
        intros hfa,
        exact lt_top_iff_ne_top.mp this hfa, },
      rw this,
      simp, }, },
  have int_g_le_int_f : ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ := measure_theory.lintegral_mono this,
  have : ⊤ ≤ ∫⁻ (a : α), g a ∂μ,
  { rw top_le_iff,
    sorry, },
  have int_f_eq_top : ∫⁻ (a : α), f a ∂μ = ⊤,
  { rw ← top_le_iff,
    calc ⊤ ≤ ∫⁻ (a : α), g a ∂μ : this
    ... ≤ ∫⁻ (a : α), f a ∂μ : int_g_le_int_f, },
  exact ennreal.not_lt_top.mpr int_f_eq_top h,
end

[Rémy Degenne]

docs#measure_theory.ae_lt_top

[Alex Kontorovich]

Argh. Seriously? library_search timed out. :(

[Alex J. Best]

You can always set the timeout a bit higher when this happens, https://leanprover-community.github.io/tips_and_tricks.html#memory-and-deterministic-timeout

[Rémy Degenne]

My experience is that as soon as you import measure theory, library_search timing out is pretty much the norm

[Rémy Degenne]

But you could have helped it by writing the hypothesis in the standard form: for ennreal we use ≠ ∞ in hypotheses and < ∞ in conclusions

[Rémy Degenne]

Also your statement did not include any measurability condition. And without a.e.-measurability the integral is zero.

[Rémy Degenne]

Unless that's not the case for lintegral but only for integral... But in any case, we don't have meaningful results for lintegral of non-a.e.-measurable functions.