# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1641754206 0
# Node ID a565a2889b49f2a15487398bdc96d28a85e6e442
# Parent  e578640c787a16fd540d69c7adda196dd5207132
Some lemmas about continuous functions with integral zero

diff -r e578640c787a -r a565a2889b49 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Jan 07 08:50:12 2022 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Jan 09 18:50:06 2022 +0000
@@ -4038,6 +4038,8 @@
     by simp
 qed
 
+subsection \<open>A non-negative continuous function whose integral is zero must be zero\<close>
+
 lemma has_integral_0_closure_imp_0:
   fixes f :: "'a::euclidean_space \<Rightarrow> real"
   assumes f: "continuous_on (closure S) f"
@@ -4092,9 +4094,8 @@
 
 lemma has_integral_0_cbox_imp_0:
   fixes f :: "'a::euclidean_space \<Rightarrow> real"
-  assumes f: "continuous_on (cbox a b) f"
-    and nonneg_interior: "\<And>x. x \<in> box a b \<Longrightarrow> 0 \<le> f x"
-  assumes int: "(f has_integral 0) (cbox a b)"
+  assumes "continuous_on (cbox a b) f" and "\<And>x. x \<in> box a b \<Longrightarrow> 0 \<le> f x"
+  assumes "(f has_integral 0) (cbox a b)"
   assumes ne: "box a b \<noteq> {}"
   assumes x: "x \<in> cbox a b"
   shows "f x = 0"
@@ -4107,6 +4108,36 @@
       (auto simp: emeasure_lborel_box_eq emeasure_lborel_cbox_eq algebra_simps mem_box)
 qed
 
+corollary integral_cbox_eq_0_iff:
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes "continuous_on (cbox a b) f" and "box a b \<noteq> {}"
+    and "\<And>x. x \<in> (cbox a b) \<Longrightarrow> f x \<ge> 0"
+  shows "integral (cbox a b) f = 0 \<longleftrightarrow> (\<forall>x \<in> (cbox a b). f x = 0)" (is "?lhs = ?rhs")
+proof
+  assume int0: ?lhs
+  show ?rhs
+    using has_integral_0_cbox_imp_0 [of a b f] assms
+    by (metis box_subset_cbox eq_integralD int0 integrable_continuous subsetD) 
+next
+  assume ?rhs then show ?lhs
+    by (meson has_integral_is_0_cbox integral_unique)
+qed
+
+lemma integral_eq_0_iff:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "continuous_on {a..b} f" and "a < b"
+    and "\<And>x. x \<in> {a..b} \<Longrightarrow> f x \<ge> 0"
+  shows "integral {a..b} f = 0 \<longleftrightarrow> (\<forall>x \<in> {a..b}. f x = 0)" 
+  using integral_cbox_eq_0_iff [of a b f] assms by simp
+
+lemma integralL_eq_0_iff:
+  fixes f :: "real \<Rightarrow> real"
+  assumes contf: "continuous_on {a..b} f" and "a < b"
+    and "\<And>x. x \<in> {a..b} \<Longrightarrow> f x \<ge> 0"
+  shows "integral\<^sup>L (lebesgue_on {a..b}) f = 0 \<longleftrightarrow> (\<forall>x \<in> {a..b}. f x = 0)" 
+  using integral_eq_0_iff [OF assms]
+  by (simp add: contf continuous_imp_integrable_real lebesgue_integral_eq_integral)
+
 subsection\<open>Various common equivalent forms of function measurability\<close>
 
 lemma indicator_sum_eq: