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