Theory Akra_Bazzi_Library

(*
  File:   Akra_Bazzi_Library.thy
  Author: Manuel Eberl <manuel@pruvisto.org>

  Lemma bucket for the Akra-Bazzi theorem.
*)

section ‹Auxiliary lemmas›
theory Akra_Bazzi_Library
imports 
  Complex_Main
  "Landau_Symbols.Landau_More"
  "Pure-ex.Guess"
begin

(* TODO: Move? *)

lemma ln_mono: "0 < x  0 < y  x  y  ln (x::real)  ln y"
  by (subst ln_le_cancel_iff) simp_all

lemma ln_mono_strict: "0 < x  0 < y  x < y  ln (x::real) < ln y"
  by (subst ln_less_cancel_iff) simp_all

declare DERIV_powr[THEN DERIV_chain2, derivative_intros]

lemma sum_pos':
  assumes "finite I"
  assumes "xI. f x > (0 :: _ :: linordered_ab_group_add)"
  assumes "x. x  I  f x  0"
  shows   "sum f I > 0"
proof-
  from assms(2) guess x by (elim bexE) note x = this
  from x have "I = insert x I" by blast
  also from assms(1) have "sum f ... = f x + sum f (I - {x})" by (rule sum.insert_remove)
  also from x assms have "... > 0" by (intro add_pos_nonneg sum_nonneg) simp_all
  finally show ?thesis .
qed


lemma min_mult_left:
  assumes "(x::real) > 0"
  shows   "x * min y z = min (x*y) (x*z)"
  using assms by (auto simp add: min_def algebra_simps)

lemma max_mult_left:
  assumes "(x::real) > 0"
  shows   "x * max y z = max (x*y) (x*z)"
  using assms by (auto simp add: max_def algebra_simps)

lemma DERIV_nonneg_imp_mono:
  assumes "t. t{x..y}  (f has_field_derivative f' t) (at t)"
  assumes "t. t{x..y}  f' t  0"
  assumes "(x::real)  y"
  shows   "(f x :: real)  f y"
proof (cases x y rule: linorder_cases)
  assume xy: "x < y"
  hence "z. x < z  z < y  f y - f x = (y - x) * f' z"
    by (rule MVT2) (insert assms(1), simp)
  then guess z by (elim exE conjE) note z = this
  from z(1,2) assms(2) xy have "0  (y - x) * f' z" by (intro mult_nonneg_nonneg) simp_all
  also note z(3)[symmetric]
  finally show "f x  f y" by simp
qed (insert assms(3), simp_all)

lemma eventually_conjE: "eventually (λx. P x  Q x) F  (eventually P F  eventually Q F  R)  R"
  apply (frule eventually_rev_mp[of _ _ P], simp)
  apply (drule eventually_rev_mp[of _ _ Q], simp)
  apply assumption
  done

lemma real_natfloor_nat: "x    real (nat x) = x" by (elim Nats_cases) simp

lemma eventually_natfloor:
  assumes "eventually P (at_top :: nat filter)"
  shows   "eventually (λx. P (nat x)) (at_top :: real filter)"
proof-
  from assms obtain N where N: "n. n  N  P n" using eventually_at_top_linorder by blast
  have "nreal N. P (nat n)" by (intro allI impI N le_nat_floor) simp_all
  thus ?thesis using eventually_at_top_linorder by blast
qed

lemma tendsto_0_smallo_1: "f  o(λx. 1 :: real)  (f  0) at_top"
  by (drule smalloD_tendsto) simp

lemma smallo_1_tendsto_0: "(f  0) at_top  f  o(λx. 1 :: real)"
  by (rule smalloI_tendsto) simp_all

lemma filterlim_at_top_smallomega_1: 
  assumes "f  ω[F](λx. 1 :: real)" "eventually (λx. f x > 0) F"
  shows   "filterlim f at_top F"
proof -
  from assms have "filterlim (λx. norm (f x / 1)) at_top F"
    by (intro smallomegaD_filterlim_at_top_norm) (auto elim: eventually_mono)
  also have "?this  ?thesis"
    using assms by (intro filterlim_cong refl) (auto elim!: eventually_mono)
  finally show ?thesis .
qed

lemma smallo_imp_abs_less_real:
  assumes "f  o[F](g)" "eventually (λx. g x > (0::real)) F"
  shows   "eventually (λx. ¦f x¦ < g x) F"
