13957
|
1 |
(* Title : CSeries.thy
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 2002 University of Edinburgh
|
|
4 |
*)
|
|
5 |
|
14406
|
6 |
header{*Finite Summation and Infinite Series for Complex Numbers*}
|
|
7 |
|
15131
|
8 |
theory CSeries
|
15140
|
9 |
imports CStar
|
15131
|
10 |
begin
|
13957
|
11 |
|
|
12 |
consts sumc :: "[nat,nat,(nat=>complex)] => complex"
|
|
13 |
primrec
|
14406
|
14 |
sumc_0: "sumc m 0 f = 0"
|
|
15 |
sumc_Suc: "sumc m (Suc n) f = (if n < m then 0 else sumc m n f + f(n))"
|
13957
|
16 |
|
|
17 |
(*
|
19765
|
18 |
definition
|
13957
|
19 |
|
|
20 |
needs convergence of complex sequences
|
|
21 |
|
|
22 |
csums :: [nat=>complex,complex] => bool (infixr 80)
|
19765
|
23 |
"f sums s = (%n. sumr 0 n f) ----C> s"
|
13957
|
24 |
|
|
25 |
csummable :: (nat=>complex) => bool
|
19765
|
26 |
"csummable f = (EX s. f csums s)"
|
13957
|
27 |
|
|
28 |
csuminf :: (nat=>complex) => complex
|
19765
|
29 |
"csuminf f = (@s. f csums s)"
|
13957
|
30 |
*)
|
|
31 |
|
14406
|
32 |
lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0"
|
15251
|
33 |
by (induct "n", auto)
|
14406
|
34 |
|
|
35 |
lemma sumc_eq_bounds [simp]: "sumc m m f = 0"
|
15251
|
36 |
by (induct "m", auto)
|
14406
|
37 |
|
|
38 |
lemma sumc_Suc_eq [simp]: "sumc m (Suc m) f = f(m)"
|
|
39 |
by auto
|
|
40 |
|
|
41 |
lemma sumc_add_lbound_zero [simp]: "sumc (m+k) k f = 0"
|
15251
|
42 |
by (induct "k", auto)
|
14406
|
43 |
|
|
44 |
lemma sumc_add: "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)"
|
15251
|
45 |
apply (induct "n")
|
14406
|
46 |
apply (auto simp add: add_ac)
|
|
47 |
done
|
|
48 |
|
|
49 |
lemma sumc_mult: "r * sumc m n f = sumc m n (%n. r * f n)"
|
15251
|
50 |
apply (induct "n", auto)
|
14406
|
51 |
apply (auto simp add: right_distrib)
|
|
52 |
done
|
|
53 |
|
|
54 |
lemma sumc_split_add [rule_format]:
|
|
55 |
"n < p --> sumc 0 n f + sumc n p f = sumc 0 p f"
|
15251
|
56 |
apply (induct "p")
|
14406
|
57 |
apply (auto dest!: leI dest: le_anti_sym)
|
|
58 |
done
|
|
59 |
|
|
60 |
lemma sumc_split_add_minus:
|
|
61 |
"n < p ==> sumc 0 p f + - sumc 0 n f = sumc n p f"
|
|
62 |
apply (drule_tac f1 = f in sumc_split_add [symmetric])
|
|
63 |
apply (simp add: add_ac)
|
|
64 |
done
|
|
65 |
|
15539
|
66 |
lemma sumc_cmod: "cmod(sumc m n f) \<le> (\<Sum>i=m..<n. cmod(f i))"
|
15251
|
67 |
apply (induct "n")
|
14406
|
68 |
apply (auto intro: complex_mod_triangle_ineq [THEN order_trans])
|
|
69 |
done
|
|
70 |
|
|
71 |
lemma sumc_fun_eq [rule_format (no_asm)]:
|
|
72 |
"(\<forall>r. m \<le> r & r < n --> f r = g r) --> sumc m n f = sumc m n g"
|
15251
|
73 |
by (induct "n", auto)
|
14406
|
74 |
|
|
75 |
lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r"
|
15251
|
76 |
apply (induct "n")
|
15013
|
77 |
apply (auto simp add: left_distrib real_of_nat_Suc)
|
14406
|
78 |
done
|
|
79 |
|
|
80 |
lemma sumc_add_mult_const:
|
|
81 |
"sumc 0 n f + -(complex_of_real(real n) * r) = sumc 0 n (%i. f i + -r)"
|
|
82 |
by (simp add: sumc_add [symmetric])
|
|
83 |
|
|
84 |
lemma sumc_diff_mult_const:
|
|
85 |
"sumc 0 n f - (complex_of_real(real n)*r) = sumc 0 n (%i. f i - r)"
|
|
86 |
by (simp add: diff_minus sumc_add_mult_const)
|
|
87 |
|
|
88 |
lemma sumc_less_bounds_zero [rule_format]: "n < m --> sumc m n f = 0"
|
15251
|
89 |
by (induct "n", auto)
|
14406
|
90 |
|
|
91 |
lemma sumc_minus: "sumc m n (%i. - f i) = - sumc m n f"
|
15251
|
92 |
by (induct "n", auto)
|
14406
|
93 |
|
|
94 |
lemma sumc_shift_bounds: "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))"
|
15251
|
95 |
by (induct "n", auto)
|
14406
|
96 |
|
|
97 |
lemma sumc_minus_one_complexpow_zero [simp]:
|
|
98 |
"sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0"
|
15251
|
99 |
by (induct "n", auto)
|
14406
|
100 |
|
|
101 |
lemma sumc_interval_const [rule_format (no_asm)]:
|
|
102 |
"(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
|
15013
|
103 |
--> sumc m na f = (complex_of_real(real (na - m)) * r)"
|
15251
|
104 |
apply (induct "na")
|
15013
|
105 |
apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
|
14406
|
106 |
done
|
|
107 |
|
|
108 |
lemma sumc_interval_const2 [rule_format (no_asm)]:
|
|
109 |
"(\<forall>n. m \<le> n --> f n = r) & m \<le> na
|
|
110 |
--> sumc m na f = (complex_of_real(real (na - m)) * r)"
|
15251
|
111 |
apply (induct "na")
|
15013
|
112 |
apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
|
14406
|
113 |
done
|
|
114 |
|
|
115 |
(***
|
|
116 |
Goal "(\<forall>n. m \<le> n --> 0 \<le> cmod(f n)) & m < k --> cmod(sumc 0 m f) \<le> cmod(sumc 0 k f)"
|
|
117 |
by (induct_tac "k" 1)
|
|
118 |
by (Step_tac 1)
|
|
119 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le])));
|
|
120 |
by (ALLGOALS(dres_inst_tac [("x","n")] spec));
|
|
121 |
by (Step_tac 1)
|
|
122 |
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1)
|
|
123 |
by (dtac add_mono 2)
|
|
124 |
by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS add_mono) 1);
|
|
125 |
by Auto_tac
|
|
126 |
qed_spec_mp "sumc_le";
|
|
127 |
|
|
128 |
Goal "!!f g. (\<forall>r. m \<le> r & r < n --> f r \<le> g r) \
|
|
129 |
\ --> sumc m n f \<le> sumc m n g";
|
|
130 |
by (induct_tac "n" 1)
|
|
131 |
by (auto_tac (claset() addIs [add_mono],
|
|
132 |
simpset() addsimps [le_def]));
|
|
133 |
qed_spec_mp "sumc_le2";
|
|
134 |
|
|
135 |
Goal "(\<forall>n. 0 \<le> f n) --> 0 \<le> sumc m n f";
|
|
136 |
by (induct_tac "n" 1)
|
|
137 |
by Auto_tac
|
|
138 |
by (dres_inst_tac [("x","n")] spec 1);
|
|
139 |
by (arith_tac 1)
|
|
140 |
qed_spec_mp "sumc_ge_zero";
|
|
141 |
|
|
142 |
Goal "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumc m n f";
|
|
143 |
by (induct_tac "n" 1)
|
|
144 |
by Auto_tac
|
|
145 |
by (dres_inst_tac [("x","n")] spec 1);
|
|
146 |
by (arith_tac 1)
|
|
147 |
qed_spec_mp "sumc_ge_zero2";
|
|
148 |
***)
|
|
149 |
|
15539
|
150 |
lemma sumr_cmod_ge_zero [iff]: "0 \<le> (\<Sum>n=m..<n::nat. cmod (f n))"
|
|
151 |
by (induct "n", auto simp add: add_increasing)
|
14406
|
152 |
|
|
153 |
lemma rabs_sumc_cmod_cancel [simp]:
|
15539
|
154 |
"abs (\<Sum>n=m..<n::nat. cmod (f n)) = (\<Sum>n=m..<n. cmod (f n))"
|
14406
|
155 |
by (simp add: abs_if linorder_not_less)
|
|
156 |
|
|
157 |
lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0"
|
15251
|
158 |
apply (induct "n")
|
14406
|
159 |
apply (case_tac [2] "n", auto)
|
|
160 |
done
|
|
161 |
|
|
162 |
lemma sumc_diff: "sumc m n f - sumc m n g = sumc m n (%n. f n - g n)"
|
|
163 |
by (simp add: diff_minus sumc_add [symmetric] sumc_minus)
|
|
164 |
|
|
165 |
lemma sumc_subst [rule_format (no_asm)]:
|
|
166 |
"(\<forall>p. (m \<le> p & p < m + n --> (f p = g p))) --> sumc m n f = sumc m n g"
|
15251
|
167 |
by (induct "n", auto)
|
14406
|
168 |
|
|
169 |
lemma sumc_group [simp]:
|
|
170 |
"sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f"
|
|
171 |
apply (subgoal_tac "k = 0 | 0 < k", auto)
|
15251
|
172 |
apply (induct "n")
|
14406
|
173 |
apply (auto simp add: sumc_split_add add_commute)
|
|
174 |
done
|
|
175 |
|
13957
|
176 |
end
|
|
177 |
|