24 |
25 |
25 csuminf :: (nat=>complex) => complex |
26 csuminf :: (nat=>complex) => complex |
26 "csuminf f == (@s. f csums s)" |
27 "csuminf f == (@s. f csums s)" |
27 *) |
28 *) |
28 |
29 |
|
30 lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0" |
|
31 by (induct_tac "n", auto) |
|
32 |
|
33 lemma sumc_eq_bounds [simp]: "sumc m m f = 0" |
|
34 by (induct_tac "m", auto) |
|
35 |
|
36 lemma sumc_Suc_eq [simp]: "sumc m (Suc m) f = f(m)" |
|
37 by auto |
|
38 |
|
39 lemma sumc_add_lbound_zero [simp]: "sumc (m+k) k f = 0" |
|
40 by (induct_tac "k", auto) |
|
41 |
|
42 lemma sumc_add: "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)" |
|
43 apply (induct_tac "n") |
|
44 apply (auto simp add: add_ac) |
|
45 done |
|
46 |
|
47 lemma sumc_mult: "r * sumc m n f = sumc m n (%n. r * f n)" |
|
48 apply (induct_tac "n", auto) |
|
49 apply (auto simp add: right_distrib) |
|
50 done |
|
51 |
|
52 lemma sumc_split_add [rule_format]: |
|
53 "n < p --> sumc 0 n f + sumc n p f = sumc 0 p f" |
|
54 apply (induct_tac "p") |
|
55 apply (auto dest!: leI dest: le_anti_sym) |
|
56 done |
|
57 |
|
58 lemma sumc_split_add_minus: |
|
59 "n < p ==> sumc 0 p f + - sumc 0 n f = sumc n p f" |
|
60 apply (drule_tac f1 = f in sumc_split_add [symmetric]) |
|
61 apply (simp add: add_ac) |
|
62 done |
|
63 |
|
64 lemma sumc_cmod: "cmod(sumc m n f) \<le> sumr m n (%i. cmod(f i))" |
|
65 apply (induct_tac "n") |
|
66 apply (auto intro: complex_mod_triangle_ineq [THEN order_trans]) |
|
67 done |
|
68 |
|
69 lemma sumc_fun_eq [rule_format (no_asm)]: |
|
70 "(\<forall>r. m \<le> r & r < n --> f r = g r) --> sumc m n f = sumc m n g" |
|
71 by (induct_tac "n", auto) |
|
72 |
|
73 lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r" |
|
74 apply (induct_tac "n") |
|
75 apply (auto simp add: left_distrib complex_of_real_add [symmetric] real_of_nat_Suc) |
|
76 done |
|
77 |
|
78 lemma sumc_add_mult_const: |
|
79 "sumc 0 n f + -(complex_of_real(real n) * r) = sumc 0 n (%i. f i + -r)" |
|
80 by (simp add: sumc_add [symmetric]) |
|
81 |
|
82 lemma sumc_diff_mult_const: |
|
83 "sumc 0 n f - (complex_of_real(real n)*r) = sumc 0 n (%i. f i - r)" |
|
84 by (simp add: diff_minus sumc_add_mult_const) |
|
85 |
|
86 lemma sumc_less_bounds_zero [rule_format]: "n < m --> sumc m n f = 0" |
|
87 by (induct_tac "n", auto) |
|
88 |
|
89 lemma sumc_minus: "sumc m n (%i. - f i) = - sumc m n f" |
|
90 by (induct_tac "n", auto) |
|
91 |
|
92 lemma sumc_shift_bounds: "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))" |
|
93 by (induct_tac "n", auto) |
|
94 |
|
95 lemma sumc_minus_one_complexpow_zero [simp]: |
|
96 "sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0" |
|
97 by (induct_tac "n", auto) |
|
98 |
|
99 lemma sumc_interval_const [rule_format (no_asm)]: |
|
100 "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na |
|
101 --> sumc m na f = (complex_of_real(real (na - m)) * r)" |
|
102 apply (induct_tac "na") |
|
103 apply (auto simp add: Suc_diff_le real_of_nat_Suc complex_of_real_add [symmetric] left_distrib) |
|
104 done |
|
105 |
|
106 lemma sumc_interval_const2 [rule_format (no_asm)]: |
|
107 "(\<forall>n. m \<le> n --> f n = r) & m \<le> na |
|
108 --> sumc m na f = (complex_of_real(real (na - m)) * r)" |
|
109 apply (induct_tac "na") |
|
110 apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc complex_of_real_add [symmetric]) |
|
111 done |
|
112 |
|
113 (*** |
|
114 Goal "(\<forall>n. m \<le> n --> 0 \<le> cmod(f n)) & m < k --> cmod(sumc 0 m f) \<le> cmod(sumc 0 k f)" |
|
115 by (induct_tac "k" 1) |
|
116 by (Step_tac 1) |
|
117 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le]))); |
|
118 by (ALLGOALS(dres_inst_tac [("x","n")] spec)); |
|
119 by (Step_tac 1) |
|
120 by (dtac le_imp_less_or_eq 1 THEN Step_tac 1) |
|
121 by (dtac add_mono 2) |
|
122 by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS add_mono) 1); |
|
123 by Auto_tac |
|
124 qed_spec_mp "sumc_le"; |
|
125 |
|
126 Goal "!!f g. (\<forall>r. m \<le> r & r < n --> f r \<le> g r) \ |
|
127 \ --> sumc m n f \<le> sumc m n g"; |
|
128 by (induct_tac "n" 1) |
|
129 by (auto_tac (claset() addIs [add_mono], |
|
130 simpset() addsimps [le_def])); |
|
131 qed_spec_mp "sumc_le2"; |
|
132 |
|
133 Goal "(\<forall>n. 0 \<le> f n) --> 0 \<le> sumc m n f"; |
|
134 by (induct_tac "n" 1) |
|
135 by Auto_tac |
|
136 by (dres_inst_tac [("x","n")] spec 1); |
|
137 by (arith_tac 1) |
|
138 qed_spec_mp "sumc_ge_zero"; |
|
139 |
|
140 Goal "(\<forall>n. m \<le> n --> 0 \<le> f n) --> 0 \<le> sumc m n f"; |
|
141 by (induct_tac "n" 1) |
|
142 by Auto_tac |
|
143 by (dres_inst_tac [("x","n")] spec 1); |
|
144 by (arith_tac 1) |
|
145 qed_spec_mp "sumc_ge_zero2"; |
|
146 ***) |
|
147 |
|
148 lemma sumr_cmod_ge_zero [iff]: "0 \<le> sumr m n (%n. cmod (f n))" |
|
149 apply (induct_tac "n", auto) |
|
150 apply (rule_tac j = 0 in real_le_trans, auto) |
|
151 done |
|
152 |
|
153 lemma rabs_sumc_cmod_cancel [simp]: |
|
154 "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))" |
|
155 by (simp add: abs_if linorder_not_less) |
|
156 |
|
157 lemma sumc_zero: |
|
158 "\<forall>n. N \<le> n --> f n = 0 |
|
159 ==> \<forall>m n. N \<le> m --> sumc m n f = 0" |
|
160 apply safe |
|
161 apply (induct_tac "n", auto) |
|
162 done |
|
163 |
|
164 lemma fun_zero_sumc_zero: |
|
165 "\<forall>n. N \<le> n --> f (Suc n) = 0 |
|
166 ==> \<forall>m n. Suc N \<le> m --> sumc m n f = 0" |
|
167 apply (rule sumc_zero, safe) |
|
168 apply (drule_tac x = "n - 1" in spec, auto, arith) |
|
169 done |
|
170 |
|
171 lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0" |
|
172 apply (induct_tac "n") |
|
173 apply (case_tac [2] "n", auto) |
|
174 done |
|
175 |
|
176 lemma sumc_diff: "sumc m n f - sumc m n g = sumc m n (%n. f n - g n)" |
|
177 by (simp add: diff_minus sumc_add [symmetric] sumc_minus) |
|
178 |
|
179 lemma sumc_subst [rule_format (no_asm)]: |
|
180 "(\<forall>p. (m \<le> p & p < m + n --> (f p = g p))) --> sumc m n f = sumc m n g" |
|
181 by (induct_tac "n", auto) |
|
182 |
|
183 lemma sumc_group [simp]: |
|
184 "sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f" |
|
185 apply (subgoal_tac "k = 0 | 0 < k", auto) |
|
186 apply (induct_tac "n") |
|
187 apply (auto simp add: sumc_split_add add_commute) |
|
188 done |
|
189 |
|
190 ML |
|
191 {* |
|
192 val sumc_Suc_zero = thm "sumc_Suc_zero"; |
|
193 val sumc_eq_bounds = thm "sumc_eq_bounds"; |
|
194 val sumc_Suc_eq = thm "sumc_Suc_eq"; |
|
195 val sumc_add_lbound_zero = thm "sumc_add_lbound_zero"; |
|
196 val sumc_add = thm "sumc_add"; |
|
197 val sumc_mult = thm "sumc_mult"; |
|
198 val sumc_split_add = thm "sumc_split_add"; |
|
199 val sumc_split_add_minus = thm "sumc_split_add_minus"; |
|
200 val sumc_cmod = thm "sumc_cmod"; |
|
201 val sumc_fun_eq = thm "sumc_fun_eq"; |
|
202 val sumc_const = thm "sumc_const"; |
|
203 val sumc_add_mult_const = thm "sumc_add_mult_const"; |
|
204 val sumc_diff_mult_const = thm "sumc_diff_mult_const"; |
|
205 val sumc_less_bounds_zero = thm "sumc_less_bounds_zero"; |
|
206 val sumc_minus = thm "sumc_minus"; |
|
207 val sumc_shift_bounds = thm "sumc_shift_bounds"; |
|
208 val sumc_minus_one_complexpow_zero = thm "sumc_minus_one_complexpow_zero"; |
|
209 val sumc_interval_const = thm "sumc_interval_const"; |
|
210 val sumc_interval_const2 = thm "sumc_interval_const2"; |
|
211 val sumr_cmod_ge_zero = thm "sumr_cmod_ge_zero"; |
|
212 val rabs_sumc_cmod_cancel = thm "rabs_sumc_cmod_cancel"; |
|
213 val sumc_zero = thm "sumc_zero"; |
|
214 val fun_zero_sumc_zero = thm "fun_zero_sumc_zero"; |
|
215 val sumc_one_lb_complexpow_zero = thm "sumc_one_lb_complexpow_zero"; |
|
216 val sumc_diff = thm "sumc_diff"; |
|
217 val sumc_subst = thm "sumc_subst"; |
|
218 val sumc_group = thm "sumc_group"; |
|
219 *} |
|
220 |
29 end |
221 end |
30 |
222 |