Theory Karatsuba.Karatsuba_Runtime_Lemmas

theory Karatsuba_Runtime_Lemmas
  imports Complex_Main "Akra_Bazzi.Akra_Bazzi_Method"
begin

text "An explicit bound for a specific class of recursive functions."

context
  fixes a b c d :: nat
  fixes f :: "nat  nat"
  assumes small_bounds: "f 0  a" "f (Suc 0)  a"
  assumes recursive_bound: "n. n > 1  f n  c * n + d + f (n div 2)"
begin

private fun g where
"g 0 = a"
| "g (Suc 0) = a"
| "g n = c * n + d + g (n div 2)"

private lemma f_g_bound: "f n  g n"
  apply (induction n rule: g.induct)
  subgoal using small_bounds by simp
  subgoal using small_bounds by simp
  subgoal for x using recursive_bound[of "Suc (Suc x)"] by auto
  done

private lemma g_mono_aux: "a  g n"
  by (induction n rule: g.induct) simp_all

private lemma g_mono: "m  n  g m  g n"
proof (induction m arbitrary: n rule: g.induct)
  case 1
  then show ?case using g_mono_aux by simp
next
  case 2
  then show ?case using g_mono_aux by simp
next
  case (3 x)
  then obtain y where "n = Suc (Suc y)" using Suc_le_D by blast
  have "g (Suc (Suc x)) = c * Suc (Suc x) + d + g (Suc (Suc x) div 2)"
    by simp
  also have "...  c * n + d + g (n div 2)"
    using 3
    by (metis add_mono add_mono_thms_linordered_semiring(3) div_le_mono nat_mult_le_cancel_disj)
  finally show ?case using n = Suc (Suc y) by simp
qed

private lemma g_powers_of_2: "g (2 ^ n) = d * n + c * (2 ^ (n + 1) - 2) + a"
proof (induction n)
  case (Suc n)
  then obtain n' where "2 ^ Suc n = Suc (Suc n')"
    by (metis g.cases less_exp not_less_eq zero_less_Suc)
  then have "g (2 ^ Suc n) = c * 2 ^ Suc n + d + g (2 ^ n)"
    by (metis g.simps(3) nonzero_mult_div_cancel_right power_Suc2 zero_neq_numeral)
  also have "... = c * 2 ^ Suc n + d + d * n + c * (2 ^ (n + 1) - 2) + a"
    using Suc by simp
  also have "... = d * Suc n + c * (2 ^ Suc n + (2 ^ (n + 1) - 2)) + a"
    using add_mult_distrib2[symmetric, of c] by simp
  finally show ?case by simp
qed simp

private lemma pow_ineq:
  assumes "m  (1 :: nat)"
  assumes "p  2"
  shows "p ^ m > m"
  using assms
  apply (induction m)
  subgoal by simp
  subgoal for m
    by (cases m) (simp_all add: less_trans_Suc)
  done

private lemma next_power_of_2:
  assumes "m  (1 :: nat)"
  shows "n k. m = 2 ^ n + k  k < 2 ^ n"
proof -
  from ex_power_ivl1[OF order.refl assms] obtain n where "2 ^ n  m" "m < 2 ^ (n + 1)"
    by auto
  then have "m = 2 ^ n + (m - 2 ^ n)" "m - 2 ^ n < 2 ^ n" by simp_all
  then show ?thesis by blast
qed

lemma div_2_recursion_linear: "f n  (2 * d + 4 * c) * n + a"
proof (cases "n  1")
  case True
  then obtain m k where "n = 2 ^ m + k" "k < 2 ^ m" using next_power_of_2 by blast
  have "f n  g n" using f_g_bound by simp
  also have "...  g (2 ^ m + 2 ^ m)" using n = 2 ^ m + k k < 2 ^ m g_mono by simp
  also have "... = d * Suc m + c * (2 ^ (Suc m + 1) - 2) + a"
    using g_powers_of_2[of "Suc m"]
    apply (subst mult_2[symmetric])
    apply (subst power_Suc[symmetric])
    .
  also have "...  d * Suc m + c * 2 ^ (Suc m + 1) + a" by simp
  also have "...  d * 2 ^ Suc m + c * 2 ^ (Suc m + 1) + a" using less_exp[of "Suc m"]
    by (meson add_le_mono less_or_eq_imp_le mult_le_mono)
  also have "... = (2 * d + 4 * c) * 2 ^ m + a" using mult.assoc add_mult_distrib by simp
  also have "...  (2 * d + 4 * c) * n + a"
    using n = 2 ^ m + k power_increasing[of m n] by simp
  finally show ?thesis .
next
  case False
  then have "n = 0" by simp
  then show ?thesis using small_bounds by simp
qed

end

text "General Lemmas for Landau notation."

