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