src/HOL/Transcendental.thy
author paulson <lp15@cam.ac.uk>
Sat, 11 Apr 2015 11:56:40 +0100
changeset 60017 b785d6d06430
parent 59869 3b5b53eb78ba
child 60020 065ecea354d0
permissions -rw-r--r--
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
     1
(*  Title:      HOL/Transcendental.thy
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
     2
    Author:     Jacques D. Fleuriot, University of Cambridge, University of Edinburgh
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
     3
    Author:     Lawrence C Paulson
51527
bd62e7ff103b move Ln.thy and Log.thy to Transcendental.thy
hoelzl
parents: 51482
diff changeset
     4
    Author:     Jeremy Avigad
12196
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     5
*)
a3be6b3a9c0b new theories from Jacques Fleuriot
paulson
parents:
diff changeset
     6
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 58834
diff changeset
     7
section{*Power Series, Transcendental Functions etc.*}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
     8
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
     9
theory Transcendental
59669
de7792ea4090 renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
    10
imports Binomial Series Deriv NthRoot
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
    11
begin
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    12
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    13
lemma of_real_fact [simp]: "of_real (fact n) = fact n"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    14
  by (metis of_nat_fact of_real_of_nat_eq)
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    15
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    16
lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    17
  by (simp add: real_of_nat_def)
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    18
59731
paulson <lp15@cam.ac.uk>
parents: 59730 59688
diff changeset
    19
lemma real_fact_int [simp]: "real (fact n :: int) = fact n"
paulson <lp15@cam.ac.uk>
parents: 59730 59688
diff changeset
    20
  by (metis of_int_of_nat_eq of_nat_fact real_of_int_def)
paulson <lp15@cam.ac.uk>
parents: 59730 59688
diff changeset
    21
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    22
lemma root_test_convergence:
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    23
  fixes f :: "nat \<Rightarrow> 'a::banach"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    24
  assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    25
  assumes "x < 1"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    26
  shows "summable f"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    27
proof -
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    28
  have "0 \<le> x"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    29
    by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1])
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    30
  from `x < 1` obtain z where z: "x < z" "z < 1"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    31
    by (metis dense)
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    32
  from f `x < z`
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    33
  have "eventually (\<lambda>n. root n (norm (f n)) < z) sequentially"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    34
    by (rule order_tendstoD)
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    35
  then have "eventually (\<lambda>n. norm (f n) \<le> z^n) sequentially"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    36
    using eventually_ge_at_top
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    37
  proof eventually_elim
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    38
    fix n assume less: "root n (norm (f n)) < z" and n: "1 \<le> n"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    39
    from power_strict_mono[OF less, of n] n
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    40
    show "norm (f n) \<le> z ^ n"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    41
      by simp
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    42
  qed
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    43
  then show "summable f"
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    44
    unfolding eventually_sequentially
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    45
    using z `0 \<le> x` by (auto intro!: summable_comparison_test[OF _  summable_geometric])
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    46
qed
e7fd64f82876 add various lemmas
hoelzl
parents: 56952
diff changeset
    47
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
    48
subsection {* Properties of Power Series *}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    49
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    50
lemma lemma_realpow_diff:
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30273
diff changeset
    51
  fixes y :: "'a::monoid_mult"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    52
  shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    53
proof -
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    54
  assume "p \<le> n"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    55
  hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le)
30273
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30082
diff changeset
    56
  thus ?thesis by (simp add: power_commutes)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
    57
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    58
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    59
lemma lemma_realpow_diff_sumr2:
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
    60
  fixes y :: "'a::{comm_ring,monoid_mult}"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
    61
  shows
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
    62
    "x ^ (Suc n) - y ^ (Suc n) =
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    63
      (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
54573
07864001495d cleaned up some messy proofs
paulson
parents: 54489
diff changeset
    64
proof (induct n)
07864001495d cleaned up some messy proofs
paulson
parents: 54489
diff changeset
    65
  case (Suc n)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    66
  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)"
54573
07864001495d cleaned up some messy proofs
paulson
parents: 54489
diff changeset
    67
    by simp
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    68
  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
54573
07864001495d cleaned up some messy proofs
paulson
parents: 54489
diff changeset
    69
    by (simp add: algebra_simps)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    70
  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
54573
07864001495d cleaned up some messy proofs
paulson
parents: 54489
diff changeset
    71
    by (simp only: Suc)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
    72
  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
    73
    by (simp only: mult.left_commute)
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    74
  also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    75
    by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
54573
07864001495d cleaned up some messy proofs
paulson
parents: 54489
diff changeset
    76
  finally show ?case .
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    77
qed simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    78
55832
8dd16f8dfe99 repaired document;
wenzelm
parents: 55734
diff changeset
    79
corollary power_diff_sumr2: --{* @{text COMPLEX_POLYFUN} in HOL Light *}
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 55719
diff changeset
    80
  fixes x :: "'a::{comm_ring,monoid_mult}"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    81
  shows   "x^n - y^n = (x - y) * (\<Sum>i<n. y^(n - Suc i) * x^i)"
55734
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 55719
diff changeset
    82
using lemma_realpow_diff_sumr2[of x "n - 1" y]
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 55719
diff changeset
    83
by (cases "n = 0") (simp_all add: field_simps)
3f5b2745d659 More complex-related lemmas
paulson <lp15@cam.ac.uk>
parents: 55719
diff changeset
    84
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
    85
