Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Real_Asymp/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 34 kB

Quelle Multiseries_Expansion_Bounds.thy Sprache: Isabelle

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')

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

quality92%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.