13957

1 
(* Title : CSeries.ML


2 
Author : Jacques D. Fleuriot


3 
Copyright : 2002 University of Edinburgh


4 
Description : Finite summation and infinite series for complex numbers


5 
*)


6 


7 


8 
Goal "sumc (Suc n) n f = 0";


9 
by (induct_tac "n" 1);


10 
by (Auto_tac);


11 
qed "sumc_Suc_zero";


12 
Addsimps [sumc_Suc_zero];


13 


14 
Goal "sumc m m f = 0";


15 
by (induct_tac "m" 1);


16 
by (Auto_tac);


17 
qed "sumc_eq_bounds";


18 
Addsimps [sumc_eq_bounds];


19 


20 
Goal "sumc m (Suc m) f = f(m)";


21 
by (Auto_tac);


22 
qed "sumc_Suc_eq";


23 
Addsimps [sumc_Suc_eq];


24 


25 
Goal "sumc (m+k) k f = 0";


26 
by (induct_tac "k" 1);


27 
by (Auto_tac);


28 
qed "sumc_add_lbound_zero";


29 
Addsimps [sumc_add_lbound_zero];


30 


31 
Goal "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)";


32 
by (induct_tac "n" 1);

14334

33 
by (auto_tac (claset(),simpset() addsimps add_ac));

13957

34 
qed "sumc_add";


35 


36 
Goal "r * sumc m n f = sumc m n (%n. r * f n)";


37 
by (induct_tac "n" 1);


38 
by (Auto_tac);


39 
by (auto_tac (claset(),simpset() addsimps

14373

40 
[right_distrib]));

13957

41 
qed "sumc_mult";


42 


43 
Goal "n < p > sumc 0 n f + sumc n p f = sumc 0 p f";


44 
by (induct_tac "p" 1);


45 
by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na",


46 
leI] addDs [le_anti_sym], simpset()));


47 
qed_spec_mp "sumc_split_add";


48 


49 
Goal "n < p ==> sumc 0 p f + \


50 
\  sumc 0 n f = sumc n p f";


51 
by (dres_inst_tac [("f1","f")] (sumc_split_add RS sym) 1);

14373

52 
by (asm_simp_tac (simpset() addsimps add_ac) 1);

13957

53 
qed "sumc_split_add_minus";


54 


55 
Goal "cmod(sumc m n f) <= sumr m n (%i. cmod(f i))";


56 
by (induct_tac "n" 1);


57 
by (auto_tac (claset() addIs [complex_mod_triangle_ineq RS order_trans],


58 
simpset()));


59 
qed "sumc_cmod";


60 


61 
Goal "!!f g. (ALL r. m <= r & r < n > f r = g r) \


62 
\ > sumc m n f = sumc m n g";


63 
by (induct_tac "n" 1);


64 
by (Auto_tac);


65 
qed_spec_mp "sumc_fun_eq";


66 


67 
Goal "sumc 0 n (%i. r) = complex_of_real (real n) * r";


68 
by (induct_tac "n" 1);


69 
by (auto_tac (claset(),

14373

70 
simpset() addsimps [left_distrib,

13957

71 
complex_of_real_add RS sym,


72 
real_of_nat_Suc]));


73 
qed "sumc_const";


74 
Addsimps [sumc_const];


75 


76 
Goal "sumc 0 n f + (complex_of_real(real n) * r) = sumc 0 n (%i. f i + r)";


77 
by (full_simp_tac (simpset() addsimps [sumc_add RS sym]) 1);


78 
qed "sumc_add_mult_const";


79 


80 
Goalw [complex_diff_def]


81 
"sumc 0 n f  (complex_of_real(real n)*r) = sumc 0 n (%i. f i  r)";


82 
by (full_simp_tac (simpset() addsimps [sumc_add_mult_const]) 1);


83 
qed "sumc_diff_mult_const";


84 


85 
Goal "n < m > sumc m n f = 0";


86 
by (induct_tac "n" 1);


87 
by Auto_tac;


88 
qed_spec_mp "sumc_less_bounds_zero";


89 
Addsimps [sumc_less_bounds_zero];


90 


91 
Goal "sumc m n (%i.  f i) =  sumc m n f";


92 
by (induct_tac "n" 1);


93 
by Auto_tac;


94 
qed "sumc_minus";


95 


96 
Goal "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))";


97 
by (induct_tac "n" 1);


98 
by (Auto_tac);


99 
qed "sumc_shift_bounds";


100 


101 
Goal "sumc 0 (2*n) (%i. (1) ^ Suc i) = 0";


102 
by (induct_tac "n" 1);


103 
by (Auto_tac);


104 
qed "sumc_minus_one_complexpow_zero";


105 
Addsimps [sumc_minus_one_complexpow_zero];


106 


107 
Goal "(ALL n. m <= Suc n > f n = r) & m <= na \


108 
\ > sumc m na f = (complex_of_real(real (na  m)) * r)";


109 
by (induct_tac "na" 1);

