The function frac. Various lemmas about limits, series, the exp function, etc.
authorpaulson <lp15@cam.ac.uk>
Thu Mar 05 17:30:29 2015 +0000 (2015-03-05)
changeset 596137103019278f0
parent 59593 304ee0a475d1
child 59614 452458cf8506
The function frac. Various lemmas about limits, series, the exp function, etc.
src/HOL/Archimedean_Field.thy
src/HOL/Complex.thy
src/HOL/Int.thy
src/HOL/Limits.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Thu Mar 05 11:11:42 2015 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Thu Mar 05 17:30:29 2015 +0000
     1.3 @@ -150,6 +150,11 @@
     1.4  lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
     1.5    using floor_correct [of x] floor_exists1 [of x] by auto
     1.6  
     1.7 +lemma floor_unique_iff:
     1.8 +  fixes x :: "'a::floor_ceiling"
     1.9 +  shows  "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
    1.10 +using floor_correct floor_unique by auto
    1.11 +
    1.12  lemma of_int_floor_le: "of_int (floor x) \<le> x"
    1.13    using floor_correct ..
    1.14  
    1.15 @@ -281,6 +286,9 @@
    1.16  lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z"
    1.17    using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
    1.18  
    1.19 +lemma floor_uminus_of_int [simp]: "floor (- (of_int z)) = - z"
    1.20 +  by (metis floor_diff_of_int [of 0] diff_0 floor_zero)
    1.21 +
    1.22  lemma floor_diff_numeral [simp]:
    1.23    "floor (x - numeral v) = floor x - numeral v"
    1.24    using floor_diff_of_int [of x "numeral v"] by simp
    1.25 @@ -464,4 +472,65 @@
    1.26  lemma ceiling_minus: "ceiling (- x) = - floor x"
    1.27    unfolding ceiling_def by simp
    1.28  
    1.29 +subsection {* Frac Function *}
    1.30 +
    1.31 +
    1.32 +definition frac :: "'a \<Rightarrow> 'a::floor_ceiling" where
    1.33 +  "frac x \<equiv> x - of_int \<lfloor>x\<rfloor>"
    1.34 +
    1.35 +lemma frac_lt_1: "frac x < 1"
    1.36 +  by  (simp add: frac_def) linarith
    1.37 +
    1.38 +lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> Ints"
    1.39 +  by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )
    1.40 +
    1.41 +lemma frac_ge_0 [simp]: "frac x \<ge> 0"
    1.42 +  unfolding frac_def
    1.43 +  by linarith
    1.44 +
    1.45 +lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> Ints"
    1.46 +  by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)
    1.47 +
    1.48 +lemma frac_of_int [simp]: "frac (of_int z) = 0"
    1.49 +  by (simp add: frac_def)
    1.50 +
    1.51 +lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"  
    1.52 +proof -
    1.53 +  {assume "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
    1.54 +   then have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
    1.55 +     by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
    1.56 +   }
    1.57 +  moreover
    1.58 +  { assume "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
    1.59 +    then have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
    1.60 +      apply (simp add: floor_unique_iff)
    1.61 +      apply (auto simp add: algebra_simps)
    1.62 +      by linarith    
    1.63 +  }
    1.64 +  ultimately show ?thesis
    1.65 +    by (auto simp add: frac_def algebra_simps)
    1.66 +qed
    1.67 +
    1.68 +lemma frac_add: "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y
    1.69 +                                 else (frac x + frac y) - 1)"  
    1.70 +  by (simp add: frac_def floor_add)
    1.71 +
    1.72 +lemma frac_unique_iff:
    1.73 +  fixes x :: "'a::floor_ceiling"
    1.74 +  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> Ints \<and> 0 \<le> a \<and> a < 1"
    1.75 +  apply (auto simp: Ints_def frac_def)
    1.76 +  apply linarith
    1.77 +  apply linarith
    1.78 +  by (metis (no_types) add.commute add.left_neutral eq_diff_eq floor_add_of_int floor_unique of_int_0)
    1.79 +
    1.80 +lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
    1.81 +  by (simp add: frac_unique_iff)
    1.82 +  
    1.83 +lemma frac_neg:
    1.84 +  fixes x :: "'a::floor_ceiling"
    1.85 +  shows  "frac (-x) = (if x \<in> Ints then 0 else 1 - frac x)"
    1.86 +  apply (auto simp add: frac_unique_iff)
    1.87 +  apply (simp add: frac_def)
    1.88 +  by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
    1.89 +
    1.90  end
     2.1 --- a/src/HOL/Complex.thy	Thu Mar 05 11:11:42 2015 +0100
     2.2 +++ b/src/HOL/Complex.thy	Thu Mar 05 17:30:29 2015 +0000
     2.3 @@ -73,7 +73,7 @@
     2.4  definition "x / (y\<Colon>complex) = x * inverse y"
     2.5  
     2.6  instance
     2.7 -  by intro_classes 
     2.8 +  by intro_classes
     2.9       (simp_all add: complex_eq_iff divide_complex_def
    2.10        distrib_left distrib_right right_diff_distrib left_diff_distrib
    2.11        power2_eq_square add_divide_distrib [symmetric])
    2.12 @@ -161,6 +161,12 @@
    2.13  lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0"
    2.14    by (simp add: of_real_def)
    2.15  
    2.16 +lemma Re_divide_numeral [simp]: "Re (z / numeral w) = Re z / numeral w"
    2.17 +  by (simp add: Re_divide sqr_conv_mult)
    2.18 +
    2.19 +lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
    2.20 +  by (simp add: Im_divide sqr_conv_mult)
    2.21 +
    2.22  subsection {* The Complex Number $i$ *}
    2.23  
    2.24  primcorec "ii" :: complex  ("\<i>") where
    2.25 @@ -206,6 +212,9 @@
    2.26  lemma complex_split_polar: "\<exists>r a. z = complex_of_real r * (cos a + \<i> * sin a)"
    2.27    by (simp add: complex_eq_iff polar_Ex)
    2.28  
    2.29 +lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
    2.30 +  by (metis mult.commute power2_i power_mult)
    2.31 +
    2.32  subsection {* Vector Norm *}
    2.33  
    2.34  instantiation complex :: real_normed_field
    2.35 @@ -501,11 +510,11 @@
    2.36  
    2.37  lemma re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
    2.38    by (auto simp add: Re_divide)
    2.39 -  
    2.40 +
    2.41  lemma im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
    2.42    by (auto simp add: Im_divide)
    2.43  
    2.44 -lemma complex_div_gt_0: 
    2.45 +lemma complex_div_gt_0:
    2.46    "(Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0) \<and> (Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0)"
    2.47  proof cases
    2.48    assume "b = 0" then show ?thesis by auto
    2.49 @@ -547,7 +556,7 @@
    2.50  
    2.51  lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
    2.52    unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
    2.53 -  
    2.54 +
    2.55  lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
    2.56    unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel)
    2.57  
    2.58 @@ -841,7 +850,7 @@
    2.59      by auto
    2.60  qed
    2.61  
    2.62 -lemma csqrt_minus [simp]: 
    2.63 +lemma csqrt_minus [simp]:
    2.64    assumes "Im x < 0 \<or> (Im x = 0 \<and> 0 \<le> Re x)"
    2.65    shows "csqrt (- x) = \<i> * csqrt x"
    2.66  proof -
     3.1 --- a/src/HOL/Int.thy	Thu Mar 05 11:11:42 2015 +0100
     3.2 +++ b/src/HOL/Int.thy	Thu Mar 05 17:30:29 2015 +0000
     3.3 @@ -498,8 +498,16 @@
     3.4  text{*Now we replace the case analysis rule by a more conventional one:
     3.5  whether an integer is negative or not.*}
     3.6  
     3.7 +text{*This version is symmetric in the two subgoals.*}
     3.8 +theorem int_cases2 [case_names nonneg nonpos, cases type: int]:
     3.9 +  "\<lbrakk>!! n. z = int n \<Longrightarrow> P;  !! n. z = - (int n) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    3.10 +apply (cases "z < 0")
    3.11 +apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
    3.12 +done
    3.13 +
    3.14 +text{*This is the default, with a negative case.*}
    3.15  theorem int_cases [case_names nonneg neg, cases type: int]:
    3.16 -  "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
    3.17 +  "[|!! n. z = int n ==> P;  !! n. z = - (int (Suc n)) ==> P |] ==> P"
    3.18  apply (cases "z < 0")
    3.19  apply (blast dest!: negD)
    3.20  apply (simp add: linorder_not_less del: of_nat_Suc)
     4.1 --- a/src/HOL/Limits.thy	Thu Mar 05 11:11:42 2015 +0100
     4.2 +++ b/src/HOL/Limits.thy	Thu Mar 05 17:30:29 2015 +0000
     4.3 @@ -42,6 +42,11 @@
     4.4    shows "filterlim f at_top F \<Longrightarrow> filterlim f at_infinity F"
     4.5    by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
     4.6  
     4.7 +lemma lim_infinity_imp_sequentially:
     4.8 +  "(f ---> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) ---> l) sequentially"
     4.9 +by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
    4.10 +
    4.11 +
    4.12  subsubsection {* Boundedness *}
    4.13  
    4.14  definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
    4.15 @@ -885,7 +890,6 @@
    4.16    qed
    4.17  qed force
    4.18  
    4.19 -
    4.20  subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
    4.21  
    4.22  text {*
    4.23 @@ -1093,6 +1097,36 @@
    4.24  lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
    4.25   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
    4.26  
    4.27 +
    4.28 +lemma at_to_infinity:
    4.29 +  fixes x :: "'a \<Colon> {real_normed_field,field_inverse_zero}"
    4.30 +  shows "(at (0::'a)) = filtermap inverse at_infinity"
    4.31 +proof (rule antisym)
    4.32 +  have "(inverse ---> (0::'a)) at_infinity"
    4.33 +    by (fact tendsto_inverse_0)
    4.34 +  then show "filtermap inverse at_infinity \<le> at (0::'a)"
    4.35 +    apply (simp add: le_principal eventually_filtermap eventually_at_infinity filterlim_def at_within_def)
    4.36 +    apply (rule_tac x="1" in exI, auto)
    4.37 +    done
    4.38 +next
    4.39 +  have "filtermap inverse (filtermap inverse (at (0::'a))) \<le> filtermap inverse at_infinity"
    4.40 +    using filterlim_inverse_at_infinity unfolding filterlim_def
    4.41 +    by (rule filtermap_mono)
    4.42 +  then show "at (0::'a) \<le> filtermap inverse at_infinity"
    4.43 +    by (simp add: filtermap_ident filtermap_filtermap)
    4.44 +qed
    4.45 +
    4.46 +lemma lim_at_infinity_0:
    4.47 +  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
    4.48 +  shows "(f ---> l) at_infinity \<longleftrightarrow> ((f o inverse) ---> l) (at (0::'a))"
    4.49 +by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap)
    4.50 +
    4.51 +lemma lim_zero_infinity:
    4.52 +  fixes l :: "'a :: {real_normed_field,field_inverse_zero}"
    4.53 +  shows "((\<lambda>x. f(1 / x)) ---> l) (at (0::'a)) \<Longrightarrow> (f ---> l) at_infinity"
    4.54 +by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def)
    4.55 +
    4.56 +
    4.57  text {*
    4.58  
    4.59  We only show rules for multiplication and addition when the functions are either against a real
     5.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Mar 05 11:11:42 2015 +0100
     5.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Mar 05 17:30:29 2015 +0000
     5.3 @@ -853,6 +853,12 @@
     5.4    shows "norm (x ^ n) = norm x ^ n"
     5.5  by (induct n) (simp_all add: norm_mult)
     5.6  
     5.7 +text{*Despite a superficial resemblance, @{text norm_eq_1} is not relevant.*}
     5.8 +lemma square_norm_one:
     5.9 +  fixes x :: "'a::real_normed_div_algebra"
    5.10 +  assumes "x^2 = 1" shows "norm x = 1"
    5.11 +  by (metis assms norm_minus_cancel norm_one power2_eq_1_iff)
    5.12 +
    5.13  lemma setprod_norm:
    5.14    fixes f :: "'a \<Rightarrow> 'b::{comm_semiring_1,real_normed_div_algebra}"
    5.15    shows "setprod (\<lambda>x. norm(f x)) A = norm (setprod f A)"
     6.1 --- a/src/HOL/Series.thy	Thu Mar 05 11:11:42 2015 +0100
     6.2 +++ b/src/HOL/Series.thy	Thu Mar 05 17:30:29 2015 +0000
     6.3 @@ -125,6 +125,11 @@
     6.4  lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
     6.5    by (metis summable_sums sums_summable sums_unique)
     6.6  
     6.7 +lemma sums_unique2:
     6.8 +  fixes a b :: "'a::{comm_monoid_add,t2_space}"
     6.9 +  shows "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b"
    6.10 +by (simp add: sums_iff)
    6.11 +
    6.12  lemma suminf_finite:
    6.13    assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
    6.14    shows "suminf f = (\<Sum>n\<in>N. f n)"
    6.15 @@ -316,6 +321,12 @@
    6.16  
    6.17  end
    6.18  
    6.19 +lemma summable_minus_iff:
    6.20 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    6.21 +  shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
    6.22 +  by (auto dest: summable_minus) --{*used two ways, hence must be outside the context above*}
    6.23 +
    6.24 +
    6.25  context
    6.26    fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
    6.27  begin
     7.1 --- a/src/HOL/Transcendental.thy	Thu Mar 05 11:11:42 2015 +0100
     7.2 +++ b/src/HOL/Transcendental.thy	Thu Mar 05 17:30:29 2015 +0000
     7.3 @@ -1011,22 +1011,22 @@
     7.4    by (rule DERIV_exp [THEN DERIV_isCont])
     7.5  
     7.6  lemma isCont_exp' [simp]:
     7.7 -  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
     7.8 +  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
     7.9    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. exp (f x)) a"
    7.10    by (rule isCont_o2 [OF _ isCont_exp])
    7.11  
    7.12  lemma tendsto_exp [tendsto_intros]:
    7.13 -  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
    7.14 +  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
    7.15    shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. exp (f x)) ---> exp a) F"
    7.16    by (rule isCont_tendsto_compose [OF isCont_exp])
    7.17  
    7.18  lemma continuous_exp [continuous_intros]:
    7.19 -  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
    7.20 +  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
    7.21    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. exp (f x))"
    7.22    unfolding continuous_def by (rule tendsto_exp)
    7.23  
    7.24  lemma continuous_on_exp [continuous_intros]:
    7.25 -  fixes f::"_ \<Rightarrow>'a::{real_normed_field,banach}"
    7.26 +  fixes f:: "_ \<Rightarrow>'a::{real_normed_field,banach}"
    7.27    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. exp (f x))"
    7.28    unfolding continuous_on_def by (auto intro: tendsto_exp)
    7.29  
    7.30 @@ -1106,6 +1106,9 @@
    7.31    shows "exp (x + y) = exp x * exp y"
    7.32    by (rule exp_add_commuting) (simp add: ac_simps)
    7.33  
    7.34 +lemma exp_double: "exp(2 * z) = exp z ^ 2"
    7.35 +  by (simp add: exp_add_commuting mult_2 power2_eq_square)
    7.36 +
    7.37  lemmas mult_exp_exp = exp_add [symmetric]
    7.38  
    7.39  lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
    7.40 @@ -1136,6 +1139,14 @@
    7.41    shows "exp (x - y) = exp x / exp y"
    7.42    using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
    7.43  
    7.44 +lemma exp_of_nat_mult:
    7.45 +  fixes x :: "'a::{real_normed_field,banach}"
    7.46 +  shows "exp(of_nat n * x) = exp(x) ^ n"
    7.47 +    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
    7.48 +
    7.49 +lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I"
    7.50 +  by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
    7.51 +
    7.52  
    7.53  subsubsection {* Properties of the Exponential Function on Reals *}
    7.54  
    7.55 @@ -1160,9 +1171,10 @@
    7.56  lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
    7.57    by simp
    7.58  
    7.59 -lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
    7.60 +(*FIXME: superseded by exp_of_nat_mult*) 
    7.61 +lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" 
    7.62    by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
    7.63 -
    7.64 +  
    7.65  text {* Strict monotonicity of exponential. *}
    7.66  
    7.67  lemma exp_ge_add_one_self_aux: 
    7.68 @@ -1481,6 +1493,36 @@
    7.69    thus ?thesis unfolding exp_first_two_terms by auto
    7.70  qed
    7.71  
    7.72 +corollary exp_half_le2: "exp(1/2) \<le> (2::real)"
    7.73 +  using exp_bound [of "1/2"]
    7.74 +  by (simp add: field_simps)
    7.75 +
    7.76 +lemma exp_bound_half: "norm(z) \<le> 1/2 \<Longrightarrow> norm(exp z) \<le> 2"
    7.77 +  by (blast intro: order_trans intro!: exp_half_le2 norm_exp)
    7.78 +
    7.79 +lemma exp_bound_lemma:
    7.80 +  assumes "norm(z) \<le> 1/2" shows "norm(exp z) \<le> 1 + 2 * norm(z)"
    7.81 +proof -
    7.82 +  have n: "(norm z)\<^sup>2 \<le> norm z * 1"
    7.83 +    unfolding power2_eq_square
    7.84 +    apply (rule mult_left_mono)
    7.85 +    using assms
    7.86 +    apply (auto simp: )
    7.87 +    done
    7.88 +  show ?thesis
    7.89 +    apply (rule order_trans [OF norm_exp])
    7.90 +    apply (rule order_trans [OF exp_bound])
    7.91 +    using assms n
    7.92 +    apply (auto simp: )
    7.93 +    done
    7.94 +qed
    7.95 +
    7.96 +lemma real_exp_bound_lemma:
    7.97 +  fixes x :: real
    7.98 +  shows "0 \<le> x \<Longrightarrow> x \<le> 1/2 \<Longrightarrow> exp(x) \<le> 1 + 2 * x"
    7.99 +using exp_bound_lemma [of x]
   7.100 +by simp
   7.101 +
   7.102  lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
   7.103  proof -
   7.104    assume a: "0 <= (x::real)" and b: "x < 1"
   7.105 @@ -1736,6 +1778,16 @@
   7.106    by (rule filterlim_at_top_at_top[where Q="\<lambda>x. True" and P="\<lambda>x. 0 < x" and g="ln"])
   7.107       (auto intro: eventually_gt_at_top)
   7.108  
   7.109 +lemma lim_exp_minus_1:
   7.110 +  fixes x :: "'a::{real_normed_field,banach}"
   7.111 +  shows "((\<lambda>z::'a. (exp(z) - 1) / z) ---> 1) (at 0)"
   7.112 +proof -
   7.113 +  have "((\<lambda>z::'a. exp(z) - 1) has_field_derivative 1) (at 0)"
   7.114 +    by (intro derivative_eq_intros | simp)+
   7.115 +  then show ?thesis
   7.116 +    by (simp add: Deriv.DERIV_iff2)
   7.117 +qed
   7.118 +
   7.119  lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
   7.120    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
   7.121       (auto simp: eventually_at_filter)