weblib/arithmetics/bigO.ma

   1 include "arithmetics/nat.ma".
   2 include "basics/sets.ma".
   3
   4 (*  O f g means g ∈ O(f) *)
   5 definition O: relation (nat→nat) ≝
   6   λf,g. ∃c.∃n0.∀n. n0 ≤ n → g n ≤ c* (f n).
   7
   8 lemma O_refl: ∀s. O s s.
   9 #s %{1} %{0} #n #_ >commutative_times <times_n_1 @le_n qed.
  10
  11 lemma O_trans: ∀s1,s2,s3. O s2 s1 → O s3 s2 → O s3 s1.
  12 #s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1*c2)}
  13 %{(max n1 n2)} #n #Hmax
  14 @(transitive_le … (H1 ??)) [@(le_maxl … Hmax)]
  15 >associative_times @le_times [//|@H2 @(le_maxr … Hmax)]
  16 qed.
  17
  18 lemma sub_O_to_O: ∀s1,s2. O s1 ⊆ O s2 → O s2 s1.
  19 #s1 #s2 #H @H // qed.
  20
  21 lemma O_to_sub_O: ∀s1,s2. O s2 s1 → O s1 ⊆ O s2.
  22 #s1 #s2 #H #g #Hg @(O_trans … H) // qed.
  23
  24 definition sum_f ≝ λf,g:nat→nat.λn.f n + g n.
  25 interpretation "function sum" 'plus f g = (sum_f f g).
  26
  27 lemma O_plus: ∀f,g,s. O s f → O s g → O s (f+g).
  28 #f #g #s * #cf * #nf #Hf * #cg * #ng #Hg
  29 %{(cf+cg)} %{(max nf ng)} #n #Hmax normalize
  30 >distributive_times_plus_r @le_plus
  31   [@Hf @(le_maxl … Hmax) |@Hg @(le_maxr … Hmax) ]
  32 qed.
  33
  34 lemma O_plus_l: ∀f,s1,s2. O s1 f → O (s1+s2) f.
  35 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean
  36 @(transitive_le … (Os1f n lean)) @le_times //
  37 qed.
  38
  39 lemma O_absorbl: ∀f,g,s. O s f → O f g → O s (g+f).
  40 #f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
  41 qed.
  42
  43 lemma O_absorbr: ∀f,g,s. O s f → O f g → O s (f+g).
  44 #f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
  45 qed.
  46
  47 (*
  48 lemma O_ff: ∀f,s. O s f → O s (f+f).
  49 #f #s #Osf /2/
  50 qed. *)
  51
  52 lemma O_ext2: ∀f,g,s. O s f → (∀x.f x = g x) → O s g.
  53 #f #g #s * #c * #a #Osf #eqfg %{c} %{a} #n #lean <eqfg @Osf //
  54 qed.
  55
  56
  57 definition not_O ≝ λf,g.∀c,n0.∃n. n0 ≤ n ∧ c* (f n) < g n .
  58
  59 (* this is the only classical result *)
  60 axiom not_O_def: ∀f,g. ¬ O f g → not_O f g.