14334

110 
by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n,

13957

111 
real_of_nat_Suc,complex_of_real_add RS sym,

14373

112 
left_distrib]));

13957

113 
qed_spec_mp "sumc_interval_const";


114 


115 
Goal "(ALL n. m <= n > f n = r) & m <= na \


116 
\ > sumc m na f = (complex_of_real(real (na  m)) * r)";


117 
by (induct_tac "na" 1);

14334

118 
by (auto_tac (claset(),simpset() addsimps [left_distrib, Suc_diff_n,

13957

119 
real_of_nat_Suc,complex_of_real_add RS sym,

14373

120 
left_distrib]));

13957

121 
qed_spec_mp "sumc_interval_const2";


122 


123 
(***


124 
Goal "(ALL n. m <= n > 0 <= cmod(f n)) & m < k > cmod(sumc 0 m f) <= cmod(sumc 0 k f)";


125 
by (induct_tac "k" 1);


126 
by (Step_tac 1);


127 
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le])));


128 
by (ALLGOALS(dres_inst_tac [("x","n")] spec));


129 
by (Step_tac 1);


130 
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);

14334

131 
by (dtac add_mono 2);


132 
by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS add_mono) 1);

13957

133 
by (Auto_tac);


134 
qed_spec_mp "sumc_le";


135 


136 
Goal "!!f g. (ALL r. m <= r & r < n > f r <= g r) \


137 
\ > sumc m n f <= sumc m n g";


138 
by (induct_tac "n" 1);

14334

139 
by (auto_tac (claset() addIs [add_mono],

13957

140 
simpset() addsimps [le_def]));


141 
qed_spec_mp "sumc_le2";


142 


143 
Goal "(ALL n. 0 <= f n) > 0 <= sumc m n f";


144 
by (induct_tac "n" 1);


145 
by Auto_tac;


146 
by (dres_inst_tac [("x","n")] spec 1);


147 
by (arith_tac 1);


148 
qed_spec_mp "sumc_ge_zero";


149 


150 
Goal "(ALL n. m <= n > 0 <= f n) > 0 <= sumc m n f";


151 
by (induct_tac "n" 1);


152 
by Auto_tac;


153 
by (dres_inst_tac [("x","n")] spec 1);


154 
by (arith_tac 1);


155 
qed_spec_mp "sumc_ge_zero2";


156 
***)


157 


158 
Goal "0 <= sumr m n (%n. cmod (f n))";


159 
by (induct_tac "n" 1);


160 
by Auto_tac;


161 
by (res_inst_tac [("j","0")] real_le_trans 1);


162 
by Auto_tac;


163 
qed "sumr_cmod_ge_zero";


164 
Addsimps [sumr_cmod_ge_zero];


165 
AddSIs [sumr_cmod_ge_zero];


166 


167 
Goal "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))";


168 
by (rtac (abs_eqI1 RS ssubst) 1 THEN Auto_tac);


169 
qed "rabs_sumc_cmod_cancel";


170 
Addsimps [rabs_sumc_cmod_cancel];


171 


172 
Goal "ALL n. N <= n > f n = 0 \


173 
\ ==> ALL m n. N <= m > sumc m n f = 0";


174 
by (Step_tac 1);


175 
by (induct_tac "n" 1);


176 
by (Auto_tac);


177 
qed "sumc_zero";


178 


179 
Goal "ALL n. N <= n > f (Suc n) = 0 \


180 
\ ==> ALL m n. Suc N <= m > sumc m n f = 0";


181 
by (rtac sumc_zero 1 THEN Step_tac 1);


182 
by (dres_inst_tac [("x","n  1")] spec 1);


183 
by Auto_tac;


184 
by (arith_tac 1);


185 
qed "fun_zero_sumc_zero";


186 


187 
Goal "sumc 1 n (%n. f(n) * 0 ^ n) = 0";


188 
by (induct_tac "n" 1);


189 
by (case_tac "n" 2);


190 
by Auto_tac;


191 
qed "sumc_one_lb_complexpow_zero";


192 
Addsimps [sumc_one_lb_complexpow_zero];


193 


194 
Goalw [complex_diff_def] "sumc m n f  sumc m n g = sumc m n (%n. f n  g n)";


195 
by (simp_tac (simpset() addsimps [sumc_add RS sym,sumc_minus]) 1);


196 
qed "sumc_diff";


197 


198 
Goal "(ALL p. (m <= p & p < m + n > (f p = g p))) > sumc m n f = sumc m n g";


199 
by (induct_tac "n" 1);


200 
by (Auto_tac);


201 
qed_spec_mp "sumc_subst";


202 


203 
Goal "sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f";


204 
by (subgoal_tac "k = 0  0 < k" 1);


205 
by (Auto_tac);


206 
by (induct_tac "n" 1);


207 
by (auto_tac (claset(),simpset() addsimps [sumc_split_add,add_commute]));


208 
qed "sumc_group";


209 
Addsimps [sumc_group];


210 
