# HG changeset patch
# User immler
# Date 1545942756 -3600
# Node ID 42e08052dae82b7af9d2147cf790aea40655ad64
# Parent  2b54f25e66c4fb6f43302670b39bdb6d7ecb57da
moved lemmas up

diff -r 2b54f25e66c4 -r 42e08052dae8 src/HOL/Analysis/Inner_Product.thy
--- a/src/HOL/Analysis/Inner_Product.thy	Thu Dec 27 21:32:34 2018 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy	Thu Dec 27 21:32:36 2018 +0100
@@ -177,11 +177,6 @@
   using isCont_power[OF continuous_ident, of x, unfolded isCont_def LIM_eq, rule_format, of e 2]
   by (force simp add: power2_eq_square)
 
-lemma norm_triangle_sub:
-  fixes x y :: "'a::real_normed_vector"
-  shows "norm x \<le> norm y + norm (x - y)"
-  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
-
 lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
   by (simp add: norm_eq_sqrt_inner)
 
diff -r 2b54f25e66c4 -r 42e08052dae8 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:32:34 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:32:36 2018 +0100
@@ -76,12 +76,6 @@
   using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
   unfolding dist_norm[symmetric] .
 
-lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
-  by (rule norm_triangle_ineq [THEN order_trans])
-
-lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
-  by (rule norm_triangle_ineq [THEN le_less_trans])
-
 lemma abs_triangle_half_r:
   fixes y :: "'a::linordered_field"
   shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e"
@@ -99,13 +93,6 @@
     and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
   by (auto simp add: insert_absorb)
 
-lemma sum_norm_bound:
-  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
-  shows "norm (sum f S) \<le> of_nat (card S)*K"
-  using sum_norm_le[OF K] sum_constant[symmetric]
-  by simp
-
 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
 proof
   assume "\<forall>x. x \<bullet> y = x \<bullet> z"
diff -r 2b54f25e66c4 -r 42e08052dae8 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Dec 27 21:32:34 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Dec 27 21:32:36 2018 +0100
@@ -725,6 +725,15 @@
   then show ?thesis by simp
 qed
 
+lemma norm_triangle_sub: "norm x \<le> norm y + norm (x - y)"
+  using norm_triangle_ineq[of "y" "x - y"] by (simp add: field_simps)
+
+lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
+  by (rule norm_triangle_ineq [THEN order_trans])
+
+lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
+  by (rule norm_triangle_ineq [THEN le_less_trans])
+
 lemma norm_add_leD: "norm (a + b) \<le> c \<Longrightarrow> norm b \<le> norm a + c"
   by (metis ab_semigroup_add_class.add.commute add_commute diff_le_eq norm_diff_ineq order_trans)
 
@@ -769,6 +778,13 @@
 lemma abs_norm_cancel [simp]: "\<bar>norm a\<bar> = norm a"
   by (rule abs_of_nonneg [OF norm_ge_zero])
 
+lemma sum_norm_bound:
+  "norm (sum f S) \<le> of_nat (card S)*K"
+  if "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
+  for f :: "'b \<Rightarrow> 'a"
+  using sum_norm_le[OF that] sum_constant[symmetric]
+  by simp
+
 lemma norm_add_less: "norm x < r \<Longrightarrow> norm y < s \<Longrightarrow> norm (x + y) < r + s"
   by (rule order_le_less_trans [OF norm_triangle_ineq add_strict_mono])