lemma lemma_realpow_rev_sumr:
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    86
   "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    87
    (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
57129
7edb7550663e introduce more powerful reindexing rules for big operators
hoelzl
parents: 57025
diff changeset
    88
  by (subst nat_diff_setsum_reindex[symmetric]) simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
    89
55719
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
    90
lemma power_diff_1_eq:
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
    91
  fixes x :: "'a::{comm_ring,monoid_mult}"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    92
  shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
59669
de7792ea4090 renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
    93
using lemma_realpow_diff_sumr2 [of x _ 1]
55719
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
    94
  by (cases n) auto
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
    95
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
    96
lemma one_diff_power_eq':
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
    97
  fixes x :: "'a::{comm_ring,monoid_mult}"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
    98
  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
59669
de7792ea4090 renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
    99
using lemma_realpow_diff_sumr2 [of 1 _ x]
55719
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
   100
  by (cases n) auto
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
   101
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
   102
lemma one_diff_power_eq:
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
   103
  fixes x :: "'a::{comm_ring,monoid_mult}"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   104
  shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
55719
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
   105
by (metis one_diff_power_eq' [of n x] nat_diff_setsum_reindex)
cdddd073bff8 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
paulson <lp15@cam.ac.uk>
parents: 55417
diff changeset
   106
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   107
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   108
  x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   109
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   110
lemma powser_insidea:
53599
78ea983f7987 generalize lemmas
huffman
parents: 53079
diff changeset
   111
  fixes x z :: "'a::real_normed_div_algebra"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   112
  assumes 1: "summable (\<lambda>n. f n * x^n)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   113
    and 2: "norm z < norm x"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   114
  shows "summable (\<lambda>n. norm (f n * z ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   115
proof -
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   116
  from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   117
  from 1 have "(\<lambda>n. f n * x^n) ----> 0"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   118
    by (rule summable_LIMSEQ_zero)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   119
  hence "convergent (\<lambda>n. f n * x^n)"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   120
    by (rule convergentI)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   121
  hence "Cauchy (\<lambda>n. f n * x^n)"
44726
8478eab380e9 generalize some lemmas
huffman
parents: 44725
diff changeset
   122
    by (rule convergent_Cauchy)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   123
  hence "Bseq (\<lambda>n. f n * x^n)"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   124
    by (rule Cauchy_Bseq)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   125
  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x^n) \<le> K"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   126
    by (simp add: Bseq_def, safe)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   127
  have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   128
                   K * norm (z ^ n) * inverse (norm (x^n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   129
  proof (intro exI allI impI)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   130
    fix n::nat
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   131
    assume "0 \<le> n"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   132
    have "norm (norm (f n * z ^ n)) * norm (x^n) =
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   133
          norm (f n * x^n) * norm (z ^ n)"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   134
      by (simp add: norm_mult abs_mult)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   135
    also have "\<dots> \<le> K * norm (z ^ n)"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   136
      by (simp only: mult_right_mono 4 norm_ge_zero)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   137
    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   138
      by (simp add: x_neq_0)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   139
    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   140
      by (simp only: mult.assoc)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   141
    finally show "norm (norm (f n * z ^ n)) \<le>
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   142
                  K * norm (z ^ n) * inverse (norm (x^n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   143
      by (simp add: mult_le_cancel_right x_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   144
  qed
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   145
  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   146
  proof -
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   147
    from 2 have "norm (norm (z * inverse x)) < 1"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   148
      using x_neq_0
53599
78ea983f7987 generalize lemmas
huffman
parents: 53079
diff changeset
   149
      by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric])
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   150
    hence "summable (\<lambda>n. norm (z * inverse x) ^ n)"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   151
      by (rule summable_geometric)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   152
    hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   153
      by (rule summable_mult)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   154
    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   155
      using x_neq_0
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   156
      by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   157
                    power_inverse norm_power mult.assoc)
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   158
  qed
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   159
  ultimately show "summable (\<lambda>n. norm (f n * z ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   160
    by (rule summable_comparison_test)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   161
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   162
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   163
lemma powser_inside:
53599
78ea983f7987 generalize lemmas
huffman
parents: 53079
diff changeset
   164
  fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   165
  shows
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   166
    "summable (\<lambda>n. f n * (x^n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   167
      summable (\<lambda>n. f n * (z ^ n))"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   168
  by (rule powser_insidea [THEN summable_norm_cancel])
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   169
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   170
lemma sum_split_even_odd:
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   171
  fixes f :: "nat \<Rightarrow> real"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   172
  shows
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   173
    "(\<Sum>i<2 * n. if even i then f i else g i) =
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   174
     (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1))"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   175
proof (induct n)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   176
  case 0
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   177
  then show ?case by simp
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   178
next
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   179
  case (Suc n)
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   180
  have "(\<Sum>i<2 * Suc n. if even i then f i else g i) =
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   181
    (\<Sum>i<n. f (2 * i)) + (\<Sum>i<n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
30082
43c5b7bfc791 make more proofs work whether or not One_nat_def is a simp rule
huffman
parents: 29803
diff changeset
   182
    using Suc.hyps unfolding One_nat_def by auto
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   183
  also have "\<dots> = (\<Sum>i<Suc n. f (2 * i)) + (\<Sum>i<Suc n. g (2 * i + 1))"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   184
    by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   185
  finally show ?case .
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   186
qed
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   187
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   188
lemma sums_if':
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   189
  fixes g :: "nat \<Rightarrow> real"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   190
  assumes "g sums x"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   191
  shows "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   192
  unfolding sums_def
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   193
proof (rule LIMSEQ_I)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   194
  fix r :: real
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   195
  assume "0 < r"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   196
  from `g sums x`[unfolded sums_def, THEN LIMSEQ_D, OF this]
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   197
  obtain no where no_eq: "\<And> n. n \<ge> no \<Longrightarrow> (norm (setsum g {..<n} - x) < r)" by blast
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   198
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   199
  let ?SUM = "\<lambda> m. \<Sum>i<m. if even i then 0 else g ((i - 1) div 2)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   200
  {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   201
    fix m
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   202
    assume "m \<ge> 2 * no"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   203
    hence "m div 2 \<ge> no" by auto
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   204
    have sum_eq: "?SUM (2 * (m div 2)) = setsum g {..< m div 2}"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   205
      using sum_split_even_odd by auto
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   206
    hence "(norm (?SUM (2 * (m div 2)) - x) < r)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   207
      using no_eq unfolding sum_eq using `m div 2 \<ge> no` by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   208
    moreover
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   209
    have "?SUM (2 * (m div 2)) = ?SUM m"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   210
    proof (cases "even m")
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   211
      case True
58710
7216a10d69ba augmented and tuned facts on even/odd and division
haftmann
parents: 58709
diff changeset
   212
      then show ?thesis by (auto simp add: even_two_times_div_two)
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   213
    next
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   214
      case False
58834
773b378d9313 more simp rules concerning dvd and even/odd
haftmann
parents: 58740
diff changeset
   215
      then have eq: "Suc (2 * (m div 2)) = m" by simp
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   216
      hence "even (2 * (m div 2))" using `odd m` by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   217
      have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   218
      also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   219
      finally show ?thesis by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   220
    qed
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   221
    ultimately have "(norm (?SUM m - x) < r)" by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   222
  }
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   223
  thus "\<exists> no. \<forall> m \<ge> no. norm (?SUM m - x) < r" by blast
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   224
qed
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   225
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   226
lemma sums_if:
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   227
  fixes g :: "nat \<Rightarrow> real"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   228
  assumes "g sums x" and "f sums y"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   229
  shows "(\<lambda> n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   230
proof -
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   231
  let ?s = "\<lambda> n. if even n then 0 else f ((n - 1) div 2)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   232
  {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   233
    fix B T E
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   234
    have "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   235
      by (cases B) auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   236
  } note if_sum = this
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   237
  have g_sums: "(\<lambda> n. if even n then 0 else g ((n - 1) div 2)) sums x"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   238
    using sums_if'[OF `g sums x`] .
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   239
  {
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 38642
diff changeset
   240
    have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   241
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   242
    have "?s sums y" using sums_if'[OF `f sums y`] .
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   243
    from this[unfolded sums_def, THEN LIMSEQ_Suc]
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   244
    have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 57275
diff changeset
   245
      by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum.reindex if_eq sums_def cong del: if_cong)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   246
  }
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   247
  from sums_add[OF g_sums this] show ?thesis unfolding if_sum .
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   248
qed
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   249
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   250
subsection {* Alternating series test / Leibniz formula *}
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   251
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   252
lemma sums_alternating_upper_lower:
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   253
  fixes a :: "nat \<Rightarrow> real"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   254
  assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57514
diff changeset
   255
  shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. (- 1)^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. (- 1)^i*a i) ----> l) \<and>
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57514
diff changeset
   256
             ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. (- 1)^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. (- 1)^i*a i) ----> l)"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   257
  (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   258
proof (rule nested_sequence_unique)
30082
43c5b7bfc791 make more proofs work whether or not One_nat_def is a simp rule
huffman
parents: 29803
diff changeset
   259
  have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   260
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   261
  show "\<forall>n. ?f n \<le> ?f (Suc n)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   262
  proof
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   263
    fix n
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   264
    show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   265
  qed
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   266
  show "\<forall>n. ?g (Suc n) \<le> ?g n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   267
  proof
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   268
    fix n
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   269
    show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   270
      unfolding One_nat_def by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   271
  qed
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   272
  show "\<forall>n. ?f n \<le> ?g n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   273
  proof
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   274
    fix n
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   275
    show "?f n \<le> ?g n" using fg_diff a_pos
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   276
      unfolding One_nat_def by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   277
  qed
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   278
  show "(\<lambda>n. ?f n - ?g n) ----> 0" unfolding fg_diff
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   279
  proof (rule LIMSEQ_I)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   280
    fix r :: real
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   281
    assume "0 < r"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   282
    with `a ----> 0`[THEN LIMSEQ_D] obtain N where "\<And> n. n \<ge> N \<Longrightarrow> norm (a n - 0) < r"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   283
      by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   284
    hence "\<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   285
    thus "\<exists>N. \<forall>n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   286
  qed
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   287
qed
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   288
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   289
lemma summable_Leibniz':
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   290
  fixes a :: "nat \<Rightarrow> real"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   291
  assumes a_zero: "a ----> 0"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   292
    and a_pos: "\<And> n. 0 \<le> a n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   293
    and a_monotone: "\<And> n. a (Suc n) \<le> a n"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   294
  shows summable: "summable (\<lambda> n. (-1)^n * a n)"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   295
    and "\<And>n. (\<Sum>i<2*n. (-1)^i*a i) \<le> (\<Sum>i. (-1)^i*a i)"
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   296
    and "(\<lambda>n. \<Sum>i<2*n. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   297
    and "\<And>n. (\<Sum>i. (-1)^i*a i) \<le> (\<Sum>i<2*n+1. (-1)^i*a i)"
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   298
    and "(\<lambda>n. \<Sum>i<2*n+1. (-1)^i*a i) ----> (\<Sum>i. (-1)^i*a i)"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   299
proof -
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   300
  let ?S = "\<lambda>n. (-1)^n * a n"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   301
  let ?P = "\<lambda>n. \<Sum>i<n. ?S i"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   302
  let ?f = "\<lambda>n. ?P (2 * n)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   303
  let ?g = "\<lambda>n. ?P (2 * n + 1)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   304
  obtain l :: real
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   305
    where below_l: "\<forall> n. ?f n \<le> l"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   306
      and "?f ----> l"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   307
      and above_l: "\<forall> n. l \<le> ?g n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   308
      and "?g ----> l"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   309
    using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   310
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   311
  let ?Sa = "\<lambda>m. \<Sum>n<m. ?S n"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   312
  have "?Sa ----> l"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   313
  proof (rule LIMSEQ_I)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   314
    fix r :: real
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   315
    assume "0 < r"
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   316
    with `?f ----> l`[THEN LIMSEQ_D]
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   317
    obtain f_no where f: "\<And> n. n \<ge> f_no \<Longrightarrow> norm (?f n - l) < r" by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   318
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   319
    from `0 < r` `?g ----> l`[THEN LIMSEQ_D]
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   320
    obtain g_no where g: "\<And> n. n \<ge> g_no \<Longrightarrow> norm (?g n - l) < r" by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   321
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   322
    {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   323
      fix n :: nat
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   324
      assume "n \<ge> (max (2 * f_no) (2 * g_no))"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   325
      hence "n \<ge> 2 * f_no" and "n \<ge> 2 * g_no" by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   326
      have "norm (?Sa n - l) < r"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   327
      proof (cases "even n")
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   328
        case True
58710
7216a10d69ba augmented and tuned facts on even/odd and division
haftmann
parents: 58709
diff changeset
   329
        then have n_eq: "2 * (n div 2) = n" by (simp add: even_two_times_div_two)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   330
        with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   331
          by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   332
        from f[OF this] show ?thesis
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   333
          unfolding n_eq atLeastLessThanSuc_atLeastAtMost .
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   334
      next
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   335
        case False
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   336
        hence "even (n - 1)" by simp
58710
7216a10d69ba augmented and tuned facts on even/odd and division
haftmann
parents: 58709
diff changeset
   337
        then have n_eq: "2 * ((n - 1) div 2) = n - 1"
7216a10d69ba augmented and tuned facts on even/odd and division
haftmann
parents: 58709
diff changeset
   338
          by (simp add: even_two_times_div_two)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   339
        hence range_eq: "n - 1 + 1 = n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   340
          using odd_pos[OF False] by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   341
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   342
        from n_eq `n \<ge> 2 * g_no` have "(n - 1) div 2 \<ge> g_no"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   343
          by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   344
        from g[OF this] show ?thesis
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   345
          unfolding n_eq range_eq .
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   346
      qed
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   347
    }
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   348
    thus "\<exists>no. \<forall>n \<ge> no. norm (?Sa n - l) < r" by blast
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   349
  qed
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   350
  hence sums_l: "(\<lambda>i. (-1)^i * a i) sums l"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   351
    unfolding sums_def .
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   352
  thus "summable ?S" using summable_def by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   353
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   354
  have "l = suminf ?S" using sums_unique[OF sums_l] .
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   355
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   356
  fix n
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   357
  show "suminf ?S \<le> ?g n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   358
    unfolding sums_unique[OF sums_l, symmetric] using above_l by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   359
  show "?f n \<le> suminf ?S"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   360
    unfolding sums_unique[OF sums_l, symmetric] using below_l by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   361
  show "?g ----> suminf ?S"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   362
    using `?g ----> l` `l = suminf ?S` by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   363
  show "?f ----> suminf ?S"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   364
    using `?f ----> l` `l = suminf ?S` by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   365
qed
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   366
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   367
theorem summable_Leibniz:
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   368
  fixes a :: "nat \<Rightarrow> real"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   369
  assumes a_zero: "a ----> 0" and "monoseq a"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   370
  shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   371
    and "0 < a 0 \<longrightarrow>
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57514
diff changeset
   372
      (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n. (- 1)^i * a i .. \<Sum>i<2*n+1. (- 1)^i * a i})" (is "?pos")
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   373
    and "a 0 < 0 \<longrightarrow>
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57514
diff changeset
   374
      (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n+1. (- 1)^i * a i .. \<Sum>i<2*n. (- 1)^i * a i})" (is "?neg")
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57514
diff changeset
   375
    and "(\<lambda>n. \<Sum>i<2*n. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?f")
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57514
diff changeset
   376
    and "(\<lambda>n. \<Sum>i<2*n+1. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?g")
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   377
proof -
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   378
  have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   379
  proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   380
    case True
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   381
    hence ord: "\<And>n m. m \<le> n \<Longrightarrow> a n \<le> a m" and ge0: "\<And> n. 0 \<le> a n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   382
      by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   383
    {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   384
      fix n
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   385
      have "a (Suc n) \<le> a n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   386
        using ord[where n="Suc n" and m=n] by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   387
    } note mono = this
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   388
    note leibniz = summable_Leibniz'[OF `a ----> 0` ge0]
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   389
    from leibniz[OF mono]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   390
    show ?thesis using `0 \<le> a 0` by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   391
  next
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   392
    let ?a = "\<lambda> n. - a n"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   393
    case False
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   394
    with monoseq_le[OF `monoseq a` `a ----> 0`]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   395
    have "(\<forall> n. a n \<le> 0) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)" by auto
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   396
    hence ord: "\<And>n m. m \<le> n \<Longrightarrow> ?a n \<le> ?a m" and ge0: "\<And> n. 0 \<le> ?a n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   397
      by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   398
    {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   399
      fix n
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   400
      have "?a (Suc n) \<le> ?a n" using ord[where n="Suc n" and m=n]
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   401
        by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   402
    } note monotone = this
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   403
    note leibniz =
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   404
      summable_Leibniz'[OF _ ge0, of "\<lambda>x. x",
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   405
        OF tendsto_minus[OF `a ----> 0`, unfolded minus_zero] monotone]
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   406
    have "summable (\<lambda> n. (-1)^n * ?a n)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   407
      using leibniz(1) by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   408
    then obtain l where "(\<lambda> n. (-1)^n * ?a n) sums l"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   409
      unfolding summable_def by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   410
    from this[THEN sums_minus] have "(\<lambda> n. (-1)^n * a n) sums -l"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   411
      by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   412
    hence ?summable unfolding summable_def by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   413
    moreover
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   414
    have "\<And>a b :: real. \<bar>- a - - b\<bar> = \<bar>a - b\<bar>"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   415
      unfolding minus_diff_minus by auto
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   416
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   417
    from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57514
