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: \ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) ≝
   6   λf,g. \ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6c.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6n0.∀n. n0 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → g n \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 (f n).
   7
   8 lemma O_refl: ∀s. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s s.
   9 #s %{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6} %{\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6} #n #_ >\ 5a href="cic:/matita/arithmetics/nat/commutative_times.def(8)"\ 6commutative_times\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/times_n_1.def(8)"\ 6times_n_1\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6 qed.
  10
  11 lemma O_trans: ∀s1,s2,s3. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2 s1 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s3 s2 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s3 s1.
  12 #s1 #s2 #s3 * #c1 * #n1 #H1 * #c2 * # n2 #H2 %{(c1\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c2)}
  13 %{(\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 n1 n2)} #n #Hmax
  14 @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … (H1 ??)) [@(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … Hmax)]
  15 >\ 5a href="cic:/matita/arithmetics/nat/associative_times.def(10)"\ 6associative_times\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 [//|@H2 @(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … Hmax)]
  16 qed.
  17
  18 lemma sub_O_to_O: ∀s1,s2. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s1 \ 5a title="subset" href="cic:/fakeuri.def(1)"\ 6⊆\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2 s1.
  19 #s1 #s2 #H @H // qed.
  20
  21 lemma O_to_sub_O: ∀s1,s2. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2 s1 → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s1 \ 5a title="subset" href="cic:/fakeuri.def(1)"\ 6⊆\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s2.
  22 #s1 #s2 #H #g #Hg @(\ 5a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"\ 6O_trans\ 5/a\ 6 … H) // qed.
  23
  24 definition sum_f ≝ λf,g:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6→\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.λn.f n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 g n.
  25 interpretation "function sum" 'plus f g = (sum_f f g).
  26
  27 lemma O_plus: ∀f,g,s. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s f → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s g → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s (f\ 5a title="function sum" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6g).
  28 #f #g #s * #cf * #nf #Hf * #cg * #ng #Hg
  29 %{(cf\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6cg)} %{(\ 5a href="cic:/matita/arithmetics/nat/max.def(2)"\ 6max\ 5/a\ 6 nf ng)} #n #Hmax normalize
  30 >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"\ 6le_plus\ 5/a\ 6
  31   [@Hf @(\ 5a href="cic:/matita/arithmetics/nat/le_maxl.def(7)"\ 6le_maxl\ 5/a\ 6 … Hmax) |@Hg @(\ 5a href="cic:/matita/arithmetics/nat/le_maxr.def(9)"\ 6le_maxr\ 5/a\ 6 … Hmax) ]
  32 qed.
  33
  34 lemma O_plus_l: ∀f,s1,s2. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s1 f → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 (s1\ 5a title="function sum" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6s2) f.
  35 #f #s1 #s2 * #c * #a #Os1f %{c} %{a} #n #lean
  36 @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … (Os1f n lean)) @\ 5a href="cic:/matita/arithmetics/nat/le_times.def(9)"\ 6le_times\ 5/a\ 6 //
  37 qed.
  38
  39 lemma O_absorbl: ∀f,g,s. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s f → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 f g → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s (g\ 5a title="function sum" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6f).
  40 #f #g #s #Osf #Ofg @(\ 5a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"\ 6O_plus\ 5/a\ 6 … Osf) @(\ 5a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"\ 6O_trans\ 5/a\ 6 … Osf) //
  41 qed.
  42
  43 lemma O_absorbr: ∀f,g,s. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s f → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 f g → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s (f\ 5a title="function sum" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6g).
  44 #f #g #s #Osf #Ofg @(\ 5a href="cic:/matita/arithmetics/bigO/O_plus.def(10)"\ 6O_plus\ 5/a\ 6 … Osf) @(\ 5a href="cic:/matita/arithmetics/bigO/O_trans.def(11)"\ 6O_trans\ 5/a\ 6 … 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. \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 s f → (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 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.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6n. n0 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 (f n) \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 g n .
  58
  59 (* this is the only classical result *)
  60 axiom not_O_def: ∀f,g. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/bigO/O.def(3)"\ 6O\ 5/a\ 6 f g → \ 5a href="cic:/matita/arithmetics/bigO/not_O.def(3)"\ 6not_O\ 5/a\ 6 f g.
  61
  62