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