Theory Landau_Symbols.Landau_More
theory Landau_More
imports
"HOL-Library.Landau_Symbols"
Landau_Simprocs
begin
lemma bigo_const_inverse [simp]:
assumes "filterlim f at_top F" "F ≠ bot"
shows "(λ_. c) ∈ O[F](λx. inverse (f x) :: real) ⟷ c = 0"
proof -
{
assume A: "(λ_. 1) ∈ O[F](λx. inverse (f x))"
from assms have "(λ_. 1) ∈ o[F](f)"
by (simp add: eventually_nonzero_simps smallomega_iff_smallo filterlim_at_top_iff_smallomega)
also from assms A have "f ∈ O[F](λ_. 1)"
by (simp add: eventually_nonzero_simps landau_divide_simps)
finally have False using assms by (simp add: landau_o.small_refl_iff)
}
thus ?thesis by (cases "c = 0") auto
qed
lemma smallo_const_inverse [simp]:
"filterlim f at_top F ⟹ F ≠ bot ⟹ (λ_. c :: real) ∈ o[F](λx. inverse (f x)) ⟷ c = 0"
by (auto dest: landau_o.small_imp_big)
lemma const_in_smallo_const [simp]: "(λ_. b) ∈ o(λ_ :: _ :: linorder. c) ⟷ b = 0" (is "?lhs ⟷ ?rhs")
by (cases "b = 0"; cases "c = 0") (simp_all add: landau_o.small_refl_iff)
lemma smallomega_1_conv_filterlim: "f ∈ ω[F](λ_. 1) ⟷ filterlim f at_infinity F"
by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)
lemma bigtheta_powr_1 [landau_simp]:
"eventually (λx. (f x :: real) ≥ 0) F ⟹ (λx. f x powr 1) ∈ Θ[F](f)"
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
lemma bigtheta_powr_0 [landau_simp]:
"eventually (λx. (f x :: real) ≠ 0) F ⟹ (λx. f x powr 0) ∈ Θ[F](λ_. 1)"
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
lemma bigtheta_powr_nonzero [landau_simp]:
"eventually (λx. (f x :: real) ≠ 0) F ⟹ (λx. if f x = 0 then g x else h x) ∈ Θ[F](h)"
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
lemma bigtheta_powr_nonzero' [landau_simp]:
"eventually (λx. (f x :: real) ≠ 0) F ⟹ (λx. if f x ≠ 0 then g x else h x) ∈ Θ[F](g)"
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
lemma bigtheta_powr_nonneg [landau_simp]:
"eventually (λx. (f x :: real) ≥ 0) F ⟹ (λx. if f x ≥ 0 then g x else h x) ∈ Θ[F](g)"
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
lemma bigtheta_powr_nonneg' [landau_simp]:
"eventually (λx. (f x :: real) ≥ 0) F ⟹ (λx. if f x < 0 then g x else h x) ∈ Θ[F](h)"
by (intro bigthetaI_cong) (auto elim!: eventually_mono)
lemma bigo_powr_iff:
assumes "0 < p" "eventually (λx. f x ≥ 0) F" "eventually (λx. g x ≥ 0) F"
shows "(λx. (f x :: real) powr p) ∈ O[F](λx. g x powr p) ⟷ f ∈ O[F](g)" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
with assms bigo_powr[OF this, of "inverse p"] show ?rhs
by (simp add: powr_powr landau_simps)
qed (insert assms, simp_all add: bigo_powr_nonneg)
lemma inverse_powr [simp]:
assumes "(x::real) ≥ 0"
shows "inverse x powr y = inverse (x powr y)"
proof (cases "x > 0")
assume x: "x > 0"
from x have "inverse x powr y = exp (y * ln (inverse x))" by (simp add: powr_def)
also have "ln (inverse x) = -ln x" by (simp add: x ln_inverse)
also have "exp (y * -ln x) = inverse (exp (y * ln x))" by (simp add: exp_minus)
also from x have "exp (y * ln x) = x powr y" by (simp add: powr_def)
finally show ?thesis .
qed (insert assms, simp)
lemma bigo_neg_powr_iff:
assumes "p < 0" "eventually (λx. f x ≥ 0) F" "eventually (λx. g x ≥ 0) F"
"eventually (λx. f x ≠ 0) F" "eventually (λx. g x ≠ 0) F"
shows "(λx. (f x :: real) powr p) ∈ O[F](λx. g x powr p) ⟷ g ∈ O[F](f)" (is "?lhs ⟷ ?rhs")
proof -
have "(λx. f x powr p) ∈ O[F](λx. g x powr p) ⟷
(λx. (inverse (f x)) powr -p) ∈ O[F](λx. (inverse (g x)) powr -p)"
using assms by (intro landau_o.big.cong_ex) (auto simp: powr_minus elim: eventually_mono)
also from assms have "… ⟷ ((λx. inverse (f x)) ∈ O[F](λx. inverse (g x)))"
by (subst bigo_powr_iff) simp_all
also from assms have "… ⟷ g ∈ O[F](f)" by (simp add: landau_o.big.inverse_cancel)
finally show ?thesis .
qed
lemma smallo_powr_iff:
assumes "0 < p" "eventually (λx. f x ≥ 0) F" "eventually (λx. g x ≥ 0) F"
shows "(λx. (f x :: real) powr p) ∈ o[F](λx. g x powr p) ⟷ f ∈ o[F](g)" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
with assms smallo_powr[OF this, of "inverse p"] show ?rhs
by (simp add: powr_powr landau_simps)
qed (insert assms, simp_all add: smallo_powr_nonneg)
lemma smallo_neg_powr_iff:
assumes "p < 0" "eventually (λx. f x ≥ 0) F" "eventually (λx. g x ≥ 0) F"
"eventually (λx. f x ≠ 0) F" "eventually (λx. g x ≠ 0) F"
shows "(λx. (f x :: real) powr p) ∈ o[F](λx. g x powr p) ⟷ g ∈ o[F](f)" (is "?lhs ⟷ ?rhs")
proof -
have "(λx. f x powr p) ∈ o[F](λx. g x powr p) ⟷
(λx. (inverse (f x)) powr -p) ∈ o[F](λx. (inverse (g x)) powr -p)"
using assms by (intro landau_o.small.cong_ex) (auto simp: powr_minus elim: eventually_mono)
also from assms have "… ⟷ ((λx. inverse (f x)) ∈ o[F](λx. inverse (g x)))"
by (subst smallo_powr_iff) simp_all
also from assms have "… ⟷ g ∈ o[F](f)" by (simp add: landau_o.small.inverse_cancel)
finally show ?thesis .
qed
lemma const_smallo_powr:
assumes "filterlim f at_top F" "F ≠ bot"
shows "(λ_. c :: real) ∈ o[F](λx. f x powr p) ⟷ p > 0 ∨ c = 0"
by (rule linorder_cases[of p 0]; cases "c = 0")
(insert assms smallo_powr_iff[of p "λ_. 1" F f] smallo_neg_powr_iff[of p f F "λ_. 1"],
auto simp: landau_simps eventually_nonzero_simps smallo_1_iff[of F f] not_less
dest: landau_o.small_asymmetric simp: eventually_False landau_o.small_refl_iff)
lemma bigo_const_powr:
assumes "filterlim f at_top F" "F ≠ bot"
shows "(λ_. c :: real) ∈ O[F](λx. f x powr p) ⟷ p ≥ 0 ∨ c = 0"
proof -
from assms have A: "(λ_. 1) ∈ o[F](f)"
by (simp add: filterlim_at_top_iff_smallomega smallomega_iff_smallo landau_o.small_imp_big)
hence B: "(λ_. 1) ∈ O[F](f)" "f ∉ O[F](λ_. 1)" using assms
by (auto simp: landau_o.small_imp_big dest: landau_o.small_big_asymmetric)
show ?thesis
by (rule linorder_cases[of p 0]; cases "c = 0")
(insert insert assms A B bigo_powr_iff[of p "λ_. 1" F f] bigo_neg_powr_iff[of p "λ_. 1" F f],
auto simp: landau_simps eventually_nonzero_simps not_less dest: landau_o.small_asymmetric)
qed
lemma filterlim_powr_at_top:
"(b::real) > 1 ⟹ filterlim (λx. b powr x) at_top at_top"
unfolding powr_def mult.commute[of _ "ln b"]
by (auto intro!: filterlim_compose[OF exp_at_top]
filterlim_tendsto_pos_mult_at_top filterlim_ident)
lemma power_smallo_exponential:
fixes b :: real
assumes b: "b > 1"
shows "(λx. x powr n) ∈ o(λx. b powr x)"
proof (rule smalloI_tendsto)
from assms have "filterlim (λx. x * ln b - n * ln x) at_top at_top"
using [[simproc add: simplify_landau_sum]]
by (simp add: filterlim_at_top_iff_smallomega eventually_nonzero_simps)
hence "((λx. exp (-(x * ln b - n * ln x))) ⤏ 0) at_top" (is ?A)
by (intro filterlim_compose[OF exp_at_bot]
filterlim_compose[OF filterlim_uminus_at_bot_at_top])
also have "?A ⟷ ((λx. x powr n / b powr x) ⤏ 0) at_top"
using b eventually_gt_at_top[of 0]
by (intro tendsto_cong)
(auto simp: exp_diff powr_def field_simps exp_of_nat_mult elim: eventually_mono)
finally show "((λx. x powr n / b powr x) ⤏ 0) at_top" .
qed (insert assms, simp_all add: eventually_nonzero_simps)
lemma powr_fast_growth_tendsto:
assumes gf: "g ∈ O[F](f)"
and n: "n ≥ 0"
and k: "k > 1"
and f: "filterlim f at_top F"
and g: "eventually (λx. g x ≥ 0) F"
shows "(λx. g x powr n) ∈ o[F](λx. k powr f x :: real)"
proof -
from f have f': "eventually (λx. f x ≥ 0) F" by (simp add: eventually_nonzero_simps)
from gf obtain c where c: "c > 0" "eventually (λx. norm (g x) ≤ c * norm (f x)) F"
by (elim landau_o.bigE)
from c(2) g f' have "eventually (λx. g x ≤ c * f x) F" by eventually_elim simp
from c(2) g f' have "eventually (λx. norm (g x powr n) ≤ norm (c powr n * f x powr n)) F"
by eventually_elim (insert n c(1), auto simp: powr_mult [symmetric] intro!: powr_mono2)
from landau_o.big_mono[OF this] c(1)
have "(λx. g x powr n) ∈ O[F](λx. f x powr n)" by simp
also from power_smallo_exponential f
have "(λx. f x powr n) ∈ o[F](λx. k powr f x)" by (rule landau_o.small.compose) fact+
finally show ?thesis .
qed
lemma bigo_abs_powr_iff [simp]:
"0 < p ⟹ (λx. ¦f x :: real¦ powr p) ∈ O[F](λx. ¦g x¦ powr p) ⟷ f ∈ O[F](g)"
by(subst bigo_powr_iff; simp)
lemma smallo_abs_powr_iff [simp]:
"0 < p ⟹ (λx. ¦f x :: real¦ powr p) ∈ o[F](λx. ¦g x¦ powr p) ⟷ f ∈ o[F](g)"
by(subst smallo_powr_iff; simp)
lemma const_smallo_inverse_powr:
assumes "filterlim f at_top at_top"
shows "(λ_ :: _ :: linorder. c :: real) ∈ o(λx. inverse (f x powr p)) ⟷ (p ≥ 0 ⟶ c = 0)"
proof(cases p "0 :: real" rule: linorder_cases)
case p: greater
have "(λ_. c) ∈ o(λx. inverse (f x powr p)) ⟷ (λ_. ¦c¦) ∈ o(λx. inverse (f x powr p))" by simp
also have "¦c¦ = ¦(¦c¦ powr (inverse p))¦ powr p" using p by(simp add: powr_powr)
also { have "eventually (λx. f x ≥ 0) at_top" using assms by(simp add: filterlim_at_top)
then have "o(λx. inverse (f x powr p)) = o(λx. ¦inverse (f x)¦ powr p)"
by(intro landau_o.small.cong)(auto elim!: eventually_rev_mp)
also have "(λ_. ¦(¦c¦ powr inverse p)¦ powr p) ∈ … ⟷ (λ_. ¦c¦ powr (inverse p)) ∈ o(λx. inverse (f x))"
using p by(rule smallo_abs_powr_iff)
also note calculation }
also have "(λ_. ¦c¦ powr (inverse p)) ∈ o(λx. inverse (f x)) ⟷ c = 0" using assms by simp
finally show ?thesis using p by simp
next
case equal
from assms have "eventually (λx. f x ≥ 1) at_top" using assms by(simp add: filterlim_at_top)
then have "o(λx. inverse (f x powr p)) = o(λx. 1)"
by(intro landau_o.small.cong)(auto simp add: equal elim!: eventually_rev_mp)
then show ?thesis using equal by simp
next
case less
from assms have nonneg: "∀⇩F x in at_top. 0 ≤ f x" by(simp add: filterlim_at_top)
with assms have "∀⇩F x in at_top. ¦¦c¦ powr (1 / - p)¦ / d ≤ ¦f x¦" (is "∀⇩F x in _. ?c ≤ _") if "d > 0" for d
by(fastforce dest!: spec[where x="?c"] simp add: filterlim_at_top elim: eventually_rev_mp)
then have "(λ_. ¦c¦ powr (1 / - p)) ∈ o(f)" by(intro landau_o.smallI)(simp add: field_simps)
then have "(λ_. ¦¦c¦ powr (1 / - p)¦ powr - p) ∈ o(λx. ¦f x¦ powr - p)"
using less by(subst smallo_powr_iff) simp_all
also have "(λ_. ¦¦c¦ powr (1 / - p)¦ powr - p) = (λ_. ¦c¦)" using less by(simp add: powr_powr)
also have "o(λx. ¦f x¦ powr - p) = o(λx. f x powr - p)" using nonneg
by(auto intro!: landau_o.small.cong elim: eventually_rev_mp)
finally have "(λ_. c) ∈ o(λx. f x powr - p)" by simp
with less show ?thesis by(simp add: powr_minus[symmetric])
qed
lemma bigo_const_inverse_powr:
assumes "filterlim f at_top at_top"
shows "(λ_ :: _ :: linorder. c :: real) ∈ O(λx. inverse (f x powr p)) ⟷ c = 0 ∨ p ≤ 0"
proof(cases p "0 :: real" rule: linorder_cases)
case p_pos: greater
have "(λ_. c) ∈ O(λx. inverse (f x powr p)) ⟷ (λ_. ¦c¦) ∈ O(λx. inverse (f x powr p))" by simp
also have "¦c¦ = ¦(¦c¦ powr inverse p)¦ powr p" using p_pos by(simp add: powr_powr)
also { have "eventually (λx. f x ≥ 0) at_top" using assms by(simp add: filterlim_at_top)
then have "O(λx. inverse (f x powr p)) = O(λx. ¦inverse (f x)¦ powr p)"
by(intro landau_o.big.cong)(auto elim!: eventually_rev_mp)
also have "(λ_. ¦(¦c¦ powr inverse p)¦ powr p) ∈ … ⟷
(λ_. ¦c¦ powr (inverse p)) ∈ O(λx. inverse (f x))"
using p_pos by (rule bigo_abs_powr_iff)
also note calculation }
also have "(λ_. ¦c¦ powr (inverse p)) ∈ O(λx. inverse (f x)) ⟷ c = 0" using assms by simp
finally show ?thesis using p_pos by simp
next
case equal
from assms have "eventually (λx. f x ≥ 1) at_top" using assms by(simp add: filterlim_at_top)
then have "O(λx. inverse (f x powr p)) = O(λx. 1)"
by(intro landau_o.big.cong) (auto simp add: equal elim!: eventually_rev_mp)
then show ?thesis using equal by simp
next
case less
from assms have *: "∀⇩F x in at_top. 1 ≤ f x" by(simp add: filterlim_at_top)
then have "(λ_. ¦c¦ powr (1 / - p)) ∈ O(f)"
by(intro bigoI[where c="¦c¦ powr (1 / - p)"])
(auto intro: order_trans[OF _ mult_left_mono, rotated] elim!: eventually_rev_mp[OF _ always_eventually])
then have "(λ_. ¦¦c¦ powr (1 / - p)¦ powr - p) ∈ O(λx. ¦f x¦ powr - p)"
using less by (subst bigo_powr_iff) simp_all
also have "(λ_. ¦¦c¦ powr (1 / - p)¦ powr - p) = (λ_. ¦c¦)" using less by(simp add: powr_powr)
also have "O(λx. ¦f x¦ powr - p) = O(λx. f x powr - p)" using *
by (auto intro!: landau_o.big.cong elim: eventually_rev_mp)
finally have "(λ_. c) ∈ O(λx. f x powr - p)" by simp
thus ?thesis using less by (simp add: powr_minus[symmetric])
qed
end