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