src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
 changeset 65204 d23eded35a33 parent 64272 f76b6dda2e56 child 65587 16a8991ab398
```     1.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Mar 12 19:06:10 2017 +0100
1.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Mar 10 23:16:40 2017 +0100
1.3 @@ -2543,4 +2543,69 @@
1.4      by simp
1.5  qed
1.6
1.7 +lemma has_integral_0_closure_imp_0:
1.8 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
1.9 +  assumes f: "continuous_on (closure S) f"
1.10 +    and nonneg_interior: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
1.11 +    and pos: "0 < emeasure lborel S"
1.12 +    and finite: "emeasure lborel S < \<infinity>"
1.13 +    and regular: "emeasure lborel (closure S) = emeasure lborel S"
1.14 +    and opn: "open S"
1.15 +  assumes int: "(f has_integral 0) (closure S)"
1.16 +  assumes x: "x \<in> closure S"
1.17 +  shows "f x = 0"
1.18 +proof -
1.19 +  have zero: "emeasure lborel (frontier S) = 0"
1.20 +    using finite closure_subset regular
1.21 +    unfolding frontier_def
1.22 +    by (subst emeasure_Diff) (auto simp: frontier_def interior_open \<open>open S\<close> )
1.23 +  have nonneg: "0 \<le> f x" if "x \<in> closure S" for x
1.24 +    using continuous_ge_on_closure[OF f that nonneg_interior] by simp
1.25 +  have "0 = integral (closure S) f"
1.26 +    by (blast intro: int sym)
1.27 +  also
1.28 +  note intl = has_integral_integrable[OF int]
1.29 +  have af: "f absolutely_integrable_on (closure S)"
1.30 +    using nonneg
1.31 +    by (intro absolutely_integrable_onI intl integrable_eq[OF _ intl]) simp
1.32 +  then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
1.33 +    by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
1.34 +  also have "\<dots> = 0 \<longleftrightarrow> (AE x in lebesgue. indicator (closure S) x *\<^sub>R f x = 0)"
1.35 +    by (rule integral_nonneg_eq_0_iff_AE[OF af]) (use nonneg in \<open>auto simp: indicator_def\<close>)
1.36 +  also have "\<dots> \<longleftrightarrow> (AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})"
1.37 +    by (auto simp: indicator_def)
1.38 +  finally have "(AE x in lebesgue. x \<in> {x. x \<in> closure S \<longrightarrow> f x = 0})" by simp
1.39 +  moreover have "(AE x in lebesgue. x \<in> - frontier S)"
1.40 +    using zero
1.41 +    by (auto simp: eventually_ae_filter null_sets_def intro!: exI[where x="frontier S"])
1.42 +  ultimately have ae: "AE x \<in> S in lebesgue. x \<in> {x \<in> closure S. f x = 0}" (is ?th)
1.43 +    by eventually_elim (use closure_subset in \<open>auto simp: \<close>)
1.44 +  have "closed {0::real}" by simp
1.45 +  with continuous_on_closed_vimage[OF closed_closure, of S f] f
1.46 +  have "closed (f -` {0} \<inter> closure S)" by blast
1.47 +  then have "closed {x \<in> closure S. f x = 0}" by (auto simp: vimage_def Int_def conj_commute)
1.48 +  with \<open>open S\<close> have "x \<in> {x \<in> closure S. f x = 0}" if "x \<in> S" for x using ae that
1.49 +    by (rule mem_closed_if_AE_lebesgue_open)
1.50 +  then have "f x = 0" if "x \<in> S" for x using that by auto
1.51 +  from continuous_constant_on_closure[OF f this \<open>x \<in> closure S\<close>]
1.52 +  show "f x = 0" .
1.53 +qed
1.54 +
1.55 +lemma has_integral_0_cbox_imp_0:
1.56 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
1.57 +  assumes f: "continuous_on (cbox a b) f"
1.58 +    and nonneg_interior: "\<And>x. x \<in> box a b \<Longrightarrow> 0 \<le> f x"
1.59 +  assumes int: "(f has_integral 0) (cbox a b)"
1.60 +  assumes ne: "box a b \<noteq> {}"
1.61 +  assumes x: "x \<in> cbox a b"
1.62 +  shows "f x = 0"
1.63 +proof -
1.64 +  have "0 < emeasure lborel (box a b)"
1.65 +    using ne x unfolding emeasure_lborel_box_eq
1.66 +    by (force intro!: prod_pos simp: mem_box algebra_simps)
1.67 +  then show ?thesis using assms
1.68 +    by (intro has_integral_0_closure_imp_0[of "box a b" f x])
1.69 +      (auto simp: emeasure_lborel_box_eq emeasure_lborel_cbox_eq algebra_simps mem_box)
1.70 +qed
1.71 +
1.72  end
```