equal
deleted
inserted
replaced
103 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
103 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
104 assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K" |
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" |
105 shows "norm (sum f S) \<le> of_nat (card S)*K" |
106 using sum_norm_le[OF K] sum_constant[symmetric] |
106 using sum_norm_le[OF K] sum_constant[symmetric] |
107 by simp |
107 by simp |
108 |
|
109 lemma sum_group: |
|
110 assumes fS: "finite S" and fT: "finite T" and fST: "f ` S \<subseteq> T" |
|
111 shows "sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) T = sum g S" |
|
112 unfolding sum_image_gen[OF fS, of g f] |
|
113 by (auto intro: sum.neutral sum.mono_neutral_right[OF fT fST]) |
|
114 |
108 |
115 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z" |
109 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z" |
116 proof |
110 proof |
117 assume "\<forall>x. x \<bullet> y = x \<bullet> z" |
111 assume "\<forall>x. x \<bullet> y = x \<bullet> z" |
118 then have "\<forall>x. x \<bullet> (y - z) = 0" |
112 then have "\<forall>x. x \<bullet> (y - z) = 0" |