(* Title : CSeries.thy Author : Jacques D. Fleuriot Copyright : 2002 University of Edinburgh *) header{*Finite Summation and Infinite Series for Complex Numbers*} theory CSeries imports CStar begin consts sumc :: "[nat,nat,(nat=>complex)] => complex" primrec sumc_0: "sumc m 0 f = 0" sumc_Suc: "sumc m (Suc n) f = (if n < m then 0 else sumc m n f + f(n))" (* constdefs needs convergence of complex sequences csums :: [nat=>complex,complex] => bool (infixr 80) "f sums s == (%n. sumr 0 n f) ----C> s" csummable :: (nat=>complex) => bool "csummable f == (EX s. f csums s)" csuminf :: (nat=>complex) => complex "csuminf f == (@s. f csums s)" *) lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0" by (induct "n", auto) lemma sumc_eq_bounds [simp]: "sumc m m f = 0" by (induct "m", auto) lemma sumc_Suc_eq [simp]: "sumc m (Suc m) f = f(m)" by auto lemma sumc_add_lbound_zero [simp]: "sumc (m+k) k f = 0" by (induct "k", auto) lemma sumc_add: "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)" apply (induct "n") apply (auto simp add: add_ac) done lemma sumc_mult: "r * sumc m n f = sumc m n (%n. r * f n)" apply (induct "n", auto) apply (auto simp add: right_distrib) done lemma sumc_split_add [rule_format]: "n < p --> sumc 0 n f + sumc n p f = sumc 0 p f" apply (induct "p") apply (auto dest!: leI dest: le_anti_sym) done lemma sumc_split_add_minus: "n < p ==> sumc 0 p f + - sumc 0 n f = sumc n p f" apply (drule_tac f1 = f in sumc_split_add [symmetric]) apply (simp add: add_ac) done lemma sumc_cmod: "cmod(sumc m n f) ≤ (∑i=m..<n. cmod(f i))" apply (induct "n") apply (auto intro: complex_mod_triangle_ineq [THEN order_trans]) done lemma sumc_fun_eq [rule_format (no_asm)]: "(∀r. m ≤ r & r < n --> f r = g r) --> sumc m n f = sumc m n g" by (induct "n", auto) lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r" apply (induct "n") apply (auto simp add: left_distrib real_of_nat_Suc) done lemma sumc_add_mult_const: "sumc 0 n f + -(complex_of_real(real n) * r) = sumc 0 n (%i. f i + -r)" by (simp add: sumc_add [symmetric]) lemma sumc_diff_mult_const: "sumc 0 n f - (complex_of_real(real n)*r) = sumc 0 n (%i. f i - r)" by (simp add: diff_minus sumc_add_mult_const) lemma sumc_less_bounds_zero [rule_format]: "n < m --> sumc m n f = 0" by (induct "n", auto) lemma sumc_minus: "sumc m n (%i. - f i) = - sumc m n f" by (induct "n", auto) lemma sumc_shift_bounds: "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))" by (induct "n", auto) lemma sumc_minus_one_complexpow_zero [simp]: "sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0" by (induct "n", auto) lemma sumc_interval_const [rule_format (no_asm)]: "(∀n. m ≤ Suc n --> f n = r) & m ≤ na --> sumc m na f = (complex_of_real(real (na - m)) * r)" apply (induct "na") apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib) done lemma sumc_interval_const2 [rule_format (no_asm)]: "(∀n. m ≤ n --> f n = r) & m ≤ na --> sumc m na f = (complex_of_real(real (na - m)) * r)" apply (induct "na") apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc) done (*** Goal "(∀n. m ≤ n --> 0 ≤ cmod(f n)) & m < k --> cmod(sumc 0 m f) ≤ cmod(sumc 0 k f)" by (induct_tac "k" 1) by (Step_tac 1) by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le]))); by (ALLGOALS(dres_inst_tac [("x","n")] spec)); by (Step_tac 1) by (dtac le_imp_less_or_eq 1 THEN Step_tac 1) by (dtac add_mono 2) by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS add_mono) 1); by Auto_tac qed_spec_mp "sumc_le"; Goal "!!f g. (∀r. m ≤ r & r < n --> f r ≤ g r) \ \ --> sumc m n f ≤ sumc m n g"; by (induct_tac "n" 1) by (auto_tac (claset() addIs [add_mono], simpset() addsimps [le_def])); qed_spec_mp "sumc_le2"; Goal "(∀n. 0 ≤ f n) --> 0 ≤ sumc m n f"; by (induct_tac "n" 1) by Auto_tac by (dres_inst_tac [("x","n")] spec 1); by (arith_tac 1) qed_spec_mp "sumc_ge_zero"; Goal "(∀n. m ≤ n --> 0 ≤ f n) --> 0 ≤ sumc m n f"; by (induct_tac "n" 1) by Auto_tac by (dres_inst_tac [("x","n")] spec 1); by (arith_tac 1) qed_spec_mp "sumc_ge_zero2"; ***) lemma sumr_cmod_ge_zero [iff]: "0 ≤ (∑n=m..<n::nat. cmod (f n))" by (induct "n", auto simp add: add_increasing) lemma rabs_sumc_cmod_cancel [simp]: "abs (∑n=m..<n::nat. cmod (f n)) = (∑n=m..<n. cmod (f n))" by (simp add: abs_if linorder_not_less) lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0" apply (induct "n") apply (case_tac [2] "n", auto) done lemma sumc_diff: "sumc m n f - sumc m n g = sumc m n (%n. f n - g n)" by (simp add: diff_minus sumc_add [symmetric] sumc_minus) lemma sumc_subst [rule_format (no_asm)]: "(∀p. (m ≤ p & p < m + n --> (f p = g p))) --> sumc m n f = sumc m n g" by (induct "n", auto) lemma sumc_group [simp]: "sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f" apply (subgoal_tac "k = 0 | 0 < k", auto) apply (induct "n") apply (auto simp add: sumc_split_add add_commute) done ML {* val sumc_Suc_zero = thm "sumc_Suc_zero"; val sumc_eq_bounds = thm "sumc_eq_bounds"; val sumc_Suc_eq = thm "sumc_Suc_eq"; val sumc_add_lbound_zero = thm "sumc_add_lbound_zero"; val sumc_add = thm "sumc_add"; val sumc_mult = thm "sumc_mult"; val sumc_split_add = thm "sumc_split_add"; val sumc_split_add_minus = thm "sumc_split_add_minus"; val sumc_cmod = thm "sumc_cmod"; val sumc_fun_eq = thm "sumc_fun_eq"; val sumc_const = thm "sumc_const"; val sumc_add_mult_const = thm "sumc_add_mult_const"; val sumc_diff_mult_const = thm "sumc_diff_mult_const"; val sumc_less_bounds_zero = thm "sumc_less_bounds_zero"; val sumc_minus = thm "sumc_minus"; val sumc_shift_bounds = thm "sumc_shift_bounds"; val sumc_minus_one_complexpow_zero = thm "sumc_minus_one_complexpow_zero"; val sumc_interval_const = thm "sumc_interval_const"; val sumc_interval_const2 = thm "sumc_interval_const2"; val sumr_cmod_ge_zero = thm "sumr_cmod_ge_zero"; val rabs_sumc_cmod_cancel = thm "rabs_sumc_cmod_cancel"; val sumc_one_lb_complexpow_zero = thm "sumc_one_lb_complexpow_zero"; val sumc_diff = thm "sumc_diff"; val sumc_subst = thm "sumc_subst"; val sumc_group = thm "sumc_group"; *} end
lemma sumc_Suc_zero:
sumc (Suc n) n f = 0
lemma sumc_eq_bounds:
sumc m m f = 0
lemma sumc_Suc_eq:
sumc m (Suc m) f = f m
lemma sumc_add_lbound_zero:
sumc (m + k) k f = 0
lemma sumc_add:
sumc m n f + sumc m n g = sumc m n (%n. f n + g n)
lemma sumc_mult:
r * sumc m n f = sumc m n (%n. r * f n)
lemma sumc_split_add:
n < p ==> sumc 0 n f + sumc n p f = sumc 0 p f
lemma sumc_split_add_minus:
n < p ==> sumc 0 p f + - sumc 0 n f = sumc n p f
lemma sumc_cmod:
cmod (sumc m n f) ≤ (∑i = m..<n. cmod (f i))
lemma sumc_fun_eq:
∀r. m ≤ r ∧ r < n --> f r = g r ==> sumc m n f = sumc m n g
lemma sumc_const:
sumc 0 n (%i. r) = complex_of_real (real n) * r
lemma sumc_add_mult_const:
sumc 0 n f + - (complex_of_real (real n) * r) = sumc 0 n (%i. f i + - r)
lemma sumc_diff_mult_const:
sumc 0 n f - complex_of_real (real n) * r = sumc 0 n (%i. f i - r)
lemma sumc_less_bounds_zero:
n < m ==> sumc m n f = 0
lemma sumc_minus:
sumc m n (%i. - f i) = - sumc m n f
lemma sumc_shift_bounds:
sumc (m + k) (n + k) f = sumc m n (%i. f (i + k))
lemma sumc_minus_one_complexpow_zero:
sumc 0 (2 * n) (%i. -1 ^ Suc i) = 0
lemma sumc_interval_const:
(∀n. m ≤ Suc n --> f n = r) ∧ m ≤ na ==> sumc m na f = complex_of_real (real (na - m)) * r
lemma sumc_interval_const2:
(∀n≥m. f n = r) ∧ m ≤ na ==> sumc m na f = complex_of_real (real (na - m)) * r
lemma sumr_cmod_ge_zero:
0 ≤ (∑n = m..<n. cmod (f n))
lemma rabs_sumc_cmod_cancel:
¦∑n = m..<n. cmod (f n)¦ = (∑n = m..<n. cmod (f n))
lemma sumc_one_lb_complexpow_zero:
sumc 1 n (%n. f n * 0 ^ n) = 0
lemma sumc_diff:
sumc m n f - sumc m n g = sumc m n (%n. f n - g n)
lemma sumc_subst:
∀p. m ≤ p ∧ p < m + n --> f p = g p ==> sumc m n f = sumc m n g
lemma sumc_group:
sumc 0 n (%m. sumc (m * k) (m * k + k) f) = sumc 0 (n * k) f