feat: any function is integrable on a finset wrt to a finite measure

From PFR
leanprover-community · Oct 29, 2024 · fa153fd · fa153fd
1 parent c8dae00
commit fa153fd
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Zhouhang Zhou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne
 -/
+import Mathlib.MeasureTheory.Integral.IntegrableOn
 import Mathlib.MeasureTheory.Integral.SetToL1
 
 /-!
@@ -1761,7 +1762,7 @@ theorem integral_countable [MeasurableSingletonClass α] (f : α → E) {s : Set
   simp
 
 theorem integral_finset [MeasurableSingletonClass α] (s : Finset α) (f : α → E)
-    (hf : Integrable f (μ.restrict s)) :
+    (hf : IntegrableOn f s μ) :
     ∫ x in s, f x ∂μ = ∑ x ∈ s, (μ {x}).toReal • f x := by
   rw [integral_countable _ s.countable_toSet hf, ← Finset.tsum_subtype']
 
@@ -1770,7 +1771,7 @@ theorem integral_fintype [MeasurableSingletonClass α] [Fintype α] (f : α →
     ∫ x, f x ∂μ = ∑ x, (μ {x}).toReal • f x := by
   -- NB: Integrable f does not follow from Fintype, because the measure itself could be non-finite
   rw [← integral_finset .univ, Finset.coe_univ, Measure.restrict_univ]
-  simp only [Finset.coe_univ, Measure.restrict_univ, hf]
+  simp [Finset.coe_univ, Measure.restrict_univ, hf]
 
 theorem integral_unique [Unique α] (f : α → E) : ∫ x, f x ∂μ = (μ univ).toReal • f default :=
   calc

diff --git a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean
@@ -188,6 +188,11 @@ theorem integrableOn_finite_iUnion [Finite β] {t : β → Set α} :
   cases nonempty_fintype β
   simpa using @integrableOn_finset_iUnion _ _ _ _ _ f μ Finset.univ t
 
+lemma IntegrableOn.finset [MeasurableSingletonClass α] {μ : Measure α} [IsFiniteMeasure μ]
+    {s : Finset α} {f : α → E} : IntegrableOn f s μ := by
+  rw [← s.toSet.biUnion_of_singleton]
+  simp [integrableOn_finset_iUnion, measure_lt_top]
+
 theorem IntegrableOn.add_measure (hμ : IntegrableOn f s μ) (hν : IntegrableOn f s ν) :
     IntegrableOn f s (μ + ν) := by
   delta IntegrableOn; rw [Measure.restrict_add]; exact hμ.integrable.add_measure hν