lintegral_eq_zero_iff' without Markov/monotone convergence

Stream: mathlib4

[Jeremy Tan]

I have proved MeasureTheory.lintegral_eq_zero_iff' without appealing to Markov's inequality or monotone convergence, as the current version of the statement does.

diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean
index d9b762bac90..8d0e1fb7e55 100644
--- a/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean
+++ b/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean
@@ -272,6 +272,37 @@ theorem setLIntegral_congr_fun {f g : α → ℝ≥0∞} {s : Set α} (hs : Meas
   rw [EventuallyEq]
   rwa [ae_restrict_iff' hs]

+/-- The integral of an a.e. measurable function is zero iff the function is a.e. zero.
+Proof by Deven Ware, https://math.stackexchange.com/a/219744 -/
+@[simp]
+theorem lintegral_eq_zero_iff'' {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
+    ∫⁻ a, f a ∂μ = 0 ↔ f =ᵐ[μ] 0 := by
+  refine ⟨fun h ↦ ?_, fun h ↦ (lintegral_congr_ae h).trans lintegral_zero⟩
+  contrapose! h
+  replace h : 0 < μ {x | 0 < f x} := by
+    rw [eventuallyEq_iff_all_subsets] at h
+    push_neg at h
+    obtain ⟨s, hs⟩ := h
+    rw [not_eventually, frequently_ae_iff] at hs
+    simp_rw [Pi.zero_apply, Classical.not_imp, ← zero_lt_iff] at hs
+    exact hs.trans_le (measure_mono (by simp))
+  have un : {x | 0 < f x} = ⋃ n : ℕ, {x | (n + 1 : ℝ≥0∞)⁻¹ < f x} := by
+    ext x; simp only [mem_setOf_eq, mem_iUnion]
+    constructor <;> intro h'
+    · rw [zero_lt_iff] at h'
+      obtain ⟨n, npos, hn⟩ := exists_nat_pos_inv_mul_lt (one_ne_top) h'
+      rw [mul_one] at hn; use n - 1; rwa [natCast_sub, Nat.cast_one, tsub_add_cancel_of_le]
+      rw [Nat.one_le_cast]; omega
+    · obtain ⟨n, hn⟩ := h'; exact lt_trans (by simp) hn
+  rw [un, zero_lt_iff, ne_eq, measure_iUnion_null_iff] at h; push_neg at h
+  obtain ⟨n, hn⟩ := h; rw [← zero_lt_iff] at hn ⊢
+  calc
+    _ ≥ ∫⁻ a in {x | (↑n + 1)⁻¹ < f x}, f a ∂μ := setLIntegral_le_lintegral _ _
+    _ ≥ ∫⁻ a in {x | (↑n + 1)⁻¹ < f x}, (↑n + 1)⁻¹ ∂μ := by
+      exact setLIntegral_mono_ae hf.restrict (ae_of_all μ fun x hx ↦ hx.le)
+    _ = (n + 1 : ℝ≥0∞)⁻¹ * μ {x | (↑n + 1)⁻¹ < f x} := by exact setLIntegral_const _ _
+    _ > _ := mul_pos_iff.mpr ⟨by simp, hn⟩
+
 /-- **Monotone convergence theorem** -- sometimes called **Beppo-Levi convergence**.
 See `lintegral_iSup_directed` for a more general form. -/
 theorem lintegral_iSup {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, Measurable (f n)) (h_mono : Monotone f) :

Can we golf this?

[Sébastien Gouëzel]

You are exactly reproving Markov inequality in this argument, so I'm not sure what the gain is.

[Jeremy Tan]

@Sébastien Gouëzel The context is #23860 regarding my splitting of Integral.Lebesgue.Basic

[Jeremy Tan]

The current version of lintegral_eq_zero_iff' relies on Markov's inequality, which in turn relies on addition of Lebesgue integrals, which in turn again relies on monotone convergence

[Jeremy Tan]

lintegral_eq_zero_iff' and friends are needed in quite a few files, so as it stands in #23860, there are quite a few import bumps

[Jeremy Tan]

Can you review that PR please?

[Jeremy Tan]

It would be better for the split if lintegral_eq_zero_iff' did not need Markov or monotone convergence

[Sébastien Gouëzel]

Are you saying that having lintegral_eq_zero_iff' available early is helpful for developing the theory without appealing to Markov inequality? Or could we just put it in the file with Markov inequality without creating issues?

Your proof goes through Markov inequality, so it shows this is the natural argument. If we can live with it, this looks better to me: a streamlined proof is always better than a hand-made proof reproving a classical argument. But if it really helps the flow of arguments, we can go for your hand-made proof, sure!

[Sébastien Gouëzel]

Oops, you've already answered my question.

[Jeremy Tan]

Umm, what now

[Sébastien Gouëzel]

So, if your proof helps streamline the flow and minimize imports, we can definitely go with it.

[Sébastien Gouëzel]

To clean up your proof, can you use a generic positive sequence tending to zero, instead of 1 / (n + 1)? This is almost always cleaner. Such a sequence is provided by exists_seq_strictAnti_tendsto'.

[Rémy Degenne]

Slight golf of your proof, and adaptation to use the lemma Sébastien suggests:

import Mathlib
open MeasureTheory Filter Set ENNReal

@[simp]
theorem lintegral_eq_zero_iff'' {α : Type*} {_ : MeasurableSpace α} {μ : Measure α}
    {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
    ∫⁻ a, f a ∂μ = 0 ↔ f =ᵐ[μ] 0 := by
  refine ⟨fun h ↦ ?_, fun h ↦ (lintegral_congr_ae h).trans lintegral_zero⟩
  contrapose! h
  replace h : 0 < μ {x | 0 < f x} := by
    rw [EventuallyEq, ae_iff] at h
    simpa [zero_lt_iff] using zero_lt_iff.mpr h
  obtain ⟨u, _, hu_mem, hu_tendsto⟩ := exists_seq_strictAnti_tendsto' zero_lt_top
  have un : {x | 0 < f x} = ⋃ n : ℕ, {x | u n < f x} := by
    ext x
    simp only [mem_setOf_eq, mem_iUnion]
    constructor <;> intro h'
    · exact (hu_tendsto.eventually_lt_const h').exists
    · obtain ⟨n, hn⟩ := h'
      exact (hu_mem n).1.trans hn
  rw [un, zero_lt_iff, ne_eq, measure_iUnion_null_iff] at h
  push_neg at h
  obtain ⟨n, hn⟩ := h
  rw [← zero_lt_iff] at hn ⊢
  calc
    _ ≥ ∫⁻ a in {x | u n < f x}, f a ∂μ := setLIntegral_le_lintegral _ _
    _ ≥ ∫⁻ a in {x | u n < f x}, u n ∂μ :=
      setLIntegral_mono_ae hf.restrict (ae_of_all μ fun x hx ↦ hx.le)
    _ = u n * μ {x | u n < f x} := setLIntegral_const _ _
    _ > _ := mul_pos_iff.mpr ⟨(hu_mem n).1, hn⟩

[Yaël Dillies]

Why can't you turn this proof into a low imports proof of Markov's inequality?

[Rémy Degenne]

You can. I have not looked at the proposed refactor: are there big imports gains there, or are we changing proofs to shave one or two files in the imports? I am not sure all of this is worth it.

[Jeremy Tan]

@Sébastien Gouëzel @Rémy Degenne #23947