27468
|
1 |
(* Title : HLog.thy
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 2000,2001 University of Edinburgh
|
|
4 |
*)
|
|
5 |
|
|
6 |
header{*Logarithms: Non-Standard Version*}
|
|
7 |
|
|
8 |
theory HLog
|
|
9 |
imports Log HTranscendental
|
|
10 |
begin
|
|
11 |
|
|
12 |
|
|
13 |
(* should be in NSA.ML *)
|
|
14 |
lemma epsilon_ge_zero [simp]: "0 \<le> epsilon"
|
|
15 |
by (simp add: epsilon_def star_n_zero_num star_n_le)
|
|
16 |
|
|
17 |
lemma hpfinite_witness: "epsilon : {x. 0 \<le> x & x : HFinite}"
|
|
18 |
by auto
|
|
19 |
|
|
20 |
|
|
21 |
definition
|
|
22 |
powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) where
|
37765
|
23 |
[transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
|
27468
|
24 |
|
|
25 |
definition
|
|
26 |
hlog :: "[hypreal,hypreal] => hypreal" where
|
37765
|
27 |
[transfer_unfold]: "hlog a x = starfun2 log a x"
|
27468
|
28 |
|
|
29 |
lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
|
|
30 |
by (simp add: powhr_def starfun2_star_n)
|
|
31 |
|
|
32 |
lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
|
|
33 |
by (transfer, simp)
|
|
34 |
|
|
35 |
lemma powhr_mult:
|
|
36 |
"!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
|
|
37 |
by (transfer, rule powr_mult)
|
|
38 |
|
|
39 |
lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a"
|
|
40 |
by (transfer, simp)
|
|
41 |
|
|
42 |
lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0"
|
|
43 |
by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym])
|
|
44 |
|
|
45 |
lemma powhr_divide:
|
|
46 |
"!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
|
|
47 |
by (transfer, rule powr_divide)
|
|
48 |
|
|
49 |
lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
|
|
50 |
by (transfer, rule powr_add)
|
|
51 |
|
|
52 |
lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
|
|
53 |
by (transfer, rule powr_powr)
|
|
54 |
|
|
55 |
lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
|
|
56 |
by (transfer, rule powr_powr_swap)
|
|
57 |
|
|
58 |
lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
|
|
59 |
by (transfer, rule powr_minus)
|
|
60 |
|
|
61 |
lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
|
|
62 |
by (simp add: divide_inverse powhr_minus)
|
|
63 |
|
|
64 |
lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
|
|
65 |
by (transfer, simp)
|
|
66 |
|
|
67 |
lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
|
|
68 |
by (transfer, simp)
|
|
69 |
|
|
70 |
lemma powhr_less_cancel_iff [simp]:
|
|
71 |
"1 < x ==> (x powhr a < x powhr b) = (a < b)"
|
|
72 |
by (blast intro: powhr_less_cancel powhr_less_mono)
|
|
73 |
|
|
74 |
lemma powhr_le_cancel_iff [simp]:
|
|
75 |
"1 < x ==> (x powhr a \<le> x powhr b) = (a \<le> b)"
|
|
76 |
by (simp add: linorder_not_less [symmetric])
|
|
77 |
|
|
78 |
lemma hlog:
|
|
79 |
"hlog (star_n X) (star_n Y) =
|
|
80 |
star_n (%n. log (X n) (Y n))"
|
|
81 |
by (simp add: hlog_def starfun2_star_n)
|
|
82 |
|
|
83 |
lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
|
|
84 |
by (transfer, rule log_ln)
|
|
85 |
|
|
86 |
lemma powhr_hlog_cancel [simp]:
|
|
87 |
"!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
|
|
88 |
by (transfer, simp)
|
|
89 |
|
|
90 |
lemma hlog_powhr_cancel [simp]:
|
|
91 |
"!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
|
|
92 |
by (transfer, simp)
|
|
93 |
|
|
94 |
lemma hlog_mult:
|
|
95 |
"!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]
|
|
96 |
==> hlog a (x * y) = hlog a x + hlog a y"
|
|
97 |
by (transfer, rule log_mult)
|
|
98 |
|
|
99 |
lemma hlog_as_starfun:
|
|
100 |
"!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
|
|
101 |
by (transfer, simp add: log_def)
|
|
102 |
|
|
103 |
lemma hlog_eq_div_starfun_ln_mult_hlog:
|
|
104 |
"!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
|
|
105 |
==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
|
|
106 |
by (transfer, rule log_eq_div_ln_mult_log)
|
|
107 |
|
|
108 |
lemma powhr_as_starfun: "!!a x. x powhr a = ( *f* exp) (a * ( *f* ln) x)"
|
|
109 |
by (transfer, simp add: powr_def)
|
|
110 |
|
|
111 |
lemma HInfinite_powhr:
|
|
112 |
"[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;
|
|
113 |
0 < a |] ==> x powhr a : HInfinite"
|
|
114 |
apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite
|
|
115 |
simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
|
|
116 |
done
|
|
117 |
|
|
118 |
lemma hlog_hrabs_HInfinite_Infinitesimal:
|
|
119 |
"[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]
|
|
120 |
==> hlog a (abs x) : Infinitesimal"
|
|
121 |
apply (frule HInfinite_gt_zero_gt_one)
|
|
122 |
apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
|
|
123 |
HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
|
|
124 |
simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
|
|
125 |
hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse)
|
|
126 |
done
|
|
127 |
|
|
128 |
lemma hlog_HInfinite_as_starfun:
|
|
129 |
"[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
|
|
130 |
by (rule hlog_as_starfun, auto)
|
|
131 |
|
|
132 |
lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
|
|
133 |
by (transfer, simp)
|
|
134 |
|
|
135 |
lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
|
|
136 |
by (transfer, rule log_eq_one)
|
|
137 |
|
|
138 |
lemma hlog_inverse:
|
|
139 |
"[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
|
|
140 |
apply (rule add_left_cancel [of "hlog a x", THEN iffD1])
|
|
141 |
apply (simp add: hlog_mult [symmetric])
|
|
142 |
done
|
|
143 |
|
|
144 |
lemma hlog_divide:
|
|
145 |
"[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
|
|
146 |
by (simp add: hlog_mult hlog_inverse divide_inverse)
|
|
147 |
|
|
148 |
lemma hlog_less_cancel_iff [simp]:
|
|
149 |
"!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
|
|
150 |
by (transfer, simp)
|
|
151 |
|
|
152 |
lemma hlog_le_cancel_iff [simp]:
|
|
153 |
"[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
|
|
154 |
by (simp add: linorder_not_less [symmetric])
|
|
155 |
|
|
156 |
end
|