proof -
  have "1/2 > (0::real)" by simp
  from landau_o.smallD[OF assms(1) this] assms(2) show ?thesis
    by eventually_elim auto
qed

lemma smallo_imp_less_real:
  assumes "f  o[F](g)" "eventually (λx. g x > (0::real)) F"
  shows   "eventually (λx. f x < g x) F"
  using smallo_imp_abs_less_real[OF assms] by eventually_elim simp

lemma smallo_imp_le_real: 
  assumes "f  o[F](g)" "eventually (λx. g x  (0::real)) F"
  shows   "eventually (λx. f x  g x) F"
  using landau_o.smallD[OF assms(1) zero_less_one] assms(2) by eventually_elim simp

(* TODO MOVE *)
lemma filterlim_at_right: 
  "filterlim f (at_right a) F  eventually (λx. f x > a) F  filterlim f (nhds a) F"
  by (subst filterlim_at) (auto elim!: eventually_mono)
(* END TODO *)

lemma one_plus_x_powr_approx_ex:
  assumes x: "abs (x::real)  1/2"
  obtains t where "abs t < 1/2" "(1 + x) powr p = 
    1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x ^ 2"
proof (cases "x = 0")
  assume x': "x  0"
  let ?f = "λx. (1 + x) powr p"
  let ?f' = "λx. p * (1 + x) powr (p - 1)"
  let ?f'' = "λx. p * (p - 1) * (1 + x) powr (p - 2)"
  let ?fs = "(!) [?f, ?f', ?f'']"
 
  have A: "m t. m < 2  t  -0.5  t  0.5  (?fs m has_real_derivative ?fs (Suc m) t) (at t)"
  proof (clarify)
    fix m :: nat and t :: real assume m: "m < 2" and t: "t  -0.5" "t  0.5"
    thus "(?fs m has_real_derivative ?fs (Suc m) t) (at t)"
      using m by (cases m) (force intro: derivative_eq_intros algebra_simps)+
  qed
  have "t. (if x < 0 then x < t  t < 0 else 0 < t  t < x) 
              (1 + x) powr p = (m<2. ?fs m 0 / (fact m) * (x - 0)^m) + 
              ?fs 2 t / (fact 2) * (x - 0)2"
    using assms x' by (intro Taylor[OF _ _ A]) simp_all
  then guess t by (elim exE conjE)
  note t = this
  with assms have "abs t < 1/2" by (auto split: if_split_asm)
  moreover from t(2) have "(1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x ^ 2"
    by (simp add: numeral_2_eq_2 of_nat_Suc)
  ultimately show ?thesis by (rule that)
next
  assume "x = 0"
  with that[of 0] show ?thesis by simp
qed

