25 using insert |
25 using insert |
26 apply auto |
26 apply auto |
27 done |
27 done |
28 qed auto |
28 qed auto |
29 |
29 |
30 lemma sum_sum_product: |
30 lemma sum_Sigma_product: |
31 assumes "finite s" |
31 assumes "finite S" |
32 and "\<forall>i\<in>s. finite (t i)" |
32 and "\<And>i. i \<in> S \<Longrightarrow> finite (T i)" |
33 shows "sum (\<lambda>i. sum (x i) (t i)::real) s = |
33 shows "(\<Sum>i\<in>S. sum (x i) (T i)) = (\<Sum>(i, j)\<in>Sigma S T. x i j)" |
34 sum (\<lambda>(i,j). x i j) {(i,j) | i j. i \<in> s \<and> j \<in> t i}" |
|
35 using assms |
34 using assms |
36 proof induct |
35 proof induct |
37 case (insert a s) |
36 case empty |
38 have *: "{(i, j) |i j. i \<in> insert a s \<and> j \<in> t i} = |
37 then show ?case |
39 (\<lambda>y. (a,y)) ` (t a) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto |
38 by simp |
|
39 next |
|
40 case (insert a S) |
40 show ?case |
41 show ?case |
41 unfolding * |
42 by (simp add: insert.hyps(1) insert.prems sum.Sigma) |
42 apply (subst sum.union_disjoint) |
43 qed |
43 unfolding sum.insert[OF insert(1-2)] |
|
44 prefer 4 |
|
45 apply (subst insert(3)) |
|
46 unfolding add_right_cancel |
|
47 proof - |
|
48 show "sum (x a) (t a) = (\<Sum>(xa, y)\<in> Pair a ` t a. x xa y)" |
|
49 apply (subst sum.reindex) |
|
50 unfolding inj_on_def |
|
51 apply auto |
|
52 done |
|
53 show "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}" |
|
54 apply (rule finite_product_dependent) |
|
55 using insert |
|
56 apply auto |
|
57 done |
|
58 qed (insert insert, auto) |
|
59 qed auto |
|
60 |
44 |
61 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib |
45 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib |
62 scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff |
46 scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff |
63 scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one |
47 scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one |
64 |
48 |