--- 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)
--- 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"
--- 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])