lemma powr_lower_bound: "(l::real) > 0; l  x; x  u  min (l powr z) (u powr z)  x powr z"
apply (cases "z  0")
apply (rule order.trans[OF min.cobounded1 powr_mono2], simp_all) []
apply (rule order.trans[OF min.cobounded2 powr_mono2'], simp_all) []
done

lemma powr_upper_bound: "(l::real) > 0; l  x; x  u  max (l powr z) (u powr z)  x powr z"
apply (cases "z  0")
apply (rule order.trans[OF powr_mono2 max.cobounded2], simp_all) []
apply (rule order.trans[OF powr_mono2' max.cobounded1], simp_all) []
done

lemma one_plus_x_powr_Taylor2:
  obtains k where "x. abs (x::real)  1/2  abs ((1 + x) powr p - 1 - p*x)  k*x^2"
proof-
  define k where "k = ¦p*(p - 1)¦ * max ((1/2) powr (p - 2)) ((3/2) powr (p - 2)) / 2"
  show ?thesis
  proof (rule that[of k])
    fix x :: real assume "abs x  1/2"
    from one_plus_x_powr_approx_ex[OF this, of p] guess t . note t = this
    from t have "abs ((1 + x) powr p - 1 - p*x) = ¦p*(p - 1)¦ * (1 + t) powr (p - 2)/2 * x2"
      by (simp add: abs_mult)
    also from t(1) have "(1 + t) powr (p - 2)  max ((1/2) powr (p - 2)) ((3/2) powr (p - 2))"
      by (intro powr_upper_bound) simp_all
    finally show "abs ((1 + x) powr p - 1 - p*x)  k*x^2" 
      by (simp add: mult_left_mono mult_right_mono k_def)
  qed
qed

lemma one_plus_x_powr_Taylor2_bigo:
  assumes lim: "(f  0) F"
  shows   "(λx. (1 + f x) powr (p::real) - 1 - p * f x)  O[F](λx. f x ^ 2)"
proof -
  from one_plus_x_powr_Taylor2[of p] guess k .
  moreover from tendstoD[OF lim, of "1/2"] 
    have "eventually (λx. abs (f x) < 1/2) F" by (simp add: dist_real_def)
  ultimately have "eventually (λx. norm ((1 + f x) powr p - 1 - p * f x)  k * norm (f x ^ 2)) F"
    by (auto elim!: eventually_mono)
  thus ?thesis by (rule bigoI)
qed

lemma one_plus_x_powr_Taylor1_bigo:
  assumes lim: "(f  0) F"
  shows   "(λx. (1 + f x) powr (p::real) - 1)  O[F](λx. f x)"
proof -
  from assms have "(λx. (1 + f x) powr p - 1 - p * f x)  O[F](λx. (f x)2)"
    by (rule one_plus_x_powr_Taylor2_bigo)
  also from assms have "f  O[F](λ_. 1)" by (intro bigoI_tendsto) simp_all
  from landau_o.big.mult[of f F f, OF _ this] have "(λx. (f x)^2)  O[F](λx. f x)"
    by (simp add: power2_eq_square)
  finally have A: "(λx. (1 + f x) powr p - 1 - p * f x)  O[F](f)" .
  have B: "(λx. p * f x)  O[F](f)" by simp
  from sum_in_bigo(1)[OF A B] show ?thesis by simp
qed

lemma x_times_x_minus_1_nonneg: "x  0  x  1  (x::_::linordered_idom) * (x - 1)  0"
proof (elim disjE)
  assume x: "x  0"
  also have "0  x^2" by simp
  finally show "x * (x - 1)  0" by (simp add: power2_eq_square algebra_simps)
qed simp

lemma x_times_x_minus_1_nonpos: "x  0  x  1  (x::_::linordered_idom) * (x - 1)  0"
  by (intro mult_nonneg_nonpos) simp_all

lemma real_powr_at_bot:
  assumes "(a::real) > 1"
  shows   "((λx. a powr x)  0) at_bot"
proof-
  from assms have "filterlim (λx. ln a * x) at_bot at_bot"
    by (intro filterlim_tendsto_pos_mult_at_bot[OF tendsto_const _ filterlim_ident]) auto
  hence "((λx. exp (x * ln a))  0) at_bot"
    by (intro filterlim_compose[OF exp_at_bot]) (simp add: algebra_simps)
  thus ?thesis using assms unfolding powr_def by simp
qed

lemma real_powr_at_bot_neg:
  assumes "(a::real) > 0" "a < 1"
  shows   "filterlim (λx. a powr x) at_top at_bot"
proof-
  from assms have "LIM x at_bot. ln (inverse a) * -x :> at_top"
    by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] filterlim_uminus_at_top_at_bot)
       (simp_all add: ln_inverse)
  with assms have "LIM x at_bot. x * ln a :> at_top" 
    by (subst (asm) ln_inverse) (simp_all add: mult.commute)
  hence "LIM x at_bot. exp (x * ln a) :> at_top"
    by (intro filterlim_compose[OF exp_at_top]) simp
  thus ?thesis using assms unfolding powr_def by simp
qed

lemma real_powr_at_top_neg: 
  assumes "(a::real) > 0" "a < 1"
  shows   "((λx. a powr x)  0) at_top"
proof-
  from assms have "LIM x at_top. ln (inverse a) * x :> at_top"
    by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const])
       (simp_all add: filterlim_ident field_simps)
  with assms have "LIM x at_top. ln a * x :> at_bot"
    by (subst filterlim_uminus_at_bot) (simp add: ln_inverse)
  hence "((λx. exp (x * ln a))  0) at_top"
    by (intro filterlim_compose[OF exp_at_bot]) (simp_all add: mult.commute)
  with assms show ?thesis unfolding powr_def by simp
qed

lemma eventually_nat_real:
  assumes "eventually P (at_top :: real filter)"
  shows   "eventually (λx. P (real x)) (at_top :: nat filter)"
  using assms filterlim_real_sequentially
  unfolding filterlim_def le_filter_def eventually_filtermap by auto

end