further Hensock tidy-up
authorpaulson <lp15@cam.ac.uk>
Mon Aug 14 18:54:25 2017 +0100 (21 months ago)
changeset 66420bc0dab0e7b40
parent 66409 f749d39c016b
child 66421 7fa0b300fb0d
further Hensock tidy-up
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 13 23:45:45 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 14 18:54:25 2017 +0100
     1.3 @@ -9,11 +9,18 @@
     1.4    Lebesgue_Measure Tagged_Division
     1.5  begin
     1.6  
     1.7 -lemma norm_triangle_le_sub: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
     1.8 -  apply (subst(asm)(2) norm_minus_cancel[symmetric])
     1.9 -  apply (drule norm_triangle_le)
    1.10 -  apply (auto simp add: algebra_simps)
    1.11 -  done
    1.12 +(*MOVE ALL THESE*)
    1.13 +lemma abs_triangle_half_r:
    1.14 +  fixes y :: "'a::linordered_field"
    1.15 +  shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
    1.16 +  by linarith
    1.17 +
    1.18 +lemma abs_triangle_half_l:
    1.19 +  fixes y :: "'a::linordered_field"
    1.20 +  assumes "abs (x - y) < e / 2"
    1.21 +    and "abs (x' - y) < e / 2"
    1.22 +  shows "abs (x - x') < e"
    1.23 +  using assms by linarith
    1.24  
    1.25  lemma eps_leI: 
    1.26    assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y"
    1.27 @@ -3775,7 +3782,7 @@
    1.28                norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))"
    1.29            by (rule arg_cong[where f=norm]) (auto simp: scaleR_left.diff)
    1.30          also have "\<dots> \<le> e/2 * norm (u - x) + e/2 * norm (v - x)"
    1.31 -          by (metis norm_triangle_le_sub add_mono * xd)
    1.32 +          by (metis norm_triangle_le_diff add_mono * xd)
    1.33          also have "\<dots> \<le> e/2 * norm (v - u)"
    1.34            using p(2)[OF xk] by (auto simp add: field_simps k)
    1.35          also have "\<dots> < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
    1.36 @@ -6273,16 +6280,16 @@
    1.37  
    1.38  lemma monotone_convergence_increasing:
    1.39    fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
    1.40 -  assumes "\<And>k. (f k) integrable_on S"
    1.41 +  assumes int_f: "\<And>k. (f k) integrable_on S"
    1.42      and "\<And>k x. x \<in> S \<Longrightarrow> (f k x) \<le> (f (Suc k) x)"
    1.43 -    and "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
    1.44 -    and "bounded (range (\<lambda>k. integral S (f k)))"
    1.45 +    and fg: "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
    1.46 +    and bou: "bounded (range (\<lambda>k. integral S (f k)))"
    1.47    shows "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
    1.48  proof -
    1.49    have lem: "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
    1.50      if f0: "\<And>k x. x \<in> S \<Longrightarrow> 0 \<le> f k x"
    1.51      and int_f: "\<And>k. (f k) integrable_on S"
    1.52 -    and le: "\<And>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x"
    1.53 +    and le: "\<And>k x. x \<in> S \<Longrightarrow> f k x \<le> f (Suc k) x"
    1.54      and lim: "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
    1.55      and bou: "bounded (range(\<lambda>k. integral S (f k)))"
    1.56      for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g S
    1.57 @@ -6294,8 +6301,7 @@
    1.58        using le  by (force intro: transitive_stepwise_le that) 
    1.59  
    1.60      obtain i where i: "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> i"
    1.61 -      using bounded_increasing_convergent [OF bou]
    1.62 -      using le int_f integral_le by blast
    1.63 +      using bounded_increasing_convergent [OF bou] le int_f integral_le by blast
    1.64      have i': "(integral S (f k))\<bullet>1 \<le> i\<bullet>1" for k
    1.65      proof -
    1.66        have *: "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
    1.67 @@ -6307,21 +6313,18 @@
    1.68          using * by (simp add: int_f integral_le)
    1.69      qed
    1.70  
    1.71 -    have int: "(\<lambda>x. if x \<in> S then f k x else 0) integrable_on cbox a b" for a b k
    1.72 +    let ?f = "(\<lambda>k x. if x \<in> S then f k x else 0)"
    1.73 +    let ?g = "(\<lambda>x. if x \<in> S then g x else 0)"
    1.74 +    have int: "?f k integrable_on cbox a b" for a b k
    1.75        by (simp add: int_f integrable_altD(1))
    1.76      have int': "\<And>k a b. f k integrable_on cbox a b \<inter> S"
    1.77        using int by (simp add: Int_commute integrable_restrict_Int) 
    1.78 -    have "(\<lambda>x. if x \<in> S then g x else 0) integrable_on cbox a b \<and>
    1.79 -          (\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0))
    1.80 -          \<longlonglongrightarrow> integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0)" for a b
    1.81 -    proof (rule monotone_convergence_interval, goal_cases)
    1.82 -      case 1
    1.83 -      show ?case by (rule int)
    1.84 -    next
    1.85 -      case 4
    1.86 -      have "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)) \<le> norm (integral S (f k))" for k
    1.87 +    have g: "?g integrable_on cbox a b \<and>
    1.88 +             (\<lambda>k. integral (cbox a b) (?f k)) \<longlonglongrightarrow> integral (cbox a b) ?g" for a b
    1.89 +    proof (rule monotone_convergence_interval)
    1.90 +      have "norm (integral (cbox a b) (?f k)) \<le> norm (integral S (f k))" for k
    1.91        proof -
    1.92 -        have "0 \<le> integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)"
    1.93 +        have "0 \<le> integral (cbox a b) (?f k)"
    1.94            by (metis (no_types) integral_nonneg Int_iff f0 inf_commute integral_restrict_Int int')
    1.95          moreover have "0 \<le> integral S (f k)"
    1.96            by (simp add: integral_nonneg f0 int_f)
    1.97 @@ -6332,121 +6335,100 @@
    1.98        qed
    1.99        moreover obtain B where "\<And>x. x \<in> range (\<lambda>k. integral S (f k)) \<Longrightarrow> norm x \<le> B"
   1.100          using bou unfolding bounded_iff by blast
   1.101 -      ultimately show ?case
   1.102 +      ultimately show "bounded (range (\<lambda>k. integral (cbox a b) (?f k)))"
   1.103          unfolding bounded_iff by (blast intro: order_trans)
   1.104 -    qed (use le lim in auto)
   1.105 -    note g = conjunctD2[OF this]
   1.106 -
   1.107 -    have "(g has_integral i) S"
   1.108 -      unfolding has_integral_alt'
   1.109 -      apply safe
   1.110 -      apply (rule g(1))
   1.111 -    proof goal_cases
   1.112 -      case (1 e)
   1.113 -      then have "e/4>0"
   1.114 -        by auto
   1.115 -      from LIMSEQ_D [OF i this] guess N..note N=this
   1.116 -      note that(2)[of N,unfolded has_integral_integral has_integral_alt'[of "f N"]]
   1.117 -      from this[THEN conjunct2,rule_format,OF \<open>e/4>0\<close>] guess B..note B=conjunctD2[OF this]
   1.118 -      show ?case
   1.119 -        apply rule
   1.120 -        apply rule
   1.121 -        apply (rule B)
   1.122 -        apply safe
   1.123 +    qed (use int le lim in auto)
   1.124 +    moreover have "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow> norm (integral (cbox a b) ?g - i) < e"
   1.125 +      if "0 < e" for e
   1.126 +    proof -
   1.127 +      have "e/4>0"
   1.128 +        using that by auto
   1.129 +      with LIMSEQ_D [OF i] obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (integral S (f n) - i) < e/4"
   1.130 +        by metis
   1.131 +      with int_f[of N, unfolded has_integral_integral has_integral_alt'[of "f N"]] 
   1.132 +      obtain B where "0 < B" and B: 
   1.133 +        "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> norm (integral (cbox a b) (?f N) - integral S (f N)) < e / 4"
   1.134 +        by (meson \<open>0 < e / 4\<close>)
   1.135 +      have "norm (integral (cbox a b) ?g - i) < e" if  ab: "ball 0 B \<subseteq> cbox a b" for a b
   1.136        proof -
   1.137 -        fix a b :: 'n
   1.138 -        assume ab: "ball 0 B \<subseteq> cbox a b"
   1.139 -        from \<open>e > 0\<close> have "e/2 > 0"
   1.140 -          by auto
   1.141 -        from LIMSEQ_D [OF g(2)[of a b] this] guess M..note M=this
   1.142 -        have **: "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f N x else 0) - i) < e/2"
   1.143 -        proof (rule norm_triangle_half_l)
   1.144 -          show "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f N x else 0) - integral S (f N))
   1.145 -                < e / 2 / 2"
   1.146 -            using B(2)[rule_format,OF ab] by simp
   1.147 -          show "norm (i - integral S (f N)) < e / 2 / 2"
   1.148 -            using N by (simp add: abs_minus_commute)
   1.149 -        qed
   1.150 -        have *: "\<And>f1 f2 g. \<bar>f1 - i\<bar> < e/2 \<longrightarrow> \<bar>f2 - g\<bar> < e/2 \<longrightarrow>
   1.151 -          f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> \<bar>g - i\<bar> < e"
   1.152 +        obtain M where M: "\<And>n. n \<ge> M \<Longrightarrow> abs (integral (cbox a b) (?f n) - integral (cbox a b) ?g) < e / 2"
   1.153 +          using \<open>e > 0\<close> g by (fastforce simp add: dest!: LIMSEQ_D [where r = "e/2"])
   1.154 +        have *: "\<And>\<alpha> \<beta> g. \<lbrakk>\<bar>\<alpha> - i\<bar> < e/2; \<bar>\<beta> - g\<bar> < e/2; \<alpha> \<le> \<beta>; \<beta> \<le> i\<rbrakk> \<Longrightarrow> \<bar>g - i\<bar> < e"
   1.155            unfolding real_inner_1_right by arith
   1.156 -        show "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0) - i) < e"
   1.157 +        show "norm (integral (cbox a b) ?g - i) < e"
   1.158            unfolding real_norm_def
   1.159 -          apply (rule *[rule_format])
   1.160 -          apply (rule **[unfolded real_norm_def])
   1.161 -          apply (rule M[rule_format,of "M + N",unfolded real_norm_def])
   1.162 -          apply (rule le_add1)
   1.163 -          apply (rule integral_le[OF int int])
   1.164 -          defer
   1.165 -           apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]])
   1.166 -        proof (safe, goal_cases)
   1.167 -          case (2 x)
   1.168 -          have "(f m x)\<bullet>1 \<le> (f n x)\<bullet>1" if "x \<in> S" "n \<ge> m" for m n
   1.169 -            apply (rule transitive_stepwise_le [OF \<open>n \<ge> m\<close> order_refl])
   1.170 -            using dual_order.trans apply blast
   1.171 -            by (simp add: le \<open>x \<in> S\<close>)
   1.172 -          then show ?case
   1.173 -            by auto
   1.174 -        next
   1.175 -          case 1
   1.176 +        proof (rule *)
   1.177 +          show "\<bar>integral (cbox a b) (?f N) - i\<bar> < e/2"
   1.178 +          proof (rule abs_triangle_half_l)
   1.179 +            show "\<bar>integral (cbox a b) (?f N) - integral S (f N)\<bar> < e / 2 / 2"
   1.180 +              using B[OF ab] by simp
   1.181 +            show "abs (i - integral S (f N)) < e / 2 / 2"
   1.182 +              using N by (simp add: abs_minus_commute)
   1.183 +          qed
   1.184 +          show "\<bar>integral (cbox a b) (?f (M + N)) - integral (cbox a b) ?g\<bar> < e / 2"
   1.185 +            by (metis le_add1 M[of "M + N"])
   1.186 +          show "integral (cbox a b) (?f N) \<le> integral (cbox a b) (?f (M + N))"
   1.187 +          proof (intro ballI integral_le[OF int int])
   1.188 +            fix x assume "x \<in> cbox a b"
   1.189 +            have "(f m x)\<bullet>1 \<le> (f n x)\<bullet>1" if "x \<in> S" "n \<ge> m" for m n
   1.190 +              apply (rule transitive_stepwise_le [OF \<open>n \<ge> m\<close> order_refl])
   1.191 +              using dual_order.trans apply blast
   1.192 +              by (simp add: le \<open>x \<in> S\<close>)
   1.193 +            then show "(?f N)x \<le> (?f (M+N))x"
   1.194 +              by auto
   1.195 +          qed
   1.196            have "integral (cbox a b \<inter> S) (f (M + N)) \<le> integral S (f (M + N))"
   1.197              by (metis Int_lower1 f0 inf_commute int' int_f integral_subset_le)
   1.198 -          then show ?case
   1.199 -            by (simp add: inf_commute integral_restrict_Int)
   1.200 +          then have "integral (cbox a b) (?f (M + N)) \<le> integral S (f (M + N))"
   1.201 +            by (metis (no_types) inf_commute integral_restrict_Int)
   1.202 +          also have "... \<le> i"
   1.203 +            using i'[of "M + N"] by auto
   1.204 +          finally show "integral (cbox a b) (?f (M + N)) \<le> i" .
   1.205          qed
   1.206        qed
   1.207 +      then show ?thesis
   1.208 +        using \<open>0 < B\<close> by blast
   1.209      qed
   1.210 +    ultimately have "(g has_integral i) S"
   1.211 +      unfolding has_integral_alt' by auto
   1.212      then show ?thesis
   1.213        using has_integral_integrable_integral i integral_unique by metis
   1.214    qed
   1.215  
   1.216    have sub: "\<And>k. integral S (\<lambda>x. f k x - f 0 x) = integral S (f k) - integral S (f 0)"
   1.217 -    by (simp add: integral_diff assms(1))
   1.218 +    by (simp add: integral_diff int_f)
   1.219    have *: "\<And>x m n. x \<in> S \<Longrightarrow> n\<ge>m \<Longrightarrow> f m x \<le> f n x"
   1.220      using assms(2) by (force intro: transitive_stepwise_le)
   1.221 -  have "(\<lambda>x. g x - f 0 x) integrable_on S \<and> ((\<lambda>k. integral S (\<lambda>x. f (Suc k) x - f 0 x)) \<longlongrightarrow>
   1.222 +  have gf: "(\<lambda>x. g x - f 0 x) integrable_on S \<and> ((\<lambda>k. integral S (\<lambda>x. f (Suc k) x - f 0 x)) \<longlongrightarrow>
   1.223      integral S (\<lambda>x. g x - f 0 x)) sequentially"
   1.224 -    apply (rule lem)
   1.225 -    apply safe
   1.226 -  proof goal_cases
   1.227 -    case (1 k x)
   1.228 -    then show ?case
   1.229 -      using *[of x 0 "Suc k"] by auto
   1.230 -  next
   1.231 -    case (2 k)
   1.232 -    then show ?case
   1.233 -      by (simp add: integrable_diff assms(1))
   1.234 -  next
   1.235 -    case (3 k x)
   1.236 -    then show ?case
   1.237 -      using *[of x "Suc k" "Suc (Suc k)"] by auto
   1.238 -  next
   1.239 -    case (4 x)
   1.240 -    then show ?case
   1.241 -      apply -
   1.242 -      apply (rule tendsto_diff)
   1.243 -      using LIMSEQ_ignore_initial_segment[OF assms(3)[rule_format],of x 1]
   1.244 -      apply auto
   1.245 -      done
   1.246 -  next
   1.247 -    case 5
   1.248 -    then show ?case
   1.249 -      using assms(4)
   1.250 -      unfolding bounded_iff
   1.251 -      apply safe
   1.252 -      apply (rule_tac x="a + norm (integral S (\<lambda>x. f 0 x))" in exI)
   1.253 -      apply safe
   1.254 -      apply (erule_tac x="integral S (\<lambda>x. f (Suc k) x)" in ballE)
   1.255 -      unfolding sub
   1.256 -      apply (rule order_trans[OF norm_triangle_ineq4])
   1.257 -      apply auto
   1.258 -      done
   1.259 -  qed
   1.260 -  note conjunctD2[OF this]
   1.261 -  note tendsto_add[OF this(2) tendsto_const[of "integral S (f 0)"]]
   1.262 -    integrable_add[OF this(1) assms(1)[rule_format,of 0]]
   1.263 -  then show ?thesis
   1.264 -    by (simp add: integral_diff assms(1) LIMSEQ_imp_Suc sub)
   1.265 +  proof (rule lem)
   1.266 +    show "\<And>k. (\<lambda>x. f (Suc k) x - f 0 x) integrable_on S"
   1.267 +      by (simp add: integrable_diff int_f)
   1.268 +    show "(\<lambda>k. f (Suc k) x - f 0 x) \<longlonglongrightarrow> g x - f 0 x" if "x \<in> S" for x
   1.269 +    proof -
   1.270 +      have "(\<lambda>n. f (Suc n) x) \<longlonglongrightarrow> g x"
   1.271 +        using LIMSEQ_ignore_initial_segment[OF fg[OF \<open>x \<in> S\<close>], of 1] by simp
   1.272 +      then show ?thesis
   1.273 +        by (simp add: tendsto_diff)
   1.274 +    qed
   1.275 +    show "bounded (range (\<lambda>k. integral S (\<lambda>x. f (Suc k) x - f 0 x)))"
   1.276 +    proof -
   1.277 +      obtain B where B: "\<And>k. norm (integral S (f k)) \<le> B"
   1.278 +        using  bou by (auto simp: bounded_iff)
   1.279 +      then have "norm (integral S (\<lambda>x. f (Suc k) x - f 0 x))
   1.280 +              \<le> B + norm (integral S (f 0))" for k
   1.281 +        unfolding sub by (meson add_le_cancel_right norm_triangle_le_diff)
   1.282 +      then show ?thesis
   1.283 +        unfolding bounded_iff by blast
   1.284 +    qed
   1.285 +  qed (use * in auto)
   1.286 +  then have "(\<lambda>x. integral S (\<lambda>xa. f (Suc x) xa - f 0 xa) + integral S (f 0))
   1.287 +             \<longlonglongrightarrow> integral S (\<lambda>x. g x - f 0 x) + integral S (f 0)"
   1.288 +    by (auto simp add: tendsto_add)
   1.289 +  moreover have "(\<lambda>x. g x - f 0 x + f 0 x) integrable_on S"
   1.290 +    using gf integrable_add int_f [of 0] by metis
   1.291 +  ultimately show ?thesis
   1.292 +    by (simp add: integral_diff int_f LIMSEQ_imp_Suc sub)
   1.293  qed
   1.294  
   1.295  lemma has_integral_monotone_convergence_increasing:
   1.296 @@ -6579,8 +6561,7 @@
   1.297        by auto
   1.298      let ?f = "(\<lambda>x. if x \<in> S then f x else 0)"
   1.299      let ?g = "(\<lambda>x. if x \<in> S then g x else 0)"
   1.300 -    have f: "?f integrable_on cbox a b" and g: "?g integrable_on cbox a b"
   1.301 -      for a b
   1.302 +    have f: "?f integrable_on cbox a b" and g: "?g integrable_on cbox a b" for a b
   1.303        using int_f int_g integrable_altD by auto
   1.304      obtain Bf where "0 < Bf"
   1.305        and Bf: "\<And>a b. ball 0 Bf \<subseteq> cbox a b \<Longrightarrow>
   1.306 @@ -6588,8 +6569,7 @@
   1.307        using integrable_integral [OF int_f,unfolded has_integral'[of f]] e that by blast
   1.308      obtain Bg where "0 < Bg"
   1.309        and Bg: "\<And>a b. ball 0 Bg \<subseteq> cbox a b \<Longrightarrow>
   1.310 -        \<exists>z. (?g has_integral z) (cbox a b) \<and>
   1.311 -            norm (z - integral S g) < e/2"
   1.312 +        \<exists>z. (?g has_integral z) (cbox a b) \<and> norm (z - integral S g) < e/2"
   1.313        using integrable_integral [OF int_g,unfolded has_integral'[of g]] e that by blast
   1.314      obtain a b::'n where ab: "ball 0 Bf \<union> ball 0 Bg \<subseteq> cbox a b"
   1.315        using ball_max_Un bounded_subset_cbox[OF bounded_ball, of _ "max Bf Bg"] by blast
     2.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sun Aug 13 23:45:45 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Mon Aug 14 18:54:25 2017 +0100
     2.3 @@ -1482,6 +1482,22 @@
     2.4  lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
     2.5    by (rule norm_triangle_ineq [THEN le_less_trans])
     2.6  
     2.7 +lemma abs_triangle_half_r:
     2.8 +  fixes y :: "'a::linordered_field"
     2.9 +  shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
    2.10 +  by linarith
    2.11 +
    2.12 +lemma abs_triangle_half_l:
    2.13 +  fixes y :: "'a::linordered_field"
    2.14 +  assumes "abs (x - y) < e / 2"
    2.15 +    and "abs (x' - y) < e / 2"
    2.16 +  shows "abs (x - x') < e"
    2.17 +  using assms by linarith
    2.18 +
    2.19 +lemma eps_leI: 
    2.20 +  assumes "(\<And>e::'a::linordered_idom. 0 < e \<Longrightarrow> x < y + e)" shows "x \<le> y"
    2.21 +  by (metis add_diff_eq assms diff_diff_add diff_gt_0_iff_gt linorder_not_less order_less_irrefl)
    2.22 +
    2.23  lemma sum_clauses:
    2.24    shows "sum f {} = 0"
    2.25      and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
     3.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Aug 13 23:45:45 2017 +0100
     3.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Aug 14 18:54:25 2017 +0100
     3.3 @@ -825,6 +825,9 @@
     3.4    then show ?thesis by simp
     3.5  qed
     3.6  
     3.7 +lemma norm_triangle_le_diff: "norm x + norm y \<le> e \<Longrightarrow> norm (x - y) \<le> e"
     3.8 +  by (meson norm_triangle_ineq4 order_trans)
     3.9 +
    3.10  lemma norm_diff_ineq: "norm a - norm b \<le> norm (a + b)"
    3.11    for a b :: "'a::real_normed_vector"
    3.12  proof -