Theory Negligible

(* Title: Negligible.thy
  Author: Andreas Lochbihler, ETH Zurich *)

section ‹Negligibility›

theory Negligible imports
  Complex_Main
  Landau_Symbols.Landau_More
begin

named_theorems negligible_intros

definition negligible :: "(nat ⇒ real) ⇒ bool" (* TODO: generalise types? *)
where "negligible f ⟷ (∀c>0. f ∈ o(λx. inverse (x powr c)))"

lemma negligibleI [intro?]:
  "(⋀c. c > 0 ⟹ f ∈ o(λx. inverse (x powr c))) ⟹ negligible f"
unfolding negligible_def by(simp)

lemma negligibleD:
  "⟦ negligible f; c > 0 ⟧ ⟹ f ∈ o(λx. inverse (x powr c))"
unfolding negligible_def by(simp)

lemma negligibleD_real:
  assumes "negligible f"
  shows "f ∈ o(λx. inverse (x powr c))"
proof -
  let ?c = "max 1 c"
  have "f ∈ o(λx. inverse (x powr ?c))" using assms by(rule negligibleD) simp
  also have "(λx. x powr c) ∈ O(λx. real x powr max 1 c)"
    by(rule bigoI[where c=1])(auto simp add: eventually_at_top_linorder intro!: exI[where x=1] powr_mono)
  then have "(λx. inverse (real x powr max 1 c)) ∈ O(λx. inverse (x powr c))"
    by(auto simp add: eventually_at_top_linorder exI[where x=1] intro: landau_o.big.inverse)
  finally show ?thesis .
qed

lemma negligible_mono: "⟦ negligible g; f ∈ O(g) ⟧ ⟹ negligible f"
by(rule negligibleI)(drule (1) negligibleD; erule (1) landau_o.big_small_trans)

lemma negligible_le: "⟦ negligible g; ⋀η. ¦f η¦ ≤ g η ⟧ ⟹ negligible f"
by(erule negligible_mono)(force intro: order_trans intro!: eventually_sequentiallyI landau_o.big_mono)

lemma negligible_K0 [negligible_intros, simp, intro!]: "negligible (λ_. 0)"
by(rule negligibleI) simp

lemma negligible_0 [negligible_intros, simp, intro!]: "negligible 0"
by(simp add: zero_fun_def)

lemma negligible_const_iff [simp]: "negligible (λ_. c :: real) ⟷ c = 0"
by(auto simp add: negligible_def const_smallo_inverse_powr filterlim_real_sequentially dest!: spec[where x=1])

lemma not_negligible_1: "¬ negligible (λ_. 1 :: real)"
by simp

lemma negligible_plus [negligible_intros]:
  "⟦ negligible f; negligible g ⟧ ⟹ negligible (λη. f η + g η)"
by(auto intro!: negligibleI dest!: negligibleD intro: sum_in_smallo)

lemma negligible_uminus [simp]: "negligible (λη. - f η) ⟷ negligible f"
by(simp add: negligible_def)

lemma negligible_uminusI [negligible_intros]: "negligible f ⟹ negligible (λη. - f η)"
by simp

lemma negligible_minus [negligible_intros]:
  "⟦ negligible f; negligible g ⟧ ⟹ negligible (λη. f η - g η)"
by(auto simp add: uminus_add_conv_diff[symmetric] negligible_plus simp del: uminus_add_conv_diff)

lemma negligible_cmult: "negligible (λη. c * f η) ⟷ negligible f ∨ c = 0"
by(auto intro!: negligibleI dest!: negligibleD)

lemma negligible_cmultI [negligible_intros]:
  "(c ≠ 0 ⟹ negligible f) ⟹ negligible (λη. c * f η)"
by(auto simp add: negligible_cmult)

lemma negligible_multc: "negligible (λη. f η * c) ⟷ negligible f ∨ c = 0"
by(subst mult.commute)(simp add: negligible_cmult)

lemma negligible_multcI [negligible_intros]:
  "(c ≠ 0 ⟹ negligible f) ⟹ negligible (λη. f η * c)"
by(auto simp add: negligible_multc)

lemma negligible_times [negligible_intros]:
  assumes f: "negligible f"
  and g: "negligible g"
  shows "negligible (λη. f η * g η :: real)"
proof
  fix c :: real
  assume "0 < c"
  hence "0 < c / 2" by simp
  from negligibleD[OF f this] negligibleD[OF g this]
  have "(λη. f η * g η) ∈ o(λx. inverse (x powr (c / 2)) * inverse (x powr (c / 2)))"
    by(rule landau_o.small_mult)
  also have "… = o(λx. inverse (x powr c))"
    by(rule landau_o.small.cong)(auto simp add: inverse_mult_distrib[symmetric] powr_add[symmetric] eventually_at_top_linorder intro!: exI[where x=1] simp del: inverse_mult_distrib)
  finally show "(λη. f η * g η) ∈ …" .
qed

lemma negligible_power [negligible_intros]:
  assumes "negligible f"
  and "n > 0"
  shows "negligible (λη. f η ^ n :: real)"
