matita/matita/lib/reverse_complexity/big_O.ma

   1
   2 include "arithmetics/nat.ma".
   3 include "basics/sets.ma".
   4
   5 (******************************** big O notation ******************************)
   6
   7 (*  O f g means g ∈ O(f) *)
   8 definition O: relation (nat→nat) ≝
   9   λf,g. ∃c.∃n0.∀n. n0 ≤ n → g n ≤ c* (f n).
  10
  11 lemma O_refl: ∀s. O s s.
  12 #s %{1} %{0} #n #_ >commutative_times <times_n_1 @le_n qed.
  13
  14 lemma O_trans: ∀s1,s2,s3. O s2 s1 → O s3 s2 → O s3 s1.
  15 #s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1*c2)}
  16 %{(max n1 n2)} #n #Hmax
  17 @(transitive_le … (H1 ??)) [@(le_maxl … Hmax)]
  18 >associative_times @le_times [//|@H2 @(le_maxr … Hmax)]
  19 qed.
  20
  21 lemma sub_O_to_O: ∀s1,s2. O s1 ⊆ O s2 → O s2 s1.
  22 #s1 #s2 #H @H // qed.
  23
  24 lemma O_to_sub_O: ∀s1,s2. O s2 s1 → O s1 ⊆ O s2.
  25 #s1 #s2 #H #g #Hg @(O_trans … H) // qed.
  26
  27 lemma le_to_O: ∀s1,s2. (∀x.s1 x ≤ s2 x) → O s2 s1.
  28 #s1 #s2 #Hle %{1} %{0} #n #_ normalize <plus_n_O @Hle
  29 qed.
  30
  31 definition sum_f ≝ λf,g:nat→nat.λn.f n + g n.
  32 interpretation "function sum" 'plus f g = (sum_f f g).
  33
  34 lemma O_plus: ∀f,g,s. O s f → O s g → O s (f+g).
  35 #f #g #s * #cf * #nf #Hf * #cg * #ng #Hg
  36 %{(cf+cg)} %{(max nf ng)} #n #Hmax normalize
  37 >distributive_times_plus_r @le_plus
  38   [@Hf @(le_maxl … Hmax) |@Hg @(le_maxr … Hmax) ]
  39 qed.
  40
  41 lemma O_plus_l: ∀f,s1,s2. O s1 f → O (s1+s2) f.
  42 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean
  43 @(transitive_le … (Os1f n lean)) @le_times //
  44 qed.
  45
  46 lemma O_plus_r: ∀f,s1,s2. O s2 f → O (s1+s2) f.
  47 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean
  48 @(transitive_le … (Os1f n lean)) @le_times //
  49 qed.
  50
  51 lemma O_absorbl: ∀f,g,s. O s f → O f g → O s (g+f).
  52 #f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
  53 qed.
  54
  55 lemma O_absorbr: ∀f,g,s. O s f → O f g → O s (f+g).
  56 #f #g #s #Osf #Ofg @(O_plus … Osf) @(O_trans … Osf) //
  57 qed.
  58
  59 lemma O_times_c: ∀f,c. O f (λx:ℕ.c*f x).
  60 #f #c %{c} %{0} //
  61 qed.
  62
  63 lemma O_ext2: ∀f,g,s. O s f → (∀x.f x = g x) → O s g.
  64 #f #g #s * #c * #a #Osf #eqfg %{c} %{a} #n #lean <eqfg @Osf //
  65 qed.
  66
  67
  68 definition not_O ≝ λf,g.∀c,n0.∃n. n0 ≤ n ∧ c* (f n) < g n .
  69
  70 (* this is the only classical result *)
  71 axiom not_O_def: ∀f,g. ¬ O f g → not_O f g.
  72
  73 (******************************* small O notation *****************************)
  74
  75 (*  o f g means g ∈ o(f) *)
  76 definition o: relation (nat→nat) ≝
  77   λf,g.∀c.∃n0.∀n. n0 ≤ n → c * (g n) < f n.
  78
  79 lemma o_irrefl: ∀s. ¬ o s s.
  80 #s % #oss cases (oss 1) #n0 #H @(absurd ? (le_n (s n0)))
  81 @lt_to_not_le >(times_n_1 (s n0)) in ⊢ (?%?); >commutative_times @H //
  82 qed.
  83
  84 lemma o_trans: ∀s1,s2,s3. o s2 s1 → o s3 s2 → o s3 s1.
  85 #s1 #s2 #s3 #H1 #H2 #c cases (H1 c) #n1 -H1 #H1 cases (H2 1) #n2 -H2 #H2
  86 %{(max n1 n2)} #n #Hmax
  87 @(transitive_lt … (H1 ??)) [@(le_maxl … Hmax)]
  88 >(times_n_1 (s2 n)) in ⊢ (?%?); >commutative_times @H2 @(le_maxr … Hmax)
  89 qed.