diff changeset
   418
    have move_minus: "(\<Sum>n. - ((- 1) ^ n * a n)) = - (\<Sum>n. (- 1) ^ n * a n)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   419
      by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   420
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   421
    have ?pos using `0 \<le> ?a 0` by auto
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   422
    moreover have ?neg
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   423
      using leibniz(2,4)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   424
      unfolding mult_minus_right setsum_negf move_minus neg_le_iff_le
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   425
      by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   426
    moreover have ?f and ?g
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   427
      using leibniz(3,5)[unfolded mult_minus_right setsum_negf move_minus, THEN tendsto_minus_cancel]
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   428
      by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   429
    ultimately show ?thesis by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   430
  qed
59669
de7792ea4090 renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
   431
  then show ?summable and ?pos and ?neg and ?f and ?g
54573
07864001495d cleaned up some messy proofs
paulson
parents: 54489
diff changeset
   432
    by safe
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   433
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   434
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   435
subsection {* Term-by-Term Differentiability of Power Series *}
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   436
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   437
definition diffs :: "(nat \<Rightarrow> 'a::ring_1) \<Rightarrow> nat \<Rightarrow> 'a"
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   438
  where "diffs c = (\<lambda>n. of_nat (Suc n) * c (Suc n))"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   439
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   440
text{*Lemma about distributing negation over it*}
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   441
lemma diffs_minus: "diffs (\<lambda>n. - c n) = (\<lambda>n. - diffs c n)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   442
  by (simp add: diffs_def)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   443
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   444
lemma sums_Suc_imp:
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   445
  "(f::nat \<Rightarrow> 'a::real_normed_vector) 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   446
  using sums_Suc_iff[of f] by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   447
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   448
lemma diffs_equiv:
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   449
  fixes x :: "'a::{real_normed_vector, ring_1}"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   450
  shows "summable (\<lambda>n. diffs c n * x^n) \<Longrightarrow>
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   451
      (\<lambda>n. of_nat n * c n * x^(n - Suc 0)) sums (\<Sum>n. diffs c n * x^n)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   452
  unfolding diffs_def
