src/HOL/Analysis/Linear_Algebra.thy
changeset 69513 42e08052dae8
parent 69510 0f31dd2e540d
child 69516 09bb8f470959
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:32:34 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Dec 27 21:32:36 2018 +0100
     1.3 @@ -76,12 +76,6 @@
     1.4    using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
     1.5    unfolding dist_norm[symmetric] .
     1.6  
     1.7 -lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e"
     1.8 -  by (rule norm_triangle_ineq [THEN order_trans])
     1.9 -
    1.10 -lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e"
    1.11 -  by (rule norm_triangle_ineq [THEN le_less_trans])
    1.12 -
    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 @@ -99,13 +93,6 @@
    1.17      and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)"
    1.18    by (auto simp add: insert_absorb)
    1.19  
    1.20 -lemma sum_norm_bound:
    1.21 -  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    1.22 -  assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
    1.23 -  shows "norm (sum f S) \<le> of_nat (card S)*K"
    1.24 -  using sum_norm_le[OF K] sum_constant[symmetric]
    1.25 -  by simp
    1.26 -
    1.27  lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
    1.28  proof
    1.29    assume "\<forall>x. x \<bullet> y = x \<bullet> z"