src/HOL/ex/Summation.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 39302 d7728f65b353 permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
```     1 (* Author: Florian Haftmann, TU Muenchen *)
```
```     2
```
```     3 header {* Some basic facts about discrete summation *}
```
```     4
```
```     5 theory Summation
```
```     6 imports Main
```
```     7 begin
```
```     8
```
```     9 text {* Auxiliary. *}
```
```    10
```
```    11 lemma add_setsum_orient:
```
```    12   "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
```
```    13   by (fact add.commute)
```
```    14
```
```    15 lemma add_setsum_int:
```
```    16   fixes j k l :: int
```
```    17   shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"
```
```    18   by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)
```
```    19
```
```    20 text {* The shift operator. *}
```
```    21
```
```    22 definition \<Delta> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> 'a" where
```
```    23   "\<Delta> f k = f (k + 1) - f k"
```
```    24
```
```    25 lemma \<Delta>_shift:
```
```    26   "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
```
```    27   by (simp add: \<Delta>_def fun_eq_iff)
```
```    28
```
```    29 lemma \<Delta>_same_shift:
```
```    30   assumes "\<Delta> f = \<Delta> g"
```
```    31   shows "\<exists>l. plus l \<circ> f = g"
```
```    32 proof -
```
```    33   fix k
```
```    34   from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
```
```    35   then have k_incr: "\<And>k. f (k + 1) - g (k + 1) = f k - g k"
```
```    36     by (simp add: \<Delta>_def algebra_simps)
```
```    37   then have "\<And>k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)"
```
```    38     by blast
```
```    39   then have k_decr: "\<And>k. f (k - 1) - g (k - 1) = f k - g k"
```
```    40     by simp
```
```    41   have "\<And>k. f k - g k = f 0 - g 0"
```
```    42   proof -
```
```    43     fix k
```
```    44     show "f k - g k = f 0 - g 0"
```
```    45       by (induct k rule: int_induct) (simp_all add: k_incr k_decr)
```
```    46   qed
```
```    47   then have "\<And>k. (plus (g 0 - f 0) \<circ> f) k = g k"
```
```    48     by (simp add: algebra_simps)
```
```    49   then have "plus (g 0 - f 0) \<circ> f = g" ..
```
```    50   then show ?thesis ..
```
```    51 qed
```
```    52
```
```    53 text {* The formal sum operator. *}
```
```    54
```
```    55 definition \<Sigma> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a" where
```
```    56   "\<Sigma> f j l = (if j < l then setsum f {j..<l}
```
```    57     else if j > l then - setsum f {l..<j}
```
```    58     else 0)"
```
```    59
```
```    60 lemma \<Sigma>_same [simp]:
```
```    61   "\<Sigma> f j j = 0"
```
```    62   by (simp add: \<Sigma>_def)
```
```    63
```
```    64 lemma \<Sigma>_positive:
```
```    65   "j < l \<Longrightarrow> \<Sigma> f j l = setsum f {j..<l}"
```
```    66   by (simp add: \<Sigma>_def)
```
```    67
```
```    68 lemma \<Sigma>_negative:
```
```    69   "j > l \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j"
```
```    70   by (simp add: \<Sigma>_def)
```
```    71
```
```    72 lemma add_\<Sigma>:
```
```    73   "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
```
```    74   by (simp add: \<Sigma>_def algebra_simps add_setsum_int)
```
```    75    (simp_all add: add_setsum_orient [of f k j l]
```
```    76       add_setsum_orient [of f j l k]
```
```    77       add_setsum_orient [of f j k l] add_setsum_int)
```
```    78
```
```    79 lemma \<Sigma>_incr_upper:
```
```    80   "\<Sigma> f j (l + 1) = \<Sigma> f j l + f l"
```
```    81 proof -
```
```    82   have "{l..<l+1} = {l}" by auto
```
```    83   then have "\<Sigma> f l (l + 1) = f l" by (simp add: \<Sigma>_def)
```
```    84   moreover have "\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)" by (simp add: add_\<Sigma>)
```
```    85   ultimately show ?thesis by simp
```
```    86 qed
```
```    87
```
```    88 text {* Fundamental lemmas: The relation between @{term \<Delta>} and @{term \<Sigma>}. *}
```
```    89
```
```    90 lemma \<Delta>_\<Sigma>:
```
```    91   "\<Delta> (\<Sigma> f j) = f"
```
```    92 proof
```
```    93   fix k
```
```    94   show "\<Delta> (\<Sigma> f j) k = f k"
```
```    95     by (simp add: \<Delta>_def \<Sigma>_incr_upper)
```
```    96 qed
```
```    97
```
```    98 lemma \<Sigma>_\<Delta>:
```
```    99   "\<Sigma> (\<Delta> f) j l = f l - f j"
```
```   100 proof -
```
```   101   from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
```
```   102   then obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
```
```   103   then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: fun_eq_iff)
```
```   104   then show ?thesis by simp
```
```   105 qed
```
```   106
```
```   107 end
```