|
section \<open>Asymptotic real interval arithmetic\<close>
(*
File: Multiseries_Expansion_Bounds.thy
Author: Manuel Eberl, TU München
Automatic computation of upper and lower expansions for real-valued functions.
Allows limited handling of functions involving oscillating functions like sin, cos, floor, etc.
*)
theory Multiseries_Expansion_Bounds
imports
Multiseries_Expansion
begin
lemma expands_to_cong_reverse:
"eventually (\x. f x = g x) at_top \ (g expands_to F) bs \ (f expands_to F) bs"
using expands_to_cong[of g F bs f] by (simp add: eq_commute)
lemma expands_to_trivial_bounds: "(f expands_to F) bs \ eventually (\x. f x \ {f x..f x}) at_top"
by simp
lemma eventually_in_atLeastAtMostI:
assumes "eventually (\x. f x \ l x) at_top" "eventually (\x. f x \ u x) at_top"
shows "eventually (\x. f x \ {l x..u x}) at_top"
using assms by eventually_elim simp_all
lemma tendsto_sandwich':
fixes l f u :: "'a \ 'b :: order_topology"
shows "eventually (\x. l x \ f x) F \ eventually (\x. f x \ u x) F \
(l \<longlongrightarrow> L1) F \<Longrightarrow> (u \<longlongrightarrow> L2) F \<Longrightarrow> L1 = L2 \<Longrightarrow> (f \<longlongrightarrow> L1) F"
using tendsto_sandwich[of l f F u L1] by simp
(* TODO: Move? *)
lemma filterlim_at_bot_mono:
fixes l f u :: "'a \ 'b :: linorder_topology"
assumes "filterlim u at_bot F" and "eventually (\x. f x \ u x) F"
shows "filterlim f at_bot F"
unfolding filterlim_at_bot
proof
fix Z :: 'b
from assms(1) have "eventually (\x. u x \ Z) F" by (auto simp: filterlim_at_bot)
with assms(2) show "eventually (\x. f x \ Z) F" by eventually_elim simp
qed
context
begin
qualified lemma eq_zero_imp_nonneg: "x = (0::real) \ x \ 0"
by simp
qualified lemma exact_to_bound: "(f expands_to F) bs \ eventually (\x. f x \ f x) at_top"
by simp
qualified lemma expands_to_abs_nonneg: "(f expands_to F) bs \ eventually (\x. abs (f x) \ 0) at_top"
by simp
qualified lemma eventually_nonpos_flip: "eventually (\x. f x \ (0::real)) F \ eventually (\x. -f x \ 0) F"
by simp
qualified lemma bounds_uminus:
fixes a b :: "real \ real"
assumes "eventually (\x. a x \ b x) at_top"
shows "eventually (\x. -b x \ -a x) at_top"
using assms by eventually_elim simp
qualified lemma
fixes a b c d :: "real \ real"
assumes "eventually (\x. a x \ b x) at_top" "eventually (\x. c x \ d x) at_top"
shows combine_bounds_add: "eventually (\x. a x + c x \ b x + d x) at_top"
and combine_bounds_diff: "eventually (\x. a x - d x \ b x - c x) at_top"
by (use assms in eventually_elim; simp add: add_mono diff_mono)+
qualified lemma
fixes a b c d :: "real \ real"
assumes "eventually (\x. a x \ b x) at_top" "eventually (\x. c x \ d x) at_top"
shows combine_bounds_min: "eventually (\x. min (a x) (c x) \ min (b x) (d x)) at_top"
and combine_bounds_max: "eventually (\x. max (a x) (c x) \ max (b x) (d x)) at_top"
by (blast intro: eventually_elim2[OF assms] min.mono max.mono)+
qualified lemma trivial_bounds_sin: "\x::real. sin x \ {-1..1}"
and trivial_bounds_cos: "\x::real. cos x \ {-1..1}"
and trivial_bounds_frac: "\x::real. frac x \ {0..1}"
by (auto simp: less_imp_le[OF frac_lt_1])
qualified lemma trivial_boundsI:
fixes f g:: "real \ real"
assumes "\x. f x \ {l..u}" and "g \ g"
shows "eventually (\x. f (g x) \ l) at_top" "eventually (\x. f (g x) \ u) at_top"
using assms by auto
qualified lemma
fixes f f' :: "real \ real"
shows transfer_lower_bound:
"eventually (\x. g x \ l x) at_top \ f \ g \ eventually (\x. f x \ l x) at_top"
and transfer_upper_bound:
"eventually (\x. g x \ u x) at_top \ f \ g \ eventually (\x. f x \ u x) at_top"
by simp_all
qualified lemma mono_bound:
fixes f g h :: "real \ real"
assumes "mono h" "eventually (\x. f x \ g x) at_top"
shows "eventually (\x. h (f x) \ h (g x)) at_top"
by (intro eventually_mono[OF assms(2)] monoD[OF assms(1)])
qualified lemma
fixes f l :: "real \ real"
assumes "(l expands_to L) bs" "trimmed_pos L" "basis_wf bs" "eventually (\x. l x \ f x) at_top"
shows expands_to_lb_ln: "eventually (\x. ln (l x) \ ln (f x)) at_top"
and expands_to_ub_ln:
"eventually (\x. f x \ u x) at_top \ eventually (\x. ln (f x) \ ln (u x)) at_top"
proof -
from assms(3,1,2) have pos: "eventually (\x. l x > 0) at_top"
by (rule expands_to_imp_eventually_pos)
from pos and assms(4)
show "eventually (\x. ln (l x) \ ln (f x)) at_top" by eventually_elim simp
assume "eventually (\x. f x \ u x) at_top"
with pos and assms(4) show "eventually (\x. ln (f x) \ ln (u x)) at_top"
by eventually_elim simp
qed
qualified lemma eventually_sgn_ge_1D:
assumes "eventually (\x::real. sgn (f x) \ l x) at_top"
"(l expands_to (const_expansion 1 :: 'a :: multiseries)) bs"
shows "((\x. sgn (f x)) expands_to (const_expansion 1 :: 'a)) bs"
proof (rule expands_to_cong)
from assms(2) have "eventually (\x. l x = 1) at_top"
by (simp add: expands_to.simps)
with assms(1) show "eventually (\x. 1 = sgn (f x)) at_top"
by eventually_elim (auto simp: sgn_if split: if_splits)
qed (insert assms, auto simp: expands_to.simps)
qualified lemma eventually_sgn_le_neg1D:
assumes "eventually (\x::real. sgn (f x) \ u x) at_top"
"(u expands_to (const_expansion (-1) :: 'a :: multiseries)) bs"
shows "((\x. sgn (f x)) expands_to (const_expansion (-1) :: 'a)) bs"
proof (rule expands_to_cong)
from assms(2) have "eventually (\x. u x = -1) at_top"
by (simp add: expands_to.simps eq_commute)
with assms(1) show "eventually (\x. -1 = sgn (f x)) at_top"
by eventually_elim (auto simp: sgn_if split: if_splits)
qed (insert assms, auto simp: expands_to.simps)
qualified lemma expands_to_squeeze:
assumes "eventually (\x. l x \ f x) at_top" "eventually (\x. f x \ g x) at_top"
"(l expands_to L) bs" "(g expands_to L) bs"
shows "(f expands_to L) bs"
proof (rule expands_to_cong[OF assms(3)])
from assms have "eventually (\x. eval L x = l x) at_top" "eventually (\x. eval L x = g x) at_top"
by (simp_all add: expands_to.simps)
with assms(1,2) show "eventually (\x. l x = f x) at_top"
by eventually_elim simp
qed
qualified lemma mono_exp_real: "mono (exp :: real \ real)"
by (auto intro!: monoI)
qualified lemma mono_sgn_real: "mono (sgn :: real \ real)"
by (auto intro!: monoI simp: sgn_if)
qualified lemma mono_arctan_real: "mono (arctan :: real \ real)"
by (auto intro!: monoI arctan_monotone')
qualified lemma mono_root_real: "n \ n \ mono (root n :: real \ real)"
by (cases n) (auto simp: mono_def)
qualified lemma mono_rfloor: "mono rfloor" and mono_rceil: "mono rceil"
by (auto intro!: monoI simp: rfloor_def floor_mono rceil_def ceiling_mono)
qualified lemma lower_bound_cong:
"eventually (\x. f x = g x) at_top \ eventually (\x. l x \ g x) at_top \
eventually (\<lambda>x. l x \<le> f x) at_top"
by (erule (1) eventually_elim2) simp
qualified lemma upper_bound_cong:
"eventually (\x. f x = g x) at_top \ eventually (\x. g x \ u x) at_top \
eventually (\<lambda>x. f x \<le> u x) at_top"
by (erule (1) eventually_elim2) simp
qualified lemma
assumes "eventually (\x. f x = (g x :: real)) at_top"
shows eventually_eq_min: "eventually (\x. min (f x) (g x) = f x) at_top"
and eventually_eq_max: "eventually (\x. max (f x) (g x) = f x) at_top"
by (rule eventually_mono[OF assms]; simp)+
qualified lemma rfloor_bound:
"eventually (\x. l x \ f x) at_top \ eventually (\x. l x - 1 \ rfloor (f x)) at_top"
"eventually (\x. f x \ u x) at_top \ eventually (\x. rfloor (f x) \ u x) at_top"
and rceil_bound:
"eventually (\x. l x \ f x) at_top \ eventually (\x. l x \ rceil (f x)) at_top"
"eventually (\x. f x \ u x) at_top \ eventually (\x. rceil (f x) \ u x + 1) at_top"
unfolding rfloor_def rceil_def by (erule eventually_mono, linarith)+
qualified lemma natmod_trivial_lower_bound:
fixes f g :: "real \ real"
assumes "f \ f" "g \ g"
shows "eventually (\x. rnatmod (f x) (g x) \ 0) at_top"
by (simp add: rnatmod_def)
qualified lemma natmod_upper_bound:
fixes f g :: "real \ real"
assumes "f \ f" and "eventually (\x. l2 x \ g x) at_top" and "eventually (\x. g x \ u2 x) at_top"
assumes "eventually (\x. l2 x - 1 \ 0) at_top"
shows "eventually (\x. rnatmod (f x) (g x) \ u2 x - 1) at_top"
using assms(2-)
proof eventually_elim
case (elim x)
have "rnatmod (f x) (g x) = real (nat \f x\ mod nat \g x\)"
by (simp add: rnatmod_def)
also have "nat \f x\ mod nat \g x\ < nat \g x\"
using elim by (intro mod_less_divisor) auto
hence "real (nat \f x\ mod nat \g x\) \ u2 x - 1"
using elim by linarith
finally show ?case .
qed
qualified lemma natmod_upper_bound':
fixes f g :: "real \ real"
assumes "g \ g" "eventually (\x. u1 x \ 0) at_top" and "eventually (\x. f x \ u1 x) at_top"
shows "eventually (\x. rnatmod (f x) (g x) \ u1 x) at_top"
using assms(2-)
proof eventually_elim
case (elim x)
have "rnatmod (f x) (g x) = real (nat \f x\ mod nat \g x\)"
by (simp add: rnatmod_def)
also have "nat \f x\ mod nat \g x\ \ nat \f x\"
by auto
hence "real (nat \f x\ mod nat \g x\) \ real (nat \f x\)"
by simp
also have "\ \ u1 x" using elim by linarith
finally show "rnatmod (f x) (g x) \ \" .
qed
qualified lemma expands_to_natmod_nonpos:
fixes f g :: "real \ real"
assumes "g \ g" "eventually (\x. u1 x \ 0) at_top" "eventually (\x. f x \ u1 x) at_top"
"((\_. 0) expands_to C) bs"
shows "((\x. rnatmod (f x) (g x)) expands_to C) bs"
by (rule expands_to_cong[OF assms(4)])
(insert assms, auto elim: eventually_elim2 simp: rnatmod_def)
qualified lemma eventually_atLeastAtMostI:
fixes f l r :: "real \ real"
assumes "eventually (\x. l x \ f x) at_top" "eventually (\x. f x \ u x) at_top"
shows "eventually (\x. f x \ {l x..u x}) at_top"
using assms by eventually_elim simp
qualified lemma eventually_atLeastAtMostD:
fixes f l r :: "real \ real"
assumes "eventually (\x. f x \ {l x..u x}) at_top"
shows "eventually (\x. l x \ f x) at_top" "eventually (\x. f x \ u x) at_top"
using assms by (simp_all add: eventually_conj_iff)
qualified lemma eventually_0_imp_prod_zero:
fixes f g :: "real \ real"
assumes "eventually (\x. f x = 0) at_top"
shows "eventually (\x. f x * g x = 0) at_top" "eventually (\x. g x * f x = 0) at_top"
by (use assms in eventually_elim; simp)+
qualified lemma mult_right_bounds:
fixes f g :: "real \ real"
shows "\x. f x \ {l x..u x} \ g x \ 0 \ f x * g x \ {l x * g x..u x * g x}"
and "\x. f x \ {l x..u x} \ g x \ 0 \ f x * g x \ {u x * g x..l x * g x}"
by (auto intro: mult_right_mono mult_right_mono_neg)
qualified lemma mult_left_bounds:
fixes f g :: "real \ real"
shows "\x. g x \ {l x..u x} \ f x \ 0 \ f x * g x \ {f x * l x..f x * u x}"
and "\x. g x \ {l x..u x} \ f x \ 0 \ f x * g x \ {f x * u x..f x * l x}"
by (auto intro: mult_left_mono mult_left_mono_neg)
qualified lemma mult_mono_nonpos_nonneg:
"a \ c \ d \ b \ a \ 0 \ d \ 0 \ a * b \ c * (d :: 'a :: linordered_ring)"
using mult_mono[of "-c" "-a" d b] by simp
qualified lemma mult_mono_nonneg_nonpos:
"c \ a \ b \ d \ a \ 0 \ d \ 0 \ a * b \ c * (d :: 'a :: {comm_ring, linordered_ring})"
using mult_mono[of c a "-d" "-b"] by (simp add: mult.commute)
qualified lemma mult_mono_nonpos_nonpos:
"c \ a \ d \ b \ c \ 0 \ b \ 0 \ a * b \ c * (d :: 'a :: linordered_ring)"
using mult_mono[of "-a" "-c" "-b" "-d"] by simp
qualified lemmas mult_monos =
mult_mono mult_mono_nonpos_nonneg mult_mono_nonneg_nonpos mult_mono_nonpos_nonpos
qualified lemma mult_bounds_real:
fixes f g l1 u1 l2 u2 l u :: "real \ real"
defines "P \ \l u x. f x \ {l1 x..u1 x} \ g x \ {l2 x..u2 x} \ f x * g x \ {l..u}"
shows "\x. l1 x \ 0 \ l2 x \ 0 \ P (l1 x * l2 x) (u1 x * u2 x) x"
and "\x. u1 x \ 0 \ l2 x \ 0 \ P (l1 x * u2 x) (u1 x * l2 x) x"
and "\x. l1 x \ 0 \ u2 x \ 0 \ P (u1 x * l2 x) (l1 x * u2 x) x"
and "\x. u1 x \ 0 \ u2 x \ 0 \ P (u1 x * u2 x) (l1 x * l2 x) x"
and "\x. l1 x \ 0 \ u1 x \ 0 \ l2 x \ 0 \ P (l1 x * u2 x) (u1 x * u2 x) x"
and "\x. l1 x \ 0 \ u1 x \ 0 \ u2 x \ 0 \ P (u1 x * l2 x) (l1 x * l2 x) x"
and "\x. l1 x \ 0 \ l2 x \ 0 \ u2 x \ 0 \ P (u1 x * l2 x) (u1 x * u2 x) x"
and "\x. u1 x \ 0 \ l2 x \ 0 \ u2 x \ 0 \ P (l1 x * u2 x) (l1 x * l2 x) x"
and "\x. l1 x \ 0 \ u1 x \ 0 \ l2 x \ 0 \ u2 x \ 0 \ l x \ l1 x * u2 x \
l x \<le> u1 x * l2 x \<longrightarrow> u x \<ge> l1 x* l2 x \<longrightarrow> u x \<ge> u1 x * u2 x \<longrightarrow> P (l x) (u x) x"
proof goal_cases
case 1
show ?case by (auto intro: mult_mono simp: P_def)
next
case 2
show ?case by (auto intro: mult_monos(2) simp: P_def)
next
case 3
show ?case unfolding P_def
by (subst (1 2 3) mult.commute) (auto intro: mult_monos(2) simp: P_def)
next
case 4
show ?case by (auto intro: mult_monos(4) simp: P_def)
next
case 5
show ?case by (auto intro: mult_monos(1,2) simp: P_def)
next
case 6
show ?case by (auto intro: mult_monos(3,4) simp: P_def)
next
case 7
show ?case unfolding P_def
by (subst (1 2 3) mult.commute) (auto intro: mult_monos(1,2))
next
case 8
show ?case unfolding P_def
by (subst (1 2 3) mult.commute) (auto intro: mult_monos(3,4))
next
case 9
show ?case
proof (safe, goal_cases)
case (1 x)
from 1(1-4) show ?case unfolding P_def
by (cases "f x \ 0"; cases "g x \ 0";
fastforce intro: mult_monos 1(5,6)[THEN order.trans] 1(7,8)[THEN order.trans[rotated]])
qed
qed
qualified lemma powr_bounds_real:
fixes f g l1 u1 l2 u2 l u :: "real \ real"
defines "P \ \l u x. f x \ {l1 x..u1 x} \ g x \ {l2 x..u2 x} \ f x powr g x \ {l..u}"
shows "\x. l1 x \ 0 \ l1 x \ 1 \ l2 x \ 0 \ P (l1 x powr l2 x) (u1 x powr u2 x) x"
and "\x. l1 x \ 0 \ u1 x \ 1 \ l2 x \ 0 \ P (l1 x powr u2 x) (u1 x powr l2 x) x"
and "\x. l1 x \ 0 \ l1 x \ 1 \ u2 x \ 0 \ P (u1 x powr l2 x) (l1 x powr u2 x) x"
and "\x. l1 x > 0 \ u1 x \ 1 \ u2 x \ 0 \ P (u1 x powr u2 x) (l1 x powr l2 x) x"
and "\x. l1 x \ 0 \ l1 x \ 1 \ u1 x \ 1 \ l2 x \ 0 \ P (l1 x powr u2 x) (u1 x powr u2 x) x"
and "\x. l1 x > 0 \ l1 x \ 1 \ u1 x \ 1 \ u2 x \ 0 \ P (u1 x powr l2 x) (l1 x powr l2 x) x"
and "\x. l1 x \ 0 \ l1 x \ 1 \ l2 x \ 0 \ u2 x \ 0 \ P (u1 x powr l2 x) (u1 x powr u2 x) x"
and "\x. l1 x > 0 \ u1 x \ 1 \ l2 x \ 0 \ u2 x \ 0 \ P (l1 x powr u2 x) (l1 x powr l2 x) x"
and "\x. l1 x > 0 \ l1 x \ 1 \ u1 x \ 1 \ l2 x \ 0 \ u2 x \ 0 \ l x \ l1 x powr u2 x \
l x \<le> u1 x powr l2 x \<longrightarrow> u x \<ge> l1 x powr l2 x \<longrightarrow> u x \<ge> u1 x powr u2 x \<longrightarrow> P (l x) (u x) x"
proof goal_cases
case 1
show ?case by (auto simp: P_def powr_def intro: mult_monos)
next
case 2
show ?case by (auto simp: P_def powr_def intro: mult_monos)
next
case 3
show ?case by (auto simp: P_def powr_def intro: mult_monos)
next
case 4
show ?case by (auto simp: P_def powr_def intro: mult_monos)
next
case 5
note comm = mult.commute[of _ "ln x" for x :: real]
show ?case by (auto simp: P_def powr_def comm intro: mult_monos)
next
case 6
note comm = mult.commute[of _ "ln x" for x :: real]
show ?case by (auto simp: P_def powr_def comm intro: mult_monos)
next
case 7
show ?case by (auto simp: P_def powr_def intro: mult_monos)
next
case 8
show ?case
by (auto simp: P_def powr_def intro: mult_monos)
next
case 9
show ?case unfolding P_def
proof (safe, goal_cases)
case (1 x)
define l' where "l' = (\<lambda>x. min (ln (l1 x) * u2 x) (ln (u1 x) * l2 x))"
define u' where "u' = (\<lambda>x. max (ln (l1 x) * l2 x) (ln (u1 x) * u2 x))"
from 1 spec[OF mult_bounds_real(9)[of "\x. ln (l1 x)" "\x. ln (u1 x)" l2 u2 l' u'
"\x. ln (f x)" g], of x]
have "ln (f x) * g x \ {l' x..u' x}" by (auto simp: powr_def mult.commute l'_def u'_def)
with 1 have "f x powr g x \ {exp (l' x)..exp (u' x)}"
by (auto simp: powr_def mult.commute)
also from 1 have "exp (l' x) = min (l1 x powr u2 x) (u1 x powr l2 x)"
by (auto simp add: l'_def powr_def min_def mult.commute)
also from 1 have "exp (u' x) = max (l1 x powr l2 x) (u1 x powr u2 x)"
by (auto simp add: u'_def powr_def max_def mult.commute)
finally show ?case using 1(5-9) by auto
qed
qed
qualified lemma powr_right_bounds:
fixes f g :: "real \ real"
shows "\x. l x \ 0 \ f x \ {l x..u x} \ g x \ 0 \ f x powr g x \ {l x powr g x..u x powr g x}"
and "\x. l x > 0 \ f x \ {l x..u x} \ g x \ 0 \ f x powr g x \ {u x powr g x..l x powr g x}"
by (auto intro: powr_mono2 powr_mono2')
(* TODO Move *)
lemma powr_mono': "a \ (b::real) \ x \ 0 \ x \ 1 \ x powr b \ x powr a"
using powr_mono[of "-b" "-a" "inverse x"] by (auto simp: powr_def ln_inverse ln_div field_split_simps)
qualified lemma powr_left_bounds:
fixes f g :: "real \ real"
shows "\x. f x > 0 \ g x \ {l x..u x} \ f x \ 1 \ f x powr g x \ {f x powr l x..f x powr u x}"
and "\x. f x > 0 \ g x \ {l x..u x} \ f x \ 1 \ f x powr g x \ {f x powr u x..f x powr l x}"
by (auto intro: powr_mono powr_mono')
qualified lemma powr_nat_bounds_transfer_ge:
"\x. l1 x \ 0 \ f x \ l1 x \ f x powr g x \ l x \ powr_nat (f x) (g x) \ l x"
by (auto simp: powr_nat_def)
qualified lemma powr_nat_bounds_transfer_le:
"\x. l1 x > 0 \ f x \ l1 x \ f x powr g x \ u x \ powr_nat (f x) (g x) \ u x"
"\x. l1 x \ 0 \ l2 x > 0 \ f x \ l1 x \ g x \ l2 x \
f x powr g x \<le> u x \<longrightarrow> powr_nat (f x) (g x) \<le> u x"
"\x. l1 x \ 0 \ u2 x < 0 \ f x \ l1 x \ g x \ u2 x \
f x powr g x \<le> u x \<longrightarrow> powr_nat (f x) (g x) \<le> u x"
"\x. l1 x \ 0 \ f x \ l1 x \ f x powr g x \ u x \ u x \ u' x \ 1 \ u' x \
powr_nat (f x) (g x) \<le> u' x"
by (auto simp: powr_nat_def)
lemma abs_powr_nat_le: "abs (powr_nat x y) \ powr_nat (abs x) y"
by (simp add: powr_nat_def abs_mult)
qualified lemma powr_nat_bounds_ge_neg:
assumes "powr_nat (abs x) y \ u"
shows "powr_nat x y \ -u" "powr_nat x y \ u"
proof -
have "abs (powr_nat x y) \ powr_nat (abs x) y"
by (rule abs_powr_nat_le)
also have "\ \ u" using assms by auto
finally show "powr_nat x y \ -u" "powr_nat x y \ u" by auto
qed
qualified lemma powr_nat_bounds_transfer_abs [eventuallized]:
"\x. powr_nat (abs (f x)) (g x) \ u x \ powr_nat (f x) (g x) \ -u x"
"\x. powr_nat (abs (f x)) (g x) \ u x \ powr_nat (f x) (g x) \ u x"
using powr_nat_bounds_ge_neg by blast+
qualified lemma eventually_powr_const_nonneg:
"f \ f \ p \ p \ eventually (\x. f x powr p \ (0::real)) at_top"
by simp
qualified lemma eventually_powr_const_mono_nonneg:
assumes "p \ (0 :: real)" "eventually (\x. l x \ 0) at_top" "eventually (\x. l x \ f x) at_top"
"eventually (\x. f x \ g x) at_top"
shows "eventually (\x. f x powr p \ g x powr p) at_top"
using assms(2-4) by eventually_elim (auto simp: assms(1) intro!: powr_mono2)
qualified lemma eventually_powr_const_mono_nonpos:
assumes "p \ (0 :: real)" "eventually (\x. l x > 0) at_top" "eventually (\x. l x \ f x) at_top"
"eventually (\x. f x \ g x) at_top"
shows "eventually (\x. f x powr p \ g x powr p) at_top"
using assms(2-4) by eventually_elim (auto simp: assms(1) intro!: powr_mono2')
qualified lemma eventually_power_mono:
assumes "eventually (\x. 0 \ l x) at_top" "eventually (\x. l x \ f x) at_top"
"eventually (\x. f x \ g x) at_top" "n \ n"
shows "eventually (\x. f x ^ n \ (g x :: real) ^ n) at_top"
using assms(1-3) by eventually_elim (auto intro: power_mono)
qualified lemma eventually_mono_power_odd:
assumes "odd n" "eventually (\x. f x \ (g x :: real)) at_top"
shows "eventually (\x. f x ^ n \ g x ^ n) at_top"
using assms(2) by eventually_elim (insert assms(1), auto intro: power_mono_odd)
qualified lemma eventually_lower_bound_power_even_nonpos:
assumes "even n" "eventually (\x. u x \ (0::real)) at_top"
"eventually (\x. f x \ u x) at_top"
shows "eventually (\x. u x ^ n \ f x ^ n) at_top"
using assms(2-) by eventually_elim (rule power_mono_even, auto simp: assms(1))
qualified lemma eventually_upper_bound_power_even_nonpos:
assumes "even n" "eventually (\x. u x \ (0::real)) at_top"
"eventually (\x. l x \ f x) at_top" "eventually (\x. f x \ u x) at_top"
shows "eventually (\x. f x ^ n \ l x ^ n) at_top"
using assms(2-) by eventually_elim (rule power_mono_even, auto simp: assms(1))
qualified lemma eventually_lower_bound_power_even_indet:
assumes "even n" "f \ f"
shows "eventually (\x. (0::real) \ f x ^ n) at_top"
using assms by (simp add: zero_le_even_power)
qualified lemma eventually_lower_bound_power_indet:
assumes "eventually (\x. l x \ f x) at_top"
assumes "eventually (\x. l' x \ l x ^ n) at_top" "eventually (\x. l' x \ 0) at_top"
shows "eventually (\x. l' x \ (f x ^ n :: real)) at_top"
using assms
proof eventually_elim
case (elim x)
thus ?case
using power_mono_odd[of n "l x" "f x"] zero_le_even_power[of n "f x"]
by (cases "even n") auto
qed
qualified lemma eventually_upper_bound_power_indet:
assumes "eventually (\x. l x \ f x) at_top" "eventually (\x. f x \ u x) at_top"
"eventually (\x. u' x \ -l x) at_top" "eventually (\x. u' x \ u x) at_top" "n \ n"
shows "eventually (\x. f x ^ n \ (u' x ^ n :: real)) at_top"
using assms(1-4)
proof eventually_elim
case (elim x)
have "f x ^ n \ \f x ^ n\" by simp
also have "\ = \f x\ ^ n" by (simp add: power_abs)
also from elim have "\ \ u' x ^ n" by (intro power_mono) auto
finally show ?case .
qed
qualified lemma expands_to_imp_exp_ln_eq:
assumes "(l expands_to L) bs" "eventually (\x. l x \ f x) at_top"
"trimmed_pos L" "basis_wf bs"
shows "eventually (\x. exp (ln (f x)) = f x) at_top"
proof -
from expands_to_imp_eventually_pos[of bs l L] assms
have "eventually (\x. l x > 0) at_top" by simp
with assms(2) show ?thesis by eventually_elim simp
qed
qualified lemma expands_to_imp_ln_powr_eq:
assumes "(l expands_to L) bs" "eventually (\x. l x \ f x) at_top"
"trimmed_pos L" "basis_wf bs"
shows "eventually (\x. ln (f x powr g x) = ln (f x) * g x) at_top"
proof -
from expands_to_imp_eventually_pos[of bs l L] assms
have "eventually (\x. l x > 0) at_top" by simp
with assms(2) show ?thesis by eventually_elim (simp add: powr_def)
qed
qualified lemma inverse_bounds_real:
fixes f l u :: "real \ real"
shows "\x. l x > 0 \ l x \ f x \ f x \ u x \ inverse (f x) \ {inverse (u x)..inverse (l x)}"
and "\x. u x < 0 \ l x \ f x \ f x \ u x \ inverse (f x) \ {inverse (u x)..inverse (l x)}"
by (auto simp: field_simps)
qualified lemma pos_imp_inverse_pos: "\x::real. f x > 0 \ inverse (f x) > (0::real)"
and neg_imp_inverse_neg: "\x::real. f x < 0 \ inverse (f x) < (0::real)"
by auto
qualified lemma transfer_divide_bounds:
fixes f g :: "real \ real"
shows "Trueprop (eventually (\x. f x \ {h x * inverse (i x)..j x}) at_top) \
Trueprop (eventually (\<lambda>x. f x \<in> {h x / i x..j x}) at_top)"
and "Trueprop (eventually (\x. f x \ {j x..h x * inverse (i x)}) at_top) \
Trueprop (eventually (\<lambda>x. f x \<in> {j x..h x / i x}) at_top)"
and "Trueprop (eventually (\x. f x * inverse (g x) \ A x) at_top) \
Trueprop (eventually (\<lambda>x. f x / g x \<in> A x) at_top)"
and "Trueprop (((\x. f x * inverse (g x)) expands_to F) bs) \
Trueprop (((\<lambda>x. f x / g x) expands_to F) bs)"
by (simp_all add: field_simps)
qualified lemma eventually_le_self: "eventually (\x::real. f x \ (f x :: real)) at_top"
by simp
qualified lemma max_eventually_eq:
"eventually (\x. f x = (g x :: real)) at_top \ eventually (\x. max (f x) (g x) = f x) at_top"
by (erule eventually_mono) simp
qualified lemma min_eventually_eq:
"eventually (\x. f x = (g x :: real)) at_top \ eventually (\x. min (f x) (g x) = f x) at_top"
by (erule eventually_mono) simp
qualified lemma
assumes "eventually (\x. f x = (g x :: 'a :: preorder)) F"
shows eventually_eq_imp_ge: "eventually (\x. f x \ g x) F"
and eventually_eq_imp_le: "eventually (\x. f x \ g x) F"
by (use assms in eventually_elim; simp)+
qualified lemma eventually_less_imp_le:
assumes "eventually (\x. f x < (g x :: 'a :: order)) F"
shows "eventually (\x. f x \ g x) F"
using assms by eventually_elim auto
qualified lemma
fixes f :: "real \ real"
shows eventually_abs_ge_0: "eventually (\x. abs (f x) \ 0) at_top"
and nonneg_abs_bounds: "\x. l x \ 0 \ f x \ {l x..u x} \ abs (f x) \ {l x..u x}"
and nonpos_abs_bounds: "\x. u x \ 0 \ f x \ {l x..u x} \ abs (f x) \ {-u x..-l x}"
and indet_abs_bounds:
"\x. l x \ 0 \ u x \ 0 \ f x \ {l x..u x} \ -l x \ h x \ u x \ h x \
abs (f x) \<in> {0..h x}"
by auto
qualified lemma eventually_le_abs_nonneg:
"eventually (\x. l x \ 0) at_top \ eventually (\x. f x \ l x) at_top \
eventually (\<lambda>x::real. l x \<le> (\<bar>f x\<bar> :: real)) at_top"
by (auto elim: eventually_elim2)
qualified lemma eventually_le_abs_nonpos:
"eventually (\x. u x \ 0) at_top \ eventually (\x. f x \ u x) at_top \
eventually (\<lambda>x::real. -u x \<le> (\<bar>f x\<bar> :: real)) at_top"
by (auto elim: eventually_elim2)
qualified lemma
fixes f g h :: "'a \ 'b :: order"
shows eventually_le_less:"eventually (\x. f x \ g x) F \ eventually (\x. g x < h x) F \
eventually (\<lambda>x. f x < h x) F"
and eventually_less_le:"eventually (\x. f x < g x) F \ eventually (\x. g x \ h x) F \
eventually (\<lambda>x. f x < h x) F"
by (erule (1) eventually_elim2; erule (1) order.trans le_less_trans less_le_trans)+
qualified lemma eventually_pos_imp_nz [eventuallized]: "\x. f x > 0 \ f x \ (0 :: 'a :: linordered_semiring)"
and eventually_neg_imp_nz [eventuallized]: "\x. f x < 0 \ f x \ 0"
by auto
qualified lemma
fixes f g l1 l2 u1 :: "'a \ real"
assumes "eventually (\x. l1 x \ f x) F"
assumes "eventually (\x. f x \ u1 x) F"
assumes "eventually (\x. abs (g x) \ l2 x) F"
assumes "eventually (\x. l2 x \ 0) F"
shows bounds_smallo_imp_smallo: "l1 \ o[F](l2) \ u1 \ o[F](l2) \ f \ o[F](g)"
and bounds_bigo_imp_bigo: "l1 \ O[F](l2) \ u1 \ O[F](l2) \ f \ O[F](g)"
proof -
assume *: "l1 \ o[F](l2)" "u1 \ o[F](l2)"
show "f \ o[F](g)"
proof (rule landau_o.smallI, goal_cases)
case (1 c)
from *[THEN landau_o.smallD[OF _ 1]] and assms show ?case
proof eventually_elim
case (elim x)
from elim have "norm (f x) \ c * l2 x" by simp
also have "\ \ c * norm (g x)" using 1 elim by (intro mult_left_mono) auto
finally show ?case .
qed
qed
next
assume *: "l1 \ O[F](l2)" "u1 \ O[F](l2)"
then obtain C1 C2 where **: "C1 > 0" "C2 > 0" "eventually (\x. norm (l1 x) \ C1 * norm (l2 x)) F"
"eventually (\x. norm (u1 x) \ C2 * norm (l2 x)) F" by (auto elim!: landau_o.bigE)
from this(3,4) and assms have "eventually (\x. norm (f x) \ max C1 C2 * norm (g x)) F"
proof eventually_elim
case (elim x)
from elim have "norm (f x) \ max C1 C2 * l2 x" by (subst max_mult_distrib_right) auto
also have "\ \ max C1 C2 * norm (g x)" using elim ** by (intro mult_left_mono) auto
finally show ?case .
qed
thus "f \ O[F](g)" by (rule bigoI)
qed
qualified lemma real_root_mono: "mono (root n)"
by (cases n) (auto simp: mono_def)
(* TODO: support for rintmod *)
ML_file \<open>multiseries_expansion_bounds.ML\<close>
method_setup real_asymp = \<open>
let
type flags = {verbose : bool, fallback : bool}
fun join_flags
{verbose = verbose1, fallback = fallback1}
{verbose = verbose2, fallback = fallback2} =
{verbose = verbose1 orelse verbose2, fallback = fallback1 orelse fallback2}
val parse_flag =
(Args.$$$ "verbose" >> K {verbose = true, fallback = false}) ||
(Args.$$$ "fallback" >> K {verbose = false, fallback = true})
val default_flags = {verbose = false, fallback = false}
val parse_flags =
Scan.optional (Args.parens (Parse.list1 parse_flag)) [] >>
(fn xs => fold join_flags xs default_flags)
in
Scan.lift parse_flags --| Method.sections Simplifier.simp_modifiers >>
(fn flags => SIMPLE_METHOD' o
(if #fallback flags then Real_Asymp_Basic.tac else Real_Asymp_Bounds.tac) (#verbose flags))
end
\<close> "Semi-automatic decision procedure for asymptotics of exp-log functions"
end
lemma "filterlim (\x::real. sin x / x) (nhds 0) at_top"
by real_asymp
lemma "(\x::real. exp (sin x)) \ O(\_. 1)"
by real_asymp
lemma "(\x::real. exp (real_of_int (floor x))) \ \(\x. exp x)"
by real_asymp
lemma "(\n::nat. n div 2 * ln (n div 2)) \ \(\n::nat. n * ln n)"
by real_asymp
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
