Theory Akra_Bazzi_Library
section ‹Auxiliary lemmas›
theory Akra_Bazzi_Library
imports
Complex_Main
"Landau_Symbols.Landau_More"
"Pure-ex.Guess"
begin
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 "∃x∈I. 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 "∀n≥real 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
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)
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 * x⇧2"
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