54573
07864001495d cleaned up some messy proofs
paulson
parents: 54489
diff changeset
   453
  by (simp add: summable_sums sums_Suc_imp)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   454
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   455
lemma lemma_termdiff1:
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30273
diff changeset
   456
  fixes z :: "'a :: {monoid_mult,comm_ring}" shows
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   457
  "(\<Sum>p<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   458
   (\<Sum>p<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   459
  by (auto simp add: algebra_simps power_add [symmetric])
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   460
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   461
lemma sumr_diff_mult_const2:
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   462
  "setsum f {..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i<n. f i - r)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   463
  by (simp add: setsum_subtractf)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   464
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   465
lemma lemma_termdiff2:
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30273
diff changeset
   466
  fixes h :: "'a :: {field}"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   467
  assumes h: "h \<noteq> 0"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   468
  shows
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   469
    "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   470
     h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p.
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   471
          (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   472
  apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   473
  apply (simp add: right_diff_distrib diff_divide_distrib h)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   474
  apply (simp add: mult.assoc [symmetric])
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   475
  apply (cases "n", simp)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   476
  apply (simp add: lemma_realpow_diff_sumr2 h
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   477
                   right_diff_distrib [symmetric] mult.assoc
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   478
              del: power_Suc setsum_lessThan_Suc of_nat_Suc)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   479
  apply (subst lemma_realpow_rev_sumr)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   480
  apply (subst sumr_diff_mult_const2)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   481
  apply simp
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   482
  apply (simp only: lemma_termdiff1 setsum_right_distrib)
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 57275
diff changeset
   483
  apply (rule setsum.cong [OF refl])
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53602
diff changeset
   484
  apply (simp add: less_iff_Suc_add)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   485
  apply (clarify)
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   486
  apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 ac_simps
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   487
              del: setsum_lessThan_Suc power_Suc)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   488
  apply (subst mult.assoc [symmetric], subst power_add [symmetric])
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   489
  apply (simp add: ac_simps)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   490
  done
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   491
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   492
lemma real_setsum_nat_ivl_bounded2:
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34974
diff changeset
   493
  fixes K :: "'a::linordered_semidom"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   494
  assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   495
    and K: "0 \<le> K"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   496
  shows "setsum f {..<n-k} \<le> of_nat n * K"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   497
  apply (rule order_trans [OF setsum_mono])
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   498
  apply (rule f, simp)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   499
  apply (simp add: mult_right_mono K)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   500
  done
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   501
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   502
lemma lemma_termdiff3:
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30273
diff changeset
   503
  fixes h z :: "'a::{real_normed_field}"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   504
  assumes 1: "h \<noteq> 0"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   505
    and 2: "norm z \<le> K"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   506
    and 3: "norm (z + h) \<le> K"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   507
  shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0))
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   508
          \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   509
proof -
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   510
  have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   511
        norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p.
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   512
          (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   513
    by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult.commute norm_mult)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   514
  also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   515
  proof (rule mult_right_mono [OF _ norm_ge_zero])
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   516
    from norm_ge_zero 2 have K: "0 \<le> K"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   517
      by (rule order_trans)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   518
    have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   519
      apply (erule subst)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   520
      apply (simp only: norm_mult norm_power power_add)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   521
      apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   522
      done
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   523
    show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   524
          \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   525
      apply (intro
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   526
         order_trans [OF norm_setsum]
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   527
         real_setsum_nat_ivl_bounded2
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   528
         mult_nonneg_nonneg
47489
04e7d09ade7a tuned some proofs;
huffman
parents: 47108
diff changeset
   529
         of_nat_0_le_iff
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   530
         zero_le_power K)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   531
      apply (rule le_Kn, simp)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   532
      done
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   533
  qed
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   534
  also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   535
    by (simp only: mult.assoc)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   536
  finally show ?thesis .
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   537
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   538
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   539
lemma lemma_termdiff4:
56167
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   540
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   541
  assumes k: "0 < (k::real)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   542
    and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   543
  shows "f -- 0 --> 0"
56167
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   544
proof (rule tendsto_norm_zero_cancel)
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   545
  show "(\<lambda>h. norm (f h)) -- 0 --> 0"
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   546
  proof (rule real_tendsto_sandwich)
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   547
    show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   548
      by simp
56167
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   549
    show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)"
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   550
      using k by (auto simp add: eventually_at dist_norm le)
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   551
    show "(\<lambda>h. 0) -- (0::'a) --> (0::real)"
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   552
      by (rule tendsto_const)
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   553
    have "(\<lambda>h. K * norm h) -- (0::'a) --> K * norm (0::'a)"
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   554
      by (intro tendsto_intros)
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   555
    then show "(\<lambda>h. K * norm h) -- (0::'a) --> 0"
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   556
      by simp
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   557
  qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   558
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   559
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15228
diff changeset
   560
lemma lemma_termdiff5:
56167
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   561
  fixes g :: "'a::real_normed_vector \<Rightarrow> nat \<Rightarrow> 'b::banach"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   562
  assumes k: "0 < (k::real)"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   563
  assumes f: "summable f"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   564
  assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   565
  shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   566
proof (rule lemma_termdiff4 [OF k])
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   567
  fix h::'a
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   568
  assume "h \<noteq> 0" and "norm h < k"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   569
  hence A: "\<forall>n. norm (g h n) \<le> f n * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   570
    by (simp add: le)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   571
  hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   572
    by simp
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   573
  moreover from f have B: "summable (\<lambda>n. f n * norm h)"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   574
    by (rule summable_mult2)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   575
  ultimately have C: "summable (\<lambda>n. norm (g h n))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   576
    by (rule summable_comparison_test)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   577
  hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   578
    by (rule summable_norm)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   579
  also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
   580
    by (rule suminf_le)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   581
  also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   582
    by (rule suminf_mult2 [symmetric])
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   583
  finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   584
qed
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   585
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   586
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   587
text{* FIXME: Long proofs*}
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   588
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   589
lemma termdiffs_aux:
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30273
diff changeset
   590
  fixes x :: "'a::{real_normed_field,banach}"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   591
  assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   592
    and 2: "norm x < norm K"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   593
  shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   594
             - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   595
proof -
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   596
  from dense [OF 2]
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   597
  obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   598
  from norm_ge_zero r1 have r: "0 < r"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   599
    by (rule order_le_less_trans)
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   600
  hence r_neq_0: "r \<noteq> 0" by simp
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   601
  show ?thesis
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   602
  proof (rule lemma_termdiff5)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   603
    show "0 < r - norm x" using r1 by simp
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   604
    from r r2 have "norm (of_real r::'a) < norm K"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   605
      by simp
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   606
    with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   607
      by (rule powser_insidea)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   608
    hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   609
      using r
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   610
      by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   611
    hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   612
      by (rule diffs_equiv [THEN sums_summable])
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   613
    also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   614
      (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   615
      apply (rule ext)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   616
      apply (simp add: diffs_def)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   617
      apply (case_tac n, simp_all add: r_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   618
      done
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   619
    finally have "summable
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   620
      (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   621
      by (rule diffs_equiv [THEN sums_summable])
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   622
    also have
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   623
      "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) *
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   624
           r ^ (n - Suc 0)) =
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   625
       (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   626
      apply (rule ext)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   627
      apply (case_tac "n", simp)
55417
01fbfb60c33e adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents: 54576
diff changeset
   628
      apply (rename_tac nat)
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   629
      apply (case_tac "nat", simp)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   630
      apply (simp add: r_neq_0)
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   631
      done
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   632
    finally
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   633
    show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   634
  next
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   635
    fix h::'a and n::nat
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   636
    assume h: "h \<noteq> 0"
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   637
    assume "norm h < r - norm x"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   638
    hence "norm x + norm h < r" by simp
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   639
    with norm_triangle_ineq have xh: "norm (x + h) < r"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   640
      by (rule order_le_less_trans)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   641
    show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   642
          \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   643
      apply (simp only: norm_mult mult.assoc)
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   644
      apply (rule mult_left_mono [OF _ norm_ge_zero])
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   645
      apply (simp add: mult.assoc [symmetric])
54575
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
   646
      apply (metis h lemma_termdiff3 less_eq_real_def r1 xh)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   647
      done
20849
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   648
  qed
389cd9c8cfe1 rewrite proofs of powser_insidea and termdiffs_aux
huffman
parents: 20692
diff changeset
   649
qed
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 19765
diff changeset
   650
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   651
lemma termdiffs:
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30273
diff changeset
   652
  fixes K x :: "'a::{real_normed_field,banach}"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   653
  assumes 1: "summable (\<lambda>n. c n * K ^ n)"
54575
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
   654
      and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
   655
      and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
   656
      and 4: "norm x < norm K"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   657
  shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. (diffs c) n * x^n)"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   658
  unfolding DERIV_def
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   659
proof (rule LIM_zero_cancel)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   660
  show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x^n)) / h
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   661
            - suminf (\<lambda>n. diffs c n * x^n)) -- 0 --> 0"
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   662
  proof (rule LIM_equal2)
