feat(MeasureTheory.Function.AEEqOfIntegral): characterize a locally i…

…ntegrable function by its integral on compact sets (#5876)

We show that, if a locally integrable function has zero integral on all compact sets, then it vanishes almost everywhere.

Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

@@ -46,7 +46,7 @@ Generally useful lemmas which are not related to integrals:
 
 open MeasureTheory TopologicalSpace NormedSpace Filter
 
-open scoped ENNReal NNReal MeasureTheory
+open scoped ENNReal NNReal MeasureTheory Topology
 
 namespace MeasureTheory
 
@@ -541,6 +541,63 @@ theorem Integrable.ae_eq_of_forall_set_integral_eq (f g : α → E) (hf : Integr
   exact Integrable.ae_eq_zero_of_forall_set_integral_eq_zero (hf.sub hg) hfg'
 #align measure_theory.integrable.ae_eq_of_forall_set_integral_eq MeasureTheory.Integrable.ae_eq_of_forall_set_integral_eq
 
+variable {β : Type _} [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β]
+
+/-- If an integrable function has zero integral on all closed sets, then it is zero
+almost everwhere.-/
+lemma ae_eq_zero_of_forall_set_integral_isClosed_eq_zero {μ : Measure β} {f : β → E}
+    (hf : Integrable f μ) (h'f : ∀ (s : Set β), IsClosed s → ∫ x in s, f x ∂μ = 0) :
+    f =ᵐ[μ] 0 := by
+  suffices : ∀ s, MeasurableSet s → ∫ x in s, f x ∂μ = 0
+  · exact hf.ae_eq_zero_of_forall_set_integral_eq_zero (fun s hs _ ↦ this s hs)
+  have A : ∀ (t : Set β), MeasurableSet t → ∫ (x : β) in t, f x ∂μ = 0
+      → ∫ (x : β) in tᶜ, f x ∂μ = 0 := by
+    intro t t_meas ht
+    have I : ∫ x, f x ∂μ = 0 := by rw [← integral_univ]; exact h'f _ isClosed_univ
+    simpa [ht, I] using integral_add_compl t_meas hf
+  intro s hs
+  refine MeasurableSet.induction_on_open (fun U hU ↦ ?_) A (fun g g_disj g_meas hg ↦ ?_) hs
+  · rw [← compl_compl U]
+    exact A _ hU.measurableSet.compl (h'f _ hU.isClosed_compl)
+  · rw [integral_iUnion g_meas g_disj hf.integrableOn]
+    simp [hg]
+
+/-- If an integrable function has zero integral on all compact sets in a sigma-compact space, then
+it is zero almost everwhere. -/
+lemma ae_eq_zero_of_forall_set_integral_isCompact_eq_zero
+    [SigmaCompactSpace β] [T2Space β] {μ : Measure β} {f : β → E} (hf : Integrable f μ)
+    (h'f : ∀ (s : Set β), IsCompact s → ∫ x in s, f x ∂μ = 0) :
+    f =ᵐ[μ] 0 := by
+  apply ae_eq_zero_of_forall_set_integral_isClosed_eq_zero hf (fun s hs ↦ ?_)
+  let t : ℕ → Set β := fun n ↦ compactCovering β n ∩ s
+  suffices H : Tendsto (fun n ↦ ∫ x in t n, f x ∂μ) atTop (𝓝 (∫ x in s, f x ∂μ))
+  · have A : ∀ n, ∫ x in t n, f x ∂μ = 0 :=
+      fun n ↦ h'f _ (IsCompact.inter_right (isCompact_compactCovering β n) hs)
+    simp_rw [A, tendsto_const_nhds_iff] at H
+    exact H.symm
+  have B : s = ⋃ n, t n := by rw [← Set.iUnion_inter, iUnion_compactCovering, Set.univ_inter]
+  rw [B]
+  apply tendsto_set_integral_of_monotone
+  · intros n
+    exact ((isCompact_compactCovering β n).inter_right hs).isClosed.measurableSet
+  · intros m n hmn
+    exact Set.inter_subset_inter_left _ (compactCovering_subset β hmn)
+  · exact hf.integrableOn
+
+/-- If a locally integrable function has zero integral on all compact sets in a sigma-compact space,
+then it is zero almost everwhere. -/
+lemma ae_eq_zero_of_forall_set_integral_isCompact_eq_zero'
+    [SigmaCompactSpace β] [T2Space β] {μ : Measure β} {f : β → E} (hf : LocallyIntegrable f μ)
+    (h'f : ∀ (s : Set β), IsCompact s → ∫ x in s, f x ∂μ = 0) :
+    f =ᵐ[μ] 0 := by
+  rw [← Measure.restrict_univ (μ := μ), ← iUnion_compactCovering]
+  apply (ae_restrict_iUnion_iff _ _).2 (fun n ↦ ?_)
+  apply ae_eq_zero_of_forall_set_integral_isCompact_eq_zero
+  · exact hf.integrableOn_isCompact (isCompact_compactCovering β n)
+  · intro s hs
+    rw [Measure.restrict_restrict hs.measurableSet]
+    exact h'f _ (hs.inter (isCompact_compactCovering β n))
+
 end AeEqOfForallSetIntegralEq
 
 section Lintegral

Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

@@ -73,24 +73,63 @@ theorem LocallyIntegrableOn.integrableOn_compact_subset (hf : LocallyIntegrableO
   (hf.mono hst).integrableOn_isCompact ht
 #align measure_theory.locally_integrable_on.integrable_on_compact_subset MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset
 
-theorem LocallyIntegrableOn.aestronglyMeasurable [SecondCountableTopology X]
-    (hf : LocallyIntegrableOn f s μ) : AEStronglyMeasurable f (μ.restrict s) := by
+/-- If a function `f` is locally integrable on a set `s` in a second countable topological space,
+then there exist countably many open sets `u` covering `s` such that `f` is integrable on each
+set `u ∩ s`. -/
+theorem LocallyIntegrableOn.exists_countable_integrableOn [SecondCountableTopology X]
+    (hf : LocallyIntegrableOn f s μ) : ∃ T : Set (Set X), T.Countable ∧
+    (∀ u ∈ T, IsOpen u) ∧ (s ⊆ ⋃ u ∈ T, u) ∧ (∀ u ∈ T, IntegrableOn f (u ∩ s) μ) := by
   have : ∀ x : s, ∃ u, IsOpen u ∧ x.1 ∈ u ∧ IntegrableOn f (u ∩ s) μ := by
     rintro ⟨x, hx⟩
     rcases hf x hx with ⟨t, ht, h't⟩
     rcases mem_nhdsWithin.1 ht with ⟨u, u_open, x_mem, u_sub⟩
     refine' ⟨u, u_open, x_mem, h't.mono_set u_sub⟩
   choose u u_open xu hu using this
-  obtain ⟨T, T_count, hT⟩ : ∃ T : Set s, T.Countable ∧ s = ⋃ i : T, u i ∩ s := by
+  obtain ⟨T, T_count, hT⟩ : ∃ T : Set s, T.Countable ∧ s ⊆ ⋃ i ∈ T, u i := by
     have : s ⊆ ⋃ x : s, u x := fun y hy => mem_iUnion_of_mem ⟨y, hy⟩ (xu ⟨y, hy⟩)
     obtain ⟨T, hT_count, hT_un⟩ := isOpen_iUnion_countable u u_open
-    refine' ⟨T, hT_count, _⟩
-    rw [← hT_un, biUnion_eq_iUnion] at this
-    rw [← iUnion_inter, eq_comm, inter_eq_right_iff_subset]
-    exact this
-  have : Countable T := countable_coe_iff.mpr T_count
-  rw [hT, aestronglyMeasurable_iUnion_iff]
-  exact fun i : T => (hu i).aestronglyMeasurable
+    exact ⟨T, hT_count, by rwa [hT_un]⟩
+  refine' ⟨u '' T, T_count.image _, _, by rwa [biUnion_image], _⟩
+  · rintro v ⟨w, -, rfl⟩
+    exact u_open _
+  · rintro v ⟨w, -, rfl⟩
+    exact hu _
+
+/-- If a function `f` is locally integrable on a set `s` in a second countable topological space,
+then there exists a sequence of open sets `u n` covering `s` such that `f` is integrable on each
+set `u n ∩ s`. -/
+theorem LocallyIntegrableOn.exists_nat_integrableOn [SecondCountableTopology X]
+    (hf : LocallyIntegrableOn f s μ) : ∃ u : ℕ → Set X,
+    (∀ n, IsOpen (u n)) ∧ (s ⊆ ⋃ n, u n) ∧ (∀ n, IntegrableOn f (u n ∩ s) μ) := by
+  rcases hf.exists_countable_integrableOn with ⟨T, T_count, T_open, sT, hT⟩
+  let T' : Set (Set X) := insert ∅ T
+  have T'_count : T'.Countable := Countable.insert ∅ T_count
+  have T'_ne : T'.Nonempty := by simp only [insert_nonempty]
+  rcases T'_count.exists_eq_range T'_ne with ⟨u, hu⟩
+  refine' ⟨u, _, _, _⟩
+  · intro n
+    have : u n ∈ T' := by rw [hu]; exact mem_range_self n
+    rcases mem_insert_iff.1 this with h|h
+    · rw [h]
+      exact isOpen_empty
+    · exact T_open _ h
+  · intro x hx
+    obtain ⟨v, hv, h'v⟩ : ∃ v, v ∈ T ∧ x ∈ v := by simpa only [mem_iUnion, exists_prop] using sT hx
+    have : v ∈ range u := by rw [← hu]; exact subset_insert ∅ T hv
+    obtain ⟨n, rfl⟩ : ∃ n, u n = v := by simpa only [mem_range] using this
+    exact mem_iUnion_of_mem _ h'v
+  · intro n
+    have : u n ∈ T' := by rw [hu]; exact mem_range_self n
+    rcases mem_insert_iff.1 this with h|h
+    · simp only [h, empty_inter, integrableOn_empty]
+    · exact hT _ h
+
+theorem LocallyIntegrableOn.aestronglyMeasurable [SecondCountableTopology X]
+    (hf : LocallyIntegrableOn f s μ) : AEStronglyMeasurable f (μ.restrict s) := by
+  rcases hf.exists_nat_integrableOn with ⟨u, -, su, hu⟩
+  have : s = ⋃ n, u n ∩ s := by rw [← iUnion_inter]; exact (inter_eq_right_iff_subset.mpr su).symm
+  rw [this, aestronglyMeasurable_iUnion_iff]
+  exact fun i : ℕ => (hu i).aestronglyMeasurable
 #align measure_theory.locally_integrable_on.ae_strongly_measurable MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
 
 /-- If `s` is either open, or closed, then `f` is locally integrable on `s` iff it is integrable on
@@ -113,6 +152,17 @@ theorem locallyIntegrableOn_iff [LocallyCompactSpace X] [T2Space X] (hs : IsClos
     simpa only [IsOpen.nhdsWithin_eq hs hx, interior_eq_nhds'] using h2K
 #align measure_theory.locally_integrable_on_iff MeasureTheory.locallyIntegrableOn_iff
 
+protected theorem LocallyIntegrableOn.add
+    (hf : LocallyIntegrableOn f s μ) (hg : LocallyIntegrableOn g s μ) :
+    LocallyIntegrableOn (f + g) s μ := fun x hx ↦ (hf x hx).add (hg x hx)
+
+protected theorem LocallyIntegrableOn.sub
+    (hf : LocallyIntegrableOn f s μ) (hg : LocallyIntegrableOn g s μ) :
+    LocallyIntegrableOn (f - g) s μ := fun x hx ↦ (hf x hx).sub (hg x hx)
+
+protected theorem LocallyIntegrableOn.neg (hf : LocallyIntegrableOn f s μ) :
+    LocallyIntegrableOn (-f) s μ := fun x hx ↦ (hf x hx).neg
+
 end LocallyIntegrableOn
 
 /-- A function `f : X → E` is *locally integrable* if it is integrable on a neighborhood of every
@@ -199,6 +249,15 @@ theorem LocallyIntegrable.aestronglyMeasurable [SecondCountableTopology X]
   simpa only [restrict_univ] using (locallyIntegrableOn_univ.mpr hf).aestronglyMeasurable
 #align measure_theory.locally_integrable.ae_strongly_measurable MeasureTheory.LocallyIntegrable.aestronglyMeasurable
 
+/-- If a function is locally integrable in a second countable topological space,
+then there exists a sequence of open sets covering the space on which it is integrable. -/
+theorem LocallyIntegrable.exists_nat_integrableOn [SecondCountableTopology X]
+    (hf : LocallyIntegrable f μ) : ∃ u : ℕ → Set X,
+    (∀ n, IsOpen (u n)) ∧ ((⋃ n, u n) = univ) ∧ (∀ n, IntegrableOn f (u n) μ) := by
+  rcases (hf.locallyIntegrableOn univ).exists_nat_integrableOn with ⟨u, u_open, u_union, hu⟩
+  refine' ⟨u, u_open, eq_univ_of_univ_subset u_union, fun n ↦ _⟩
+  simpa only [inter_univ] using hu n
+
 theorem locallyIntegrable_const [IsLocallyFiniteMeasure μ] (c : E) :
     LocallyIntegrable (fun _ => c) μ := by
   intro x
@@ -234,6 +293,15 @@ theorem locallyIntegrable_map_homeomorph [BorelSpace X] [BorelSpace Y] (e : X 
     simp only [mem_preimage, Homeomorph.symm_apply_apply]
 #align measure_theory.locally_integrable_map_homeomorph MeasureTheory.locallyIntegrable_map_homeomorph
 
+protected theorem LocallyIntegrable.add (hf : LocallyIntegrable f μ) (hg : LocallyIntegrable g μ) :
+    LocallyIntegrable (f + g) μ := fun x ↦ (hf x).add (hg x)
+
+protected theorem LocallyIntegrable.sub (hf : LocallyIntegrable f μ) (hg : LocallyIntegrable g μ) :
+    LocallyIntegrable (f - g) μ := fun x ↦ (hf x).sub (hg x)
+
+protected theorem LocallyIntegrable.neg (hf : LocallyIntegrable f μ) :
+    LocallyIntegrable (-f) μ := fun x ↦ (hf x).neg
+
 end MeasureTheory
 
 open MeasureTheory

Mathlib/MeasureTheory/Integral/IntegrableOn.lean

@@ -400,6 +400,25 @@ protected theorem IntegrableAtFilter.eventually (h : IntegrableAtFilter f l μ)
   Iff.mpr (eventually_small_sets' fun _s _t hst ht => ht.mono_set hst) h
 #align measure_theory.integrable_at_filter.eventually MeasureTheory.IntegrableAtFilter.eventually
 
+protected theorem IntegrableAtFilter.add {f g : α → E}
+    (hf : IntegrableAtFilter f l μ) (hg : IntegrableAtFilter g l μ) :
+    IntegrableAtFilter (f + g) l μ := by
+  rcases hf with ⟨s, sl, hs⟩
+  rcases hg with ⟨t, tl, ht⟩
+  refine ⟨s ∩ t, inter_mem sl tl, ?_⟩
+  exact (hs.mono_set (inter_subset_left _ _)).add (ht.mono_set (inter_subset_right _ _))
+
+protected theorem IntegrableAtFilter.neg {f : α → E} (hf : IntegrableAtFilter f l μ) :
+    IntegrableAtFilter (-f) l μ := by
+  rcases hf with ⟨s, sl, hs⟩
+  exact ⟨s, sl, hs.neg⟩
+
+protected theorem IntegrableAtFilter.sub {f g : α → E}
+    (hf : IntegrableAtFilter f l μ) (hg : IntegrableAtFilter g l μ) :
+    IntegrableAtFilter (f - g) l μ := by
+  rw [sub_eq_add_neg]
+  exact hf.add hg.neg
+
 theorem IntegrableAtFilter.filter_mono (hl : l ≤ l') (hl' : IntegrableAtFilter f l' μ) :
     IntegrableAtFilter f l μ :=
   let ⟨s, hs, hsf⟩ := hl'