moved lemmas up
authorimmler
Thu Dec 27 21:32:36 2018 +0100 (4 months ago)
changeset 6951342e08052dae8
parent 69512 2b54f25e66c4
child 69515 5bbb2bd564fa
moved lemmas up
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Thu Dec 27 21:32:34 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Thu Dec 27 21:32:36 2018 +0100
     1.3 @@ -177,11 +177,6 @@
     1.4    using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
     1.5    by (force simp add: power2_eq_square)
     1.6  
     1.7 -lemma norm_triangle_sub:
     1.8 -  fixes x y :: "'a::real_normed_vector"
     1.9 -  shows "norm x \<le> norm y + norm (x - y)"
    1.10 -  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
    1.11 -
    1.12  lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
    1.13    by (simp add: norm_eq_sqrt_inner)
    1.14  
     2.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:32:34 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:32:36 2018 +0100
     2.3 @@ -76,12 +76,6 @@
     2.4    using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
     2.5    unfolding dist_norm[symmetric] .
     2.6  
     2.7 -lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
     2.8 -  by (rule norm_triangle_ineq [THEN order_trans])
     2.9 -
    2.10 -lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
    2.11 -  by (rule norm_triangle_ineq [THEN le_less_trans])
    2.12 -
    2.13  lemma abs_triangle_half_r:
    2.14    fixes y :: "'a::linordered_field"
    2.15    shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
    2.16 @@ -99,13 +93,6 @@
    2.17      and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
    2.18    by (auto simp add: insert_absorb)
    2.19  
    2.20 -lemma sum_norm_bound:
    2.21 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    2.22 -  assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
    2.23 -  shows "norm (sum f S) \<le> of_nat (card S)*K"
    2.24 -  using sum_norm_le[OF K] sum_constant[symmetric]
    2.25 -  by simp
    2.26 -
    2.27  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
    2.28  proof
    2.29    assume "\<forall>x. x \<bullet> y = x \<bullet> z"
     3.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Dec 27 21:32:34 2018 +0100
     3.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Dec 27 21:32:36 2018 +0100
     3.3 @@ -725,6 +725,15 @@
     3.4    then show ?thesis by simp
     3.5  qed
     3.6  
     3.7 +lemma norm_triangle_sub: "norm x \<le> norm y + norm (x - y)"
     3.8 +  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
     3.9 +
    3.10 +lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
    3.11 +  by (rule norm_triangle_ineq [THEN order_trans])
    3.12 +
    3.13 +lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
    3.14 +  by (rule norm_triangle_ineq [THEN le_less_trans])
    3.15 +
    3.16  lemma norm_add_leD: "norm (a + b) \<le> c \<Longrightarrow> norm b \<le> norm a + c"
    3.17    by (metis ab_semigroup_add_class.add.commute add_commute diff_le_eq norm_diff_ineq order_trans)
    3.18  
    3.19 @@ -769,6 +778,13 @@
    3.20  lemma abs_norm_cancel [simp]: "\<bar>norm a\<bar> = norm a"
    3.21    by (rule abs_of_nonneg [OF norm_ge_zero])
    3.22  
    3.23 +lemma sum_norm_bound:
    3.24 +  "norm (sum f S) \<le> of_nat (card S)*K"
    3.25 +  if "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
    3.26 +  for f :: "'b \<Rightarrow> 'a"
    3.27 +  using sum_norm_le[OF that] sum_constant[symmetric]
    3.28 +  by simp
    3.29 +
    3.30  lemma norm_add_less: "norm x < r \<Longrightarrow> norm y < s \<Longrightarrow> norm (x + y) < r + s"
    3.31    by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono])
    3.32