29163
e72d07a878f8 clean up some proofs; remove unused lemmas
huffman
parents: 28952
diff changeset
   663
    show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   664
  next
23082
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   665
    fix h :: 'a
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   666
    assume "norm (h - 0) < norm K - norm x"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   667
    hence "norm x + norm h < norm K" by simp
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   668
    hence 5: "norm (x + h) < norm K"
ffef77eed382 generalize powerseries and termdiffs lemmas using axclasses
huffman
parents: 23069
diff changeset
   669
      by (rule norm_triangle_ineq [THEN order_le_less_trans])
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   670
    have "summable (\<lambda>n. c n * x^n)"
56167
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   671
      and "summable (\<lambda>n. c n * (x + h) ^ n)"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   672
      and "summable (\<lambda>n. diffs c n * x^n)"
56167
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   673
      using 1 2 4 5 by (auto elim: powser_inside)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   674
    then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   675
          (\<Sum>n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))"
56167
ac8098b0e458 tuned proofs
huffman
parents: 55832
diff changeset
   676
      by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   677
    then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   678
          (\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
54575
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
   679
      by (simp add: algebra_simps)
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   680
  next
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   681
    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   682
      by (rule termdiffs_aux [OF 3 4])
20860
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   683
  qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   684
qed
1a8efd618190 reorganize and speed up termdiffs proofs
huffman
parents: 20849
diff changeset
   685
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   686
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   687
subsection {* Derivability of power series *}
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   688
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   689
lemma DERIV_series':
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   690
  fixes f :: "real \<Rightarrow> nat \<Rightarrow> real"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   691
  assumes DERIV_f: "\<And> n. DERIV (\<lambda> x. f x n) x0 :> (f' x0 n)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   692
    and allf_summable: "\<And> x. x \<in> {a <..< b} \<Longrightarrow> summable (f x)" and x0_in_I: "x0 \<in> {a <..< b}"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   693
    and "summable (f' x0)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   694
    and "summable L"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   695
    and L_def: "\<And>n x y. \<lbrakk> x \<in> { a <..< b} ; y \<in> { a <..< b} \<rbrakk> \<Longrightarrow> \<bar>f x n - f y n\<bar> \<le> L n * \<bar>x - y\<bar>"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   696
  shows "DERIV (\<lambda> x. suminf (f x)) x0 :> (suminf (f' x0))"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   697
  unfolding DERIV_def
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   698
proof (rule LIM_I)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   699
  fix r :: real
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   700
  assume "0 < r" hence "0 < r/3" by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   701
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   702
  obtain N_L where N_L: "\<And> n. N_L \<le> n \<Longrightarrow> \<bar> \<Sum> i. L (i + n) \<bar> < r/3"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   703
    using suminf_exist_split[OF `0 < r/3` `summable L`] by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   704
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   705
  obtain N_f' where N_f': "\<And> n. N_f' \<le> n \<Longrightarrow> \<bar> \<Sum> i. f' x0 (i + n) \<bar> < r/3"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   706
    using suminf_exist_split[OF `0 < r/3` `summable (f' x0)`] by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   707
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   708
  let ?N = "Suc (max N_L N_f')"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   709
  have "\<bar> \<Sum> i. f' x0 (i + ?N) \<bar> < r/3" (is "?f'_part < r/3") and
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   710
    L_estimate: "\<bar> \<Sum> i. L (i + ?N) \<bar> < r/3" using N_L[of "?N"] and N_f' [of "?N"] by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   711
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   712
  let ?diff = "\<lambda>i x. (f (x0 + x) i - f x0 i) / x"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   713
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   714
  let ?r = "r / (3 * real ?N)"
56541
0e3abadbef39 made divide_pos_pos a simp rule
nipkow
parents: 56536
diff changeset
   715
  from `0 < r` have "0 < ?r" by simp
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   716
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   717
  let ?s = "\<lambda>n. SOME s. 0 < s \<and> (\<forall> x. x \<noteq> 0 \<and> \<bar> x \<bar> < s \<longrightarrow> \<bar> ?diff n x - f' x0 n \<bar> < ?r)"
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   718
  def S' \<equiv> "Min (?s ` {..< ?N })"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   719
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   720
  have "0 < S'" unfolding S'_def
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   721
  proof (rule iffD2[OF Min_gr_iff])
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   722
    show "\<forall>x \<in> (?s ` {..< ?N }). 0 < x"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   723
    proof
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   724
      fix x
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   725
      assume "x \<in> ?s ` {..<?N}"
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   726
      then obtain n where "x = ?s n" and "n \<in> {..<?N}"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   727
        using image_iff[THEN iffD1] by blast
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   728
      from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def]
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   729
      obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   730
        by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   731
      have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound)
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   732
      thus "0 < x" unfolding `x = ?s n` .
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   733
    qed
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   734
  qed auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   735
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   736
  def S \<equiv> "min (min (x0 - a) (b - x0)) S'"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   737
  hence "0 < S" and S_a: "S \<le> x0 - a" and S_b: "S \<le> b - x0"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   738
    and "S \<le> S'" using x0_in_I and `0 < S'`
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   739
    by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   740
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   741
  {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   742
    fix x
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   743
    assume "x \<noteq> 0" and "\<bar> x \<bar> < S"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   744
    hence x_in_I: "x0 + x \<in> { a <..< b }"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   745
      using S_a S_b by auto
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   746
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   747
    note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   748
    note div_smbl = summable_divide[OF diff_smbl]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   749
    note all_smbl = summable_diff[OF div_smbl `summable (f' x0)`]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   750
    note ign = summable_ignore_initial_segment[where k="?N"]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   751
    note diff_shft_smbl = summable_diff[OF ign[OF allf_summable[OF x_in_I]] ign[OF allf_summable[OF x0_in_I]]]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   752
    note div_shft_smbl = summable_divide[OF diff_shft_smbl]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   753
    note all_shft_smbl = summable_diff[OF div_smbl ign[OF `summable (f' x0)`]]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   754
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   755
    { fix n
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   756
      have "\<bar> ?diff (n + ?N) x \<bar> \<le> L (n + ?N) * \<bar> (x0 + x) - x0 \<bar> / \<bar> x \<bar>"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   757
        using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero]
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   758
        unfolding abs_divide .
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   759
      hence "\<bar> (\<bar>?diff (n + ?N) x \<bar>) \<bar> \<le> L (n + ?N)"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   760
        using `x \<noteq> 0` by auto }
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   761
    note 1 = this and 2 = summable_rabs_comparison_test[OF _ ign[OF `summable L`]]
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   762
    then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))"
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
   763
      by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF `summable L`]]])
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   764
    then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3")
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   765
      using L_estimate by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   766
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   767
    have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> \<le> (\<Sum>n<?N. \<bar>?diff n x - f' x0 n \<bar>)" ..
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   768
    also have "\<dots> < (\<Sum>n<?N. ?r)"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   769
    proof (rule setsum_strict_mono)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   770
      fix n
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   771
      assume "n \<in> {..< ?N}"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   772
      have "\<bar>x\<bar> < S" using `\<bar>x\<bar> < S` .
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   773
      also have "S \<le> S'" using `S \<le> S'` .
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   774
      also have "S' \<le> ?s n" unfolding S'_def
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   775
      proof (rule Min_le_iff[THEN iffD2])
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   776
        have "?s n \<in> (?s ` {..<?N}) \<and> ?s n \<le> ?s n"
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   777
          using `n \<in> {..< ?N}` by auto
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   778
        thus "\<exists> a \<in> (?s ` {..<?N}). a \<le> ?s n" by blast
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   779
      qed auto
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   780
      finally have "\<bar>x\<bar> < ?s n" .
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   781
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   782
      from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF `0 < ?r`, unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   783
      have "\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < ?s n \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r" .
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   784
      with `x \<noteq> 0` and `\<bar>x\<bar> < ?s n` show "\<bar>?diff n x - f' x0 n\<bar> < ?r"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   785
        by blast
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   786
    qed auto
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   787
    also have "\<dots> = of_nat (card {..<?N}) * ?r"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   788
      by (rule setsum_constant)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   789
    also have "\<dots> = real ?N * ?r"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   790
      unfolding real_eq_of_nat by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   791
    also have "\<dots> = r/3" by auto
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   792
    finally have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   793
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   794
    from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   795
    have "\<bar>(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)\<bar> =
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   796
        \<bar>\<Sum>n. ?diff n x - f' x0 n\<bar>"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   797
      unfolding suminf_diff[OF div_smbl `summable (f' x0)`, symmetric]
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   798
      using suminf_divide[OF diff_smbl, symmetric] by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   799
    also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   800
      unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"]
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   801
      unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]]
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   802
      apply (subst (5) add.commute)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   803
      by (rule abs_triangle_ineq)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   804
    also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   805
      using abs_triangle_ineq4 by auto
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   806
    also have "\<dots> < r /3 + r/3 + r/3"
