added lemmas
authornipkow
Tue May 13 22:14:12 2014 +0200 (2014-05-13)
changeset 56952efa2a83d548b
parent 56951 4fca7e1470e2
child 56953 e503d80f7f35
child 56958 b2c2f74d1c93
added lemmas
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Transcendental.thy	Tue May 13 16:18:16 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Tue May 13 22:14:12 2014 +0200
     1.3 @@ -1963,6 +1963,12 @@
     1.4  lemma ln_powr: "ln (x powr y) = y * ln x"
     1.5    by (simp add: powr_def)
     1.6  
     1.7 +lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
     1.8 +by(simp add: root_powr_inverse ln_powr)
     1.9 +
    1.10 +lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
    1.11 +by(simp add: log_def ln_root)
    1.12 +
    1.13  lemma log_powr: "log b (x powr y) = y * log b x"
    1.14    by (simp add: log_def ln_powr)
    1.15  
    1.16 @@ -1978,6 +1984,9 @@
    1.17  lemma log_base_powr: "log (a powr b) x = log a x / b"
    1.18    by (simp add: log_def ln_powr)
    1.19  
    1.20 +lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
    1.21 +by(simp add: log_def ln_root)
    1.22 +
    1.23  lemma ln_bound: "1 <= x ==> ln x <= x"
    1.24    apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
    1.25    apply simp