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)"
        by (intro arg_cong[where f = "(*) c2"] powr_mult norm_ge_zero)
      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