36842
99745a4b9cc9 fix some linarith_split_limit warnings
huffman
parents: 36824
diff changeset
   807
      using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3`
99745a4b9cc9 fix some linarith_split_limit warnings
huffman
parents: 36824
diff changeset
   808
      by (rule add_strict_mono [OF add_less_le_mono])
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   809
    finally have "\<bar>(suminf (f (x0 + x)) - suminf (f x0)) / x - suminf (f' x0)\<bar> < r"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   810
      by auto
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   811
  }
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   812
  thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   813
      norm (((\<Sum>n. f (x0 + x) n) - (\<Sum>n. f x0 n)) / x - (\<Sum>n. f' x0 n)) < r"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   814
    using `0 < S` unfolding real_norm_def diff_0_right by blast
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   815
qed
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   816
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   817
lemma DERIV_power_series':
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   818
  fixes f :: "nat \<Rightarrow> real"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   819
  assumes converges: "\<And> x. x \<in> {-R <..< R} \<Longrightarrow> summable (\<lambda> n. f n * real (Suc n) * x^n)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   820
    and x0_in_I: "x0 \<in> {-R <..< R}" and "0 < R"
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   821
  shows "DERIV (\<lambda> x. (\<Sum> n. f n * x^(Suc n))) x0 :> (\<Sum> n. f n * real (Suc n) * x0^n)"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   822
  (is "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))")
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   823
proof -
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   824
  {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   825
    fix R'
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   826
    assume "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   827
    hence "x0 \<in> {-R' <..< R'}" and "R' \<in> {-R <..< R}" and "x0 \<in> {-R <..< R}"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   828
      by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   829
    have "DERIV (\<lambda> x. (suminf (?f x))) x0 :> (suminf (?f' x0))"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   830
    proof (rule DERIV_series')
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   831
      show "summable (\<lambda> n. \<bar>f n * real (Suc n) * R'^n\<bar>)"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   832
      proof -
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   833
        have "(R' + R) / 2 < R" and "0 < (R' + R) / 2"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   834
          using `0 < R'` `0 < R` `R' < R` by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   835
        hence in_Rball: "(R' + R) / 2 \<in> {-R <..< R}"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   836
          using `R' < R` by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   837
        have "norm R' < norm ((R' + R) / 2)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   838
          using `0 < R'` `0 < R` `R' < R` by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   839
        from powser_insidea[OF converges[OF in_Rball] this] show ?thesis
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   840
          by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   841
      qed
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   842
      {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   843
        fix n x y
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   844
        assume "x \<in> {-R' <..< R'}" and "y \<in> {-R' <..< R'}"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   845
        show "\<bar>?f x n - ?f y n\<bar> \<le> \<bar>f n * real (Suc n) * R'^n\<bar> * \<bar>x-y\<bar>"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   846
        proof -
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   847
          have "\<bar>f n * x ^ (Suc n) - f n * y ^ (Suc n)\<bar> =
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   848
            (\<bar>f n\<bar> * \<bar>x-y\<bar>) * \<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar>"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   849
            unfolding right_diff_distrib[symmetric] lemma_realpow_diff_sumr2 abs_mult
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   850
            by auto
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   851
          also have "\<dots> \<le> (\<bar>f n\<bar> * \<bar>x-y\<bar>) * (\<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   852
          proof (rule mult_left_mono)
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   853
            have "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> (\<Sum>p<Suc n. \<bar>x ^ p * y ^ (n - p)\<bar>)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   854
              by (rule setsum_abs)
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   855
            also have "\<dots> \<le> (\<Sum>p<Suc n. R' ^ n)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   856
            proof (rule setsum_mono)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   857
              fix p
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   858
              assume "p \<in> {..<Suc n}"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   859
              hence "p \<le> n" by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   860
              {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   861
                fix n
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   862
                fix x :: real
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   863
                assume "x \<in> {-R'<..<R'}"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   864
                hence "\<bar>x\<bar> \<le> R'"  by auto
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   865
                hence "\<bar>x^n\<bar> \<le> R'^n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   866
                  unfolding power_abs by (rule power_mono, auto)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   867
              }
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   868
              from mult_mono[OF this[OF `x \<in> {-R'<..<R'}`, of p] this[OF `y \<in> {-R'<..<R'}`, of "n-p"]] `0 < R'`
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   869
              have "\<bar>x^p * y^(n-p)\<bar> \<le> R'^p * R'^(n-p)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   870
                unfolding abs_mult by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   871
              thus "\<bar>x^p * y^(n-p)\<bar> \<le> R'^n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   872
                unfolding power_add[symmetric] using `p \<le> n` by auto
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   873
            qed
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   874
            also have "\<dots> = real (Suc n) * R' ^ n"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   875
              unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   876
            finally show "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   877
              unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] .
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   878
            show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   879
              unfolding abs_mult[symmetric] by auto
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   880
          qed
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   881
          also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   882
            unfolding abs_mult mult.assoc[symmetric] by algebra
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   883
          finally show ?thesis .
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   884
        qed
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   885
      }
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   886
      {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   887
        fix n
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   888
        show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
   889
          by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   890
      }
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   891
      {
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   892
        fix x
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   893
        assume "x \<in> {-R' <..< R'}"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   894
        hence "R' \<in> {-R <..< R}" and "norm x < norm R'"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   895
          using assms `R' < R` by auto
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   896
        have "summable (\<lambda> n. f n * x^n)"
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   897
        proof (rule summable_comparison_test, intro exI allI impI)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32047
diff changeset
   898
          fix n
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   899
          have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   900
            by (rule mult_left_mono) auto
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   901
          show "norm (f n * x^n) \<le> norm (f n * real (Suc n) * x^n)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   902
            unfolding real_norm_def abs_mult
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   903
            by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   904
        qed (rule powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`])
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
   905
        from this[THEN summable_mult2[where c=x], unfolded mult.assoc, unfolded mult.commute]
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   906
        show "summable (?f x)" by auto
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   907
      }
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   908
      show "summable (?f' x0)"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   909
        using converges[OF `x0 \<in> {-R <..< R}`] .
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   910
      show "x0 \<in> {-R' <..< R'}"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   911
        using `x0 \<in> {-R' <..< R'}` .
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   912
    qed
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   913
  } note for_subinterval = this
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   914
  let ?R = "(R + \<bar>x0\<bar>) / 2"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   915
  have "\<bar>x0\<bar> < ?R" using assms by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   916
  hence "- ?R < x0"
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   917
  proof (cases "x0 < 0")
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   918
    case True
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   919
    hence "- x0 < ?R" using `\<bar>x0\<bar> < ?R` by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   920
    thus ?thesis unfolding neg_less_iff_less[symmetric, of "- x0"] by auto
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   921
  next
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   922
    case False
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   923
    have "- ?R < 0" using assms by auto
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   924
    also have "\<dots> \<le> x0" using False by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   925
    finally show ?thesis .
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   926
  qed
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   927
  hence "0 < ?R" "?R < R" "- ?R < x0" and "x0 < ?R"
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   928
    using assms by auto
29803
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   929
  from for_subinterval[OF this]
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   930
  show ?thesis .
c56a5571f60a Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents: 29695
diff changeset
   931
qed
29695
171146a93106 Added real related theorems from Fact.thy
chaieb
parents: 29667
diff changeset
   932
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   933
29164
0d49c5b55046 move sin and cos to their own subsection
huffman
parents: 29163
diff changeset
   934
subsection {* Exponential Function *}
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   935
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
   936
definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   937
  where "exp = (\<lambda>x. \<Sum>n. x^n /\<^sub>R fact n)"
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   938
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   939
lemma summable_exp_generic:
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30273
diff changeset
   940
  fixes x :: "'a::{real_normed_algebra_1,banach}"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   941
  defines S_def: "S \<equiv> \<lambda>n. x^n /\<^sub>R fact n"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   942
  shows "summable S"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   943
proof -
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   944
  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R (Suc n)"
30273
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30082
diff changeset
   945
    unfolding S_def by (simp del: mult_Suc)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   946
  obtain r :: real where r0: "0 < r" and r1: "r < 1"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   947
    using dense [OF zero_less_one] by fast
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   948
  obtain N :: nat where N: "norm x < real N * r"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   949
    using reals_Archimedean3 [OF r0] by fast
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   950
  from r1 show ?thesis
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
   951
  proof (rule summable_ratio_test [rule_format])
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   952
    fix n :: nat
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   953
    assume n: "N \<le> n"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   954
    have "norm x \<le> real N * r"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   955
      using N by (rule order_less_imp_le)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   956
    also have "real N * r \<le> real (Suc n) * r"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   957
      using r0 n by (simp add: mult_right_mono)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   958
    finally have "norm x * norm (S n) \<le> real (Suc n) * r * norm (S n)"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   959
      using norm_ge_zero by (rule mult_right_mono)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   960
    hence "norm (x * S n) \<le> real (Suc n) * r * norm (S n)"
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   961
      by (rule order_trans [OF norm_mult_ineq])
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   962
    hence "norm (x * S n) / real (Suc n) \<le> r * norm (S n)"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   963
      by (simp add: pos_divide_le_eq ac_simps)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   964
    thus "norm (S (Suc n)) \<le> r * norm (S n)"
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35213
diff changeset
   965
      by (simp add: S_Suc inverse_eq_divide)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   966
  qed
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   967
qed
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   968
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   969
lemma summable_norm_exp:
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30273
diff changeset
   970
  fixes x :: "'a::{real_normed_algebra_1,banach}"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   971
  shows "summable (\<lambda>n. norm (x^n /\<^sub>R fact n))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   972
proof (rule summable_norm_comparison_test [OF exI, rule_format])
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   973
  show "summable (\<lambda>n. norm x^n /\<^sub>R fact n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   974
    by (rule summable_exp_generic)
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   975
  fix n
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   976
  show "norm (x^n /\<^sub>R fact n) \<le> norm x^n /\<^sub>R fact n"
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35213
diff changeset
   977
    by (simp add: norm_power_ineq)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   978
qed
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   979
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   980
lemma summable_exp: 
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   981
  fixes x :: "'a::{real_normed_field,banach}"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   982
  shows "summable (\<lambda>n. inverse (fact n) * x^n)"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   983
  using summable_exp_generic [where x=x]
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   984
  by (simp add: scaleR_conv_of_real nonzero_of_real_inverse)
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   985
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   986
lemma exp_converges: "(\<lambda>n. x^n /\<^sub>R fact n) sums exp x"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   987
  unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
23043
5dbfd67516a4 rearranged sections
huffman
parents: 23011
diff changeset
   988
41970
47d6e13d1710 generalize infinite sums
hoelzl
parents: 41550
diff changeset
   989
lemma exp_fdiffs:
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   990
  fixes XXX :: "'a::{real_normed_field,banach}"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   991
  shows "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a))"
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   992
  by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
   993
           del: mult_Suc of_nat_Suc)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   994
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   995
lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   996
  by (simp add: diffs_def)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
   997
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
   998
lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
   999
  unfolding exp_def scaleR_conv_of_real
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1000
  apply (rule DERIV_cong)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1001
  apply (rule termdiffs [where K="of_real (1 + norm x)"])
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1002
  apply (simp_all only: diffs_of_real scaleR_conv_of_real exp_fdiffs)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1003
  apply (rule exp_converges [THEN sums_summable, unfolded scaleR_conv_of_real])+
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1004
  apply (simp del: of_real_add)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1005
  done
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1006
56381
0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros
hoelzl
parents: 56371
diff changeset
  1007
declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
51527
bd62e7ff103b move Ln.thy and Log.thy to Transcendental.thy
hoelzl
parents: 51482
diff changeset
  1008
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1009
lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1010
proof -
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1011
  from summable_norm[OF summable_norm_exp, of x]
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
  1012
  have "norm (exp x) \<le> (\<Sum>n. inverse (fact n) * norm (x^n))"
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1013
    by (simp add: exp_def)
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1014
  also have "\<dots> \<le> exp (norm x)"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1015
    using summable_exp_generic[of "norm x"] summable_norm_exp[of x]
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1016
    by (auto simp: exp_def intro!: suminf_le norm_power_ineq)
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1017
  finally show ?thesis .
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1018
qed
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1019
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1020
lemma isCont_exp:
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1021
  fixes x::"'a::{real_normed_field,banach}"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1022
  shows "isCont exp x"
44311
42c5cbf68052 Transcendental.thy: add tendsto_intros lemmas;
huffman
parents: 44308
diff changeset
  1023
  by (rule DERIV_exp [THEN DERIV_isCont])
42c5cbf68052 Transcendental.thy: add tendsto_intros lemmas;
huffman
parents: 44308
diff changeset
  1024
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1025
lemma isCont_exp' [simp]:
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1026
  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1027
  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
44311
42c5cbf68052 Transcendental.thy: add tendsto_intros lemmas;
huffman
parents: 44308
diff changeset
  1028
  by (rule isCont_o2 [OF _ isCont_exp])
42c5cbf68052 Transcendental.thy: add tendsto_intros lemmas;
huffman
parents: 44308
diff changeset
  1029
42c5cbf68052 Transcendental.thy: add tendsto_intros lemmas;
huffman
parents: 44308
diff changeset
  1030
lemma tendsto_exp [tendsto_intros]:
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1031
  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1032
  shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
44311
42c5cbf68052 Transcendental.thy: add tendsto_intros lemmas;
huffman
parents: 44308
diff changeset
  1033
  by (rule isCont_tendsto_compose [OF isCont_exp])
23045
95e04f335940 add lemmas about inverse functions; cleaned up proof of polar_ex
huffman
parents: 23043
diff changeset
  1034
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1035
lemma continuous_exp [continuous_intros]:
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1036
  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1037
  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51477
diff changeset
  1038
  unfolding continuous_def by (rule tendsto_exp)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51477
diff changeset
  1039
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56261
diff changeset
  1040
lemma continuous_on_exp [continuous_intros]:
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1041
  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1042
  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51477
diff changeset
  1043
  unfolding continuous_on_def by (auto intro: tendsto_exp)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51477
diff changeset
  1044
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1045
29167
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1046
subsubsection {* Properties of the Exponential Function *}
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1047
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
  1048
lemma powser_zero:
31017
2c227493ea56 stripped class recpower further
haftmann
parents: 30273
diff changeset
  1049
  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1}"
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
  1050
  shows "(\<Sum>n. f n * 0 ^ n) = f 0"
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1051
proof -
56193
c726ecfb22b6 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents: 56181
diff changeset
  1052
  have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1053
    by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
30082
43c5b7bfc791 make more proofs work whether or not One_nat_def is a simp rule
huffman
parents: 29803
diff changeset
  1054
  thus ?thesis unfolding One_nat_def by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1055
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1056
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
  1057
lemma exp_zero [simp]: "exp 0 = 1"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1058
  unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
23278
375335bf619f clean up proofs of exp_zero, sin_zero, cos_zero
huffman
parents: 23255
diff changeset
  1059
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1060
lemma exp_series_add_commuting:
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1061
  fixes x y :: "'a::{real_normed_algebra_1, banach}"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
  1062
  defines S_def: "S \<equiv> \<lambda>x n. x^n /\<^sub>R fact n"
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1063
  assumes comm: "x * y = y * x"
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1064
  shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1065
proof (induct n)
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1066
  case 0
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1067
  show ?case
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1068
    unfolding S_def by simp
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1069
next
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1070
  case (Suc n)
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
  1071
  have S_Suc: "\<And>x n. S x (Suc n) = (x * S x n) /\<^sub>R real (Suc n)"
30273
ecd6f0ca62ea declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents: 30082
diff changeset
  1072
    unfolding S_def by (simp del: mult_Suc)
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
  1073
  hence times_S: "\<And>x n. x * S x n = real (Suc n) *\<^sub>R S x (Suc n)"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1074
    by simp
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1075
  have S_comm: "\<And>n. S x n * y = y * S x n"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1076
    by (simp add: power_commuting_commutes comm S_def)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1077
25062
af5ef0d4d655 global class syntax
haftmann
parents: 23477
diff changeset
  1078
  have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1079
    by (simp only: times_S)
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1080
  also have "\<dots> = (x + y) * (\<Sum>i\<le>n. S x i * S y (n-i))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1081
    by (simp only: Suc)
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1082
  also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (n-i))
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1083
                + y * (\<Sum>i\<le>n. S x i * S y (n-i))"
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 47489
diff changeset
  1084
    by (rule distrib_right)
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1085
  also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n-i))
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1086
                + (\<Sum>i\<le>n. S x i * y * S y (n-i))"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1087
    by (simp add: setsum_right_distrib ac_simps S_comm)
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1088
  also have "\<dots> = (\<Sum>i\<le>n. x * S x i * S y (n-i))
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1089
                + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1090
    by (simp add: ac_simps)
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1091
  also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1092
                + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1093
    by (simp add: times_S Suc_diff_le)
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1094
  also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1095
             (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1096
    by (subst setsum_atMost_Suc_shift) simp
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1097
  also have "(\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1098
             (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1099
    by simp
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1100
  also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1101
             (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1102
             (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
57418
6ab1c7cb0b8d fact consolidation
haftmann
parents: 57275
diff changeset
  1103
    by (simp only: setsum.distrib [symmetric] scaleR_left_distrib [symmetric]
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1104
                   real_of_nat_add [symmetric]) simp
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1105
  also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n-i))"
23127
56ee8105c002 simplify names of locale interpretations
huffman
parents: 23115
diff changeset
  1106
    by (simp only: scaleR_right.setsum)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1107
  finally show
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1108
    "S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
35216
7641e8d831d2 get rid of many duplicate simp rule warnings
huffman
parents: 35213
diff changeset
  1109
    by (simp del: setsum_cl_ivl_Suc)
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1110
qed
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1111
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1112
lemma exp_add_commuting: "x * y = y * x \<Longrightarrow> exp (x + y) = exp x * exp y"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1113
  unfolding exp_def
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1114
  by (simp only: Cauchy_product summable_norm_exp exp_series_add_commuting)
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1115
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1116
lemma exp_add:
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1117
  fixes x y::"'a::{real_normed_field,banach}"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1118
  shows "exp (x + y) = exp x * exp y"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1119
  by (rule exp_add_commuting) (simp add: ac_simps)
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1120
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1121
lemma exp_double: "exp(2 * z) = exp z ^ 2"
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1122
  by (simp add: exp_add_commuting mult_2 power2_eq_square)
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1123
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1124
lemmas mult_exp_exp = exp_add [symmetric]
29170
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1125
23241
5f12b40a95bf add lemma exp_of_real
huffman
parents: 23177
diff changeset
  1126
lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1127
  unfolding exp_def
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1128
  apply (subst suminf_of_real)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1129
  apply (rule summable_exp_generic)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1130
  apply (simp add: scaleR_conv_of_real)
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1131
  done
23241
5f12b40a95bf add lemma exp_of_real
huffman
parents: 23177
diff changeset
  1132
59862
44b3f4fa33ca New material and binomial fix
paulson <lp15@cam.ac.uk>
parents: 59751
diff changeset
  1133
corollary exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
44b3f4fa33ca New material and binomial fix
paulson <lp15@cam.ac.uk>
parents: 59751
diff changeset
  1134
  by (metis Reals_cases Reals_of_real exp_of_real)
44b3f4fa33ca New material and binomial fix
paulson <lp15@cam.ac.uk>
parents: 59751
diff changeset
  1135
29170
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1136
lemma exp_not_eq_zero [simp]: "exp x \<noteq> 0"
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1137
proof
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1138
  have "exp x * exp (- x) = 1" by (simp add: exp_add_commuting[symmetric])
29170
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1139
  also assume "exp x = 0"
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1140
  finally show "False" by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1141
qed
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1142
58656
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1143
lemma exp_minus_inverse:
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1144
  shows "exp x * exp (- x) = 1"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1145
  by (simp add: exp_add_commuting[symmetric])
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1146
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1147
lemma exp_minus:
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1148
  fixes x :: "'a::{real_normed_field, banach}"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1149
  shows "exp (- x) = inverse (exp x)"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1150
  by (intro inverse_unique [symmetric] exp_minus_inverse)
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1151
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1152
lemma exp_diff:
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1153
  fixes x :: "'a::{real_normed_field, banach}"
7f14d5d9b933 relaxed class constraints for exp
immler
parents: 58410
diff changeset
  1154
  shows "exp (x - y) = exp x / exp y"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 53602
diff changeset
  1155
  using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1156
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1157
lemma exp_of_nat_mult:
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1158
  fixes x :: "'a::{real_normed_field,banach}"
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1159
  shows "exp(of_nat n * x) = exp(x) ^ n"
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1160
    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1161
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1162
lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I"
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1163
  by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59587
diff changeset
  1164
29167
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1165
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1166
subsubsection {* Properties of the Exponential Function on Reals *}
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1167
29170
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1168
text {* Comparisons of @{term "exp x"} with zero. *}
29167
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1169
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1170
text{*Proof: because every exponential can be seen as a square.*}
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1171
lemma exp_ge_zero [simp]: "0 \<le> exp (x::real)"
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1172
proof -
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1173
  have "0 \<le> exp (x/2) * exp (x/2)" by simp
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1174
  thus ?thesis by (simp add: exp_add [symmetric])
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1175
qed
37a952bb9ebc rearranged subsections; cleaned up some proofs
huffman
parents: 29166
diff changeset
  1176
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1177
lemma exp_gt_zero [simp]: "0 < exp (x::real)"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1178
  by (simp add: order_less_le)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1179
29170
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1180
lemma not_exp_less_zero [simp]: "\<not> exp (x::real) < 0"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1181
  by (simp add: not_less)
29170
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1182
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1183
lemma not_exp_le_zero [simp]: "\<not> exp (x::real) \<le> 0"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1184
  by (simp add: not_le)
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1185
23115
4615b2078592 generalized exp to work over any complete field; new proof of exp_add
huffman
parents: 23112
diff changeset
  1186
lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
53079
ade63ccd6f4e tuned proofs;
wenzelm
parents: 53076
diff changeset
  1187
  by simp
15077
89840837108e converting Hyperreal/Transcendental to Isar script
paulson
parents: 15013
diff changeset
  1188
59669
de7792ea4090 renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
  1189
(*FIXME: superseded by exp_of_nat_mult*)
de7792ea4090 renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
  1190
lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 57492
diff changeset
  1191
  by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
59669
de7792ea4090 renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
  1192
29170
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1193
text {* Strict monotonicity of exponential. *}
dad3933c88dd clean up lemmas about exp
huffman
parents: 29167
diff changeset
  1194
59669
de7792ea4090 renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
  1195
lemma exp_ge_add_one_self_aux:
54575
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
  1196
  assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
  1197
using order_le_imp_less_or_eq [OF assms]
59669
de7792ea4090 renaming HOL/Fact.thy -> Binomial.thy
paulson <lp15@cam.ac.uk>
parents: 59658
diff changeset
  1198
proof
54575
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
  1199
  assume "0 < x"
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
  1200
  have "1+x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
54575
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
  1201
    by (auto simp add: numeral_2_eq_2)
59730
b7c394c7a619 The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents: 59669
diff changeset
  1202
  also have "... \<le> (\<Sum>n. inverse (fact n) * x^n)"
56213
e5720d3c18f0 further renaming in Series
hoelzl
parents: 56193
diff changeset
  1203
    apply (rule setsum_le_suminf [OF summable_exp])
54575
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
  1204
    using `0 < x`
0b9ca2c865cb cleaned up more messy proofs
paulson
parents: 54573
diff changeset
  1205
    apply (auto  simp add:  zero_le_mult_iff)
0b9ca2c865cb cleaned up more messy proofs
paulson
p