equal
deleted
inserted
replaced
126 |
126 |
127 lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2" |
127 lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2" |
128 unfolding power2_norm_eq_inner inner_simps inner_commute by auto |
128 unfolding power2_norm_eq_inner inner_simps inner_commute by auto |
129 |
129 |
130 lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2" |
130 lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2" |
131 unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:algebra_simps) |
131 unfolding power2_norm_eq_inner inner_simps inner_commute |
|
132 by (auto simp add: algebra_simps) |
132 |
133 |
133 text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *} |
134 text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *} |
134 |
135 |
135 lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs") |
136 lemma vector_eq: "x = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y \<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs") |
136 proof |
137 proof |
159 lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e" |
160 lemma norm_triangle_lt: "norm(x) + norm(y) < e ==> norm(x + y) < e" |
160 by (rule norm_triangle_ineq [THEN le_less_trans]) |
161 by (rule norm_triangle_ineq [THEN le_less_trans]) |
161 |
162 |
162 lemma setsum_clauses: |
163 lemma setsum_clauses: |
163 shows "setsum f {} = 0" |
164 shows "setsum f {} = 0" |
164 and "finite S \<Longrightarrow> setsum f (insert x S) = (if x \<in> S then setsum f S else f x + setsum f S)" |
165 and "finite S \<Longrightarrow> setsum f (insert x S) = (if x \<in> S then setsum f S else f x + setsum f S)" |
165 by (auto simp add: insert_absorb) |
166 by (auto simp add: insert_absorb) |
166 |
167 |
167 lemma setsum_norm_le: |
168 lemma setsum_norm_le: |
168 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
169 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
169 assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x" |
170 assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x" |
408 done |
409 done |
409 |
410 |
410 |
411 |
411 lemma infinite_enumerate: assumes fS: "infinite S" |
412 lemma infinite_enumerate: assumes fS: "infinite S" |
412 shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)" |
413 shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)" |
413 unfolding subseq_def |
414 unfolding subseq_def |
414 using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto |
415 using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto |
415 |
416 |
416 lemma approachable_lt_le: "(\<exists>(d::real)>0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)" |
417 lemma approachable_lt_le: "(\<exists>(d::real)>0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)" |
417 apply auto |
418 apply auto |
418 apply (rule_tac x="d/2" in exI) |
419 apply (rule_tac x="d/2" in exI) |
419 apply auto |
420 apply auto |