feat (MeasureTheory/Function): trivial cases of integrability / summability (#13872)

Any function on a finite type is multipliable / summable; a function on a discrete measurable space is integrable iff its norm is summable.

Author: loefflerd

Mathlib/MeasureTheory/Function/L1Space.lean

@@ -939,6 +939,43 @@ theorem coe_toNNReal_ae_eq {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x < 
   simp only [hx.ne, Ne, not_false_iff, coe_toNNReal]
 #align measure_theory.coe_to_nnreal_ae_eq MeasureTheory.coe_toNNReal_ae_eq
 
+section count
+
+variable [MeasurableSingletonClass α] {f : α → β}
+
+/-- A function has finite integral for the counting measure iff its norm is summable. -/
+lemma hasFiniteIntegral_count_iff :
+    HasFiniteIntegral f Measure.count ↔ Summable (‖f ·‖) := by
+  simp only [HasFiniteIntegral, lintegral_count, lt_top_iff_ne_top,
+    ENNReal.tsum_coe_ne_top_iff_summable,  ← NNReal.summable_coe, coe_nnnorm]
+
+/-- A function is integrable for the counting measure iff its norm is summable. -/
+lemma integrable_count_iff :
+    Integrable f Measure.count ↔ Summable (‖f ·‖) := by
+  -- Note: this proof would be much easier if we assumed `SecondCountableTopology G`. Without
+  -- this we have to justify the claim that `f` lands a.e. in a separable subset, which is true
+  -- (because summable functions have countable range) but slightly tedious to check.
+  rw [Integrable, hasFiniteIntegral_count_iff, and_iff_right_iff_imp]
+  intro hs
+  have hs' : (Function.support f).Countable := by
+    simpa only [Ne, Pi.zero_apply, eq_comm, Function.support, norm_eq_zero]
+      using hs.countable_support
+  letI : MeasurableSpace β := borel β
+  haveI : BorelSpace β := ⟨rfl⟩
+  refine aestronglyMeasurable_iff_aemeasurable_separable.mpr ⟨?_, ?_⟩
+  · refine (measurable_zero.measurable_of_countable_ne ?_).aemeasurable
+    simpa only [Ne, Pi.zero_apply, eq_comm, Function.support] using hs'
+  · refine ⟨f '' univ, ?_, ae_of_all _ fun a ↦ ⟨a, ⟨mem_univ _, rfl⟩⟩⟩
+    suffices f '' univ ⊆ (f '' f.support) ∪ {0} from
+      (((hs'.image f).union (countable_singleton 0)).mono this).isSeparable
+    intro g hg
+    rcases eq_or_ne g 0 with rfl | hg'
+    · exact Or.inr (mem_singleton _)
+    · obtain ⟨x, -, rfl⟩ := (mem_image ..).mp hg
+      exact Or.inl ⟨x, hg', rfl⟩
+
+end count
+
 section
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

@@ -132,6 +132,10 @@ protected theorem Set.Finite.multipliable {s : Set β} (hs : s.Finite) (f : β 
 theorem multipliable_of_finite_mulSupport (h : (mulSupport f).Finite) : Multipliable f := by
   apply multipliable_of_ne_finset_one (s := h.toFinset); simp
 
+@[to_additive]
+lemma Multipliable.of_finite [Finite β] {f : β → α} : Multipliable f :=
+  multipliable_of_finite_mulSupport <| Set.finite_univ.subset (Set.subset_univ _)
+
 @[to_additive]
 theorem hasProd_single {f : β → α} (b : β) (hf : ∀ (b') (_ : b' ≠ b), f b' = 1) : HasProd f (f b) :=
   suffices HasProd f (∏ b' ∈ {b}, f b') by simpa using this