equal
deleted
inserted
replaced
879 |
879 |
880 lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))" |
880 lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))" |
881 by (simp add: diffs_def) |
881 by (simp add: diffs_def) |
882 |
882 |
883 lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))" |
883 lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))" |
884 by (auto intro!: ext simp add: exp_def) |
884 by (auto simp add: exp_def) |
885 |
885 |
886 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" |
886 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" |
887 apply (simp add: exp_def) |
887 apply (simp add: exp_def) |
888 apply (subst lemma_exp_ext) |
888 apply (subst lemma_exp_ext) |
889 apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)") |
889 apply (subgoal_tac "DERIV (\<lambda>u. \<Sum>n. of_real (inverse (real (fact n))) * u ^ n) x :> (\<Sum>n. diffs (\<lambda>n. of_real (inverse (real (fact n)))) n * x ^ n)") |
1246 hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)" unfolding DERIV_iff repos . |
1246 hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)" unfolding DERIV_iff repos . |
1247 ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))" |
1247 ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))" |
1248 by (rule DERIV_diff) |
1248 by (rule DERIV_diff) |
1249 thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto |
1249 thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto |
1250 qed (auto simp add: assms) |
1250 qed (auto simp add: assms) |
1251 thus ?thesis by (auto simp add: suminf_zero) |
1251 thus ?thesis by auto |
1252 qed |
1252 qed |
1253 |
1253 |
1254 subsection {* Sine and Cosine *} |
1254 subsection {* Sine and Cosine *} |
1255 |
1255 |
1256 definition |
1256 definition |
1335 |
1335 |
1336 lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))" |
1336 lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))" |
1337 by (auto intro!: sums_unique sums_minus sin_converges) |
1337 by (auto intro!: sums_unique sums_minus sin_converges) |
1338 |
1338 |
1339 lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)" |
1339 lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)" |
1340 by (auto intro!: ext simp add: sin_def) |
1340 by (auto simp add: sin_def) |
1341 |
1341 |
1342 lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)" |
1342 lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)" |
1343 by (auto intro!: ext simp add: cos_def) |
1343 by (auto simp add: cos_def) |
1344 |
1344 |
1345 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)" |
1345 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)" |
1346 apply (simp add: cos_def) |
1346 apply (simp add: cos_def) |
1347 apply (subst lemma_sin_ext) |
1347 apply (subst lemma_sin_ext) |
1348 apply (auto simp add: sin_fdiffs2 [symmetric]) |
1348 apply (auto simp add: sin_fdiffs2 [symmetric]) |