author paulson Thu, 04 May 2017 15:14:49 +0100 changeset 65719 7c57d79d61b7 parent 65711 ff8a7f20ff32 child 65720 c5b19f997214
A few more new lemmas
```--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu May 04 11:34:42 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu May 04 15:14:49 2017 +0100
@@ -709,14 +709,16 @@
apply (simp only: pos_le_divide_eq [symmetric], linarith)
done

-text\<open>An odd contrast with the much more easily proved @{thm exp_le}\<close>
-lemma e_less_3: "exp 1 < (3::real)"
+lemma e_less_272: "exp 1 < (272/100::real)"
using e_approx_32
by (simp add: abs_if split: if_split_asm)

+lemma ln_272_gt_1: "ln (272/100) > (1::real)"
+  by (metis e_less_272 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
+
+text\<open>Apparently redundant. But many arguments involve integers.\<close>
lemma ln3_gt_1: "ln 3 > (1::real)"
-  by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
-
+  by (simp add: less_trans [OF ln_272_gt_1])

subsection\<open>The argument of a complex number\<close>

@@ -1071,6 +1073,9 @@
lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
using Ln_of_real by force

+lemma Ln_Reals_eq: "\<lbrakk>x \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> ln x = of_real (ln (Re x))"
+  using Ln_of_real by force
+
lemma Ln_1 [simp]: "ln 1 = (0::complex)"
proof -
have "ln (exp 0) = (0::complex)"
@@ -1185,6 +1190,28 @@
lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"

+lemma divide_ln_mono:
+  fixes x y::real
+  assumes "3 \<le> x" "x \<le> y"
+  shows "x / ln x \<le> y / ln y"
+proof (rule exE [OF complex_mvt_line [of x y "\<lambda>z. z / Ln z" "\<lambda>z. 1/(Ln z) - 1/(Ln z)^2"]];
+    clarsimp simp add: closed_segment_Reals closed_segment_eq_real_ivl assms)
+  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)"
+    using \<open>3 \<le> x\<close> apply -
+    apply (rule derivative_eq_intros | simp)+
+    apply (force simp: field_simps power_eq_if)
+    done
+  show "x / ln x \<le> y / ln y"
+    if "Re (y / Ln y) - Re (x / Ln x) = (Re (1 / Ln u) - Re (1 / (Ln u)\<^sup>2)) * (y - x)"
+    and x: "x \<le> u" "u \<le> y" for u
+  proof -
+    have eq: "y / ln y = (1 / ln u - 1 / (ln u)\<^sup>2) * (y - x) + x / ln x"
+      using that \<open>3 \<le> x\<close> by (auto simp: Ln_Reals_eq in_Reals_norm group_add_class.diff_eq_eq)
+    show ?thesis
+      using exp_le \<open>3 \<le> x\<close> x by (simp add: eq) (simp add: power_eq_if divide_simps ln_ge_iff)
+  qed
+qed
+

@@ -1717,6 +1744,9 @@
shows "0 \<le> x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"

+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)"
+  by (metis linear not_le of_real_Re powr_of_real)
+
lemma norm_powr_real_mono:
"\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
\<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
@@ -1727,6 +1757,15 @@
\<Longrightarrow> (x * y) powr z = x powr z * y powr z"
by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)

+lemma Re_powr_le: "r \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> Re (r powr z) \<le> Re r powr Re z"
+  by (auto simp: powr_def nonneg_Reals_def order_trans [OF complex_Re_le_cmod])
+
+lemma
+  fixes w::complex
+  shows Reals_powr [simp]: "\<lbrakk>w \<in> \<real>\<^sub>\<ge>\<^sub>0; z \<in> \<real>\<rbrakk> \<Longrightarrow> w powr z \<in> \<real>"
+  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"
+  by (auto simp: nonneg_Reals_def Reals_def powr_of_real)
+
lemma powr_neg_real_complex:
shows   "(- of_real x) powr a = (-1) powr (of_real (sgn x) * a) * of_real x powr (a :: complex)"
proof (cases "x = 0")
@@ -1938,12 +1977,6 @@
lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
using lim_Ln_over_power [of 1] by simp

-lemma Ln_Reals_eq: "\<lbrakk>x \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> Ln x = of_real (ln (Re x))"
-  using Ln_of_real by force
-
-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)"
-  by (metis linear not_le of_real_Re powr_of_real)
-
lemma lim_ln_over_power:
fixes s :: real
assumes "0 < s"
@@ -1965,8 +1998,8 @@
shows "((\<lambda>n. 1 / (of_nat n powr s)) \<longlongrightarrow> 0) sequentially"
proof -
have "\<forall>n>0. 3 \<le> n \<longrightarrow> 1 \<le> ln (real_of_nat n)"
-    using ln3_gt_1
-    by (force intro: order_trans [of _ "ln 3"] ln3_gt_1)
+    using ln_272_gt_1
+    by (force intro: order_trans [of _ "ln (272/100)"])
moreover have "(\<lambda>n. cmod (Ln (of_nat n) / of_nat n powr s)) \<longlonglongrightarrow> 0"
using lim_Ln_over_power [OF assms]
by (metis tendsto_norm_zero_iff)
@@ -2018,6 +2051,42 @@
apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide)
done

+lemma lim_ln1_over_ln: "(\<lambda>n. ln(Suc n) / ln n) \<longlonglongrightarrow> 1"
+proof (rule Lim_transform_eventually)
+  have "(\<lambda>n. ln(1 + 1/n) / ln n) \<longlonglongrightarrow> 0"
+  proof (rule Lim_transform_bound)
+    show "(inverse o real) \<longlonglongrightarrow> 0"
+      by (metis comp_def seq_harmonic tendsto_explicit)
+    show "\<forall>\<^sub>F n in sequentially. norm (ln (1 + 1 / n) / ln n) \<le> norm ((inverse \<circ> real) n)"
+    proof
+      fix n::nat
+      assume n: "3 \<le> n"
+      then have "ln 3 \<le> ln n" and ln0: "0 \<le> ln n"
+        by auto
+      with ln3_gt_1 have "1/ ln n \<le> 1"
+      moreover have "ln (1 + 1 / real n) \<le> 1/n"
+      ultimately have "ln (1 + 1 / real n) * (1 / ln n) \<le> (1/n) * 1"
+        by (intro mult_mono) (use n in auto)
+      then show "norm (ln (1 + 1 / n) / ln n) \<le> norm ((inverse \<circ> real) n)"
+        by (simp add: field_simps ln0)
+      qed
+  qed
+  then show "(\<lambda>n. 1 + ln(1 + 1/n) / ln n) \<longlonglongrightarrow> 1"
+  show "\<forall>\<^sub>F k in sequentially. 1 + ln (1 + 1 / k) / ln k = ln(Suc k) / ln k"
+    by (simp add: divide_simps ln_div eventually_sequentiallyI [of 2])
+qed
+
+lemma lim_ln_over_ln1: "(\<lambda>n. ln n / ln(Suc n)) \<longlonglongrightarrow> 1"
+proof -
+  have "(\<lambda>n. inverse (ln(Suc n) / ln n)) \<longlonglongrightarrow> inverse 1"
+    by (rule tendsto_inverse [OF lim_ln1_over_ln]) auto
+  then show ?thesis
+    by simp
+qed
+

subsection\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
```
```--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu May 04 11:34:42 2017 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu May 04 15:14:49 2017 +0100
@@ -7273,6 +7273,28 @@
"open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
by (simp add: open_segment_def closed_segment_translation translation_diff)

+lemma closed_segment_of_real:
+    "closed_segment (of_real x) (of_real y) = of_real ` closed_segment x y"
+  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
+    apply (rule_tac x="(1-u)*x + u*y" in bexI)
+  apply (auto simp: in_segment)
+  done
+
+lemma open_segment_of_real:
+    "open_segment (of_real x) (of_real y) = of_real ` open_segment x y"
+  apply (auto simp: image_iff in_segment scaleR_conv_of_real)
+    apply (rule_tac x="(1-u)*x + u*y" in bexI)
+  apply (auto simp: in_segment)
+  done
+
+lemma closed_segment_Reals:
+    "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> closed_segment x y = of_real ` closed_segment (Re x) (Re y)"
+  by (metis closed_segment_of_real of_real_Re)
+
+lemma open_segment_Reals:
+    "\<lbrakk>x \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> open_segment x y = of_real ` open_segment (Re x) (Re y)"
+  by (metis open_segment_of_real of_real_Re)
+
lemma open_segment_PairD:
"(x, x') \<in> open_segment (a, a') (b, b')
\<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"```