equal
deleted
inserted
replaced
1 section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close> |
1 section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close> |
2 |
2 |
3 theory Cartesian_Euclidean_Space |
3 theory Cartesian_Euclidean_Space |
4 imports Finite_Cartesian_Product Derivative (* Henstock_Kurzweil_Integration *) |
4 imports Finite_Cartesian_Product Derivative |
5 begin |
5 begin |
6 |
6 |
7 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}" |
7 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}" |
8 by (simp add: subspace_def) |
8 by (simp add: subspace_def) |
9 |
9 |
10 lemma delta_mult_idempotent: |
10 lemma delta_mult_idempotent: |
11 "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" |
11 "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" |
12 by simp |
12 by simp |
13 |
13 |
|
14 (*move up?*) |
14 lemma setsum_UNIV_sum: |
15 lemma setsum_UNIV_sum: |
15 fixes g :: "'a::finite + 'b::finite \<Rightarrow> _" |
16 fixes g :: "'a::finite + 'b::finite \<Rightarrow> _" |
16 shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))" |
17 shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))" |
17 apply (subst UNIV_Plus_UNIV [symmetric]) |
18 apply (subst UNIV_Plus_UNIV [symmetric]) |
18 apply (subst setsum.Plus) |
19 apply (subst setsum.Plus) |
30 fix j assume "j \<in> {i * B..<i * B + B}" |
31 fix j assume "j \<in> {i * B..<i * B + B}" |
31 then show "j \<in> (\<lambda>j. j + i * B) ` {..<B}" |
32 then show "j \<in> (\<lambda>j. j + i * B) ` {..<B}" |
32 by (auto intro!: image_eqI[of _ _ "j - i * B"]) |
33 by (auto intro!: image_eqI[of _ _ "j - i * B"]) |
33 qed simp |
34 qed simp |
34 qed simp |
35 qed simp |
35 |
|
36 |
36 |
37 subsection\<open>Basic componentwise operations on vectors.\<close> |
37 subsection\<open>Basic componentwise operations on vectors.\<close> |
38 |
38 |
39 instantiation vec :: (times, finite) times |
39 instantiation vec :: (times, finite) times |
40 begin |
40 begin |
596 by (simp add: axis_def if_distrib setsum.If_cases vec_eq_iff) |
596 by (simp add: axis_def if_distrib setsum.If_cases vec_eq_iff) |
597 |
597 |
598 lemma basis_expansion: "setsum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" |
598 lemma basis_expansion: "setsum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" |
599 by (auto simp add: axis_def vec_eq_iff if_distrib setsum.If_cases cong del: if_weak_cong) |
599 by (auto simp add: axis_def vec_eq_iff if_distrib setsum.If_cases cong del: if_weak_cong) |
600 |
600 |
601 lemma linear_componentwise: |
601 lemma linear_componentwise_expansion: |
602 fixes f:: "real ^'m \<Rightarrow> real ^ _" |
602 fixes f:: "real ^'m \<Rightarrow> real ^ _" |
603 assumes lf: "linear f" |
603 assumes lf: "linear f" |
604 shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") |
604 shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") |
605 proof - |
605 proof - |
606 let ?M = "(UNIV :: 'm set)" |
606 let ?M = "(UNIV :: 'm set)" |
634 |
634 |
635 lemma matrix_works: |
635 lemma matrix_works: |
636 assumes lf: "linear f" |
636 assumes lf: "linear f" |
637 shows "matrix f *v x = f (x::real ^ 'n)" |
637 shows "matrix f *v x = f (x::real ^ 'n)" |
638 apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute) |
638 apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute) |
639 apply clarify |
639 by (simp add: linear_componentwise_expansion lf) |
640 apply (rule linear_componentwise[OF lf, symmetric]) |
|
641 done |
|
642 |
640 |
643 lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))" |
641 lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))" |
644 by (simp add: ext matrix_works) |
642 by (simp add: ext matrix_works) |
645 |
643 |
646 lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A" |
644 lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A" |