24 "x powhr a == Ifun2_of (op powr) x a" |
24 "x powhr a == Ifun2_of (op powr) x a" |
25 |
25 |
26 hlog :: "[hypreal,hypreal] => hypreal" |
26 hlog :: "[hypreal,hypreal] => hypreal" |
27 "hlog a x == Ifun2_of log a x" |
27 "hlog a x == Ifun2_of log a x" |
28 |
28 |
|
29 declare powhr_def [transfer_unfold] |
|
30 declare hlog_def [transfer_unfold] |
29 |
31 |
30 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))" |
32 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))" |
31 by (simp add: powhr_def Ifun2_of_def star_of_def Ifun_star_n) |
33 by (simp add: powhr_def Ifun2_of_def star_of_def Ifun_star_n) |
32 |
34 |
33 lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1" |
35 lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1" |
34 by (unfold powhr_def, transfer, simp) |
36 by (transfer, simp) |
35 |
37 |
36 lemma powhr_mult: |
38 lemma powhr_mult: |
37 "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)" |
39 "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)" |
38 by (unfold powhr_def, transfer, rule powr_mult) |
40 by (transfer, rule powr_mult) |
39 |
41 |
40 lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a" |
42 lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a" |
41 by (unfold powhr_def, transfer, simp) |
43 by (transfer, simp) |
42 |
44 |
43 lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0" |
45 lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0" |
44 by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym]) |
46 by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym]) |
45 |
47 |
46 lemma powhr_divide: |
48 lemma powhr_divide: |
47 "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)" |
49 "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)" |
48 by (unfold powhr_def, transfer, rule powr_divide) |
50 by (transfer, rule powr_divide) |
49 |
51 |
50 lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)" |
52 lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)" |
51 by (unfold powhr_def, transfer, rule powr_add) |
53 by (transfer, rule powr_add) |
52 |
54 |
53 lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)" |
55 lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)" |
54 by (unfold powhr_def, transfer, rule powr_powr) |
56 by (transfer, rule powr_powr) |
55 |
57 |
56 lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a" |
58 lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a" |
57 by (unfold powhr_def, transfer, rule powr_powr_swap) |
59 by (transfer, rule powr_powr_swap) |
58 |
60 |
59 lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)" |
61 lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)" |
60 by (unfold powhr_def, transfer, rule powr_minus) |
62 by (transfer, rule powr_minus) |
61 |
63 |
62 lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)" |
64 lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)" |
63 by (simp add: divide_inverse powhr_minus) |
65 by (simp add: divide_inverse powhr_minus) |
64 |
66 |
65 lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b" |
67 lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b" |
66 by (unfold powhr_def, transfer, simp) |
68 by (transfer, simp) |
67 |
69 |
68 lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b" |
70 lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b" |
69 by (unfold powhr_def, transfer, simp) |
71 by (transfer, simp) |
70 |
72 |
71 lemma powhr_less_cancel_iff [simp]: |
73 lemma powhr_less_cancel_iff [simp]: |
72 "1 < x ==> (x powhr a < x powhr b) = (a < b)" |
74 "1 < x ==> (x powhr a < x powhr b) = (a < b)" |
73 by (blast intro: powhr_less_cancel powhr_less_mono) |
75 by (blast intro: powhr_less_cancel powhr_less_mono) |
74 |
76 |
80 "hlog (star_n X) (star_n Y) = |
82 "hlog (star_n X) (star_n Y) = |
81 star_n (%n. log (X n) (Y n))" |
83 star_n (%n. log (X n) (Y n))" |
82 by (simp add: hlog_def Ifun2_of_def star_of_def Ifun_star_n) |
84 by (simp add: hlog_def Ifun2_of_def star_of_def Ifun_star_n) |
83 |
85 |
84 lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x" |
86 lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x" |
85 by (unfold hlog_def, transfer, rule log_ln) |
87 by (transfer, rule log_ln) |
86 |
88 |
87 lemma powhr_hlog_cancel [simp]: |
89 lemma powhr_hlog_cancel [simp]: |
88 "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x" |
90 "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x" |
89 by (unfold powhr_def hlog_def, transfer, simp) |
91 by (transfer, simp) |
90 |
92 |
91 lemma hlog_powhr_cancel [simp]: |
93 lemma hlog_powhr_cancel [simp]: |
92 "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y" |
94 "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y" |
93 by (unfold powhr_def hlog_def, transfer, simp) |
95 by (transfer, simp) |
94 |
96 |
95 lemma hlog_mult: |
97 lemma hlog_mult: |
96 "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y |] |
98 "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y |] |
97 ==> hlog a (x * y) = hlog a x + hlog a y" |
99 ==> hlog a (x * y) = hlog a x + hlog a y" |
98 by (unfold powhr_def hlog_def, transfer, rule log_mult) |
100 by (transfer, rule log_mult) |
99 |
101 |
100 lemma hlog_as_starfun: |
102 lemma hlog_as_starfun: |
101 "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a" |
103 "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a" |
102 by (unfold hlog_def, transfer, simp add: log_def) |
104 by (transfer, simp add: log_def) |
103 |
105 |
104 lemma hlog_eq_div_starfun_ln_mult_hlog: |
106 lemma hlog_eq_div_starfun_ln_mult_hlog: |
105 "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |] |
107 "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |] |
106 ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x" |
108 ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x" |
107 by (unfold hlog_def, transfer, rule log_eq_div_ln_mult_log) |
109 by (transfer, rule log_eq_div_ln_mult_log) |
108 |
110 |
109 lemma powhr_as_starfun: "!!a x. x powhr a = ( *f* exp) (a * ( *f* ln) x)" |
111 lemma powhr_as_starfun: "!!a x. x powhr a = ( *f* exp) (a * ( *f* ln) x)" |
110 by (unfold powhr_def, transfer, simp add: powr_def) |
112 by (transfer, simp add: powr_def) |
111 |
113 |
112 lemma HInfinite_powhr: |
114 lemma HInfinite_powhr: |
113 "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal; |
115 "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal; |
114 0 < a |] ==> x powhr a : HInfinite" |
116 0 < a |] ==> x powhr a : HInfinite" |
115 apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite |
117 apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite |
129 lemma hlog_HInfinite_as_starfun: |
131 lemma hlog_HInfinite_as_starfun: |
130 "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a" |
132 "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a" |
131 by (rule hlog_as_starfun, auto) |
133 by (rule hlog_as_starfun, auto) |
132 |
134 |
133 lemma hlog_one [simp]: "!!a. hlog a 1 = 0" |
135 lemma hlog_one [simp]: "!!a. hlog a 1 = 0" |
134 by (unfold hlog_def, transfer, simp) |
136 by (transfer, simp) |
135 |
137 |
136 lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1" |
138 lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1" |
137 by (unfold hlog_def, transfer, rule log_eq_one) |
139 by (transfer, rule log_eq_one) |
138 |
140 |
139 lemma hlog_inverse: |
141 lemma hlog_inverse: |
140 "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x" |
142 "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x" |
141 apply (rule add_left_cancel [of "hlog a x", THEN iffD1]) |
143 apply (rule add_left_cancel [of "hlog a x", THEN iffD1]) |
142 apply (simp add: hlog_mult [symmetric]) |
144 apply (simp add: hlog_mult [symmetric]) |
146 "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y" |
148 "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y" |
147 by (simp add: hlog_mult hlog_inverse divide_inverse) |
149 by (simp add: hlog_mult hlog_inverse divide_inverse) |
148 |
150 |
149 lemma hlog_less_cancel_iff [simp]: |
151 lemma hlog_less_cancel_iff [simp]: |
150 "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)" |
152 "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)" |
151 by (unfold hlog_def, transfer, simp) |
153 by (transfer, simp) |
152 |
154 |
153 lemma hlog_le_cancel_iff [simp]: |
155 lemma hlog_le_cancel_iff [simp]: |
154 "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)" |
156 "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)" |
155 by (simp add: linorder_not_less [symmetric]) |
157 by (simp add: linorder_not_less [symmetric]) |
156 |
158 |