feat: missing small lemmas in measure theory, cleanup (leanprover-community#40106)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/MeasureTheory/Function/AEEqFun.lean

@@ -658,6 +658,12 @@ theorem coeFn_const_eq [NeZero μ] (b : β) (x : α) : (const α b : α →ₘ[
   simp_rw [const, mk_eq_mk, EventuallyEq, ← const_def, eventually_const] at this
   rw [Function.const, this]
 
+theorem coeFn_const_eq' (b : β) : ∃ b', ((const α b : α →ₘ[μ] β) : α → β) = fun _ ↦ b' := by
+  simp only [cast]
+  split_ifs with h
+  case neg => exact h.elim ⟨b, rfl⟩
+  exact ⟨Classical.choose h, by ext; simp⟩
+
 variable {α}
 
 instance instInhabited [Inhabited β] : Inhabited (α →ₘ[μ] β) :=
@@ -782,6 +788,24 @@ end Monoid
 instance instCommMonoid [CommMonoid γ] [ContinuousMul γ] : CommMonoid (α →ₘ[μ] γ) :=
   toGerm_injective.commMonoid toGerm one_toGerm mul_toGerm pow_toGerm
 
+@[to_additive]
+theorem coeFn_finsetProd [CommMonoid γ] [ContinuousMul γ]
+    {ι : Type*} (s : Finset ι) (f : ι → α →ₘ[μ] γ) :
+    ⇑(∏ i ∈ s, f i) =ᵐ[μ] ∏ i ∈ s, ⇑(f i) := by
+  classical
+  induction s using Finset.induction with
+  | empty => simp [coeFn_one]
+  | insert a s ha ih =>
+    simp only [ha, not_false_eq_true, Finset.prod_insert]
+    grw [coeFn_mul, ih]
+
+@[to_additive]
+theorem coeFn_fun_finsetProd [CommMonoid γ] [ContinuousMul γ]
+    {ι : Type*} (s : Finset ι) (f : ι → α →ₘ[μ] γ) :
+    ⇑(∏ i ∈ s, f i) =ᵐ[μ] fun x ↦ ∏ i ∈ s, f i x := by
+  grw [coeFn_finsetProd]
+  filter_upwards with x using by simp
+
 section Group
 
 variable [Group γ] [IsTopologicalGroup γ]

Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

@@ -245,9 +245,9 @@ theorem hasFiniteIntegral_zero_measure {m : MeasurableSpace α} (f : α → ε)
   simp only [HasFiniteIntegral, lintegral_zero_measure, zero_lt_top]
 
 variable (α μ) in
-@[fun_prop, simp]
+@[to_fun (attr := fun_prop, simp) hasFiniteIntegral_fun_zero]
 theorem hasFiniteIntegral_zero {ε : Type*} [TopologicalSpace ε] [ESeminormedAddMonoid ε] :
-    HasFiniteIntegral (fun _ : α => (0 : ε)) μ := by
+    HasFiniteIntegral (0 : α → ε) μ := by
   simp [hasFiniteIntegral_iff_enorm]
 
 @[fun_prop]

Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

@@ -405,9 +405,9 @@ section ESeminormedAddMonoid
 variable {ε' : Type*} [TopologicalSpace ε'] [ESeminormedAddMonoid ε']
 
 variable (α ε') in
-@[simp]
-theorem integrable_zero (μ : Measure α) : Integrable (fun _ => (0 : ε')) μ := by
-  simp [Integrable, aestronglyMeasurable_const]
+@[to_fun (attr := fun_prop, simp) integrable_fun_zero]
+theorem integrable_zero (μ : Measure α) : Integrable (0 : α → ε') μ := by
+  simp [Integrable, aestronglyMeasurable_zero]
 
 theorem Integrable.add' {f g : α → ε'} (hf : Integrable f μ) (hg : Integrable g μ) :
     HasFiniteIntegral (f + g) μ :=

Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

@@ -199,6 +199,15 @@ theorem coeFn_add (f g : Lp E p μ) : ⇑(f + g) =ᵐ[μ] f + g :=
 theorem coeFn_sub (f g : Lp E p μ) : ⇑(f - g) =ᵐ[μ] f - g :=
   AEEqFun.coeFn_sub _ _
 
+theorem coeFn_finsetSum {ι : Type*} (s : Finset ι) (f : ι → Lp E p μ) :
+    ⇑(∑ i ∈ s, f i) =ᵐ[μ] ∑ i ∈ s, ⇑(f i) := by
+  simp [AEEqFun.coeFn_finsetSum]
+
+theorem coeFn_fun_finsetSum {ι : Type*} (s : Finset ι) (f : ι → Lp E p μ) :
+    ⇑(∑ i ∈ s, f i) =ᵐ[μ] fun x ↦ ∑ i ∈ s, f i x := by
+  grw [coeFn_finsetSum]
+  filter_upwards with x using by simp
+
 theorem const_mem_Lp (α) {_ : MeasurableSpace α} (μ : Measure α) (c : E) [IsFiniteMeasure μ] :
     @AEEqFun.const α _ _ μ _ c ∈ Lp E p μ :=
   (memLp_const c).eLpNorm_mk_lt_top

Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

@@ -316,15 +316,19 @@ protected theorem inv [Inv β] [ContinuousInv β] (hf : AEStronglyMeasurable[m]
     AEStronglyMeasurable[m] f⁻¹ μ :=
   ⟨(hf.mk f)⁻¹, hf.stronglyMeasurable_mk.inv, hf.ae_eq_mk.inv⟩
 
+@[fun_prop]
+theorem inv₀ [GroupWithZero β] [ContinuousInv₀ β] [MetrizableSpace β]
+    (hf : AEStronglyMeasurable[m] f μ) : AEStronglyMeasurable[m] f⁻¹ μ :=
+  ⟨(hf.mk f)⁻¹, hf.stronglyMeasurable_mk.inv₀, hf.ae_eq_mk.inv⟩
+
 @[to_additive (attr := fun_prop)]
 protected theorem div [Group β] [IsTopologicalGroup β] (hf : AEStronglyMeasurable[m] f μ)
     (hg : AEStronglyMeasurable[m] g μ) : AEStronglyMeasurable[m] (f / g) μ :=
   ⟨hf.mk f / hg.mk g, hf.stronglyMeasurable_mk.div' hg.stronglyMeasurable_mk,
     hf.ae_eq_mk.div hg.ae_eq_mk⟩
 
 @[fun_prop]
-theorem div₀ [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β] [PseudoMetrizableSpace β]
-    [MeasurableSpace β] [BorelSpace β] [MeasurableSingletonClass β]
+theorem div₀ [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β] [MetrizableSpace β]
     (hf : AEStronglyMeasurable[m] f μ) (hg : AEStronglyMeasurable[m] g μ) :
     AEStronglyMeasurable[m] (f / g) μ :=
   ⟨hf.mk f / hg.mk g, hf.stronglyMeasurable_mk.div hg.stronglyMeasurable_mk,

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -416,6 +416,21 @@ protected theorem inv [Inv β] [ContinuousInv β] (hf : StronglyMeasurable f) :
     StronglyMeasurable f⁻¹ :=
   ⟨fun n => (hf.approx n)⁻¹, fun x => (hf.tendsto_approx x).inv⟩
 
+@[fun_prop]
+protected theorem inv₀ [GroupWithZero β] [ContinuousInv₀ β] [MetrizableSpace β]
+    (hf : StronglyMeasurable f) : StronglyMeasurable f⁻¹ := by
+  borelize β
+  refine ⟨fun n => ((hf.approx n).restrict {x | f x ≠ 0})⁻¹, fun x => ?_⟩
+  have : MeasurableSet {x | f x ≠ 0} := ((MeasurableSet.singleton 0).preimage hf.measurable).compl
+  by_cases h : f x = 0
+  · simp_all only [ne_eq, measurableSet_setOf, SimpleFunc.coe_inv, SimpleFunc.coe_restrict,
+      Pi.inv_apply, mem_setOf_eq, not_true_eq_false, not_false_eq_true, indicator_of_notMem,
+      _root_.inv_zero]
+    exact tendsto_const_nhds
+  · simp_all only [ne_eq, measurableSet_setOf, SimpleFunc.coe_inv, SimpleFunc.coe_restrict,
+      Pi.inv_apply, mem_setOf_eq, not_false_eq_true, indicator_of_mem]
+    apply (hf.tendsto_approx x).inv₀ h
+
 @[to_additive (attr := fun_prop) sub]
 protected theorem div' [Div β] [ContinuousDiv β] (hf : StronglyMeasurable f)
     (hg : StronglyMeasurable g) : StronglyMeasurable (f / g) :=
@@ -428,10 +443,10 @@ theorem div₀ [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β] (hf :
     fun x => (hf.tendsto_approx x).div (hg.tendsto_approx x) (h₀ x)⟩
 
 @[fun_prop]
-theorem div [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β] [PseudoMetrizableSpace β]
-    [MeasurableSpace β] [BorelSpace β] [MeasurableSingletonClass β] (hf : StronglyMeasurable f)
-    (hg : StronglyMeasurable g) :
+theorem div [GroupWithZero β] [ContinuousMul β] [ContinuousInv₀ β] [MetrizableSpace β]
+    (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
     StronglyMeasurable (f / g) := by
+  borelize β
   refine ⟨fun n => hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}, fun x => ?_⟩
   have : MeasurableSet {x | g x ≠ 0} := ((MeasurableSet.singleton 0).preimage hg.measurable).compl
   by_cases h : g x = 0

Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

@@ -214,6 +214,10 @@ theorem integral_non_aestronglyMeasurable {f : α → G} (h : ¬AEStronglyMeasur
     ∫ a, f a ∂μ = 0 :=
   integral_undef <| not_and_of_not_left _ h
 
+theorem integral_of_not_completeSpace {f : α → G} (hG : ¬CompleteSpace G) :
+    ∫ a, f a ∂μ = 0 := by
+  simp [integral, hG]
+
 variable (α G)
 
 @[simp]

Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

@@ -545,14 +545,16 @@ theorem setLIntegral_eq_const {f : α → ℝ≥0∞} (hf : Measurable f) (r : 
   · rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
   · exact hf (measurableSet_singleton r)
 
+@[to_fun lintegral_indicator_fun_one_le]
 theorem lintegral_indicator_one_le (s : Set α) : ∫⁻ a, s.indicator 1 a ∂μ ≤ μ s :=
   (lintegral_indicator_const_le _ _).trans <| (one_mul _).le
 
-@[simp]
+@[to_fun (attr := simp) lintegral_indicator_fun_one₀]
 theorem lintegral_indicator_one₀ {s : Set α} (hs : NullMeasurableSet s μ) :
     ∫⁻ a, s.indicator 1 a ∂μ = μ s :=
   (lintegral_indicator_const₀ hs _).trans <| one_mul _
 
+@[to_fun lintegral_indicator_fun_one]
 theorem lintegral_indicator_one {s : Set α} (hs : MeasurableSet s) :
     ∫⁻ a, s.indicator 1 a ∂μ = μ s := by
   simp [hs]

Mathlib/MeasureTheory/Integral/SetToL1.lean

@@ -715,9 +715,7 @@ theorem setToFun_smul_left' (hT : DominatedFinMeasAdditive μ T C)
 theorem setToFun_zero (hT : DominatedFinMeasAdditive μ T C) : setToFun μ T hT (0 : α → E) = 0 := by
   by_cases hF : CompleteSpace F; swap
   · simp [setToFun, hF]
-  rw [Pi.zero_def, setToFun_eq hT (integrable_zero _ _ _)]
-  simp only [← Pi.zero_def]
-  rw [Integrable.toL1_zero, map_zero]
+  rw [setToFun_eq hT (integrable_zero _ _ _), Integrable.toL1_zero, map_zero]
 
 @[simp]
 theorem setToFun_zero_left {hT : DominatedFinMeasAdditive μ (0 : Set α → E →L[ℝ] F) C} :

Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean

@@ -63,7 +63,7 @@ theorem withDensityᵥ_apply (hf : Integrable f μ) {s : Set α} (hs : Measurabl
 @[simp]
 theorem withDensityᵥ_zero : μ.withDensityᵥ (0 : α → E) = 0 := by
   ext1 s hs
-  rw [Pi.zero_def, withDensityᵥ_apply (integrable_zero α E μ) hs]
+  rw [withDensityᵥ_apply (integrable_zero α E μ) hs]
   simp
 
 @[simp]