# HG changeset patch
# User hoelzl
# Date 1458557685 -3600
# Node ID 092cb9c96c99a9b9f4bd7eb61b32192d9f155b2a
# Parent  843ff6f1de384f97d33faf325b7c12360250fc6b
add le_log_of_power and le_log2_of_power by Tobias Nipkow

diff -r 843ff6f1de38 -r 092cb9c96c99 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sat Mar 19 16:53:09 2016 +0100
+++ b/src/HOL/Transcendental.thy	Mon Mar 21 11:54:45 2016 +0100
@@ -12,7 +12,7 @@
 
 text \<open>A fact theorem on reals.\<close>
 
-lemma square_fact_le_2_fact: 
+lemma square_fact_le_2_fact:
   shows "fact n * fact n \<le> (fact (2 * n) :: real)"
 proof (induct n)
   case 0 then show ?case by simp
@@ -2377,8 +2377,8 @@
   and less_powr_iff = log_less_iff[symmetric]
   and le_powr_iff = log_le_iff[symmetric]
 
-lemma
-  floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
+lemma floor_log_eq_powr_iff:
+  "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
   by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
 
 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
@@ -2387,10 +2387,10 @@
 lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   by (metis of_nat_numeral powr_realpow)
 
-lemma powr_real_of_int: 
+lemma powr_real_of_int:
   "x > 0 \<Longrightarrow> x powr real_of_int n = (if n \<ge> 0 then x ^ nat n else inverse (x ^ nat (-n)))"
   using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
-  by (auto simp: field_simps powr_minus)  
+  by (auto simp: field_simps powr_minus)
 
 lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
 by(simp add: powr_numeral)
@@ -2455,6 +2455,18 @@
 lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
   by (simp add: log_powr powr_realpow [symmetric])
 
+lemma le_log_of_power: assumes "1 < b" "b ^ n \<le> m" shows "n \<le> log b m"
+proof -
+   from assms have "0 < m"
+     by (metis less_trans zero_less_power less_le_trans zero_less_one)
+   have "n = log b (b ^ n)" using assms(1) by (simp add: log_nat_power)
+   also have "\<dots> \<le> log b m" using assms `0 < m` by simp
+   finally show ?thesis .
+qed
+
+lemma le_log2_of_power: "2 ^ n \<le> (m::nat) \<Longrightarrow> n \<le> log 2 m"
+  using le_log_of_power[of 2] by simp
+
 lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
   by (simp add: log_def)
 
@@ -2517,9 +2529,9 @@
   by (simp add: powr_def root_powr_inverse sqrt_def)
 
 lemma ln_powr_bound:
-  fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
-by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute mult_imp_le_div_pos not_less powr_gt_zero)
-
+  fixes x::real shows "1 \<le> x \<Longrightarrow> 0 < a \<Longrightarrow> ln x \<le> (x powr a) / a"
+  by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute
+            mult_imp_le_div_pos not_less powr_gt_zero)
 
 lemma ln_powr_bound2:
   fixes x::real
@@ -3615,13 +3627,13 @@
     by (auto simp: algebra_simps cos_diff assms)
   then have "\<exists>!x. 0 \<le> x \<and> x \<le> pi \<and> cos x = 0"
     by (auto simp: intro!: cos_total)
-  then obtain \<theta> where \<theta>: "0 \<le> \<theta>" "\<theta> \<le> pi" "cos \<theta> = 0" 
+  then obtain \<theta> where \<theta>: "0 \<le> \<theta>" "\<theta> \<le> pi" "cos \<theta> = 0"
                   and uniq: "\<And>\<phi>. \<lbrakk>0 \<le> \<phi>; \<phi> \<le> pi; cos \<phi> = 0\<rbrakk> \<Longrightarrow> \<phi> = \<theta>"
     by blast
   then have "x - real n * pi = \<theta>"
     using x by blast
   moreover have "pi/2 = \<theta>"
-    using pi_half_ge_zero uniq by fastforce 
+    using pi_half_ge_zero uniq by fastforce
   ultimately show ?thesis
     by (rule_tac x = "Suc (2 * n)" in exI) (simp add: algebra_simps)
 qed
@@ -3650,7 +3662,7 @@
     assume "cos x = 0" then show ?rhs
       using cos_zero_lemma [of x] cos_zero_lemma [of "-x"] by force
   next
-    assume ?rhs then show "cos x = 0" 
+    assume ?rhs then show "cos x = 0"
     by (auto dest: * simp del: eq_divide_eq_numeral1)
   qed
 qed
@@ -3663,7 +3675,7 @@
   assume "sin x = 0" then show ?rhs
     using sin_zero_lemma [of x] sin_zero_lemma [of "-x"] by force
 next
-  assume ?rhs then show "sin x = 0" 
+  assume ?rhs then show "sin x = 0"
     by (auto elim: evenE)
 qed
 
@@ -3690,7 +3702,7 @@
 proof safe
   assume "sin x = 0"
   then show "\<exists>n. even n \<and> x = of_int n * (pi / 2)"
-    apply (simp add: sin_zero_iff, safe)    
+    apply (simp add: sin_zero_iff, safe)
     apply (metis even_int_iff of_int_of_nat_eq)
     apply (rule_tac x="- (int n)" in exI, simp)
     done
@@ -4233,7 +4245,7 @@
   case True
   hence i_nat: "of_int i = of_int (nat i)" by auto
   show ?thesis unfolding i_nat
-    by (metis of_int_of_nat_eq tan_periodic_nat) 
+    by (metis of_int_of_nat_eq tan_periodic_nat)
 next
   case False
   hence i_nat: "of_int i = - of_int (nat (-i))" by auto
@@ -4241,7 +4253,7 @@
     by auto
   also have "\<dots> = tan (x + of_int i * pi)"
     unfolding i_nat mult_minus_left diff_minus_eq_add
-    by (metis of_int_of_nat_eq tan_periodic_nat)    
+    by (metis of_int_of_nat_eq tan_periodic_nat)
   finally show ?thesis by auto
 qed
 
@@ -4950,7 +4962,7 @@
 lemma machin_Euler: "5 * arctan(1/7) + 2 * arctan(3/79) = pi/4"
 proof -
   have 17: "\<bar>1/7\<bar> < (1 :: real)" by auto
-  with arctan_double have "2 * arctan (1/7) = arctan (7/24)" 
+  with arctan_double have "2 * arctan (1/7) = arctan (7/24)"
     by simp (simp add: field_simps)
   moreover have "\<bar>7/24\<bar> < (1 :: real)" by auto
   with arctan_double have "2 * arctan (7/24) = arctan (336/527)"  by simp (simp add: field_simps)