equal
deleted
inserted
replaced
19 |
19 |
20 |
20 |
21 constdefs |
21 constdefs |
22 |
22 |
23 powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) |
23 powhr :: "[hypreal,hypreal] => hypreal" (infixr "powhr" 80) |
24 "x powhr a == Ifun2_of (op powr) x a" |
24 "x powhr a == starfun2 (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 == starfun2 log a x" |
28 |
28 |
29 declare powhr_def [transfer_unfold] |
29 declare powhr_def [transfer_unfold] |
30 declare hlog_def [transfer_unfold] |
30 declare hlog_def [transfer_unfold] |
31 |
31 |
32 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))" |
33 by (simp add: powhr_def Ifun2_of_def star_of_def Ifun_star_n) |
33 by (simp add: powhr_def starfun2_star_n) |
34 |
34 |
35 lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1" |
35 lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1" |
36 by (transfer, simp) |
36 by (transfer, simp) |
37 |
37 |
38 lemma powhr_mult: |
38 lemma powhr_mult: |
79 by (simp add: linorder_not_less [symmetric]) |
79 by (simp add: linorder_not_less [symmetric]) |
80 |
80 |
81 lemma hlog: |
81 lemma hlog: |
82 "hlog (star_n X) (star_n Y) = |
82 "hlog (star_n X) (star_n Y) = |
83 star_n (%n. log (X n) (Y n))" |
83 star_n (%n. log (X n) (Y n))" |
84 by (simp add: hlog_def Ifun2_of_def star_of_def Ifun_star_n) |
84 by (simp add: hlog_def starfun2_star_n) |
85 |
85 |
86 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" |
87 by (transfer, rule log_ln) |
87 by (transfer, rule log_ln) |
88 |
88 |
89 lemma powhr_hlog_cancel [simp]: |
89 lemma powhr_hlog_cancel [simp]: |