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.61  subsection\<open>Quadrant-type results for Ln\<close>
    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.132 +        by (simp add: ln_add_one_self_le_self)
   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.140 +    by (metis (full_types) add.right_neutral tendsto_add_const_iff)
   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