433 show "inner x y = inner y x" |
433 show "inner x y = inner y x" |
434 unfolding inner_vec_def |
434 unfolding inner_vec_def |
435 by (simp add: inner_commute) |
435 by (simp add: inner_commute) |
436 show "inner (x + y) z = inner x z + inner y z" |
436 show "inner (x + y) z = inner x z + inner y z" |
437 unfolding inner_vec_def |
437 unfolding inner_vec_def |
438 by (simp add: inner_add_left setsum_addf) |
438 by (simp add: inner_add_left setsum.distrib) |
439 show "inner (scaleR r x) y = r * inner x y" |
439 show "inner (scaleR r x) y = r * inner x y" |
440 unfolding inner_vec_def |
440 unfolding inner_vec_def |
441 by (simp add: setsum_right_distrib) |
441 by (simp add: setsum_right_distrib) |
442 show "0 \<le> inner x x" |
442 show "0 \<le> inner x x" |
443 unfolding inner_vec_def |
443 unfolding inner_vec_def |
468 lemma inner_axis_axis: |
468 lemma inner_axis_axis: |
469 "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)" |
469 "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)" |
470 unfolding inner_vec_def |
470 unfolding inner_vec_def |
471 apply (cases "i = j") |
471 apply (cases "i = j") |
472 apply clarsimp |
472 apply clarsimp |
473 apply (subst setsum_diff1' [where a=j], simp_all) |
473 apply (subst setsum.remove [of _ j], simp_all) |
474 apply (rule setsum_0', simp add: axis_def) |
474 apply (rule setsum.neutral, simp add: axis_def) |
475 apply (rule setsum_0', simp add: axis_def) |
475 apply (rule setsum.neutral, simp add: axis_def) |
476 done |
476 done |
477 |
477 |
478 lemma setsum_single: |
478 lemma setsum_single: |
479 assumes "finite A" and "k \<in> A" and "f k = y" |
479 assumes "finite A" and "k \<in> A" and "f k = y" |
480 assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0" |
480 assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0" |
481 shows "(\<Sum>i\<in>A. f i) = y" |
481 shows "(\<Sum>i\<in>A. f i) = y" |
482 apply (subst setsum_diff1' [OF assms(1,2)]) |
482 apply (subst setsum.remove [OF assms(1,2)]) |
483 apply (simp add: setsum_0' assms(3,4)) |
483 apply (simp add: setsum.neutral assms(3,4)) |
484 done |
484 done |
485 |
485 |
486 lemma inner_axis: "inner x (axis i y) = inner (x $ i) y" |
486 lemma inner_axis: "inner x (axis i y) = inner (x $ i) y" |
487 unfolding inner_vec_def |
487 unfolding inner_vec_def |
488 apply (rule_tac k=i in setsum_single) |
488 apply (rule_tac k=i in setsum_single) |