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