:: Algebra of Polynomially Bounded Sequences and Negligible Functions
:: by Hiroyuki Okazaki
::
:: Received August 15, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SEQ_1, FUNCT_2, TARSKI, REAL_1, BINOP_1,
SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, CARD_1, NAT_1, RLVECT_1,
RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0, REALSET1, XXREAL_0,
CARD_3, COMPLEX1, SEQ_2, ORDINAL2, RSSPACE, ASYMPT_1, FUNCSDOM, FINSET_1,
POWER, ORDINAL4, FUNCOP_1, VECTSP_1, PARTFUN3, PRE_TOPC, FINSEQ_1,
MESFUNC1, ASYMPT_2, ASYMPT_3, ASYMPT_0, ORDINAL1, INT_1, AFINSQ_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1,
FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1,
INT_1, COMPLEX1, VALUED_1, SEQ_1, SEQ_2, RVSUM_1, POWER, SERIES_1,
ASYMPT_0, ASYMPT_1, AFINSQ_1, PARTFUN3, AFINSQ_2, STRUCT_0, ALGSTR_0,
PRE_TOPC, GROUP_1, RLVECT_1, VECTSP_1, FUNCSDOM, RSSPACE, ASYMPT_2;
constructors REAL_1, SEQ_2, SERIES_1, REALSET1, RLSUB_1, RELSET_1, COMSEQ_2,
SEQ_1, FUNCSDOM, INTEGRA2, XXREAL_2, RECDEF_1, FCONT_1, PREPOWER,
ASYMPT_0, ASYMPT_1, PARTFUN3, AFINSQ_2, FUNCT_4, PARTFUN2, RSSPACE4,
PROB_1, NEWTON, VALUED_2, ASYMPT_2, GROUP_1, RVSUM_1, RFINSEQ2, METRIC_1,
MATRPROB;
registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1,
MEMBERED, VALUED_0, FUNCSDOM, RLVECT_1, STRUCT_0, FUNCOP_1, VALUED_1,
FUNCT_2, AFINSQ_1, AFINSQ_2, XBOOLE_0, SUBSET_1, RELAT_1, INT_1,
ASYMPT_0, POWER, ASYMPT_1, RSSPACE, PARTFUN3, REALSET1, NEWTON, COMPLEX1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_2, ALGSTR_0, RLVECT_1, VECTSP_1;
equalities REALSET1, STRUCT_0, ALGSTR_0, FUNCSDOM, BINOP_1, RLVECT_1,
ORDINAL1, ASYMPT_0;
expansions TARSKI, RLVECT_1, FUNCT_1, PARTFUN3, GROUP_1, FUNCSDOM, STRUCT_0,
VECTSP_1, ASYMPT_2;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, SEQ_1, SEQ_2, ABSVALUE, RELAT_1,
XBOOLE_0, XBOOLE_1, XCMPLX_1, COMPLEX1, FUNCOP_1, XREAL_1, XXREAL_0,
ORDINAL1, VALUED_1, XREAL_0, AFINSQ_1, AFINSQ_2, INT_1, ASYMPT_0,
ASYMPT_1, POWER, FUNCSDOM, PRE_FF, TAYLOR_1, RLVECT_1, VECTSP_1,
REALSET1, ZFMISC_1, ASYMPT_2, PARTFUN3, GROUP_1;
schemes NAT_1, SEQ_1, XBOOLE_0;
begin :: Preliminaries
theorem TCL001:
for r be Real holds r < |. r .| + 1
proof
let r be Real;
r + 0 < |. r .| +1 by XREAL_1:8,ABSVALUE:4;
hence r < |. r .| +1;
end;
theorem
LMC31: for r be Real ex N be Nat
st for n be Nat st N <=n holds r < n /log(2,n)
proof
let r0 be Real;
ex r be Real st 0 < r & r0 <=r
proof
per cases;
suppose A1:0 < r0;
take r = r0;
thus 0 < r & r0 <=r by A1;
end;
suppose A2:not 0 < r0;
set r=1;
take r;
thus 0 < r & r0 <=r by A2;
end;
end; then
consider r be Real such that
AS: 0 < r & r0 <=r;
set a0 = max(log(2,r),number_e);
A01: log(2,r) <= a0 & number_e <= a0 by XXREAL_0:25;
set k = [/ a0 \] + 1;
a0 < k by INT_1:32;
k in NAT by INT_1:3,TAYLOR_1:11,A01; then
reconsider k as Nat;
A0: log(2,r) < k & number_e < k by A01,XXREAL_0:2,INT_1:32;
2 to_power log(2,r) < 2 to_power k by A0,POWER:39; then
A1:r < 2 to_power k by AS,POWER:def 3;
consider N be Nat such that
A2: for n be Nat st N<=n
holds 2 to_power k <= n/log(2,n) by ASYMPT_2:13,A0;
reconsider N as Element of NAT by ORDINAL1:def 12;
take N;
thus for n be Nat st N <=n holds r0 < n /log(2,n)
proof
let n be Nat;
assume N<=n; then
2 to_power k <= n/log(2,n) by A2; then
r < n /log(2,n) by A1,XXREAL_0:2;
hence r0 < n /log(2,n) by AS,XXREAL_0:2;
end;
end;
theorem L1:
for k be Nat
ex N be Nat st
for x be Nat st N <= x holds x to_power k < 2 to_power x
proof
let k be Nat;
consider N0 be Nat such that
P1: for x be Nat st N0 <= x holds k < x /log(2,x) by LMC31;
set N=N0+2;
take N;
now let x be Nat;
assume AS2: N<= x;
N0 <= N by NAT_1:12; then
N0 <= x by XXREAL_0:2,AS2; then
E1:k < x /log(2,x) by P1;
2 <= N by NAT_1:11; then
2 <= x by XXREAL_0:2,AS2; then
log(2,2) <= log(2,x) by PRE_FF:10; then
P3: 0 < log(2,x) by POWER:52; then
k*log(2,x) < x /log(2,x) * log(2,x) by XREAL_1:68,E1; then
P4: k*log(2,x) < x by P3,XCMPLX_1:87;
2 to_power (log(2,x)*k) = 2 to_power (log(2,x)) to_power k by POWER:33
.= x to_power k by AS2,POWER:def 3;
hence x to_power k < 2 to_power x by P4,POWER:39;
end;
hence thesis;
end;
theorem L2:
for k be Nat
ex N be Nat st
for x be Nat st N <= x holds 1/ (2 to_power x) < 1/ (x to_power k)
proof
let k be Nat;
consider N0 be Nat such that
P1: for x be Nat st N0 <= x
holds x to_power k < 2 to_power x by L1;
set N=N0+2;
take N;
now let x be Nat;
assume AS: N <=x;
N0 <= N by NAT_1:12; then
N0 <= x by XXREAL_0:2,AS; then
E1:x to_power k < 2 to_power x by P1;
0 < x to_power k by POWER:34,AS;
hence 1/ (2 to_power x) < 1/ (x to_power k)
by XREAL_1:76,E1;
end;
hence thesis;
end;
theorem
for z be Nat st 2 <= z holds
for k be Nat
ex N be Nat st
for x be Nat st N <= x holds 1/ (z to_power x) < 1/ (x to_power k)
proof
let z be Nat;
assume P0: 2 <=z;
let k be Nat;
consider N be Nat such that
P1: for x be Nat st N <= x
holds 1/ (2 to_power x) < 1/ (x to_power k) by L2;
take N;
now let x be Nat;
assume N <=x; then
E1:1/ (2 to_power x) < 1/ (x to_power k) by P1;
P3: 0 < 2 to_power x by POWER:34;
2 to_power x <= z to_power x
proof
now per cases by P0,XXREAL_0:1;
case 2 = z;
hence thesis;
end;
case LL1: 2 < z;
now per cases;
case LL2: x= 0;then
2 to_power x = 1 by POWER:24
.= z to_power x by POWER:24,LL2;
hence thesis;
end;
case 0 < x;
hence thesis by POWER:37,LL1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then 1/ (z to_power x) <= 1/ (2 to_power x) by P3,XREAL_1:118;
hence 1/ (z to_power x) < 1/ (x to_power k) by E1,XXREAL_0:2;
end;
hence thesis;
end;
registration
cluster positive-yielding for XFinSequence of REAL;
correctness
proof
reconsider z = <% 1 %> as XFinSequence of REAL;
now let r be Real;
assume r in rng z;
then
r in {1} by AFINSQ_1:33;
hence 0 < r;
end;
then
z is positive-yielding;
hence thesis;
end;
end;
registration
cluster non empty for positive-yielding XFinSequence of REAL;
correctness
proof
reconsider z = <% 1 %> as XFinSequence of REAL;
now let r be Real;
assume r in rng z; then
r in {1} by AFINSQ_1:33;
hence 0 < r;
end;
then
z is positive-yielding;
hence thesis;
end;
end;
theorem
for c be XFinSequence of REAL,
a be Real
holds a (#) c is XFinSequence of REAL;
registration
let c be XFinSequence of REAL,
a be Real;
cluster a (#) c -> finite for Sequence of REAL;
correctness;
end;
theorem NLM2:
for c be non empty positive-yielding XFinSequence of REAL,
a be Real
st 0 < a
holds a (#) c is non empty positive-yielding XFinSequence of REAL
proof
let c be non empty positive-yielding XFinSequence of REAL,
a be Real;
assume AS: 0 < a;
P2: dom (a (#) c) = dom c by VALUED_1:def 5;
for r being Real st r in rng (a (#) c) holds 0 < r by PARTFUN3:def 1,AS;
then
a (#) c is positive-yielding;
hence thesis by P2;
end;
registration
let c be non empty positive-yielding XFinSequence of REAL,
a be positive Real;
cluster a (#) c -> non empty positive-yielding for XFinSequence of REAL;
correctness by NLM2;
end;
notation
let c be XFinSequence of REAL;
synonym polynom(c) for seq_p(c);
end;
theorem NLM3:
for c be non empty positive-yielding XFinSequence of REAL,
x be Nat
holds 0 < (polynom(c)).x
proof
defpred P[Nat] means
for c be non empty positive-yielding XFinSequence of REAL
st len c = $1 holds
for x be Nat
holds 0 < (polynom(c)).x;
P0: P[0];
P1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A1: P[k];
let d be non empty positive-yielding XFinSequence of REAL;
assume A2: len d = k+1;
then
consider a be Real,d1 be XFinSequence of REAL,
y be Real_Sequence such that
A3: len d1 = k & d1= d | k & a = d.k &
d =d1^<% a %> & polynom(d) = polynom(d1) + y &
for i be Nat holds
y.i = a* (i to_power k) by ASYMPT_2:28;
per cases;
suppose X1:k = 0; then
consider a be Real such that
A4:a = d.0 &
for x be Nat holds (polynom(d)).x = a by ASYMPT_2:29,A2;
0 in Segm (0+1) by NAT_1:44;
then d.0 in rng d by FUNCT_1:3,X1,A2;
then
A5:0 < d.0 by PARTFUN3:def 1;
let x be Nat;
reconsider n =x as Nat;
thus 0 < (polynom(d)).x by A5,A4;
end;
suppose A7:k <> 0;
now let r be Real;
assume r in rng d1; then
consider x be object such that
P4: x in dom d1 & r = d1.x by FUNCT_1:def 3;
P5: d1.x = d.x by P4,A3,FUNCT_1:47;
x in dom d by P4,A3,RELAT_1:60,TARSKI:def 3;
then
d.x in rng d by FUNCT_1:3;
hence 0 < r by PARTFUN3:def 1,P5,P4;
end;
then
A8: d1 is positive-yielding;
reconsider d1 as non empty positive-yielding XFinSequence of REAL
by A7,A8,A3;
let x be Nat;
reconsider n=x as Nat;
A9: 0 < (polynom(d1)).n by A1,A3;
A10: (polynom(d)).n
= (polynom(d1)).n + y.n by SEQ_1:7,A3;
A11: y.n = a* (n to_power k) by A3;
k < k+1 by NAT_1:13;
then k in Segm (k+1) by NAT_1:44;then
d.k in rng d by FUNCT_1:3,A2;
then
0 < d.k by PARTFUN3:def 1;
hence 0 < (polynom(d)).x by A10,A9,A11,A3;
end;
end;
P2: for k be Nat holds P[k] from NAT_1:sch 2(P0,P1);
let c be non empty positive-yielding XFinSequence of REAL,
x be Nat;
len c is Nat;
hence 0 < (polynom(c)).x by P2;
end;
theorem NLM4:
for c,c1 be non empty positive-yielding XFinSequence of REAL,
a be Real
st c1=a(#)c holds
for x be Nat
holds (polynom(c1)).x = a* ( (polynom(c)).x)
proof
let c,c1 be non empty positive-yielding XFinSequence of REAL,
a be Real;
assume AS: c1=a(#)c;
let x be Nat;
D1: dom (c1 (#) seq_a^(x,1,0)) = dom c1 by ASYMPT_2:26
.= dom c by VALUED_1:def 5,AS;
D2: dom (a (#) ( c (#) seq_a^(x,1,0) ))
=dom ( c (#) seq_a^(x,1,0) ) by VALUED_1:def 5
.= dom c by ASYMPT_2:26;
for i be object
st i in dom (c1 (#) seq_a^(x,1,0))
holds
(c1 (#) seq_a^(x,1,0)).i = (a (#) ( c (#) seq_a^(x,1,0) )).i
proof
let i be object;
assume D3: i in dom (c1 (#) seq_a^(x,1,0));
then
D4: i in dom c1 by ASYMPT_2:26;
thus (c1 (#) seq_a^(x,1,0)).i
= c1.i * (seq_a^(x,1,0)).i by D4,ASYMPT_2:26
.= a*c.i * (seq_a^(x,1,0)).i by AS,VALUED_1:6
.= a* ( c.i * (seq_a^(x,1,0)).i )
.= a* ( c (#) seq_a^(x,1,0) ).i by D3,D1,ASYMPT_2:26
.= (a (#) ( c (#) seq_a^(x,1,0) )).i by VALUED_1:6;
end;
then
P2: c1 (#) seq_a^(x,1,0) = a (#) ( c (#) seq_a^(x,1,0) ) by D1,D2;
thus (polynom(c1)).x = Sum( c1 (#) seq_a^(x,1,0)) by ASYMPT_2:def 2
.= a* Sum( c (#) seq_a^(x,1,0)) by AFINSQ_2:64,P2
.= a* (polynom(c)).x by ASYMPT_2:def 2;
end;
begin :: Algebra of polynomially bounded functions
definition
let p be Real_Sequence;
attr p is polynomially-abs-bounded means
:defabs:
ex k be Nat st |.p.| in Big_Oh(seq_n^(k));
end;
registration
cluster polynomially-bounded -> polynomially-abs-bounded for Real_Sequence;
coherence
proof
let p be Real_Sequence;
assume p is polynomially-bounded;
then consider k be Nat such that L1:
p in Big_Oh(seq_n^(k));
consider t be Element of Funcs(NAT, REAL) such that L2: p = t &
ex c be Real, N be Element of NAT st
c > 0 & for n be Element of NAT st n >= N holds
t.n <= c*((seq_n^(k)).n) & t.n >= 0 by L1;
consider c be Real, N be Element of NAT such that
L3: c > 0 & for n be Element of NAT st n >= N holds
t.n <= c*((seq_n^(k)).n) & t.n >= 0 by L2;
reconsider abst = |. t .| as Element of Funcs(NAT, REAL) by FUNCT_2:8;
for n be Element of NAT st n >= N holds
abst.n <= c*((seq_n^(k)).n) & abst.n >= 0
proof
let n be Element of NAT;
assume LL2:n >= N;then
t.n = |. t.n .| by ABSVALUE:def 1,L3
.= |. t.|.n by VALUED_1:18;
hence thesis by LL2,L3;
end;then
|. p .| in Big_Oh(seq_n^(k)) by L2,L3;
hence thesis;
end;
end;
theorem LM1:
for r be Element of NAT holds
for s be Real_Sequence
st s = NAT --> r
holds s is polynomially-abs-bounded
proof
let r be Element of NAT;
let s1 be Real_Sequence;
assume AS: s1 = NAT --> r;
set s=|.s1.|;
P1: s in Funcs(NAT, REAL) by FUNCT_2:8;
now
let n be Element of NAT;
assume A2: n >= r;
n = 0 or n > 0;
then
A4: (seq_n^ 1) . n = n to_power 1 by ASYMPT_1:def 3
.=n;
A5: s.n = |. s1.n .| by VALUED_1:18
.= |. r .| by AS
.= r by ABSVALUE:def 1;
hence s.n <= 1*(seq_n^ 1).n by A2,A4;
thus s.n >= 0 by A5;
end;
then
s in Big_Oh(seq_n^ 1) by P1;
hence thesis;
end;
reconsider rr = 0 as Element of REAL by XREAL_0:def 1;
registration
cluster polynomially-abs-bounded for Function of NAT,REAL;
existence
proof
take NAT --> rr;
thus thesis by LM1;
end;
end;
registration
let f,g be polynomially-abs-bounded Function of NAT,REAL;
cluster f + g -> polynomially-abs-bounded for Function of NAT,REAL;
coherence
proof
set h = f + g;
A3: for n be Nat holds |.h.| .n <= |.f.|.n + |.g.|.n
proof
let n be Nat;
S1: n in NAT by ORDINAL1:def 12;
A30: |.h.| .n =|. h.n .| by VALUED_1:18
.= |. f.n + g.n.| by S1,VALUED_1:1;
|. f.n .| + |.g.n.| = |. f .|.n + |.g.n.| by VALUED_1:18
.= |.f.|.n + |.g.|.n by VALUED_1:18;
hence thesis by COMPLEX1:56,A30;
end;
consider k1 be Nat such that
A4: |.f.| in Big_Oh(seq_n^(k1)) by defabs;
consider k2 be Nat such that
A5: |.g.| in Big_Oh(seq_n^(k2)) by defabs;
consider t1 be Element of Funcs(NAT, REAL) such that
A6: |.f.|=t1 &
ex c1 be Real,N1 be Element of NAT st c1 > 0
& for n be Element of NAT
st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n
& t1.n >= 0 by A4;
consider t2 be Element of Funcs(NAT, REAL) such that
A7: |.g.|=t2
&
ex c2 be Real,N2 be Element of NAT
st c2 > 0
& for n be Element of NAT
st n >= N2 holds t2.n <= c2*(seq_n^(k2)).n
& t2.n >= 0 by A5;
consider c1 be Real,N1 be Element of NAT such that
A8: c1 > 0
& for n be Element of NAT
st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n
& t1.n >= 0 by A6;
consider c2 be Real,N2 be Element of NAT such that
A9: c2 > 0
& for n be Element of NAT
st n >= N2 holds t2.n <= c2*(seq_n^(k2)).n
& t2.n >= 0 by A7;
set c = c1+c2;
set N = N1+N2;
set k = k1+k2;
reconsider t = |.h.| as Element of Funcs(NAT, REAL) by FUNCT_2:8;
now let n be Element of NAT;
assume B11: n >= N+2;
N<=N+2 & 2 <= N+2 by NAT_1:12;
then
A11: N <= n & 2 <= n by B11,XXREAL_0:2;
N1 <= N & N2<= N by NAT_1:12;
then
A12: N1<=n & N2<=n by A11,XXREAL_0:2;
then
A13: t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A8;
A14: t2.n <= c2*(seq_n^(k2)).n & t2.n >= 0 by A12,A9;
B15: 1 < n by A11,XXREAL_0:2;
B14: k1 <= k & k2 <= k by NAT_1:12;
S1: (seq_n^(k1)).n = n to_power k1 by B11,ASYMPT_1:def 3;
S2: (seq_n^(k2)).n = n to_power k2 by B11,ASYMPT_1:def 3;
S3: (seq_n^(k)).n = n to_power k by B11,ASYMPT_1:def 3;
k1 < k or k1=k by XXREAL_0:1,B14; then
(seq_n^(k1)).n <= (seq_n^(k)).n by S1,S3,B15,POWER:39;
then
S4:c1*(seq_n^(k1)).n <= c1*((seq_n^(k)).n) by XREAL_1:64,A8;
k2 < k or k2=k by XXREAL_0:1,B14; then
(seq_n^(k2)).n <= (seq_n^(k)).n by S2,S3,B15,POWER:39;
then c2*(seq_n^(k2)).n <= c2*((seq_n^(k)).n) by XREAL_1:64,A9;
then
S6: (c1*(seq_n^(k1)).n) + (c2*(seq_n^(k2)).n)
<= c1*(seq_n^(k)).n + c2*(seq_n^(k)).n by S4,XREAL_1:7;
t1.n + t2.n <= (c1*(seq_n^(k1)).n) + (c2*(seq_n^(k2)).n)
by XREAL_1:7,A13,A14;
then
A15:t1.n + t2.n <= c *(seq_n^(k)).n by S6,XXREAL_0:2;
t.n <= t1.n + t2.n by A3,A6,A7;
hence t.n <= c *(seq_n^(k)).n by A15,XXREAL_0:2;
|.h.| .n =|. h.n .| by VALUED_1:18;
hence 0 <=t.n;
end;
then |.h.| in Big_Oh(seq_n^(k)) by A8,A9;
hence thesis;
end;
cluster f (#) g -> polynomially-abs-bounded for Function of NAT,REAL;
coherence
proof
set h = f(#)g;
A3: for n be Nat holds |.h.| .n = |.f.|.n * |.g.|.n
proof
let n be Nat;
thus |.h.| .n =|. h.n .| by VALUED_1:18
.= |. f.n * g.n.| by VALUED_1:5
.= |. f.n .| * |.g.n.| by COMPLEX1:65
.= |. f .|.n * |.g.n.| by VALUED_1:18
.= |.f.|.n * |.g.|.n by VALUED_1:18;
end;
consider k1 be Nat such that
A4: |.f.| in Big_Oh(seq_n^(k1)) by defabs;
consider k2 be Nat such that
A5: |.g.| in Big_Oh(seq_n^(k2)) by defabs;
consider t1 be Element of Funcs(NAT, REAL) such that
A6: |.f.|=t1
&
ex c1 be Real,N1 be Element of NAT
st c1 > 0
& for n be Element of NAT
st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n
& t1.n >= 0 by A4;
consider t2 be Element of Funcs(NAT, REAL) such that
A7: |.g.|=t2
&
ex c2 be Real,N2 be Element of NAT
st c2 > 0
& for n be Element of NAT
st n >= N2 holds t2.n <= c2*(seq_n^(k2)).n
& t2.n >= 0 by A5;
consider c1 be Real,N1 be Element of NAT such that
A8: c1 > 0
& for n be Element of NAT
st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n
& t1.n >= 0 by A6;
consider c2 be Real,N2 be Element of NAT such that
A9: c2 > 0
& for n be Element of NAT
st n >= N2 holds t2.n <= c2*(seq_n^(k2)).n
& t2.n >= 0 by A7;
set c = c1*c2;
set N = N1+N2;
set k = k1+k2;
reconsider t = |.h.| as Element of Funcs(NAT, REAL) by FUNCT_2:8;
now let n be Element of NAT;
assume B11: n >= N+2;
N<=N+2 & 2 <= N+2 by NAT_1:12;
then A11n: N <= n & 2 <= n by B11,XXREAL_0:2;
N1 <= N & N2<= N by NAT_1:12; then
A12: N1<=n & N2<=n by A11n,XXREAL_0:2; then
A13: t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A8;
A14: t2.n <= c2*(seq_n^(k2)).n & t2.n >= 0 by A12,A9;
A15: t1.n * t2.n <= (c1*(seq_n^(k1)).n) * (c2*(seq_n^(k2)).n)
by XREAL_1:66,A13,A14;
(c1*(seq_n^(k1)).n) * (c2*(seq_n^(k2)).n)
=c1*c2* ( (seq_n^(k1)).n * (seq_n^(k2)).n)
.=c1*c2*( (n to_power k1) * (seq_n^(k2)).n) by B11,ASYMPT_1:def 3
.=c1*c2*( (n to_power k1) * (n to_power k2)) by B11,ASYMPT_1:def 3
.=c1*c2*( n to_power (k1+k2) ) by B11,POWER:27
.=c*(seq_n^(k)).n by B11,ASYMPT_1:def 3;
hence t.n <= c*(seq_n^(k)).n by A15,A3,A6,A7;
0 <= t1.n * t2.n by A13,A14;
hence 0 <=t.n by A3,A6,A7;
end;
then |.h.| in Big_Oh(seq_n^(k)) by A8,A9;
hence thesis;
end;
end;
registration
let f be polynomially-abs-bounded Function of NAT,REAL;
let a be Element of REAL;
cluster a (#) f -> polynomially-abs-bounded for Function of NAT,REAL;
coherence
proof
set h = a (#) f;
per cases;
suppose CS1: a= 0;
X0: dom h = NAT by FUNCT_2:def 1;
now let z be object;
assume z in dom h; then
reconsider n=z as Element of NAT;
thus h.z = 0 * f.n by CS1,VALUED_1:6
.= 0;
end;
then h = NAT --> 0 by FUNCOP_1:11,X0;
hence thesis by LM1;
end;
suppose A0: a <> 0;
A3: for n be Nat holds |.h.| .n = |.a.| * |.f.|.n
proof
let n be Nat;
thus |.h.| .n =|. h.n .| by VALUED_1:18
.= |. a*f.n .| by VALUED_1:6
.= |.a.| * |. f.n .| by COMPLEX1:65
.= |.a.| *|. f .|.n by VALUED_1:18;
end;
consider k1 be Nat such that
A4: |.f.| in Big_Oh(seq_n^(k1)) by defabs;
consider t1 be Element of Funcs(NAT, REAL) such that
A6: |.f.|=t1 &
ex c1 be Real,N1 be Element of NAT
st c1 > 0
& for n be Element of NAT
st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n
& t1.n >= 0 by A4;
consider c1 be Real,N1 be Element of NAT such that
A8: c1 > 0
& for n be Element of NAT
st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A6;
set c = |.a.| *c1;
reconsider t = |.h.| as Element of Funcs(NAT, REAL) by FUNCT_2:8;
now let n be Element of NAT;
assume B11: n >= N1+2;
N1<=N1+2 & 2 <= N1+2 by NAT_1:12; then
N1 <= n & 2 <= n by B11,XXREAL_0:2; then
A13: t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A8; then
A15: |.a.|*t1.n <= |.a.|*(c1*(seq_n^(k1)).n) by XREAL_1:66;
thus t.n <= c*(seq_n^(k1)).n by A15,A3,A6;
0 <= |.a.|*t1.n by A13;
hence 0 <=t.n by A3,A6;
end;
then |.h.| in Big_Oh(seq_n^(k1)) by A8,A0;
hence thesis;
end;
end;
end;
definition
func Big_Oh_poly -> Subset of RAlgebra (NAT) means
:DefX1:
for x being object holds x in it
iff x is polynomially-abs-bounded Function of NAT,REAL;
existence
proof
defpred P[object] means
$1 is polynomially-abs-bounded Function of NAT,REAL;
consider IT being set such that
A01: for x being object holds x in IT iff x in Funcs(NAT,REAL) &
P[x] from XBOOLE_0:sch 1;
A1: for x being object holds x in IT
iff x is polynomially-abs-bounded Function of NAT,REAL
proof
let x being object;
x is polynomially-abs-bounded Function of NAT,REAL
implies x in Funcs(NAT,REAL) by FUNCT_2:8;
hence thesis by A01;
end;
for x be object st x in IT holds x in Funcs(NAT,REAL)
proof
let x be object;
assume x in IT; then
x is polynomially-abs-bounded Function of NAT,REAL by A1;
hence x in Funcs(NAT,REAL) by FUNCT_2:8;
end;
then IT is Subset of RAlgebra(NAT) by TARSKI:def 3;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of RAlgebra(NAT);
assume that
A2: for x being object holds x in X1 iff x is polynomially-abs-bounded
Function of NAT,REAL and
A3: for x being object holds x in X2 iff x is polynomially-abs-bounded
Function of NAT,REAL;
thus X1 c= X2
proof
let x be object;
assume x in X1;
then x is polynomially-abs-bounded Function
of NAT,REAL by A2;
hence thesis by A3;
end;
let x be object;
assume x in X2;
then x is polynomially-abs-bounded Function of NAT,REAL
by A3;
hence thesis by A2;
end;
end;
registration
cluster Big_Oh_poly -> non empty;
coherence
proof
the polynomially-abs-bounded Function of NAT,REAL in Big_Oh_poly by DefX1;
hence thesis;
end;
end;
definition
func R_Algebra_of_Big_Oh_poly -> strict AlgebraStr means
:defAlgebra:
the carrier of it = Big_Oh_poly
& the multF of it = (RealFuncMult(NAT)) || Big_Oh_poly
& the addF of it = (RealFuncAdd(NAT)) || Big_Oh_poly
& the Mult of it = (RealFuncExtMult(NAT)) | [:REAL,Big_Oh_poly:]
& the OneF of it = RealFuncUnit(NAT)
& the ZeroF of it = RealFuncZero(NAT);
correctness
proof
set X = Big_Oh_poly;
set m = (RealFuncMult(NAT)) || X;
set a = (RealFuncAdd(NAT)) || X;
set E = (RealFuncExtMult(NAT)) | [:REAL,X:];
set O = RealFuncUnit(NAT);
set Z = RealFuncZero(NAT);
for x being set holds x in [: X,X:] implies (RealFuncMult(NAT)).x in X
proof
let x be set;
assume x in [: X,X:];
then consider f,g be object such that
B2: f in X & g in X & x =[f,g] by ZFMISC_1:def 2;
reconsider f,g as polynomially-abs-bounded
Function of NAT,REAL by DefX1,B2;
set h = (RealFuncMult(NAT)).x;
reconsider f1=f,g1=g as Element of Funcs(NAT,REAL) by FUNCT_2:8;
B5: h= (RealFuncMult(NAT)).(f1,g1) by B2;
reconsider h as Function of NAT,REAL by B5;
h = f(#)g
proof
let n be Element of NAT;
thus h.n = f.n*g.n by B5,FUNCSDOM:2
.= (f(#)g).n by VALUED_1:5;
end;
hence thesis by DefX1;
end;
then X is Preserv of (RealFuncMult(NAT)) by REALSET1:def 1;
then reconsider m as BinOp of X by REALSET1:2;
for x being set holds x in [: X,X:] implies
(RealFuncAdd(NAT)).x in X
proof
let x be set;
assume x in [: X,X:];
then
consider f,g be object such that
B2: f in X & g in X & x =[f,g] by ZFMISC_1:def 2;
reconsider f,g as polynomially-abs-bounded Function of
NAT,REAL by DefX1,B2;
set h = (RealFuncAdd(NAT)).x;
reconsider f1=f,g1=g as Element of Funcs(NAT,REAL)
by FUNCT_2:8;
B5: h= (RealFuncAdd(NAT)).(f1,g1) by B2;
then reconsider h as Function of NAT,REAL;
h = f+g
proof
let n be Element of NAT;
thus h.n = f.n+g.n by B5,FUNCSDOM:1
.= (f+g).n by VALUED_1:1;
end;
hence thesis by DefX1;
end;
then X is Preserv of (RealFuncAdd(NAT)) by REALSET1:def 1;
then reconsider a as BinOp of X by REALSET1:2;
Q0: [:REAL,X:] c= [:REAL,Funcs(NAT,REAL):] by ZFMISC_1:95;
[:REAL,Funcs(NAT,REAL):]
= dom (RealFuncExtMult(NAT)) by FUNCT_2:def 1;
then
Q1: dom E = [:REAL,X:] by RELAT_1:62,Q0;
for h being object st h in rng E holds h in X
proof
let h be object;
assume h in rng E;
then consider x be object such that
Q2: x in dom E & h = E.x by FUNCT_1:def 3;
consider s,f be object such that
B2: s in REAL & f in X and
B3: x =[s,f] by Q1,Q2,ZFMISC_1:def 2;
reconsider f as polynomially-abs-bounded Function
of NAT,REAL by DefX1,B2;
reconsider s as Element of REAL by B2;
H1: h = (RealFuncExtMult(NAT)).x by Q1,Q2,FUNCT_1:49;
reconsider f1=f as Element of Funcs(NAT,REAL) by FUNCT_2:8;
reconsider h1=h as Element of Funcs(NAT,REAL) by H1,FUNCT_2:5,Q2;
reconsider h1 as Function of NAT,REAL;
h1 = s(#)f
proof
let n be Element of NAT;
thus h1.n = s*f1.n by B3,H1,FUNCSDOM:4
.= (s(#)f).n by VALUED_1:6;
end;
hence h in X by DefX1;
end;
then
rng E c= X;
then
reconsider E as Function of [:REAL,X:],X by Q1,FUNCT_2:2;
reconsider O as Real_Sequence;
O in Funcs(NAT,REAL) & seq_id O is polynomially-abs-bounded by LM1;
then
reconsider O as Element of X by DefX1;
reconsider Z as Real_Sequence;
Z in Funcs(NAT,REAL) & seq_id Z is polynomially-abs-bounded by LM1;
then reconsider Z as Element of X by DefX1;
set S = AlgebraStr(#X,m,a,E,O,Z#);
S is strict AlgebraStr;
hence thesis;
end;
end;
registration
cluster R_Algebra_of_Big_Oh_poly -> non empty;
correctness by defAlgebra;
end;
theorem LM12:
the carrier of R_Algebra_of_Big_Oh_poly c= the carrier of RAlgebra (NAT)
proof
the carrier of R_Algebra_of_Big_Oh_poly = Big_Oh_poly by defAlgebra;
hence thesis;
end;
theorem LM14:
for f be object holds
f in R_Algebra_of_Big_Oh_poly
iff f is polynomially-abs-bounded Function of NAT,REAL
proof
let f be object;
the carrier of R_Algebra_of_Big_Oh_poly = Big_Oh_poly by defAlgebra;
hence f in R_Algebra_of_Big_Oh_poly
iff f is polynomially-abs-bounded Function of NAT,REAL by DefX1;
end;
theorem LM15:
for f,g be Point of R_Algebra_of_Big_Oh_poly,
f1,g1 be Point of RAlgebra NAT st f=f1 & g=g1 holds
f*g = f1*g1
proof
let f,g be Point of R_Algebra_of_Big_Oh_poly,
f1,g1 be Point of RAlgebra NAT;
assume A1: f=f1 & g=g1;
set X = Big_Oh_poly;
set S = R_Algebra_of_Big_Oh_poly;
A3a: the carrier of R_Algebra_of_Big_Oh_poly = X by defAlgebra;
thus f*g = ((RealFuncMult(NAT)) || X). ( [f,g] ) by defAlgebra
.=f1*g1 by A1,A3a,FUNCT_1:49;
end;
theorem LM16:
for f,g be Point of R_Algebra_of_Big_Oh_poly,
f1,g1 be Point of RAlgebra NAT
st f=f1 & g=g1 holds
f+g = f1+g1
proof
let f,g be Point of R_Algebra_of_Big_Oh_poly,
f1,g1 be Point of RAlgebra NAT;
assume A1: f=f1 & g=g1;
set X = Big_Oh_poly;
set S = R_Algebra_of_Big_Oh_poly;
A3: the carrier of R_Algebra_of_Big_Oh_poly
= X by defAlgebra;
thus f+g = ((RealFuncAdd(NAT)) || X). ( [f,g] ) by defAlgebra
.=f1+g1 by A1,A3,FUNCT_1:49;
end;
theorem LM17:
for f be Point of R_Algebra_of_Big_Oh_poly,
f1 be Point of RAlgebra NAT,
a be Element of REAL st f=f1 holds
a*f = a*f1
proof
let f be Point of R_Algebra_of_Big_Oh_poly,
f1 be Point of RAlgebra NAT,
a be Element of REAL;
assume A1: f=f1;
set X = Big_Oh_poly;
set S = R_Algebra_of_Big_Oh_poly;
A3: the carrier of R_Algebra_of_Big_Oh_poly
= X by defAlgebra;
thus a*f = ((RealFuncExtMult(NAT)) | [:REAL,X:]). ( [a,f] ) by defAlgebra
.=a*f1 by A1,A3,
FUNCT_1:49;
end;
theorem LM18:
0.R_Algebra_of_Big_Oh_poly = 0.(RAlgebra NAT) by defAlgebra;
theorem LM19:
1. (R_Algebra_of_Big_Oh_poly) = 1. (RAlgebra NAT) by defAlgebra;
registration
cluster R_Algebra_of_Big_Oh_poly
-> strict Abelian add-associative right_zeroed
right_complementable commutative associative right_unital
right-distributive vector-associative scalar-associative
vector-distributive scalar-distributive;
correctness
proof
set S = R_Algebra_of_Big_Oh_poly;
thus S is strict;
thus S is Abelian
proof
let x,y be Element of S;
reconsider x1=x,y1=y as Element of RAlgebra NAT by LM12;
thus x+y = x1+y1 by LM16
.=y + x by LM16;
end;
thus S is add-associative
proof
let x,y,z be Element of S;
reconsider x1=x,y1=y,z1=z as Element of RAlgebra NAT by LM12;
D1: x+y = x1+y1 by LM16;
D2: y+z = y1+z1 by LM16;
thus (x+y)+z= (x1+y1)+z1 by D1,LM16
.=x1+(y1+z1) by RLVECT_1:def 3
.=x+ (y + z) by D2,LM16;
end;
thus S is right_zeroed
proof let x be Element of S;
reconsider x1=x as Element of RAlgebra NAT
by LM12;
thus x+0.S = x1+ 0.(RAlgebra NAT) by LM18,LM16
.= x;
end;
thus S is right_complementable
proof
let x be Element of S;
reconsider x1=x as Element of RAlgebra NAT by LM12;
set t1=(-1)*x;
take t1;
-1 is Element of REAL by XREAL_0:def 1; then
D1: (-1)*x = (-1)*x1 by LM17;
thus x+t1 = x1+ (-1)*x1 by D1,LM16
.= 0.(RAlgebra NAT) by FUNCSDOM:11
.= 0.S by defAlgebra;
end;
for x,y be Element of S holds x*y = y*x
proof
let x,y be Element of S;
reconsider x1=x,y1=y as Element of RAlgebra NAT by LM12;
thus x*y = x1*y1 by LM15
.=y * x by LM15;
end;
hence S is commutative;
for x,y,z be Element of S holds x*y*z = x*(y*z)
proof
let x,y,z be Element of S;
reconsider x1=x,y1=y,z1=z as Element of RAlgebra NAT by LM12;
D1: x*y = x1*y1 by LM15;
D2: y*z = y1*z1 by LM15;
thus (x*y)*z= (x1*y1)*z1 by D1,LM15
.=x1*(y1*z1) by GROUP_1:def 3
.=x* (y * z) by D2,LM15;
end;
hence S is associative;
thus S is right_unital
proof
let x be Element of S;
reconsider x1=x as Element of RAlgebra NAT by LM12;
thus x*(1.S) = x1*1.(RAlgebra NAT) by LM19,LM15
.=x by VECTSP_1:def 4;
end;
for x,y,z be Element of S holds x*(y+z) =x*y+x*z
proof
let x,y,z be Element of S;
reconsider x1=x,y1=y,z1=z
as Element of RAlgebra NAT by LM12;
D1: x*y = x1*y1 by LM15;
D2: x*z = x1*z1 by LM15;
D3: y+z = y1+z1 by LM16;
thus x*(y+z) = x1*(y1+z1) by D3,LM15
.=x1*y1+x1*z1 by VECTSP_1:def 2
.=x*y + x*z by D1,D2,LM16;
end;
hence S is right-distributive;
for x, y being Element of S
for s being Real holds s * (x * y) = (s * x) * y
proof
let x,y be Element of S;
let s be Real;
reconsider x1=x,y1=y
as Element of RAlgebra NAT by LM12;
D1: x*y = x1*y1 by LM15;
D3: s is Element of REAL by XREAL_0:def 1;
then
D2: s*x = s*x1 by LM17;
thus s * (x * y) = s * (x1 * y1) by LM17,D1,D3
.=(s*x1)*y1 by FUNCSDOM:def 9
.= (s*x)*y by LM15,D2;
end;
hence S is vector-associative;
for s,t be Real,x be Element of S holds (s*t)*x = s*(t*x)
proof
let s,t be Real;
let x be Element of S;
reconsider x1=x as Element of RAlgebra NAT by LM12;
D0: s is Element of REAL
& t is Element of REAL by XREAL_0:def 1;
D2: s*t is Element of REAL by XREAL_0:def 1;
D1: t*x = t*x1 by D0,LM17;
thus (s*t)*x =(s*t)*x1 by D2,LM17
.=s*(t*x1) by RLVECT_1:def 7
.=s*(t*x) by D0,D1,LM17;
end;
hence S is scalar-associative;
for s being Real
for x, y being Element of S
holds s * (x + y) = s * x + s * y
proof
let s be Real;
let x,y be Element of S;
reconsider x1=x,y1=y
as Element of RAlgebra NAT by LM12;
D1: x+y = x1+y1 by LM16;
D3: s is Element of REAL by XREAL_0:def 1; then
D2: s*x = s*x1 by LM17;
D4: s*y = s*y1 by LM17,D3;
thus s * (x + y) = s * (x1 + y1) by LM17,D1,D3
.=s*x1+ s*y1 by RLVECT_1:def 5
.= s*x + s*y by LM16,D2,D4;
end;
hence S is vector-distributive;
let s,t be Real, v being Element of S;
reconsider s,t as Element of REAL by XREAL_0:def 1;
reconsider v1=v
as Element of RAlgebra NAT by LM12;
D2: s*v = s*v1 by LM17;
D4: t*v = t*v1 by LM17;
(s + t) * v = (s + t) * v1 by LM17
.= s*v1 +t*v1 by RLVECT_1:def 6
.= s*v +t*v by D2,D4,LM16;
hence thesis;
end;
end;
theorem
R_Algebra_of_Big_Oh_poly is Algebra;
theorem TH11:
for f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly
for f9,g9,h9 be Function of NAT,REAL
st f9=f & g9=g & h9=h holds
(h = f+g iff for x be Nat holds h9.x = f9.x + g9.x)
proof
let f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly;
reconsider f1=f,g1=g,h1=h as VECTOR of RAlgebra NAT by LM12;
let f9,g9,h9 be Function of NAT,REAL such that
A2: f9=f & g9=g & h9=h;
A3: now
assume
A4: h = f+g;
let x be Nat;
LXN:x in NAT by ORDINAL1:def 12;
h1=f1+g1 by A4,LM16;
hence h9.x=f9.x+g9.x by A2,FUNCSDOM:1,LXN;
end;
now
assume LAS:for x be Nat holds h9.x=f9.x+g9.x;
for x be Element of NAT holds h9.x=f9.x+g9.x by LAS;
then h1=f1+g1 by A2,FUNCSDOM:1;
hence h =f+g by LM16;
end;
hence thesis by A3;
end;
theorem TH11A:
for f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly
for f9,g9,h9 be Function of NAT,REAL
st f9=f & g9=g & h9=h holds
(h = f*g iff for x be Nat holds h9.x = f9.x * g9.x )
proof
let f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly;
reconsider f1=f,g1=g,h1=h as VECTOR of RAlgebra NAT by LM12;
let f9,g9,h9 be Function of NAT,REAL such that
A2: f9=f & g9=g & h9=h;
A3: now
assume
A4: h = f*g;
let x be Nat;
LXN:x in NAT by ORDINAL1:def 12;
h1=f1*g1 by A4,LM15;
hence h9.x=f9.x*g9.x by A2,FUNCSDOM:2,LXN;
end;
now
assume for x be Element of NAT holds h9.x=f9.x*g9.x;
then h1=f1*g1 by A2,FUNCSDOM:2;
hence h =f*g by LM15;
end;
hence thesis by A3;
end;
theorem TH12:
for f,h be VECTOR of R_Algebra_of_Big_Oh_poly
for f9,h9 be Function of NAT,REAL
st f9=f & h9=h
for a be Real holds h = a*f iff
for x be Nat holds h9.x = a*f9.x
proof
let f,h be VECTOR of R_Algebra_of_Big_Oh_poly;
let f9,h9 be Function of NAT,REAL such that
A1: f9=f & h9=h;
let a be Real;
A0:a is Element of REAL by XREAL_0:def 1;
reconsider f1=f, h1=h as VECTOR of RAlgebra NAT by LM12;
A3: now
assume
A4: h = a*f;
let x be Nat;
LXN:x in NAT by ORDINAL1:def 12;
h1=a*f1 by A4,LM17,A0;
hence h9.x=a*f9.x by A1,FUNCSDOM:4,LXN;
end;
now
assume for x be Element of NAT holds h9.x=a*f9.x;
then h1=a*f1 by A1,FUNCSDOM:4;
hence h =a*f by A0,LM17;
end;
hence thesis by A3;
end;
begin :: negligible functions
definition
let f be Function of NAT,REAL;
attr f is negligible means
:defneg:
for c be non empty positive-yielding XFinSequence of REAL holds
ex N be Nat st
for x be Nat st N <=x holds |. f.x .| < 1/((polynom(c)).x);
end;
theorem PXR1:
for r be Real st 0 < r holds
ex c be non empty positive-yielding XFinSequence of REAL st
for x be Nat holds (polynom(c)).x = r
proof
let r be Real;
assume AS: 0 < r;
r is Element of REAL by XREAL_0:def 1;then
reconsider z= <% r %> as XFinSequence of REAL;
now let x be Real;
assume x in rng z; then
x in {r} by AFINSQ_1:33;
hence 0 < x by AS,TARSKI:def 1;
end;
then
A1: z is positive-yielding;
reconsider z as non empty
positive-yielding XFinSequence of REAL by A1;
take z;
len z = 1 by AFINSQ_1:34;
then consider a be Real such that
A2: a = z.0 &
for x be Nat holds (seq_p(z)).x = a by ASYMPT_2:29;
thus thesis by A2;
end;
theorem PXR2:
for f be Function of NAT,REAL
st f is negligible
holds for r be Real st 0 < r
holds
ex N be Nat st for x be Nat st N <=x holds |. f.x .| < r
proof
let f be Function of NAT,REAL;
assume AS: f is negligible;
let r be Real;
assume 0 < r;then
consider c be non empty positive-yielding XFinSequence of REAL
such that
P1: for x be Nat holds (polynom(c)).x = 1/r by PXR1;
consider N be Nat such that
P2: for x be Nat
st N <=x holds |. f.x .| < 1/((polynom(c)).x) by AS;
take N;
thus for x be Nat
st N <=x holds |. f.x .| < r
proof
let x be Nat;
assume N <=x;
then
|. f.x .| < 1/((polynom(c)).x) by P2;
then
|. f.x .| < 1/(1/r) by P1;
hence
|. f.x .| < r by XCMPLX_1:52;
end;
end;
theorem
for f be Function of NAT,REAL
st f is negligible
holds f is convergent & lim f = 0
proof
let f be Function of NAT,REAL;
assume AS: f is negligible;
A1:for p be Real st 0<p ex n be Nat st for m be Nat
st n<=m holds |. f.m - 0 .| < p
proof
let p be Real;
assume 0<p;
then
consider N be Nat such that
P1: for x be Nat
st N <=x holds |. f.x .| < p by AS,PXR2;
reconsider N as Nat;
take N;
let m be Nat;
assume P2: N<=m;
reconsider x=m as Element of NAT by ORDINAL1:def 12;
thus |. f.m - 0 .| < p by P1,P2;
end;
hence f is convergent by SEQ_2:def 6;
hence lim f = 0 by A1,SEQ_2:def 7;
end;
registration
cluster seq_const 0 -> negligible;
coherence
proof
set f = seq_const 0;
let c be non empty positive-yielding XFinSequence of REAL;
take N = 0;
let x be Nat;
D2: |. f.x .| = |. 0 .| by SEQ_1:57
.= 0;
0 < (polynom(c)).x by NLM3;
hence thesis by D2;
end;
end;
registration
cluster negligible for Function of NAT,REAL;
correctness
proof
seq_const 0 is negligible;
hence thesis;
end;
end;
registration
let f be negligible Function of NAT,REAL;
cluster |.f.| -> negligible for Function of NAT,REAL;
coherence
proof
let g be Function of NAT,REAL such that
A1: g = |.f.|;
let c be non empty positive-yielding XFinSequence of REAL;
consider N be Nat such that
D3: for x be Nat
st N <=x holds |. f.x .| < 1/((polynom(c)).x) by defneg;
take N;
let x be Nat;
assume B1: N <=x;
|. |.f.|.x .| = |. |.f.x.| .| by SEQ_1:12
.= |. f.x .|;
hence thesis by A1,D3,B1;
end;
end;
registration
let f be negligible Function of NAT,REAL,
a be Real;
cluster a(#)f -> negligible for Function of NAT,REAL;
coherence
proof
let g be Function of NAT,REAL such that
A1: g = a(#)f;
let c be non empty positive-yielding XFinSequence of REAL;
per cases;
suppose D1: a=0;
take N = 0;
let x be Nat;
assume N <=x;
D2: |. (a(#)f).x .| = |. a*f.x .| by VALUED_1:6
.= 0 by D1;
0 < (polynom(c)).x by NLM3;
hence thesis by A1,D2;
end;
suppose F1: a<>0;
reconsider c1 = |.a .| (#) c as
non empty positive-yielding XFinSequence of REAL by F1;
consider N be Nat such that
F3: for x be Nat
st N <=x holds |. f.x .| < 1/((polynom(c1)).x) by defneg;
take N;
let x be Nat;
assume F4: N <=x;
K2: 0 < (polynom(c)).x by NLM3;
F6: (polynom(c1)).x = |. a .| * ((polynom(c)).x) by NLM4;
K4: 0 < (polynom(c1)).x by NLM3;
|. f.x .| < 1/((polynom(c1)).x) by F3,F4;
then
|. f.x .| * ((polynom(c1)).x)< 1/((polynom(c1)).x)
* ((polynom(c1)).x) by K4,XREAL_1:68; then
(|. f.x .|* |. a .|) * (polynom(c)).x < 1 by F6,K4,XCMPLX_1:87;
then
|. a*f.x .|* ((polynom(c)).x) < 1 by COMPLEX1:65;
then
|. (a(#)f).x .|* ((polynom(c)).x) < 1 by VALUED_1:6;
then
|. (a(#)f).x .|* ((polynom(c)).x)/((polynom(c)).x)
< 1/((polynom(c)).x) by K2,XREAL_1:74;
hence thesis by A1,K2,XCMPLX_1:89;
end;
end;
end;
registration
let f,g be negligible Function of NAT,REAL;
cluster f+g -> negligible for Function of NAT,REAL;
coherence
proof
let h be Function of NAT,REAL such that
A0: h = f+g;
let c be non empty positive-yielding XFinSequence of REAL;
reconsider c1 = 2 (#) c as
non empty positive-yielding XFinSequence of REAL;
consider N1 be Nat such that
D1: for x be Nat
st N1 <=x holds |. f.x .| < 1/((polynom(c1)).x) by defneg;
consider N2 be Nat such that
D2: for x be Nat
st N2 <=x holds |. g.x .| < 1/((polynom(c1)).x) by defneg;
take N=N1+N2;
let x be Nat;
assume D3: N <=x;
N1 <= N by NAT_1:12;
then
N1<= x by D3,XXREAL_0:2;
then
D4: |. f.x .| < 1/((polynom(c1)).x) by D1;
N2 <= N by NAT_1:12;
then
N2<= x by D3,XXREAL_0:2;
then
D5: |. g.x .| < 1/((polynom(c1)).x) by D2;
F6: (polynom(c1)).x = 2 * ((polynom(c)).x) by NLM4;
|. (f+g).x .| = |. f.x + g.x .|
proof
x in NAT by ORDINAL1:def 12;
hence thesis by VALUED_1:1;
end;
then
D6: |. (f+g).x .| <= |. f.x .| + |. g.x .| by COMPLEX1:56;
|. f.x .| + |. g.x .|
< (1/((polynom(c1)).x)) + (1/((polynom(c1)).x))
by D4,D5,XREAL_1:8;
then
|. (f+g).x .| < 2* (1/((polynom(c1)).x))
by XXREAL_0:2,D6;
hence thesis by A0,XCMPLX_1:92,F6;
end;
end;
registration
let f,g be negligible Function of NAT,REAL;
cluster f(#)g -> negligible for Function of NAT,REAL;
coherence
proof
let h be Function of NAT,REAL such that
A0: h = f(#)g;
let c1 be non empty positive-yielding XFinSequence of REAL;
consider N1 be Nat such that
D1: for x be Nat
st N1 <=x holds |. f.x .| < 1/2 by PXR2;
consider N2 be Nat such that
D2: for x be Nat
st N2 <=x holds |. g.x .| < 1/((polynom(c1)).x) by defneg;
take N=N1+N2;
let x be Nat;
assume D3: N <=x;
N1 <= N by NAT_1:12; then
N1<= x by D3,XXREAL_0:2; then
D4: |. f.x .| < 1/2 by D1;
N2 <= N by NAT_1:12; then
N2<= x by D3,XXREAL_0:2; then
D5: |. g.x .| < 1/((polynom(c1)).x) by D2; then
F6: (1/2) * (1/((polynom(c1)).x))
< 1* (1/((polynom(c1)).x)) by XREAL_1:97;
|. (f(#)g).x .| = |. f.x * g.x .| by VALUED_1:5; then
D6: |. (f(#)g).x .| = |. f.x .| * |. g.x .| by COMPLEX1:65;
|. f.x .| * |. g.x .| <= (1/2) * (1/((polynom(c1)).x))
by D4,D5,XREAL_1:66;
hence thesis by A0,F6,XXREAL_0:2,D6;
end;
end;
theorem TH3:
for f be Function of NAT,REAL
st for x be Nat holds f.x = 1/ (2 to_power x)
holds f is negligible
proof
let f be Function of NAT,REAL;
assume AS: for x be Nat holds f.x = 1/ (2 to_power x);
let c be non empty positive-yielding XFinSequence of REAL;
set k = len c;
deffunc F(Nat) = 1*($1 to_power k);
consider y be Real_Sequence such that
P1: for x be Nat holds y.x = F(x) from SEQ_1:sch 1;
consider N1 be Nat such that
P2: for x be Nat st N1 <=x holds |.(seq_p(c)).x .| <= y.x
by ASYMPT_2:43,P1;
consider N2 be Nat such that
P3: for x be Nat st N2 <= x
holds 1/ (2 to_power x) < 1/ (x to_power k) by L2;
set N=N1+N2;
reconsider N as Element of NAT by ORDINAL1:def 12;
take N;
thus for x be Nat
st N <=x holds |. f.x .| < 1/((polynom(c)).x)
proof
let x be Nat;
assume D3:N <=x;
K1: f.x = 1/ (2 to_power x) by AS;
N2 <= N by NAT_1:12; then
N2<= x by D3,XXREAL_0:2; then
1/ (2 to_power x) < 1/ (x to_power k) by P3; then
P4: |.f.x .| < 1/ (x to_power k) by K1,ABSVALUE:def 1;
N1 <= N by NAT_1:12; then
N1<= x by D3,XXREAL_0:2; then
|.(polynom(c)).x .| <= y.x by P2; then
(polynom(c)).x <= y.x by ABSVALUE:def 1; then
(polynom(c)).x <= 1*(x to_power k) by P1; then
1/ x to_power k <= 1/ ((polynom(c)).x) by XREAL_1:118,NLM3;
hence |.f.x .| < 1/ ((polynom(c)).x) by P4,XXREAL_0:2;
end;
end;
theorem TH4:
for f,g be Function of NAT,REAL
st f is negligible &
for x be Nat holds |. g.x .| <= |. f.x .| holds
g is negligible
proof
let f,g be Function of NAT,REAL;
assume AS: f is negligible &
for x be Nat holds |. g.x .| <= |.f.x.|;
thus g is negligible
proof
let c be non empty positive-yielding XFinSequence of REAL;
consider N be Nat such that
D3: for x be Nat st N <=x holds |. f.x .| < 1/((polynom(c)).x) by AS;
take N;
let x be Nat;
assume N <=x;
then
D2: |. f.x .| < 1/((polynom(c)).x) by D3;
|. g.x .| <= |. f.x .| by AS;
hence thesis by D2,XXREAL_0:2;
end;
end;
registration
cluster negligible -> polynomially-abs-bounded for Function of NAT,REAL;
coherence
proof
let f be Function of NAT,REAL;
assume
A0: f is negligible;
consider c be non empty positive-yielding XFinSequence of REAL
such that
P1: for x be Nat holds (polynom(c)).x = 1 by PXR1;
consider N be Nat such that
P2: for x be Nat
st N <=x holds |. f.x .| < 1/((polynom(c)).x) by A0;
set s =|. f .|;
ZP1: s in Funcs(NAT, REAL) by FUNCT_2:8;
now
let n be Element of NAT;
assume A2: n >= N+2;
2<=N+2 by NAT_1:12; then
2 <= n by A2,XXREAL_0:2;
then A3: n > 1 by XXREAL_0:2;
A4: (seq_n^ 1) . n = n to_power 1 by A2, ASYMPT_1:def 3
.=n;
A5: s.n = |. f.n .| by VALUED_1:18;
N <= N+2 by NAT_1:12; then
N <= n by A2,XXREAL_0:2; then
s.n < 1/((polynom(c)).n) by A5,P2; then
s.n < 1/1 by P1;
hence s.n <= 1*(seq_n^ 1).n by XXREAL_0:2,A3,A4;
thus s.n >= 0 by A5;
end;
then s in Big_Oh(seq_n^ 1) by ZP1;
hence thesis;
end;
end;
definition
func negligibleFuncs -> Subset of Big_Oh_poly means
:Def1:
for x being object holds x in it
iff x is negligible Function of NAT,REAL;
existence
proof
defpred P[object] means $1 is negligible Function of NAT,REAL;
consider IT being set such that
A01: for x being object holds x in IT iff x in Funcs(NAT,REAL)
& P[x] from XBOOLE_0:sch 1;
A1: for x being object holds x in IT
iff x is negligible Function of NAT,REAL
proof
let x be object;
x is negligible Function of NAT,REAL implies
x in Funcs(NAT,REAL) by FUNCT_2:8;
hence thesis by A01;
end;
for x be object st x in IT holds x in Big_Oh_poly
proof
let x be object;
assume x in IT; then
x is negligible Function of NAT,REAL by A1;
hence x in Big_Oh_poly by DefX1;
end;
then IT is Subset of Big_Oh_poly by TARSKI:def 3;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of Big_Oh_poly;
assume that
A2: for x being object holds x in X1 iff
x is negligible Function of NAT,REAL and
A3: for x being object holds x in X2 iff
x is negligible Function of NAT,REAL;
thus X1 c= X2
proof
let x be object;
assume x in X1;
then x is negligible Function of NAT,REAL by A2;
hence thesis by A3;
end;
let x be object;
assume x in X2;
then x is negligible Function of NAT,REAL by A3;
hence thesis by A2;
end;
end;
registration
cluster negligibleFuncs -> non empty;
coherence
proof
the negligible Function of NAT,REAL in negligibleFuncs by Def1;
hence thesis;
end;
end;
theorem RSSPAC2:
for v, w being VECTOR of R_Algebra_of_Big_Oh_poly,
v1,w1 being Function of NAT,REAL
st v=v1 & w1=w
holds v + w = v1 + w1
proof
let v, w be VECTOR of R_Algebra_of_Big_Oh_poly,
v1,w1 being Function of NAT,REAL;
assume A0: v=v1 & w1=w;
v+w in the carrier of R_Algebra_of_Big_Oh_poly;
then
v+w in Big_Oh_poly by defAlgebra;then
reconsider h=v+w as Function of NAT,REAL by DefX1;
h = v1 + w1
proof
let n be Element of NAT;
thus h. n = (v1 . n) + (w1 . n) by A0,TH11
.= (v1 + w1) . n by VALUED_1:1;
end;
hence v + w = v1 + w1;
end;
theorem RSSPAC2A:
for v, w being VECTOR of R_Algebra_of_Big_Oh_poly,
v1,w1 being Function of NAT,REAL
st v=v1 & w1=w
holds v * w = v1 (#) w1
proof
let v, w be VECTOR of R_Algebra_of_Big_Oh_poly,
v1,w1 be Function of NAT,REAL;
assume A0: v=v1 & w1=w;
v*w in the carrier of R_Algebra_of_Big_Oh_poly;
then
v*w in Big_Oh_poly by defAlgebra;then
reconsider h=v*w as Function of NAT,REAL by DefX1;
h = v1 (#) w1
proof
let n be Element of NAT;
thus h. n = (v1 . n) * (w1 . n) by TH11A,A0
.= (v1 (#) w1) . n by VALUED_1:5;
end;
hence v * w = v1 (#) w1;
end;
theorem RSSPAC3:
for a be Real,v being VECTOR of R_Algebra_of_Big_Oh_poly,
v1 be Function of NAT,REAL
st v=v1
holds a*v= a (#) v1
proof
let a be Real;
let v be VECTOR of R_Algebra_of_Big_Oh_poly,
v1 be Function of NAT,REAL;
assume A0: v=v1;
a*v in the carrier of R_Algebra_of_Big_Oh_poly;
then
a*v in Big_Oh_poly by defAlgebra;then
reconsider h=a*v as Function of NAT,REAL by DefX1;
h = a (#) v1
proof
let n be Element of NAT;
thus h. n = a* (v1 . n) by TH12,A0
.= (a (#) v1) . n by VALUED_1:6;
end;
hence a*v = a (#) v1;
end;
theorem
for a be Real
for v be VECTOR of R_Algebra_of_Big_Oh_poly
st v in negligibleFuncs
holds a * v in negligibleFuncs
proof
let a be Real;
let v be VECTOR of R_Algebra_of_Big_Oh_poly;
assume v in negligibleFuncs;
then
reconsider v1=v as negligible Function of NAT,REAL by Def1;
a(#)v1 is negligible;
then
a*v is negligible Function of NAT,REAL by RSSPAC3;
hence thesis by Def1;
end;
theorem
for v,u be VECTOR of R_Algebra_of_Big_Oh_poly
st v in negligibleFuncs & u in negligibleFuncs
holds v + u in negligibleFuncs
proof
let v,u be VECTOR of R_Algebra_of_Big_Oh_poly;
assume v in negligibleFuncs & u in negligibleFuncs; then
reconsider v1=v,u1=u as negligible Function of NAT,REAL by Def1;
v1+u1 is negligible; then
v+u is negligible Function of NAT,REAL by RSSPAC2;
hence thesis by Def1;
end;
theorem
for v,u be VECTOR of R_Algebra_of_Big_Oh_poly
st v in negligibleFuncs & u in negligibleFuncs
holds v * u in negligibleFuncs
proof
let v,u be VECTOR of R_Algebra_of_Big_Oh_poly;
assume v in negligibleFuncs
& u in negligibleFuncs;
then
reconsider v1=v,u1=u as negligible Function of NAT,REAL by Def1;
v1(#)u1 is negligible;
then
v*u is negligible Function of NAT,REAL by RSSPAC2A;
hence thesis by Def1;
end;
definition
let f,g be Function of NAT,REAL;
pred f negligibleEQ g means
ex h be Function of NAT,REAL
st h is negligible
&
for x be Nat holds |. f.x - g.x .| <= |.h.x.|;
reflexivity
proof
let f be Function of NAT,REAL;
deffunc F(Nat) = 1/ (2 to_power $1);
consider h be Real_Sequence such that
P1: for x be Nat holds h.x = F(x) from SEQ_1:sch 1;
take h;
thus h is negligible by TH3,P1;
let x be Nat;
|. f.x - f.x .| = 0;
hence |. f.x - f.x .| <=|.h.x.|;
end;
symmetry
proof
let f,g be Function of NAT,REAL;
given h be Function of NAT,REAL such that
P1: h is negligible &
for x be Nat holds |. f.x - g.x .| <= |.h.x.|;
take h;
thus h is negligible by P1;
let x be Nat;
|. f.x - g.x .| <= |.h.x.| by P1;
hence |. g.x - f.x .| <= |.h.x.| by COMPLEX1:60;
end;
end;
theorem
for f,g,h be Function of NAT,REAL
st f negligibleEQ g & g negligibleEQ h
holds f negligibleEQ h
proof
let f,g,h be Function of NAT,REAL;
given v be Function of NAT,REAL such that
B1: v is negligible
&
for x be Nat holds
|. f.x - g.x .| <= |.v.x.|;
given w be Function of NAT,REAL such that
B2: w is negligible
&
for x be Nat
holds |. g.x - h.x .| <= |.w.x.|;
take u = |.v.| + |.w.|;
thus u is negligible by B1,B2;
let x be Nat;
B4: |. f.x - g.x .| <= |.v.x.| by B1;
B5: |. g.x - h.x .| <= |.w.x.| by B2;
|. f.x - h.x .| = |. (f.x -g.x) + (g.x - h.x) .|;
then
B6: |. f.x - h.x .| <= |. (f.x -g.x) .|
+ |. (g.x -h.x) .| by COMPLEX1:56;
|. (f.x -g.x) .| + |. g.x - h.x .|
<= |.v.x.| + |.w.x.| by B4,B5,XREAL_1:7;
then
B7: |. f.x - h.x .| <= |.v.x.| + |.w.x.| by B6,XXREAL_0:2;
x in NAT by ORDINAL1:def 12;then
consider y be Element of NAT such that LXY: x=y;
|.v.x.| + |.w.x.| = (|. v .|).x + |.w.x.| by SEQ_1:12
.= (|. v .|).x + (|. w .|).x by SEQ_1:12
.= (|. v .|+|. w .|).x by LXY,VALUED_1:1;
hence |. f.x - h.x .| <= |. u.x .| by B7,ABSVALUE:def 1;
end;
theorem
for f,g be Function of NAT,REAL
holds f negligibleEQ g iff f-g is negligible
proof
let f,g be Function of NAT,REAL;
hereby assume
A1: f negligibleEQ g;
consider v be Function of NAT,REAL such that
B1: v is negligible &
for x be Nat
holds |. f.x - g.x .| <= |.v.x.| by A1;
for x be Nat holds |. (f-g).x .| <= |.v.x.|
proof
let x be Nat;
x in NAT by ORDINAL1:def 12;then
consider y be Element of NAT such that LXY: x=y;
|. (f-g).y .| = |. f.y-g.y .| by VALUED_1:15;
hence thesis by B1,LXY;
end;
hence (f-g) is negligible by B1,TH4;
end;
set v = f-g;
for x be Nat holds |. f.x-g.x .| <= |.v.x.|
proof
let x be Nat;
x in NAT by ORDINAL1:def 12;
hence thesis by VALUED_1:15;
end;
hence thesis;
end;
theorem LRNG1:
for c be non empty positive-yielding XFinSequence of REAL
ex a be Real, k,N be Nat
st 0 < a & 0 < k
& for x be Nat st N<= x holds (polynom(c)).x <=a* (x to_power k)
proof
let c be non empty positive-yielding XFinSequence of REAL;
1 - 1 <= (len c) -1 by XREAL_1:9,NAT_1:14;then
(len c) -1 in NAT by INT_1:3;then
reconsider k = (len c) -1 as Nat;
C1:len c = k+1;
k+1 -1 < len c - 0 by XREAL_1:15;
then
k in Segm(len c) by NAT_1:44; then
C2: c.k in rng c by FUNCT_1:3;
for n being Nat st 0 <= n holds
0 <= (seq_p(c)).n by NLM3;
then
reconsider f = seq_p(c) as
eventually-nonnegative Real_Sequence by ASYMPT_0:def 2;
f in Big_Oh( seq_n^(k) ) by ASYMPT_2:45,C1,C2,PARTFUN3:def 1;
then
consider N be Nat such that C5:
for x be Nat st N <= x holds
f.x <= (seq_n^(k+1)).x by ASYMPT_2:39;
reconsider m = k+1 as Nat;
reconsider M = N+1 as Nat;
take 1,m,M;
for x be Nat st M <= x holds f.x <= 1* (x to_power m)
proof
let x be Nat;
assume C8:M <= x;
CX: x is Element of NAT by ORDINAL1:def 12;
N+1 -1 < M -0 by XREAL_1:15; then
N < x by C8,XXREAL_0:2; then
f.x <= (seq_n^(m)).x by C5;
hence thesis by C8,ASYMPT_1:def 3,CX;
end;
hence thesis;
end;
registration
let a be nonnegative-yielding XFinSequence of REAL,
b be nonnegative-yielding Real_Sequence;
cluster a (#) b -> nonnegative-yielding;
coherence;
end;
registration
let a,b be nonnegative-yielding XFinSequence of REAL;
cluster a ^ b -> nonnegative-yielding;
coherence
proof
for r being Real st r in rng (a^b) holds 0 <= r
proof
let r be Real;
assume r in rng (a^b);then
r in (rng a \/ rng b) by AFINSQ_1:26;
then
r in rng a or r in rng b by XBOOLE_0:def 3;
hence thesis by PARTFUN3:def 4;
end;
hence thesis;
end;
end;
registration
let a,b,c be non negative Real;
cluster seq_a^(a,b,c) -> nonnegative-yielding;
coherence
proof
set f = seq_a^(a,b,c);
for r be Real st r in rng f holds r >= 0
proof
let r be Real;
assume r in rng f; then
consider n being object such that
A2: n in dom f & r = f.n by FUNCT_1:def 3;
reconsider n as Element of NAT by A2;
LL1:r = a to_power (b*n+c) by ASYMPT_1:def 1,A2;
now per cases;
case CA0: a = 0;
now per cases;
case b*n+c <>0;
hence thesis by CA0,LL1,POWER:def 2;
end;
case b*n+c = 0;
hence thesis by POWER:24,LL1;
end;
end;
hence thesis;
end;
case 0 < a;
hence thesis by LL1,POWER:34;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
theorem LRNG2:
for a be Real, k be Nat holds
ex c be non empty positive-yielding XFinSequence of REAL
st for x be Nat holds a* (x to_power k) <= (polynom(c)).x
proof
let a be Real,k be Nat;
reconsider c = Segm (k+1) --> (|. a .| +1 ) as XFinSequence of REAL;
reconsider c as non empty positive-yielding XFinSequence of REAL;
take c;
for x be Nat holds a* (x to_power k) <=(polynom(c)).x
proof
let x be Nat;
set c2 = c (#) seq_a^(x,1,0);
T0: (polynom(c)).x = Sum(c2) by ASYMPT_2:def 2;
LN2:k +0 < k+1 by XREAL_1:8;
T1:dom c2 = dom c /\ dom seq_a^(x,1,0) by VALUED_1:def 4
.= dom c /\ NAT by SEQ_1:1
.= (Segm (k+1)) /\ NAT;
T3:c2.k=(c.k)*((seq_a^(x,1,0)).k) by VALUED_1:5
.=(c.k)*(x to_power (1*k+0)) by ASYMPT_1:def 1
.= (|. a .| +1)*(x to_power k) by FUNCOP_1:7,NAT_1:44,LN2;
a < (|. a .| +1) by TCL001; then
T4:a*(x to_power k) <= (|. a .| +1)*(x to_power k) by XREAL_1:64;
len c2 = k+1 by T1,XBOOLE_1:28;then
Sum c2 >= (|. a .| +1)*(x to_power k) by T3,AFINSQ_2:61,NAT_1:44,LN2;
hence thesis by T4,XXREAL_0:2,T0;
end;
hence thesis;
end;
theorem RNG0:
for c,s be non empty positive-yielding XFinSequence of REAL
ex d be non empty positive-yielding XFinSequence of REAL,
N be Nat
st for x be Nat st N<= x holds
(polynom(c)).x * (polynom(s)).x <= (polynom(d)).x
proof
let c,s be non empty positive-yielding
XFinSequence of REAL;
consider a1 be Real, k1,N1 be Nat such that
P1: 0 < a1 & 0 < k1
& for x be Nat st N1<= x
holds (polynom(c)).x <=a1* (x to_power k1) by LRNG1;
consider a2 be Real, k2,N2 be Nat such that
P2: 0 < a2 & 0 < k2
& for x be Nat st N2<= x
holds (polynom(s)).x <=a2* (x to_power k2) by LRNG1;
consider d be non empty positive-yielding
XFinSequence of REAL such that
P3: for x be Nat
holds (a1*a2)*(x to_power (k1+k2)) <=(polynom(d)).x by LRNG2;
set N = N1+N2;
take d,N;
let x be Nat;
assume P4:N <=x;
N1<=N by NAT_1:12; then
N1<=x by XXREAL_0:2,P4; then
P5: (polynom(c)).x <=a1* (x to_power k1) by P1;
N2<=N by NAT_1:12; then
N2<=x by XXREAL_0:2,P4; then
P6: (polynom(s)).x <=a2* (x to_power k2) by P2;
P7: 0 < (polynom(c)).x by NLM3;
P8: 0 < (polynom(s)).x by NLM3;
P9: (polynom(c)).x * (polynom(s)).x
<= (a1* (x to_power k1))*(a2* (x to_power k2))
by XREAL_1:66,P5,P6,P7,P8;
P10: (a1* (x to_power k1))*(a2* (x to_power k2))
=(a1*a2)*(x to_power (k1+k2))
proof
per cases;
suppose P11: x=0;
P12: x to_power k1 = 0 by P1,P11,POWER:def 2;
x to_power (k1+k2) =0 by P2,P11,POWER:def 2;
hence thesis by P12;
end;
suppose x<>0; then
(x to_power k1) * (x to_power k2)
= x to_power (k1+k2) by POWER:27;
hence thesis;
end;
end;
(a1*a2)*(x to_power (k1+k2)) <= (polynom(d)).x by P3;
hence (polynom(c)).x * (polynom(s)).x
<=(polynom(d)).x by P9,P10,XXREAL_0:2;
end;
registration
let f be negligible Function of NAT,REAL,
c be non empty positive-yielding XFinSequence of REAL;
cluster (polynom(c)) (#) f -> negligible for Function of NAT,REAL;
coherence
proof
let g be Function of NAT,REAL such that
A0: g = (polynom(c)) (#) f;
let s be non empty positive-yielding XFinSequence of REAL;
consider d be non empty positive-yielding XFinSequence of REAL,
N0 be Nat such that P1: for x be Nat st N0 <= x
holds (polynom(c)).x * (polynom(s)).x <= (polynom(d)).x by RNG0;
consider N1 be Nat such that
P2: for x be Nat
st N1 <=x holds |. f.x .| < 1/((polynom(d)).x) by defneg;
take N=N0+N1;
let x be Nat;
assume P3:N <=x;
P4: 0 < (polynom(c)).x by NLM3;
Q4: 0 < (polynom(d)).x by NLM3;
N1 <= N by NAT_1:12; then
N1<=x by P3,XXREAL_0:2; then
P7: |. f.x .| < 1/((polynom(d)).x) by P2;
P6: |. f.x .|*(polynom(c)).x
< 1/((polynom(d)).x) * (polynom(c)).x by P7,P4,XREAL_1:97;
Q6: 0 < (polynom(s)).x by NLM3;
N0 <= N by NAT_1:12; then
N0<=x by P3,XXREAL_0:2; then
(polynom(c)).x * (polynom(s)).x <= (polynom(d)).x by P1; then
1/(polynom(d)).x <= 1/((polynom(c)).x * (polynom(s)).x)
by P4,Q6,XREAL_1:118; then
P8: 1/(polynom(d)).x * (polynom(c)).x
<= 1/((polynom(c)).x * (polynom(s)).x)
* (polynom(c)).x by Q4,P4,XREAL_1:66;
P5: 1/((polynom(c)).x * (polynom(s)).x ) * (polynom(c)).x
= 1/((polynom(s)).x) by P4,XCMPLX_1:92;
|. f.x .|*(polynom(c)).x = |. f.x .|*|.(polynom(c)).x .|
by P4,ABSVALUE:def 1
.= |. ((polynom(c)).x)*(f.x) .| by COMPLEX1:65
.= |. ((polynom(c))(#)f).x .| by VALUED_1:5;
hence thesis by A0,P5,XXREAL_0:2,P6,P8;
end;
end;
theorem RNG2:
for g be polynomially-abs-bounded Function of NAT,REAL
ex d be non empty positive-yielding XFinSequence of REAL,
N be Nat st for x be Nat
st N<= x holds |. g.x .| <= (polynom(d)).x
proof
let g be polynomially-abs-bounded Function of NAT,REAL;
consider k1 be Nat such that
A4: |.g.| in Big_Oh(seq_n^(k1)) by defabs;
consider t1 be Element of Funcs(NAT, REAL) such that
A6: |.g.|=t1 &
ex c1 be Real,N1 be Element of NAT
st c1 > 0
& for n be Element of NAT
st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n
& t1.n >= 0 by A4;
consider c1 be Real,N1 be Element of NAT such that
A7: c1 > 0
& for n be Element of NAT
st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n
& t1.n >= 0 by A6;
consider d be non empty positive-yielding
XFinSequence of REAL such that
A8: for x be Nat holds
c1* (x to_power k1) <=(polynom(d)).x by LRNG2;
reconsider N=N1+1 as Nat;
take d,N;
let x be Nat;
assume
B1: N<=x;
LXN: x is Element of NAT by ORDINAL1:def 12;
N1<=N by NAT_1:12; then
N1<=x by XXREAL_0:2,B1; then
A9:t1.x <= c1*(seq_n^(k1)).x & t1.x >= 0 by A7,LXN;
A10:(seq_n^(k1)).x = x to_power k1
by ASYMPT_1:def 3,LXN,B1;
c1* (x to_power k1) <=(polynom(d)).x by A8; then
t1.x <= (polynom(d)).x by A10,A9,XXREAL_0:2;
hence |.g.x.| <= (polynom(d)).x by A6,VALUED_1:18;
end;
registration
let f be negligible Function of NAT,REAL,
g be polynomially-abs-bounded Function of NAT,REAL;
cluster g(#)f -> negligible for Function of NAT,REAL;
coherence
proof
let h be Function of NAT,REAL such that
A0: h = g(#)f;
consider s be non empty positive-yielding XFinSequence of REAL,
N0 be Nat such that
P1: for x be Nat st N0 <= x
holds |. g.x .| <= (polynom(s)).x by RNG2;
let d be non empty positive-yielding XFinSequence of REAL;
(polynom(s))(#)f is negligible;
then
consider N1 be Nat such that
P2: for x be Nat
st N1 <=x holds |. ((polynom(s))(#)f).x .| < 1/((polynom(d)).x);
take N=N1+N0;
let x be Nat;
assume P3: N <=x;
P4: |. ( g(#)f ).x .| = |.g.x * f.x .| by VALUED_1:5
.=|.g.x.| *|.f.x.| by COMPLEX1:65;
N0 <= N by NAT_1:12; then
N0 <= x by XXREAL_0:2,P3; then
P6: |. g.x .| <= (polynom(s)).x by P1;
Q7: 0 < (polynom(s)).x by NLM3;
(polynom(s)).x * |.f.x.| = |.(polynom(s)).x .| * |.f.x.|
by Q7,ABSVALUE:def 1
.= |. ((polynom(s)).x)*(f.x) .| by COMPLEX1:65
.= |. ((polynom(s))(#)f).x .| by VALUED_1:5; then
P8: |. ( g(#)f ).x .| <= |. ((polynom(s))(#)f).x .| by P4,XREAL_1:66,P6;
N1<=N by NAT_1:12; then
N1 <= x by P3,XXREAL_0:2; then
|. ((polynom(s))(#)f).x .| < 1/((polynom(d)).x) by P2;
hence thesis by A0,P8,XXREAL_0:2;
end;
end;
theorem
for v,w be VECTOR of R_Algebra_of_Big_Oh_poly
st w in negligibleFuncs
holds v * w in negligibleFuncs
proof
let v,w be VECTOR of R_Algebra_of_Big_Oh_poly;
assume w in negligibleFuncs; then
reconsider w1=w as negligible Function of NAT,REAL by Def1;
v in R_Algebra_of_Big_Oh_poly; then
reconsider v1=v
as polynomially-abs-bounded Function of NAT,REAL by LM14;
v1(#)w1 is negligible; then
v*w is negligible Function of NAT,REAL by RSSPAC2A;
hence thesis by Def1;
end;