src/HOL/Analysis/Complex_Transcendental.thy
 changeset 65719 7c57d79d61b7 parent 65587 16a8991ab398 child 66252 b73f94b366b7
```     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu May 04 11:34:42 2017 +0200
1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu May 04 15:14:49 2017 +0100
1.3 @@ -709,14 +709,16 @@
1.4    apply (simp only: pos_le_divide_eq [symmetric], linarith)
1.5    done
1.6
1.7 -text\<open>An odd contrast with the much more easily proved @{thm exp_le}\<close>
1.8 -lemma e_less_3: "exp 1 < (3::real)"
1.9 +lemma e_less_272: "exp 1 < (272/100::real)"
1.10    using e_approx_32
1.11    by (simp add: abs_if split: if_split_asm)
1.12
1.13 +lemma ln_272_gt_1: "ln (272/100) > (1::real)"
1.14 +  by (metis e_less_272 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
1.15 +
1.16 +text\<open>Apparently redundant. But many arguments involve integers.\<close>
1.17  lemma ln3_gt_1: "ln 3 > (1::real)"
1.18 -  by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
1.19 -
1.20 +  by (simp add: less_trans [OF ln_272_gt_1])
1.21
1.22  subsection\<open>The argument of a complex number\<close>
1.23
1.24 @@ -1071,6 +1073,9 @@
1.25  lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
1.26    using Ln_of_real by force
1.27
1.28 +lemma Ln_Reals_eq: "\<lbrakk>x \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> ln x = of_real (ln (Re x))"
1.29 +  using Ln_of_real by force
1.30 +
1.31  lemma Ln_1 [simp]: "ln 1 = (0::complex)"
1.32  proof -
1.33    have "ln (exp 0) = (0::complex)"
1.34 @@ -1185,6 +1190,28 @@
1.35  lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
1.36    by (simp add: field_differentiable_within_Ln holomorphic_on_def)
1.37
1.38 +lemma divide_ln_mono:
1.39 +  fixes x y::real
1.40 +  assumes "3 \<le> x" "x \<le> y"
1.41 +  shows "x / ln x \<le> y / ln y"
1.42 +proof (rule exE [OF complex_mvt_line [of x y "\<lambda>z. z / Ln z" "\<lambda>z. 1/(Ln z) - 1/(Ln z)^2"]];
1.43 +    clarsimp simp add: closed_segment_Reals closed_segment_eq_real_ivl assms)
1.44 +  show "\<And>u. \<lbrakk>x \<le> u; u \<le> y\<rbrakk> \<Longrightarrow> ((\<lambda>z. z / Ln z) has_field_derivative 1 / Ln u - 1 / (Ln u)\<^sup>2) (at u)"
1.45 +    using \<open>3 \<le> x\<close> apply -
1.46 +    apply (rule derivative_eq_intros | simp)+
1.47 +    apply (force simp: field_simps power_eq_if)
1.48 +    done
1.49 +  show "x / ln x \<le> y / ln y"
1.50 +    if "Re (y / Ln y) - Re (x / Ln x) = (Re (1 / Ln u) - Re (1 / (Ln u)\<^sup>2)) * (y - x)"
1.51 +    and x: "x \<le> u" "u \<le> y" for u
1.52 +  proof -
1.53 +    have eq: "y / ln y = (1 / ln u - 1 / (ln u)\<^sup>2) * (y - x) + x / ln x"
1.54 +      using that \<open>3 \<le> x\<close> by (auto simp: Ln_Reals_eq in_Reals_norm group_add_class.diff_eq_eq)
1.55 +    show ?thesis
1.56 +      using exp_le \<open>3 \<le> x\<close> x by (simp add: eq) (simp add: power_eq_if divide_simps ln_ge_iff)
1.57 +  qed
1.58 +qed
1.59 +
1.60
1.62
1.63 @@ -1717,6 +1744,9 @@
1.64    shows "0 \<le> x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
1.65    by (simp_all add: powr_def exp_eq_polar)
1.66
1.67 +lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
1.68 +  by (metis linear not_le of_real_Re powr_of_real)
1.69 +
1.70  lemma norm_powr_real_mono:
1.71      "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
1.72       \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
1.73 @@ -1727,6 +1757,15 @@
1.74             \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
1.75    by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
1.76
1.77 +lemma Re_powr_le: "r \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> Re (r powr z) \<le> Re r powr Re z"
1.78 +  by (auto simp: powr_def nonneg_Reals_def order_trans [OF complex_Re_le_cmod])
1.79 +
1.80 +lemma
1.81 +  fixes w::complex
1.82 +  shows Reals_powr [simp]: "\<lbrakk>w \<in> \<real>\<^sub>\<ge>\<^sub>0; z \<in> \<real>\<rbrakk> \<Longrightarrow> w powr z \<in> \<real>"
1.83 +  and nonneg_Reals_powr [simp]: "\<lbrakk>w \<in> \<real>\<^sub>\<ge>\<^sub>0; z \<in> \<real>\<rbrakk> \<Longrightarrow> w powr z \<in> \<real>\<^sub>\<ge>\<^sub>0"
1.84 +  by (auto simp: nonneg_Reals_def Reals_def powr_of_real)
1.85 +
1.86  lemma powr_neg_real_complex:
1.87    shows   "(- of_real x) powr a = (-1) powr (of_real (sgn x) * a) * of_real x powr (a :: complex)"
1.88  proof (cases "x = 0")
1.89 @@ -1938,12 +1977,6 @@
1.90  lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
1.91    using lim_Ln_over_power [of 1] by simp
1.92
1.93 -lemma Ln_Reals_eq: "\<lbrakk>x \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> Ln x = of_real (ln (Re x))"
1.94 -  using Ln_of_real by force
1.95 -
1.96 -lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
1.97 -  by (metis linear not_le of_real_Re powr_of_real)
1.98 -
1.99  lemma lim_ln_over_power:
1.100    fixes s :: real
1.101    assumes "0 < s"
1.102 @@ -1965,8 +1998,8 @@
1.103      shows "((\<lambda>n. 1 / (of_nat n powr s)) \<longlongrightarrow> 0) sequentially"
1.104  proof -
1.105    have "\<forall>n>0. 3 \<le> n \<longrightarrow> 1 \<le> ln (real_of_nat n)"
1.106 -    using ln3_gt_1
1.107 -    by (force intro: order_trans [of _ "ln 3"] ln3_gt_1)
1.108 +    using ln_272_gt_1
1.109 +    by (force intro: order_trans [of _ "ln (272/100)"])
1.110    moreover have "(\<lambda>n. cmod (Ln (of_nat n) / of_nat n powr s)) \<longlonglongrightarrow> 0"
1.111      using lim_Ln_over_power [OF assms]
1.112      by (metis tendsto_norm_zero_iff)
1.113 @@ -2018,6 +2051,42 @@
1.114    apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide)
1.115    done
1.116
1.117 +lemma lim_ln1_over_ln: "(\<lambda>n. ln(Suc n) / ln n) \<longlonglongrightarrow> 1"
1.118 +proof (rule Lim_transform_eventually)
1.119 +  have "(\<lambda>n. ln(1 + 1/n) / ln n) \<longlonglongrightarrow> 0"
1.120 +  proof (rule Lim_transform_bound)
1.121 +    show "(inverse o real) \<longlonglongrightarrow> 0"
1.122 +      by (metis comp_def seq_harmonic tendsto_explicit)
1.123 +    show "\<forall>\<^sub>F n in sequentially. norm (ln (1 + 1 / n) / ln n) \<le> norm ((inverse \<circ> real) n)"
1.124 +    proof
1.125 +      fix n::nat
1.126 +      assume n: "3 \<le> n"
1.127 +      then have "ln 3 \<le> ln n" and ln0: "0 \<le> ln n"
1.128 +        by auto
1.129 +      with ln3_gt_1 have "1/ ln n \<le> 1"
1.130 +        by (simp add: divide_simps)
1.131 +      moreover have "ln (1 + 1 / real n) \<le> 1/n"
1.133 +      ultimately have "ln (1 + 1 / real n) * (1 / ln n) \<le> (1/n) * 1"
1.134 +        by (intro mult_mono) (use n in auto)
1.135 +      then show "norm (ln (1 + 1 / n) / ln n) \<le> norm ((inverse \<circ> real) n)"
1.136 +        by (simp add: field_simps ln0)
1.137 +      qed
1.138 +  qed
1.139 +  then show "(\<lambda>n. 1 + ln(1 + 1/n) / ln n) \<longlonglongrightarrow> 1"
1.141 +  show "\<forall>\<^sub>F k in sequentially. 1 + ln (1 + 1 / k) / ln k = ln(Suc k) / ln k"
1.142 +    by (simp add: divide_simps ln_div eventually_sequentiallyI [of 2])
1.143 +qed
1.144 +
1.145 +lemma lim_ln_over_ln1: "(\<lambda>n. ln n / ln(Suc n)) \<longlonglongrightarrow> 1"
1.146 +proof -
1.147 +  have "(\<lambda>n. inverse (ln(Suc n) / ln n)) \<longlonglongrightarrow> inverse 1"
1.148 +    by (rule tendsto_inverse [OF lim_ln1_over_ln]) auto
1.149 +  then show ?thesis
1.150 +    by simp
1.151 +qed
1.152 +
1.153
1.154  subsection\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
1.155
```