src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 66504 04b3a4548323
parent 66503 7685861f337d
child 66505 b81e1d194e4c
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 17:15:53 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 21:41:13 2017 +0100
     1.3 @@ -11,8 +11,8 @@
     1.4  
     1.5  (*FIXME DELETE*)
     1.6  lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
     1.7 -
     1.8  (* try instead structured proofs below *)
     1.9 +
    1.10  lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
    1.11    \<Longrightarrow> norm(y-x) \<le> e"
    1.12    using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
    1.13 @@ -4627,142 +4627,88 @@
    1.14  
    1.15  lemma has_integral':
    1.16    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    1.17 -  shows "(f has_integral i) s \<longleftrightarrow>
    1.18 +  shows "(f has_integral i) S \<longleftrightarrow>
    1.19      (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
    1.20 -      (\<exists>z. ((\<lambda>x. if x \<in> s then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - i) < e))"
    1.21 +      (\<exists>z. ((\<lambda>x. if x \<in> S then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - i) < e))"
    1.22    (is "?l \<longleftrightarrow> (\<forall>e>0. ?r e)")
    1.23 -proof -
    1.24 -  {
    1.25 -    presume *: "\<exists>a b. s = cbox a b \<Longrightarrow> ?thesis"
    1.26 -    show ?thesis
    1.27 -      apply cases
    1.28 -      apply (rule *)
    1.29 -      apply assumption
    1.30 -      apply (subst has_integral_alt)
    1.31 -      apply auto
    1.32 -      done
    1.33 -  }
    1.34 -  assume "\<exists>a b. s = cbox a b"
    1.35 -  then obtain a b where s: "s = cbox a b"
    1.36 -    by blast
    1.37 -  from bounded_cbox[of a b, unfolded bounded_pos] 
    1.38 +proof (cases "\<exists>a b. S = cbox a b")
    1.39 +  case False then show ?thesis 
    1.40 +    by (simp add: has_integral_alt)
    1.41 +next
    1.42 +  case True
    1.43 +  then obtain a b where S: "S = cbox a b"
    1.44 +    by blast 
    1.45    obtain B where " 0 < B" and B: "\<And>x. x \<in> cbox a b \<Longrightarrow> norm x \<le> B"
    1.46 -    by blast
    1.47 +    using bounded_cbox[unfolded bounded_pos] by blast
    1.48    show ?thesis
    1.49    proof safe
    1.50      fix e :: real
    1.51      assume ?l and "e > 0"
    1.52 -    show "?r e"
    1.53 +    have "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) (cbox c d)"
    1.54 +      if "ball 0 (B+1) \<subseteq> cbox c d" for c d
    1.55 +        unfolding S using B that
    1.56 +        by (force intro: \<open>?l\<close>[unfolded S] has_integral_restrict_closed_subinterval)
    1.57 +    then show "?r e"
    1.58        apply (rule_tac x="B+1" in exI)
    1.59 -      apply safe
    1.60 -      defer
    1.61 -      apply (rule_tac x=i in exI)
    1.62 -    proof
    1.63 -      fix c d :: 'n
    1.64 -      assume as: "ball 0 (B+1) \<subseteq> cbox c d"
    1.65 -      then show "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) (cbox c d)"
    1.66 -        unfolding s
    1.67 -        apply -
    1.68 -        apply (rule has_integral_restrict_closed_subinterval)
    1.69 -        apply (rule \<open>?l\<close>[unfolded s])
    1.70 -        apply safe
    1.71 -        apply (drule B[rule_format])
    1.72 -        unfolding subset_eq
    1.73 -        apply (erule_tac x=x in ballE)
    1.74 -        apply (auto simp add: dist_norm)
    1.75 -        done
    1.76 -    qed (insert \<open>B>0\<close> \<open>e>0\<close>, auto)
    1.77 +      using \<open>B>0\<close> \<open>e>0\<close> by force
    1.78    next
    1.79      assume as: "\<forall>e>0. ?r e"
    1.80 -    from this[rule_format,OF zero_less_one] guess C..note C=conjunctD2[OF this,rule_format]
    1.81 +    then obtain C 
    1.82 +      where C: "\<And>a b. ball 0 C \<subseteq> cbox a b \<Longrightarrow>
    1.83 +                \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b)"
    1.84 +      by (meson zero_less_one)
    1.85      define c :: 'n where "c = (\<Sum>i\<in>Basis. (- max B C) *\<^sub>R i)"
    1.86      define d :: 'n where "d = (\<Sum>i\<in>Basis. max B C *\<^sub>R i)"
    1.87 -    have c_d: "cbox a b \<subseteq> cbox c d"
    1.88 -      apply safe
    1.89 -      apply (drule B)
    1.90 -      unfolding mem_box
    1.91 -    proof
    1.92 -      fix x i
    1.93 -      show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm x \<le> B" and "i \<in> Basis"
    1.94 -        using that and Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x]
    1.95 -        unfolding c_def d_def
    1.96 -        by (auto simp add: field_simps sum_negf)
    1.97 -    qed
    1.98 -    have "ball 0 C \<subseteq> cbox c d"
    1.99 -      apply (rule subsetI)
   1.100 -      unfolding mem_box mem_ball dist_norm
   1.101 -    proof
   1.102 -      fix x i :: 'n
   1.103 -      assume x: "norm (0 - x) < C" and i: "i \<in> Basis"
   1.104 -      show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
   1.105 -        using Basis_le_norm[OF i, of x] and x i
   1.106 -        unfolding c_def d_def
   1.107 -        by (auto simp: sum_negf)
   1.108 -    qed
   1.109 -    from C(2)[OF this] have "\<exists>y. (f has_integral y) (cbox a b)"
   1.110 -      unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,symmetric]
   1.111 -      unfolding s
   1.112 -      by auto
   1.113 -    then guess y..note y=this
   1.114 -
   1.115 +    have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm x \<le> B" "i \<in> Basis" for x i
   1.116 +      using that and Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x]
   1.117 +      by (auto simp add: field_simps sum_negf c_def d_def)
   1.118 +    then have c_d: "cbox a b \<subseteq> cbox c d"
   1.119 +      by (meson B mem_box(2) subsetI)
   1.120 +    have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
   1.121 +      if x: "norm (0 - x) < C" and i: "i \<in> Basis" for x i
   1.122 +        using Basis_le_norm[OF i, of x] x i by (auto simp: sum_negf c_def d_def)
   1.123 +      then have "ball 0 C \<subseteq> cbox c d"
   1.124 +        by (auto simp: mem_box dist_norm)
   1.125 +    with C obtain y where y: "(f has_integral y) (cbox a b)"
   1.126 +      using c_d has_integral_restrict_closed_subintervals_eq S by blast
   1.127      have "y = i"
   1.128      proof (rule ccontr)
   1.129 -      assume "\<not> ?thesis"
   1.130 +      assume "y \<noteq> i"
   1.131        then have "0 < norm (y - i)"
   1.132          by auto
   1.133 -      from as[rule_format,OF this] guess C ..  note C=conjunctD2[OF this,rule_format]
   1.134 +      from as[rule_format,OF this]
   1.135 +      obtain C where C: "\<And>a b. ball 0 C \<subseteq> cbox a b \<Longrightarrow> 
   1.136 +           \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z-i) < norm (y-i)"
   1.137 +        by auto
   1.138        define c :: 'n where "c = (\<Sum>i\<in>Basis. (- max B C) *\<^sub>R i)"
   1.139        define d :: 'n where "d = (\<Sum>i\<in>Basis. max B C *\<^sub>R i)"
   1.140 -      have c_d: "cbox a b \<subseteq> cbox c d"
   1.141 -        apply safe
   1.142 -        apply (drule B)
   1.143 -        unfolding mem_box
   1.144 -      proof
   1.145 -        fix x i :: 'n
   1.146 -        assume "norm x \<le> B" and "i \<in> Basis"
   1.147 -        then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
   1.148 -          using Basis_le_norm[of i x]
   1.149 -          unfolding c_def d_def
   1.150 -          by (auto simp add: field_simps sum_negf)
   1.151 -      qed
   1.152 -      have "ball 0 C \<subseteq> cbox c d"
   1.153 -        apply (rule subsetI)
   1.154 -        unfolding mem_box mem_ball dist_norm
   1.155 -      proof
   1.156 -        fix x i :: 'n
   1.157 -        assume "norm (0 - x) < C" and "i \<in> Basis"
   1.158 -        then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
   1.159 -          using Basis_le_norm[of i x]
   1.160 -          unfolding c_def d_def
   1.161 -          by (auto simp: sum_negf)
   1.162 -      qed
   1.163 -      note C(2)[OF this] then guess z..note z = conjunctD2[OF this, unfolded s]
   1.164 -      note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]]
   1.165 -      then have "z = y" and "norm (z - i) < norm (y - i)"
   1.166 -        apply -
   1.167 -        apply (rule has_integral_unique[OF _ y(1)])
   1.168 -        apply assumption
   1.169 -        apply assumption
   1.170 -        done
   1.171 -      then show False
   1.172 +      have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
   1.173 +        if "norm x \<le> B" and "i \<in> Basis" for x i
   1.174 +          using that Basis_le_norm[of i x] by (auto simp add: field_simps sum_negf c_def d_def)
   1.175 +        then have c_d: "cbox a b \<subseteq> cbox c d"
   1.176 +        by (simp add: B mem_box(2) subset_eq)
   1.177 +      have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm (0 - x) < C" and "i \<in> Basis" for x i
   1.178 +        using Basis_le_norm[of i x] that by (auto simp: sum_negf c_def d_def)
   1.179 +      then have "ball 0 C \<subseteq> cbox c d"
   1.180 +        by (auto simp: mem_box dist_norm)
   1.181 +      with C obtain z where z: "(f has_integral z) (cbox a b)" "norm (z-i) < norm (y-i)"
   1.182 +        using has_integral_restrict_closed_subintervals_eq[OF c_d] S by blast
   1.183 +      moreover then have "z = y" 
   1.184 +        by (blast intro: has_integral_unique[OF _ y])
   1.185 +      ultimately show False
   1.186          by auto
   1.187      qed
   1.188      then show ?l
   1.189 -      using y
   1.190 -      unfolding s
   1.191 -      by auto
   1.192 +      using y by (auto simp: S)
   1.193    qed
   1.194  qed
   1.195  
   1.196  lemma has_integral_le:
   1.197    fixes f :: "'n::euclidean_space \<Rightarrow> real"
   1.198 -  assumes "(f has_integral i) S"
   1.199 -    and "(g has_integral j) S"
   1.200 -    and "\<And>x. x \<in> S \<Longrightarrow> f x \<le> g x"
   1.201 +  assumes fg: "(f has_integral i) S" "(g has_integral j) S"
   1.202 +    and le: "\<And>x. x \<in> S \<Longrightarrow> f x \<le> g x"
   1.203    shows "i \<le> j"
   1.204 -  using has_integral_component_le[OF _ assms(1-2), of 1]
   1.205 -  using assms(3)
   1.206 -  by auto
   1.207 +  using has_integral_component_le[OF _ fg, of 1] le  by auto
   1.208  
   1.209  lemma integral_le:
   1.210    fixes f :: "'n::euclidean_space \<Rightarrow> real"