Theory Landau_Ext
section ‹Landau Symbols›
theory Landau_Ext
imports
"HOL-Library.Landau_Symbols"
"HOL.Topological_Spaces"
begin
text ‹This section contains results about Landau Symbols in addition to "HOL-Library.Landau".›
lemma landau_sum:
assumes "eventually (λx. g1 x ≥ (0::real)) F"
assumes "eventually (λx. g2 x ≥ 0) F"
assumes "f1 ∈ O[F](g1)"
assumes "f2 ∈ O[F](g2)"
shows "(λx. f1 x + f2 x) ∈ O[F](λx. g1 x + g2 x)"
proof -
obtain c1 where a1: "c1 > 0" and b1: "eventually (λx. abs (f1 x) ≤ c1 * abs (g1 x)) F"
using assms(3) by (simp add:bigo_def, blast)
obtain c2 where a2: "c2 > 0" and b2: "eventually (λx. abs (f2 x) ≤ c2 * abs (g2 x)) F"
using assms(4) by (simp add:bigo_def, blast)
have "eventually (λx. abs (f1 x + f2 x) ≤ (max c1 c2) * abs (g1 x + g2 x)) F"
proof (rule eventually_mono[OF eventually_conj[OF b1 eventually_conj[OF b2 eventually_conj[OF assms(1,2)]]]])
fix x
assume a: "¦f1 x¦ ≤ c1 * ¦g1 x¦ ∧ ¦f2 x¦ ≤ c2 * ¦g2 x¦ ∧ 0 ≤ g1 x ∧ 0 ≤ g2 x"
have "¦f1 x + f2 x¦ ≤ ¦f1 x ¦ + ¦f2 x¦" using abs_triangle_ineq by blast
also have "... ≤ c1 * ¦g1 x¦ + c2 * ¦g2 x¦" using a add_mono by blast
also have "... ≤ max c1 c2 * ¦g1 x¦ + max c1 c2 * ¦g2 x¦"
by (intro add_mono mult_right_mono) auto
also have "... = max c1 c2 * (¦g1 x¦ + ¦g2 x¦)"
by (simp add:algebra_simps)
also have "... ≤ max c1 c2 * (¦g1 x + g2 x¦)"
using a a1 a2 by (intro mult_left_mono) auto
finally show "¦f1 x + f2 x¦ ≤ max c1 c2 * ¦g1 x + g2 x¦"
by (simp add:algebra_simps)
qed
hence " 0 < max c1 c2 ∧ (∀⇩F x in F. ¦f1 x + f2 x¦ ≤ max c1 c2 * ¦g1 x + g2 x¦)"
using a1 a2 by linarith
thus ?thesis
by (simp add: bigo_def, blast)
qed
lemma landau_sum_1:
assumes "eventually (λx. g1 x ≥ (0::real)) F"
assumes "eventually (λx. g2 x ≥ 0) F"
assumes "f ∈ O[F](g1)"
shows "f ∈ O[F](λx. g1 x + g2 x)"
proof -
have "f = (λx. f x + 0)" by simp
also have "... ∈ O[F](λx. g1 x + g2 x)"
using assms zero_in_bigo by (intro landau_sum)
finally show ?thesis by simp
qed
lemma landau_sum_2:
assumes "eventually (λx. g1 x ≥ (0::real)) F"
assumes "eventually (λx. g2 x ≥ 0) F"
assumes "f ∈ O[F](g2)"
shows "f ∈ O[F](λx. g1 x + g2 x)"
proof -
have "f = (λx. 0 + f x)" by simp
also have "... ∈ O[F](λx. g1 x + g2 x)"
using assms zero_in_bigo by (intro landau_sum)
finally show ?thesis by simp
qed
lemma landau_ln_3:
assumes "eventually (λx. (1::real) ≤ f x) F"
assumes "f ∈ O[F](g)"
shows "(λx. ln (f x)) ∈ O[F](g)"
proof -
have "1 ≤ x ⟹ ¦ln x¦ ≤ ¦x¦" for x :: real
using ln_bound by auto
hence "(λx. ln (f x)) ∈ O[F](f)"
by (intro landau_o.big_mono eventually_mono[OF assms(1)]) simp
thus ?thesis
using assms(2) landau_o.big_trans by blast
qed
lemma landau_ln_2:
assumes "a > (1::real)"
assumes "eventually (λx. 1 ≤ f x) F"
assumes "eventually (λx. a ≤ g x) F"
assumes "f ∈ O[F](g)"
shows "(λx. ln (f x)) ∈ O[F](λx. ln (g x))"
proof -
obtain c where a: "c > 0" and b: "eventually (λx. abs (f x) ≤ c * abs (g x)) F"
using assms(4) by (simp add:bigo_def, blast)
define d where "d = 1 + (max 0 (ln c)) / ln a"
have d:"eventually (λx. abs (ln (f x)) ≤ d * abs (ln (g x))) F"
proof (rule eventually_mono[OF eventually_conj[OF b eventually_conj[OF assms(3,2)]]])
fix x
assume c:"¦f x¦ ≤ c * ¦g x¦ ∧ a ≤ g x ∧ 1 ≤ f x"
have "abs (ln (f x)) = ln (f x)"
by (subst abs_of_nonneg, rule ln_ge_zero, metis c, simp)
also have "... ≤ ln (c * abs (g x))"
using c assms(1) mult_pos_pos[OF a] by auto
also have "... ≤ ln c + ln (abs (g x))"
using c assms(1)
by (simp add: ln_mult[OF a])
also have "... ≤ (d-1)*ln a + ln (g x)"
using assms(1) c
by (intro add_mono iffD2[OF ln_le_cancel_iff], simp_all add:d_def)
also have "... ≤ (d-1)* ln (g x) + ln (g x)"
using assms(1) c
by (intro add_mono mult_left_mono iffD2[OF ln_le_cancel_iff], simp_all add:d_def)
also have "... = d * ln (g x)" by (simp add:algebra_simps)
also have "... = d * abs (ln (g x))"
using c assms(1) by auto
finally show "abs (ln (f x)) ≤ d * abs (ln (g x))" by simp
qed
hence "∀⇩F x in F. ¦ln (f x)¦ ≤ d * ¦ln (g x)¦"
by simp
moreover have "0 < d"
unfolding d_def using assms(1)
by (intro add_pos_nonneg divide_nonneg_pos, auto)
ultimately show ?thesis
by (auto simp:bigo_def)
qed
lemma landau_real_nat:
fixes f :: "'a ⇒ int"
assumes "(λx. of_int (f x)) ∈ O[F](g)"
shows "(λx. real (nat (f x))) ∈ O[F](g)"
proof -
obtain c where a: "c > 0" and b: "eventually (λx. abs (of_int (f x)) ≤ c * abs (g x)) F"
using assms(1) by (simp add:bigo_def, blast)
have "∀⇩F x in F. real (nat (f x)) ≤ c * ¦g x¦"
by (rule eventually_mono[OF b], simp)
thus ?thesis using a
by (auto simp:bigo_def)
qed
lemma landau_ceil:
assumes "(λ_. 1) ∈ O[F'](g)"
assumes "f ∈ O[F'](g)"
shows "(λx. real_of_int ⌈f x⌉) ∈ O[F'](g)"
proof -
have "(λx. real_of_int ⌈f x⌉) ∈ O[F'](λx. 1 + abs (f x))"
by (intro landau_o.big_mono always_eventually allI, simp, linarith)
also have "(λx. 1 + abs(f x)) ∈ O[F'](g)"
using assms(2) by (intro sum_in_bigo assms(1), auto)
finally show ?thesis by simp
qed
lemma landau_rat_ceil:
assumes "(λ_. 1) ∈ O[F'](g)"
assumes "(λx. real_of_rat (f x)) ∈ O[F'](g)"
shows "(λx. real_of_int ⌈f x⌉) ∈ O[F'](g)"
proof -
have a:"¦real_of_int ⌈x⌉¦ ≤ 1 + real_of_rat ¦x¦" for x :: rat
proof (cases "x ≥ 0")
case True
then show ?thesis
by (simp, metis add.commute of_int_ceiling_le_add_one of_rat_ceiling)
next
case False
have "real_of_rat x - 1 ≤ real_of_rat x"
by simp
also have "... ≤ real_of_int ⌈x⌉"
by (metis ceiling_correct of_rat_ceiling)
finally have " real_of_rat (x)-1 ≤ real_of_int ⌈x⌉" by simp
hence "- real_of_int ⌈x⌉ ≤ 1 + real_of_rat (- x)"
by (simp add: of_rat_minus)
then show ?thesis using False by simp
qed
have "(λx. real_of_int ⌈f x⌉) ∈ O[F'](λx. 1 + abs (real_of_rat (f x)))"
using a
by (intro landau_o.big_mono always_eventually allI, simp)
also have "(λx. 1 + abs (real_of_rat (f x))) ∈ O[F'](g)"
using assms
by (intro sum_in_bigo assms(1), subst landau_o.big.abs_in_iff, simp)
finally show ?thesis by simp
qed
lemma landau_nat_ceil:
assumes "(λ_. 1) ∈ O[F'](g)"
assumes "f ∈ O[F'](g)"
shows "(λx. real (nat ⌈f x⌉)) ∈ O[F'](g)"
using assms
by (intro landau_real_nat landau_ceil, auto)
lemma eventually_prod1':
assumes "B ≠ bot"
assumes " (∀⇩F x in A. P x)"
shows "(∀⇩F x in A ×⇩F B. P (fst x))"
proof -
have "(∀⇩F x in A ×⇩F B. P (fst x)) = (∀⇩F (x,y) in A ×⇩F B. P x)"
by (simp add:case_prod_beta')
also have "... = (∀⇩F x in A. P x)"
by (subst eventually_prod1[OF assms(1)], simp)
finally show ?thesis using assms(2) by simp
qed
lemma eventually_prod2':
assumes "A ≠ bot"
assumes " (∀⇩F x in B. P x)"
shows "(∀⇩F x in A ×⇩F B. P (snd x))"
proof -
have "(∀⇩F x in A ×⇩F B. P (snd x)) = (∀⇩F (x,y) in A ×⇩F B. P y)"
by (simp add:case_prod_beta')
also have "... = (∀⇩F x in B. P x)"
by (subst eventually_prod2[OF assms(1)], simp)
finally show ?thesis using assms(2) by simp
qed
lemma sequentially_inf: "∀⇩F x in sequentially. n ≤ real x"
by (meson eventually_at_top_linorder nat_ceiling_le_eq)
instantiation rat :: linorder_topology
begin
definition open_rat :: "rat set ⇒ bool"
where "open_rat = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))"
instance
by standard (rule open_rat_def)
end
lemma inv_at_right_0_inf:
"∀⇩F x in at_right 0. c ≤ 1 / real_of_rat x"
proof -
have a:" c ≤ 1 / real_of_rat x" if b:" x ∈ {0<..<1 / rat_of_int (max ⌈c⌉ 1)}" for x
proof -
have "c * real_of_rat x ≤ real_of_int (max ⌈c⌉ 1) * real_of_rat x"
using b by (intro mult_right_mono, linarith, auto)
also have "... < real_of_int (max ⌈c⌉ 1) * real_of_rat (1/rat_of_int (max ⌈c⌉ 1) )"
using b by (intro mult_strict_left_mono iffD2[OF of_rat_less], auto)
also have "... ≤ 1"
by (simp add:of_rat_divide)
finally have "c * real_of_rat x ≤ 1" by simp
moreover have "0 < real_of_rat x"
using b by simp
ultimately show ?thesis by (subst pos_le_divide_eq, auto)
qed
show ?thesis
using a
by (intro eventually_at_rightI[where b="1/rat_of_int (max ⌈c⌉ 1)"], simp_all)
qed
end