author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 47595  836b4c4d7c86 
child 50247  491c5c81c2e8 
permissions  rwrr 
12224  1 
(* Title : Log.thy 
2 
Author : Jacques D. Fleuriot 

16819  3 
Additional contributions by Jeremy Avigad 
12224  4 
Copyright : 2000,2001 University of Edinburgh 
5 
*) 

6 

14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

7 
header{*Logarithms: Standard Version*} 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

8 

15131  9 
theory Log 
15140  10 
imports Transcendental 
15131  11 
begin 
12224  12 

19765  13 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

14 
powr :: "[real,real] => real" (infixr "powr" 80) where 
14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

15 
{*exponentation with real exponent*} 
19765  16 
"x powr a = exp(a * ln x)" 
12224  17 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

18 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19765
diff
changeset

19 
log :: "[real,real] => real" where 
15053  20 
{*logarithm of @{term x} to base @{term a}*} 
19765  21 
"log a x = ln x / ln a" 
12224  22 

14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

23 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

24 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

25 
lemma powr_one_eq_one [simp]: "1 powr a = 1" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

26 
by (simp add: powr_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

27 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

28 
lemma powr_zero_eq_one [simp]: "x powr 0 = 1" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

29 
by (simp add: powr_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

30 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

31 
lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

32 
by (simp add: powr_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

33 
declare powr_one_gt_zero_iff [THEN iffD2, simp] 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

34 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

35 
lemma powr_mult: 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

36 
"[ 0 < x; 0 < y ] ==> (x * y) powr a = (x powr a) * (y powr a)" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47595
diff
changeset

37 
by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left) 
14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

38 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

39 
lemma powr_gt_zero [simp]: "0 < x powr a" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

40 
by (simp add: powr_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

41 

16819  42 
lemma powr_ge_pzero [simp]: "0 <= x powr y" 
43 
by (rule order_less_imp_le, rule powr_gt_zero) 

44 

14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

45 
lemma powr_not_zero [simp]: "x powr a \<noteq> 0" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

46 
by (simp add: powr_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

47 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

48 
lemma powr_divide: 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

49 
"[ 0 < x; 0 < y ] ==> (x / y) powr a = (x powr a)/(y powr a)" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14411
diff
changeset

50 
apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult) 
14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

51 
apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

52 
done 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

53 

16819  54 
lemma powr_divide2: "x powr a / x powr b = x powr (a  b)" 
55 
apply (simp add: powr_def) 

56 
apply (subst exp_diff [THEN sym]) 

57 
apply (simp add: left_diff_distrib) 

58 
done 

59 

14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

60 
lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47595
diff
changeset

61 
by (simp add: powr_def exp_add [symmetric] distrib_right) 
14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

62 

45930  63 
lemma powr_mult_base: 
64 
"0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)" 

65 
using assms by (auto simp: powr_add) 

66 

14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

67 
lemma powr_powr: "(x powr a) powr b = x powr (a * b)" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

68 
by (simp add: powr_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

69 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

70 
lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a" 
36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
36622
diff
changeset

71 
by (simp add: powr_powr mult_commute) 
14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

72 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

73 
lemma powr_minus: "x powr (a) = inverse (x powr a)" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

74 
by (simp add: powr_def exp_minus [symmetric]) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

75 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

76 
lemma powr_minus_divide: "x powr (a) = 1/(x powr a)" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14411
diff
changeset

77 
by (simp add: divide_inverse powr_minus) 
14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

78 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

79 
lemma powr_less_mono: "[ a < b; 1 < x ] ==> x powr a < x powr b" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

80 
by (simp add: powr_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

81 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

82 
lemma powr_less_cancel: "[ x powr a < x powr b; 1 < x ] ==> a < b" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

83 
by (simp add: powr_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

84 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

85 
lemma powr_less_cancel_iff [simp]: "1 < x ==> (x powr a < x powr b) = (a < b)" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

86 
by (blast intro: powr_less_cancel powr_less_mono) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

87 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

88 
lemma powr_le_cancel_iff [simp]: "1 < x ==> (x powr a \<le> x powr b) = (a \<le> b)" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

89 
by (simp add: linorder_not_less [symmetric]) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

90 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

91 
lemma log_ln: "ln x = log (exp(1)) x" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

92 
by (simp add: log_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

93 

45916  94 
lemma DERIV_log: assumes "x > 0" shows "DERIV (\<lambda>y. log b y) x :> 1 / (ln b * x)" 
95 
proof  

96 
def lb \<equiv> "1 / ln b" 

97 
moreover have "DERIV (\<lambda>y. lb * ln y) x :> lb / x" 

98 
using `x > 0` by (auto intro!: DERIV_intros) 

99 
ultimately show ?thesis 

100 
by (simp add: log_def) 

101 
qed 

102 

103 
lemmas DERIV_log[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] 

33716  104 

14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

105 
lemma powr_log_cancel [simp]: 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

106 
"[ 0 < a; a \<noteq> 1; 0 < x ] ==> a powr (log a x) = x" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

107 
by (simp add: powr_def log_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

108 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

109 
lemma log_powr_cancel [simp]: "[ 0 < a; a \<noteq> 1 ] ==> log a (a powr y) = y" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

110 
by (simp add: log_def powr_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

111 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

112 
lemma log_mult: 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

113 
"[ 0 < a; a \<noteq> 1; 0 < x; 0 < y ] 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

114 
==> log a (x * y) = log a x + log a y" 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47595
diff
changeset

115 
by (simp add: log_def ln_mult divide_inverse distrib_right) 
14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

116 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

117 
lemma log_eq_div_ln_mult_log: 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

118 
"[ 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x ] 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

119 
==> log a x = (ln b/ln a) * log b x" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14411
diff
changeset

120 
by (simp add: log_def divide_inverse) 
14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

121 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

122 
text{*Base 10 logarithms*} 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

123 
lemma log_base_10_eq1: "0 < x ==> log 10 x = (ln (exp 1) / ln 10) * ln x" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

124 
by (simp add: log_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

125 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

126 
lemma log_base_10_eq2: "0 < x ==> log 10 x = (log 10 (exp 1)) * ln x" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

127 
by (simp add: log_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

128 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

129 
lemma log_one [simp]: "log a 1 = 0" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

130 
by (simp add: log_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

131 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

132 
lemma log_eq_one [simp]: "[ 0 < a; a \<noteq> 1 ] ==> log a a = 1" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

133 
by (simp add: log_def) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

134 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

135 
lemma log_inverse: 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

136 
"[ 0 < a; a \<noteq> 1; 0 < x ] ==> log a (inverse x) =  log a x" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

137 
apply (rule_tac a1 = "log a x" in add_left_cancel [THEN iffD1]) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

138 
apply (simp add: log_mult [symmetric]) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

139 
done 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

140 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

141 
lemma log_divide: 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

142 
"[0 < a; a \<noteq> 1; 0 < x; 0 < y] ==> log a (x/y) = log a x  log a y" 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14411
diff
changeset

143 
by (simp add: log_mult divide_inverse log_inverse) 
14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

144 

7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

145 
lemma log_less_cancel_iff [simp]: 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

146 
"[ 1 < a; 0 < x; 0 < y ] ==> (log a x < log a y) = (x < y)" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

147 
apply safe 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

148 
apply (rule_tac [2] powr_less_cancel) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

149 
apply (drule_tac a = "log a x" in powr_less_mono, auto) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

150 
done 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

151 

36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

152 
lemma log_inj: assumes "1 < b" shows "inj_on (log b) {0 <..}" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

153 
proof (rule inj_onI, simp) 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

154 
fix x y assume pos: "0 < x" "0 < y" and *: "log b x = log b y" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

155 
show "x = y" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

156 
proof (cases rule: linorder_cases) 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

157 
assume "x < y" hence "log b x < log b y" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

158 
using log_less_cancel_iff[OF `1 < b`] pos by simp 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

159 
thus ?thesis using * by simp 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

160 
next 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

161 
assume "y < x" hence "log b y < log b x" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

162 
using log_less_cancel_iff[OF `1 < b`] pos by simp 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

163 
thus ?thesis using * by simp 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

164 
qed simp 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

165 
qed 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
33716
diff
changeset

166 

14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

167 
lemma log_le_cancel_iff [simp]: 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

168 
"[ 1 < a; 0 < x; 0 < y ] ==> (log a x \<le> log a y) = (x \<le> y)" 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

169 
by (simp add: linorder_not_less [symmetric]) 
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

170 

47593  171 
lemma zero_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < log a x \<longleftrightarrow> 1 < x" 
172 
using log_less_cancel_iff[of a 1 x] by simp 

173 

174 
lemma zero_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 \<le> log a x \<longleftrightarrow> 1 \<le> x" 

175 
using log_le_cancel_iff[of a 1 x] by simp 

176 

177 
lemma log_less_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 0 \<longleftrightarrow> x < 1" 

178 
using log_less_cancel_iff[of a x 1] by simp 

179 

180 
lemma log_le_zero_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 0 \<longleftrightarrow> x \<le> 1" 

181 
using log_le_cancel_iff[of a x 1] by simp 

182 

183 
lemma one_less_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 < log a x \<longleftrightarrow> a < x" 

184 
using log_less_cancel_iff[of a a x] by simp 

185 

186 
lemma one_le_log_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> log a x \<longleftrightarrow> a \<le> x" 

187 
using log_le_cancel_iff[of a a x] by simp 

188 

189 
lemma log_less_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x < 1 \<longleftrightarrow> x < a" 

190 
using log_less_cancel_iff[of a x a] by simp 

191 

192 
lemma log_le_one_cancel_iff[simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> log a x \<le> 1 \<longleftrightarrow> x \<le> a" 

193 
using log_le_cancel_iff[of a x a] by simp 

14411
7851e526b8b7
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
paulson
parents:
12224
diff
changeset

194 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

195 
lemma powr_realpow: "0 < x ==> x powr (real n) = x^n" 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

196 
apply (induct n, simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

197 
apply (subgoal_tac "real(Suc n) = real n + 1") 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

198 
apply (erule ssubst) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

199 
apply (subst powr_add, simp, simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

200 
done 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

201 

47594  202 
lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))" 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

203 
apply (case_tac "x = 0", simp, simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

204 
apply (rule powr_realpow [THEN sym], simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

205 
done 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

206 

47594  207 
lemma powr_int: 
208 
assumes "x > 0" 

209 
shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (i))" 

210 
proof cases 

211 
assume "i < 0" 

212 
have r: "x powr i = 1 / x powr (i)" by (simp add: powr_minus field_simps) 

213 
show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric]) 

214 
qed (simp add: assms powr_realpow[symmetric]) 

215 

216 
lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x^numeral n" 

217 
using powr_realpow[of x "numeral n"] by simp 

218 

219 
lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr neg_numeral n = 1 / x^numeral n" 

220 
using powr_int[of x "neg_numeral n"] by simp 

221 

45930  222 
lemma root_powr_inverse: 
223 
"0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)" 

224 
by (auto simp: root_def powr_realpow[symmetric] powr_powr) 

225 

33716  226 
lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x" 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

227 
by (unfold powr_def, simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

228 

33716  229 
lemma log_powr: "0 < x ==> 0 \<le> y ==> log b (x powr y) = y * log b x" 
230 
apply (case_tac "y = 0") 

231 
apply force 

232 
apply (auto simp add: log_def ln_powr field_simps) 

233 
done 

234 

235 
lemma log_nat_power: "0 < x ==> log b (x^n) = real n * log b x" 

236 
apply (subst powr_realpow [symmetric]) 

237 
apply (auto simp add: log_powr) 

238 
done 

239 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

240 
lemma ln_bound: "1 <= x ==> ln x <= x" 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

241 
apply (subgoal_tac "ln(1 + (x  1)) <= x  1") 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

242 
apply simp 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

243 
apply (rule ln_add_one_self_le_self, simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

244 
done 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

245 

5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

246 
lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b" 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

247 
apply (case_tac "x = 1", simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

248 
apply (case_tac "a = b", simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

249 
apply (rule order_less_imp_le) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

250 
apply (rule powr_less_mono, auto) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

251 
done 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

252 

5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

253 
lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a" 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

254 
apply (subst powr_zero_eq_one [THEN sym]) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

255 
apply (rule powr_mono, assumption+) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

256 
done 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

257 

5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

258 
lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

259 
y powr a" 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

260 
apply (unfold powr_def) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

261 
apply (rule exp_less_mono) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

262 
apply (rule mult_strict_left_mono) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

263 
apply (subst ln_less_cancel_iff, assumption) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

264 
apply (rule order_less_trans) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

265 
prefer 2 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

266 
apply assumption+ 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

267 
done 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

268 

16819  269 
lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < 
270 
x powr a" 

271 
apply (unfold powr_def) 

272 
apply (rule exp_less_mono) 

273 
apply (rule mult_strict_left_mono_neg) 

274 
apply (subst ln_less_cancel_iff) 

275 
apply assumption 

276 
apply (rule order_less_trans) 

277 
prefer 2 

278 
apply assumption+ 

279 
done 

280 

281 
lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a" 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

282 
apply (case_tac "a = 0", simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

283 
apply (case_tac "x = y", simp) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

284 
apply (rule order_less_imp_le) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

285 
apply (rule powr_less_mono2, auto) 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

286 
done 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

287 

47595  288 
lemma powr_inj: 
289 
"0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y" 

290 
unfolding powr_def exp_inj_iff by simp 

291 

16819  292 
lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a" 
293 
apply (rule mult_imp_le_div_pos) 

294 
apply (assumption) 

295 
apply (subst mult_commute) 

33716  296 
apply (subst ln_powr [THEN sym]) 
16819  297 
apply auto 
298 
apply (rule ln_bound) 

299 
apply (erule ge_one_powr_ge_zero) 

300 
apply (erule order_less_imp_le) 

301 
done 

302 

41550  303 
lemma ln_powr_bound2: 
304 
assumes "1 < x" and "0 < a" 

305 
shows "(ln x) powr a <= (a powr a) * x" 

16819  306 
proof  
41550  307 
from assms have "ln x <= (x powr (1 / a)) / (1 / a)" 
16819  308 
apply (intro ln_powr_bound) 
309 
apply (erule order_less_imp_le) 

310 
apply (rule divide_pos_pos) 

311 
apply simp_all 

312 
done 

313 
also have "... = a * (x powr (1 / a))" 

314 
by simp 

315 
finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a" 

316 
apply (intro powr_mono2) 

41550  317 
apply (rule order_less_imp_le, rule assms) 
16819  318 
apply (rule ln_gt_zero) 
41550  319 
apply (rule assms) 
16819  320 
apply assumption 
321 
done 

322 
also have "... = (a powr a) * ((x powr (1 / a)) powr a)" 

323 
apply (rule powr_mult) 

41550  324 
apply (rule assms) 
16819  325 
apply (rule powr_gt_zero) 
326 
done 

327 
also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)" 

328 
by (rule powr_powr) 

329 
also have "... = x" 

330 
apply simp 

331 
apply (subgoal_tac "a ~= 0") 

41550  332 
using assms apply auto 
16819  333 
done 
334 
finally show ?thesis . 

335 
qed 

336 

45915  337 
lemma tendsto_powr [tendsto_intros]: 
338 
"\<lbrakk>(f > a) F; (g > b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) > a powr b) F" 

339 
unfolding powr_def by (intro tendsto_intros) 

340 

45892  341 
(* FIXME: generalize by replacing d by with g x and g > d? *) 
342 
lemma tendsto_zero_powrI: 

343 
assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f > 0) F" 

344 
assumes "0 < d" 

345 
shows "((\<lambda>x. f x powr d) > 0) F" 

346 
proof (rule tendstoI) 

347 
fix e :: real assume "0 < e" 

348 
def Z \<equiv> "e powr (1 / d)" 

349 
with `0 < e` have "0 < Z" by simp 

350 
with assms have "eventually (\<lambda>x. 0 < f x \<and> dist (f x) 0 < Z) F" 

351 
by (intro eventually_conj tendstoD) 

352 
moreover 

353 
from assms have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> x powr d < Z powr d" 

354 
by (intro powr_less_mono2) (auto simp: dist_real_def) 

355 
with assms `0 < e` have "\<And>x. 0 < x \<and> dist x 0 < Z \<Longrightarrow> dist (x powr d) 0 < e" 

356 
unfolding dist_real_def Z_def by (auto simp: powr_powr) 

357 
ultimately 

358 
show "eventually (\<lambda>x. dist (f x powr d) 0 < e) F" by (rule eventually_elim1) 

359 
qed 

360 

361 
lemma tendsto_neg_powr: 

362 
assumes "s < 0" and "real_tendsto_inf f F" 

363 
shows "((\<lambda>x. f x powr s) > 0) F" 

364 
proof (rule tendstoI) 

365 
fix e :: real assume "0 < e" 

366 
def Z \<equiv> "e powr (1 / s)" 

367 
from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: real_tendsto_inf_def) 

368 
moreover 

369 
from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s" 

370 
by (auto simp: Z_def intro!: powr_less_mono2_neg) 

371 
with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e" 

372 
by (simp add: powr_powr Z_def dist_real_def) 

373 
ultimately 

374 
show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1) 

41550  375 
qed 
16819  376 

12224  377 
end 