using ‹n > 0›
proof(induct n)
  case (Suc n)
  thus ?case using ‹negligible f› by(cases n)(simp_all add: negligible_times)
qed simp

lemma negligible_powr [negligible_intros]:
  assumes f: "negligible f"
  and p: "p > 0"         
  shows "negligible (λx. ¦f x¦ powr p :: real)"
proof
  fix c :: real
  let ?c = "c / p"
  assume c: "0 < c"
  with p have "0 < ?c" by simp
  with f have "f ∈ o(λx. inverse (x powr ?c))" by(rule negligibleD)
  hence "(λx. ¦f x¦ powr p) ∈ o(λx. ¦inverse (x powr ?c)¦ powr p)" using p by(rule smallo_powr)
  also have "… = o(λx. inverse (x powr c))"
    apply(rule landau_o.small.cong) using p by(auto simp add: powr_powr)
  finally show "(λx. ¦f x¦ powr p) ∈ …" .
qed

lemma negligible_abs [simp]: "negligible (λx. ¦f x¦) ⟷ negligible f"
by(simp add: negligible_def)

lemma negligible_absI [negligible_intros]: "negligible f ⟹ negligible (λx. ¦f x¦)"
by(simp)

lemma negligible_powrI [negligible_intros]:
  assumes "0 ≤ k" "k < 1"
  shows "negligible (λx. k powr x)"
proof(cases "k = 0")
  case True
  thus ?thesis by simp
next
  case False
  show ?thesis
  proof
    fix c :: real
    assume "0 < c"
    then have "(λx. real x powr c) ∈ o(λx. inverse k powr real x)" using assms False
      by(intro powr_fast_growth_tendsto)(simp_all add: one_less_inverse_iff filterlim_real_sequentially)
    then have "(λx. inverse (k powr - real x)) ∈ o(λx. inverse (real x powr c))" using assms
      by(intro landau_o.small.inverse)(auto simp add: False eventually_sequentially powr_minus intro: exI[where x=1])
    also have "(λx. inverse (k powr - real x)) = (λx. k powr real x)" by(simp add: powr_minus)
    finally show "… ∈ o(λx. inverse (x powr c))" .
  qed
qed

lemma negligible_powerI [negligible_intros]:
  fixes k :: real
  assumes "¦k¦ < 1"
  shows "negligible (λn. k ^ n)"
proof(cases "k = 0")
  case True
  show ?thesis using negligible_K0
    by(rule negligible_mono)(auto intro: exI[where x=1] simp add: True eventually_at_top_linorder)
next
  case False
  hence "0 < ¦k¦" by auto
  from assms have "negligible (λx. ¦k¦ powr real x)" using negligible_powrI[of "¦k¦"] by simp
  hence "negligible (λx. ¦k¦ ^ x)" using False
    by(elim negligible_mono)(simp add: powr_realpow)
  then show ?thesis by(simp add: power_abs[symmetric])
qed

lemma negligible_inverse_powerI [negligible_intros]: "¦k¦ > 1 ⟹ negligible (λη. 1 / k ^ η)"
using negligible_powerI[of "1 / k"] by(simp add: power_one_over)

inductive polynomial :: "(nat ⇒ real) ⇒ bool"
  for f
where "f ∈ O(λx. x powr n) ⟹ polynomial f"

lemma negligible_times_poly:
  assumes f: "negligible f"
  and g: "g ∈ O(λx. x powr n)"
  shows "negligible (λx. f x * g x)"
proof
  fix c :: real
  assume c: "0 < c"
  from negligibleD_real[OF f] g
  have "(λx. f x * g x) ∈ o(λx. inverse (x powr (c + n)) * x powr n)"
    by(rule landau_o.small_big_mult)
  also have "… = o(λx. inverse (x powr c))"
    by(rule landau_o.small.cong)(auto simp add: powr_minus[symmetric] powr_add[symmetric] intro!: exI[where x=0])
  finally show "(λx. f x * g x) ∈ o(λx. inverse (x powr c))" .
qed

lemma negligible_poly_times:
  "⟦ f ∈ O(λx. x powr n); negligible g ⟧ ⟹ negligible (λx. f x * g x)"
by(subst mult.commute)(rule negligible_times_poly)

lemma negligible_times_polynomial [negligible_intros]:
  "⟦ negligible f; polynomial g ⟧ ⟹ negligible (λx. f x * g x)"
by(clarsimp simp add: polynomial.simps negligible_times_poly)

lemma negligible_polynomial_times [negligible_intros]:
  "⟦ polynomial f; negligible g ⟧ ⟹ negligible (λx. f x * g x)"
by(clarsimp simp add: polynomial.simps negligible_poly_times)

lemma negligible_divide_poly1:
  "⟦ f ∈ O(λx. x powr n); negligible (λη. 1 / g η) ⟧ ⟹ negligible (λη. real (f η) / g η)"
by(drule (1) negligible_times_poly) simp

lemma negligible_divide_polynomial1 [negligible_intros]:
  "⟦ polynomial f; negligible (λη. 1 / g η) ⟧ ⟹ negligible (λη. real (f η) / g η)"
by(clarsimp simp add: polynomial.simps negligible_divide_poly1)

end