71 apply (simp add: sumhr hypnat_add hypreal_zero_def) |
71 apply (simp add: sumhr hypnat_add hypreal_zero_def) |
72 done |
72 done |
73 |
73 |
74 lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)" |
74 lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)" |
75 apply (cases m, cases n) |
75 apply (cases m, cases n) |
76 apply (simp add: sumhr hypreal_add sumr_add) |
76 apply (simp add: sumhr hypreal_add setsum_addf) |
77 done |
77 done |
78 |
78 |
79 lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)" |
79 lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)" |
80 apply (cases m, cases n) |
80 apply (cases m, cases n) |
81 apply (simp add: sumhr hypreal_of_real_def hypreal_mult sumr_mult) |
81 apply (simp add: sumhr hypreal_of_real_def hypreal_mult setsum_mult) |
82 done |
82 done |
83 |
83 |
84 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)" |
84 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)" |
85 apply (cases n, cases p) |
85 apply (cases n, cases p) |
86 apply (auto elim!: FreeUltrafilterNat_subset simp |
86 apply (auto elim!: FreeUltrafilterNat_subset simp |
90 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)" |
90 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)" |
91 by (drule_tac f1 = f in sumhr_split_add [symmetric], simp) |
91 by (drule_tac f1 = f in sumhr_split_add [symmetric], simp) |
92 |
92 |
93 lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))" |
93 lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))" |
94 apply (cases n, cases m) |
94 apply (cases n, cases m) |
95 apply (simp add: sumhr hypreal_le hypreal_hrabs sumr_rabs) |
95 apply (simp add: sumhr hypreal_le hypreal_hrabs setsum_abs) |
96 done |
96 done |
97 |
97 |
98 text{* other general version also needed *} |
98 text{* other general version also needed *} |
99 lemma sumhr_fun_hypnat_eq: |
99 lemma sumhr_fun_hypnat_eq: |
100 "(\<forall>r. m \<le> r & r < n --> f r = g r) --> |
100 "(\<forall>r. m \<le> r & r < n --> f r = g r) --> |
101 sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = |
101 sumhr(hypnat_of_nat m, hypnat_of_nat n, f) = |
102 sumhr(hypnat_of_nat m, hypnat_of_nat n, g)" |
102 sumhr(hypnat_of_nat m, hypnat_of_nat n, g)" |
103 apply (safe, drule sumr_fun_eq) |
103 by (fastsimp simp add: sumhr hypnat_of_nat_eq intro:setsum_cong) |
104 apply (simp add: sumhr hypnat_of_nat_eq) |
104 |
105 done |
|
106 |
105 |
107 lemma sumhr_const: |
106 lemma sumhr_const: |
108 "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r" |
107 "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r" |
109 apply (cases n) |
108 apply (cases n) |
110 apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat |
109 apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat |
117 simp add: sumhr hypnat_less hypreal_zero_def) |
116 simp add: sumhr hypnat_less hypreal_zero_def) |
118 done |
117 done |
119 |
118 |
120 lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)" |
119 lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)" |
121 apply (cases m, cases n) |
120 apply (cases m, cases n) |
122 apply (simp add: sumhr hypreal_minus sumr_minus) |
121 apply (simp add: sumhr hypreal_minus setsum_negf) |
123 done |
122 done |
124 |
123 |
125 lemma sumhr_shift_bounds: |
124 lemma sumhr_shift_bounds: |
126 "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))" |
125 "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))" |
127 apply (cases m, cases n) |
126 apply (cases m, cases n) |