equal
deleted
inserted
replaced
72 using z \<open>0 \<le> x\<close> by (auto intro!: summable_comparison_test[OF _ summable_geometric]) |
72 using z \<open>0 \<le> x\<close> by (auto intro!: summable_comparison_test[OF _ summable_geometric]) |
73 qed |
73 qed |
74 |
74 |
75 subsection \<open>Properties of Power Series\<close> |
75 subsection \<open>Properties of Power Series\<close> |
76 |
76 |
77 lemma powser_zero: |
77 lemma powser_zero [simp]: |
78 fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra_1" |
78 fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra_1" |
79 shows "(\<Sum>n. f n * 0 ^ n) = f 0" |
79 shows "(\<Sum>n. f n * 0 ^ n) = f 0" |
80 proof - |
80 proof - |
81 have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)" |
81 have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)" |
82 by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left) |
82 by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left) |
86 lemma powser_sums_zero: |
86 lemma powser_sums_zero: |
87 fixes a :: "nat \<Rightarrow> 'a::real_normed_div_algebra" |
87 fixes a :: "nat \<Rightarrow> 'a::real_normed_div_algebra" |
88 shows "(\<lambda>n. a n * 0^n) sums a 0" |
88 shows "(\<lambda>n. a n * 0^n) sums a 0" |
89 using sums_finite [of "{0}" "\<lambda>n. a n * 0 ^ n"] |
89 using sums_finite [of "{0}" "\<lambda>n. a n * 0 ^ n"] |
90 by simp |
90 by simp |
|
91 |
|
92 lemma powser_sums_zero_iff [simp]: |
|
93 fixes a :: "nat \<Rightarrow> 'a::real_normed_div_algebra" |
|
94 shows "(\<lambda>n. a n * 0^n) sums x \<longleftrightarrow> a 0 = x" |
|
95 using powser_sums_zero sums_unique2 by blast |
91 |
96 |
92 text\<open>Power series has a circle or radius of convergence: if it sums for @{term |
97 text\<open>Power series has a circle or radius of convergence: if it sums for @{term |
93 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.\<close> |
98 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.\<close> |
94 |
99 |
95 lemma powser_insidea: |
100 lemma powser_insidea: |
1340 by (simp add: exp_of_nat_mult) |
1345 by (simp add: exp_of_nat_mult) |
1341 |
1346 |
1342 lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I" |
1347 lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I" |
1343 by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute) |
1348 by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute) |
1344 |
1349 |
|
1350 lemma exp_divide_power_eq: |
|
1351 fixes x:: "'a::{real_normed_field,banach}" |
|
1352 assumes "n>0" shows "exp (x / of_nat n) ^ n = exp x" |
|
1353 using assms |
|
1354 proof (induction n arbitrary: x) |
|
1355 case 0 then show ?case by simp |
|
1356 next |
|
1357 case (Suc n) |
|
1358 show ?case |
|
1359 proof (cases "n=0") |
|
1360 case True then show ?thesis by simp |
|
1361 next |
|
1362 case False |
|
1363 then have [simp]: "x * of_nat n / (1 + of_nat n) / of_nat n = x / (1 + of_nat n)" |
|
1364 by simp |
|
1365 have [simp]: "x / (1 + of_nat n) + x * of_nat n / (1 + of_nat n) = x" |
|
1366 apply (simp add: divide_simps) |
|
1367 using of_nat_eq_0_iff apply (fastforce simp: distrib_left) |
|
1368 done |
|
1369 show ?thesis |
|
1370 using Suc.IH [of "x * of_nat n / (1 + of_nat n)"] False |
|
1371 by (simp add: exp_add [symmetric]) |
|
1372 qed |
|
1373 qed |
|
1374 |
1345 |
1375 |
1346 subsubsection \<open>Properties of the Exponential Function on Reals\<close> |
1376 subsubsection \<open>Properties of the Exponential Function on Reals\<close> |
1347 |
1377 |
1348 text \<open>Comparisons of @{term "exp x"} with zero.\<close> |
1378 text \<open>Comparisons of @{term "exp x"} with zero.\<close> |
1349 |
1379 |