equal
deleted
inserted
replaced
74 and "norm (x' - y) < e / 2" |
74 and "norm (x' - y) < e / 2" |
75 shows "norm (x - x') < e" |
75 shows "norm (x - x') < e" |
76 using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]] |
76 using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]] |
77 unfolding dist_norm[symmetric] . |
77 unfolding dist_norm[symmetric] . |
78 |
78 |
79 lemma norm_triangle_le: "norm x + norm y \<le> e \<Longrightarrow> norm (x + y) \<le> e" |
|
80 by (rule norm_triangle_ineq [THEN order_trans]) |
|
81 |
|
82 lemma norm_triangle_lt: "norm x + norm y < e \<Longrightarrow> norm (x + y) < e" |
|
83 by (rule norm_triangle_ineq [THEN le_less_trans]) |
|
84 |
|
85 lemma abs_triangle_half_r: |
79 lemma abs_triangle_half_r: |
86 fixes y :: "'a::linordered_field" |
80 fixes y :: "'a::linordered_field" |
87 shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e" |
81 shows "abs (y - x1) < e / 2 \<Longrightarrow> abs (y - x2) < e / 2 \<Longrightarrow> abs (x1 - x2) < e" |
88 by linarith |
82 by linarith |
89 |
83 |
96 |
90 |
97 lemma sum_clauses: |
91 lemma sum_clauses: |
98 shows "sum f {} = 0" |
92 shows "sum f {} = 0" |
99 and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)" |
93 and "finite S \<Longrightarrow> sum f (insert x S) = (if x \<in> S then sum f S else f x + sum f S)" |
100 by (auto simp add: insert_absorb) |
94 by (auto simp add: insert_absorb) |
101 |
|
102 lemma sum_norm_bound: |
|
103 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
|
104 assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K" |
|
105 shows "norm (sum f S) \<le> of_nat (card S)*K" |
|
106 using sum_norm_le[OF K] sum_constant[symmetric] |
|
107 by simp |
|
108 |
95 |
109 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z" |
96 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z" |
110 proof |
97 proof |
111 assume "\<forall>x. x \<bullet> y = x \<bullet> z" |
98 assume "\<forall>x. x \<bullet> y = x \<bullet> z" |
112 then have "\<forall>x. x \<bullet> (y - z) = 0" |
99 then have "\<forall>x. x \<bullet> (y - z) = 0" |