summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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