feat(MeasureTheory/Integral/Bochner): add exists_ne_zero_of_integral_ne_zero and exists_ne_zero_of_setIntegral_ne_zero

Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

@@ -367,6 +367,12 @@ theorem edist_integral_le_lintegral_edist
 theorem integral_eq_zero_of_ae {f : α → G} (hf : f =ᵐ[μ] 0) : ∫ a, f a ∂μ = 0 := by
   simp [integral_congr_ae hf, integral_zero]
 
+theorem exists_ne_zero_of_integral_ne_zero {f : α → G}
+    (h : ∫ a, f a ∂μ ≠ 0) : ∃ a, f a ≠ 0 := by
+  contrapose! h
+  exact integral_eq_zero_of_ae ((Set.eqOn_univ f 0).mp fun ⦃x⦄ _ ↦ h x).eventuallyEq
+
+
 /-- If `f` has finite integral, then `∫ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
 to zero as `μ s` tends to zero. -/
 theorem HasFiniteIntegral.tendsto_setIntegral_nhds_zero {ι} {f : α → G}

Mathlib/MeasureTheory/Integral/Bochner/Set.lean

@@ -352,6 +352,12 @@ theorem setIntegral_eq_zero_of_forall_eq_zero (ht_eq : ∀ x ∈ t, f x = 0) :
     ∫ x in t, f x ∂μ = 0 :=
   setIntegral_eq_zero_of_ae_eq_zero (Eventually.of_forall ht_eq)
 
+theorem exists_ne_zero_of_setIntegral_ne_zero (hU : ∫ x in t, f x ∂μ ≠ 0) :
+    ∃ x, x ∈ t ∧ f x ≠ 0 := by
+  contrapose! hU
+  exact setIntegral_eq_zero_of_forall_eq_zero hU
+
+
 theorem integral_union_eq_left_of_ae_aux (ht_eq : ∀ᵐ x ∂μ.restrict t, f x = 0)
     (haux : StronglyMeasurable f) (H : IntegrableOn f (s ∪ t) μ) :
     ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ := by