A few more new lemmas
authorpaulson <lp15@cam.ac.uk>
Thu May 04 15:14:49 2017 +0100 (2017-05-04)
changeset 657197c57d79d61b7
parent 65711 ff8a7f20ff32
child 65720 c5b19f997214
A few more new lemmas
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
     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  
     2.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu May 04 11:34:42 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu May 04 15:14:49 2017 +0100
     2.3 @@ -7273,6 +7273,28 @@
     2.4      "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
     2.5  by (simp add: open_segment_def closed_segment_translation translation_diff)
     2.6  
     2.7 +lemma closed_segment_of_real:
     2.8 +    "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y"
     2.9 +  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
    2.10 +    apply (rule_tac x="(1-u)*x + u*y" in bexI)
    2.11 +  apply (auto simp: in_segment)
    2.12 +  done
    2.13 +
    2.14 +lemma open_segment_of_real:
    2.15 +    "open_segment (of_real x) (of_real y) = of_real ` open_segment x y"
    2.16 +  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
    2.17 +    apply (rule_tac x="(1-u)*x + u*y" in bexI)
    2.18 +  apply (auto simp: in_segment)
    2.19 +  done
    2.20 +
    2.21 +lemma closed_segment_Reals:
    2.22 +    "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)"
    2.23 +  by (metis closed_segment_of_real of_real_Re)
    2.24 +
    2.25 +lemma open_segment_Reals:
    2.26 +    "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)"
    2.27 +  by (metis open_segment_of_real of_real_Re)
    2.28 +
    2.29  lemma open_segment_PairD:
    2.30      "(x, x') \<in> open_segment (a, a') (b, b')
    2.31       \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"