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