lemma landau_o_plus_aux':
  fixes f g
  assumes "f  o[F](g)"
  shows "O[F](g) = O[F](λx. f x + g x)"
  apply (intro equalityI subsetI)
  subgoal using landau_o.big.trans[OF _ landau_o.plus_aux[OF assms]] by simp
  subgoal for h
    using assms by simp
  done

lemma powr_bigo_linear_index_transformation:
  fixes fl :: "nat  nat"
  fixes f :: "nat  real"
  assumes "(λx. real (fl x))  O(λn. real n)"
  assumes "f  O(λn. real n powr p)"
  assumes "p > 0"
  shows "f  fl  O(λn. real n powr p)"
proof -
  obtain c1 where "c1 > 0" "F x in sequentially. norm (real (fl x))  c1 * norm (real x)"
    using landau_o.bigE[OF assms(1)] by auto
  then obtain N1 where fl_bound: "x. x  N1  norm (real (fl x))  c1 * norm (real x)"
    unfolding eventually_at_top_linorder by blast
  obtain c2 where "c2 > 0" "F x in sequentially. norm (f x)  c2 * norm (real x powr p)"
    using landau_o.bigE[OF assms(2)] by auto
  then obtain N2 where f_bound: "x. x  N2  norm (f x)  c2 * norm (real x powr p)"
    unfolding eventually_at_top_linorder by blast

  define cf :: real where "cf = Max {norm (f y) | y. y  N2}"
  then have "cf  0" using Max_in[of "{norm (f y) | y. y  N2}"] norm_ge_zero by fastforce
  define c where "c = c2 * c1 powr p"
  then have "c > 0" using c1 > 0 c2 > 0 by simp

  have "x. x  N1  norm (f (fl x))  cf + c * norm (real x) powr p"
  proof (intro allI impI)
    fix x
    assume "x  N1"
    show "norm (f (fl x))  cf + c * norm (real x) powr p"
    proof (cases "fl x  N2")
      case True
      then have "norm (f (fl x))  c2 * norm (real (fl x) powr p)"
        using f_bound by simp
      also have "... = c2 * norm (real (fl x)) powr p"
        by simp
      also have "...  c2 * (c1 * norm (real x)) powr p"
        apply (intro mult_mono order.refl powr_mono2 norm_ge_zero)
        subgoal using p > 0 by simp
        subgoal using fl_bound x  N1 by simp
        subgoal using c2 > 0 by simp
        subgoal by simp
        done
      also have "... = c2 * (c1 powr p * norm (real x) powr p)"
        apply (intro arg_cong[where f = "(*) c2"] powr_mult norm_ge_zero)
        using c1 > 0 by simp
      also have "... = c * norm (real x) powr p" unfolding c_def by simp
      also have "...  cf + c * norm (real x) powr p" using cf  0 by simp
      finally show ?thesis .
    next
      case False
      then have "norm (f (fl x))  cf" unfolding cf_def
        by (intro Max_ge) auto
      also have "...  cf + c * norm (real x) powr p"
        using c > 0 by simp
      finally show ?thesis .
    qed
  qed
  then have "f  fl  O(λx. cf + c * (real x) powr p)"
    apply (intro landau_o.big_mono)
    unfolding eventually_at_top_linorder comp_apply by fastforce
  also have "... = O(λx. c * (real x) powr p)"
  proof (intro landau_o_plus_aux'[symmetric])
    have "(λx. cf)  O(λx. real x powr 0)" by simp
    moreover have "(λx. real x powr 0)  o(λx. real x powr p)"
      using iffD2[OF powr_smallo_iff, OF filterlim_real_sequentially sequentially_bot p > 0] .
    ultimately have "(λx. cf)  o(λx. real x powr p)"
      by (rule landau_o.big_small_trans)
    also have "... = o(λx. c * (real x) powr p)"
      using landau_o.small.cmult c > 0 by simp
    finally show "(λx. cf)  ..." .
  qed
  also have "... = O(λx. (real x) powr p)" using landau_o.big.cmult c > 0 by simp
  finally show ?thesis .
qed

lemma real_mono: "(a  b) = (real a  real b)"
  by simp

lemma real_linear: "real (a + b) = real a + real b"
  by simp

lemma real_multiplicative: "real (a * b) = real a * real b"
  by simp

lemma (in landau_pair) big_1_mult_left:
  fixes f g h
  assumes "f  L F (g)" "h  L F (λ_. 1)"
  shows "(λx. h x * f x)  L F (g)"
proof -
  have "(λx. f x * h x)  L F (g)" using assms by (rule big_1_mult)
  also have "(λx. f x * h x) = (λx. h x * f x)" by auto
  finally show ?thesis .
qed

lemma norm_nonneg: "x  0  norm x = x" by simp

lemma landau_mono_always:
  fixes f g
  assumes "x. f x  (0 :: real)" "x. g x  0"
  assumes "x. f x  g x"
  shows "f  O[F](g)"
  apply (intro landau_o.bigI[of 1])
  using assms by simp_all

end