set p = seq_const 1;
set G = Big_Oh (seq_const 1);
reconsider F = {(seq_n^ 1)} as FUNCTION_DOMAIN of NAT , REAL by FUNCT_2:121;
let h be eventually-nonnegative Real_Sequence; ex F being FUNCTION_DOMAIN of NAT , REAL st
( F = {(seq_n^ 1)} & ( h in F to_power (Big_Oh (seq_const 1)) implies ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ) ) ) & ( ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ) ) implies h in F to_power (Big_Oh (seq_const 1)) ) )
take
F
; ( F = {(seq_n^ 1)} & ( h in F to_power (Big_Oh (seq_const 1)) implies ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ) ) ) & ( ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ) ) implies h in F to_power (Big_Oh (seq_const 1)) ) )
thus
F = {(seq_n^ 1)}
; ( h in F to_power (Big_Oh (seq_const 1)) iff ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ) ) )
now ( ( h in F to_power (Big_Oh (seq_const 1)) implies ex N being Element of NAT ex i, k being Element of NAT st
( i > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= i * ((seq_n^ k) . n) ) ) ) ) & ( ex N0 being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N0 holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ) ) implies h in F to_power (Big_Oh (seq_const 1)) ) )hereby ( ex N0 being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N0 holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ) ) implies h in F to_power (Big_Oh (seq_const 1)) )
reconsider i = 1 as
Element of
NAT ;
assume
h in F to_power (Big_Oh (seq_const 1))
;
ex N being Element of NAT ex i, k being Element of NAT st
( i > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= i * ((seq_n^ k) . n) ) ) )then consider t being
Element of
Funcs (
NAT,
REAL)
such that A1:
h = t
and A2:
ex
f,
g being
Element of
Funcs (
NAT,
REAL) ex
N being
Element of
NAT st
(
f in F &
g in Big_Oh (seq_const 1) & ( for
n being
Element of
NAT st
n >= N holds
t . n = (f . n) to_power (g . n) ) )
;
consider f,
g being
Element of
Funcs (
NAT,
REAL),
N0 being
Element of
NAT such that A3:
f in F
and A4:
g in Big_Oh (seq_const 1)
and A5:
for
n being
Element of
NAT st
n >= N0 holds
t . n = (f . n) to_power (g . n)
by A2;
consider g9 being
Element of
Funcs (
NAT,
REAL)
such that A6:
g = g9
and A7:
ex
c being
Real ex
N being
Element of
NAT st
(
c > 0 & ( for
n being
Element of
NAT st
n >= N holds
(
g9 . n <= c * ((seq_const 1) . n) &
g9 . n >= 0 ) ) )
by A4;
consider c being
Real,
N1 being
Element of
NAT such that A8:
c > 0
and A9:
for
n being
Element of
NAT st
n >= N1 holds
(
g9 . n <= c * ((seq_const 1) . n) &
g9 . n >= 0 )
by A7;
set k =
[/c\];
A10:
[/c\] > 0
by A8, INT_1:def 7;
set N =
max (2,
(max (N0,N1)));
A11:
max (2,
(max (N0,N1)))
>= max (
N0,
N1)
by XXREAL_0:25;
max (
N0,
N1)
>= N0
by XXREAL_0:25;
then A12:
max (2,
(max (N0,N1)))
>= N0
by A11, XXREAL_0:2;
A13:
[/c\] >= c
by INT_1:def 7;
reconsider k =
[/c\] as
Element of
NAT by A10, INT_1:3;
take N =
max (2,
(max (N0,N1)));
ex i, k being Element of NAT st
( i > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= i * ((seq_n^ k) . n) ) ) )take i =
i;
ex k being Element of NAT st
( i > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= i * ((seq_n^ k) . n) ) ) )take k =
k;
( i > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= i * ((seq_n^ k) . n) ) ) )thus
i > 0
;
for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= i * ((seq_n^ k) . n) )let n be
Element of
NAT ;
( n >= N implies ( 1 <= h . n & h . n <= i * ((seq_n^ k) . n) ) )assume A14:
n >= N
;
( 1 <= h . n & h . n <= i * ((seq_n^ k) . n) )A15:
N >= 2
by XXREAL_0:25;
then
n >= 2
by A14, XXREAL_0:2;
then A16:
n > 1
by XXREAL_0:2;
then A17:
n to_power c <= n to_power k
by A13, PRE_FF:8;
f = seq_n^ 1
by A3, TARSKI:def 1;
then f . n =
n to_power 1
by A15, A14, Def3
.=
n
by POWER:25
;
then A18:
h . n = n to_power (g . n)
by A1, A5, A12, A14, XXREAL_0:2;
max (
N0,
N1)
>= N1
by XXREAL_0:25;
then
N >= N1
by A11, XXREAL_0:2;
then A19:
n >= N1
by A14, XXREAL_0:2;
then
n to_power (g . n) >= n to_power 0
by A6, A16, PRE_FF:8, A9;
hence
1
<= h . n
by A18, POWER:24;
h . n <= i * ((seq_n^ k) . n)A20:
(seq_const 1) . n = 1
by FUNCOP_1:7;
g . n <= c * ((seq_const 1) . n)
by A6, A9, A19;
then
h . n <= n to_power (c * 1)
by A20, A16, A18, PRE_FF:8;
then
h . n <= n to_power k
by A17, XXREAL_0:2;
hence
h . n <= i * ((seq_n^ k) . n)
by A15, A14, Def3;
verum
end; reconsider f =
seq_n^ 1 as
Element of
Funcs (
NAT,
REAL)
by FUNCT_2:8;
reconsider t =
h as
Element of
Funcs (
NAT,
REAL)
by FUNCT_2:8;
given N0 being
Element of
NAT ,
c being
Real,
k being
Element of
NAT such that
c > 0
and A21:
for
n being
Element of
NAT st
n >= N0 holds
( 1
<= h . n &
h . n <= c * ((seq_n^ k) . n) )
;
h in F to_power (Big_Oh (seq_const 1))reconsider N =
max (
N0,2) as
Element of
REAL by XREAL_0:def 1;
defpred S1[
Element of
NAT ,
Real]
means ( ( $1
< N implies $2
= 1 ) & ( $1
>= N implies $2
= log ($1,
(t . $1)) ) );
A22:
N >= 2
by XXREAL_0:25;
then A23:
N > 1
by XXREAL_0:2;
A24:
for
x being
Element of
NAT ex
y being
Element of
REAL st
S1[
x,
y]
consider g being
sequence of
REAL such that A27:
for
x being
Element of
NAT holds
S1[
x,
g . x]
from FUNCT_2:sch 3(A24);
A28:
N >= N0
by XXREAL_0:25;
set c1 =
max (
c,2);
A32:
N <> 1
by XXREAL_0:25;
set a =
log (
N,
(max (c,2)));
set b =
k + (log (N,(max (c,2))));
A33:
max (
c,2)
>= 2
by XXREAL_0:25;
then A34:
max (
c,2)
> 1
by XXREAL_0:2;
A35:
f in F
by TARSKI:def 1;
A36:
g is
Element of
Funcs (
NAT,
REAL)
by FUNCT_2:8;
A37:
N > 0
by XXREAL_0:25;
now ( k + (log (N,(max (c,2)))) > 0 & ( for n being Element of NAT st n >= N holds
( g . n <= (k + (log (N,(max (c,2))))) * ((seq_const 1) . n) & g . n >= 0 ) ) )
log (
N,1)
= 0
by A37, A32, POWER:51;
then
log (
N,
(max (c,2)))
> 0
by A23, A34, POWER:57;
hence
k + (log (N,(max (c,2)))) > 0
;
for n being Element of NAT st n >= N holds
( g . n <= (k + (log (N,(max (c,2))))) * ((seq_const 1) . n) & g . n >= 0 )let n be
Element of
NAT ;
( n >= N implies ( g . n <= (k + (log (N,(max (c,2))))) * ((seq_const 1) . n) & g . n >= 0 ) )A38:
(seq_const 1) . n = 1
by FUNCOP_1:7;
assume A39:
n >= N
;
( g . n <= (k + (log (N,(max (c,2))))) * ((seq_const 1) . n) & g . n >= 0 )then A40:
n <> 1
by A22, XXREAL_0:2;
A41:
(seq_n^ k) . n = n to_power k
by A22, A39, Def3;
then A42:
c * ((seq_n^ k) . n) <= (max (c,2)) * ((seq_n^ k) . n)
by XREAL_1:64, XXREAL_0:25;
(seq_n^ k) . n > 0
by A22, A39, A41, POWER:34;
then A43:
log (
n,
((max (c,2)) * ((seq_n^ k) . n))) =
(log (n,(max (c,2)))) + (log (n,(n to_power k)))
by A22, A33, A39, A40, A41, POWER:53
.=
(log (n,(max (c,2)))) + (k * (log (n,n)))
by A22, A39, A40, POWER:55
.=
(log (n,(max (c,2)))) + (k * 1)
by A22, A39, A40, POWER:52
;
log (
N,
(max (c,2)))
>= log (
n,
(max (c,2)))
by A23, A34, A39, Lm19;
then A44:
(log (n,(max (c,2)))) + k <= (log (N,(max (c,2)))) + k
by XREAL_1:6;
A45:
n >= N0
by A28, A39, XXREAL_0:2;
then A46:
1
<= t . n
by A21;
t . n =
(f . n) to_power (g . n)
by A29, A39
.=
(n to_power 1) to_power (g . n)
by A22, A39, Def3
.=
n to_power (g . n)
by POWER:25
;
then A47:
log (
n,
(t . n)) =
(g . n) * (log (n,n))
by A22, A39, A40, POWER:55
.=
(g . n) * 1
by A22, A39, A40, POWER:52
;
n >= 2
by A22, A39, XXREAL_0:2;
then A48:
n > 1
by XXREAL_0:2;
t . n <= c * ((seq_n^ k) . n)
by A21, A45;
then
t . n <= (max (c,2)) * ((seq_n^ k) . n)
by A42, XXREAL_0:2;
then
log (
n,
(t . n))
<= log (
n,
((max (c,2)) * ((seq_n^ k) . n)))
by A48, A46, PRE_FF:10;
hence
g . n <= (k + (log (N,(max (c,2))))) * ((seq_const 1) . n)
by A47, A43, A44, A38, XXREAL_0:2;
g . n >= 0
g . n = log (
n,
(t . n))
by A27, A39;
then
g . n >= log (
n,1)
by A48, A46, PRE_FF:10;
hence
g . n >= 0
by A22, A39, A40, POWER:51;
verum end; then
g in Big_Oh (seq_const 1)
by A36;
hence
h in F to_power (Big_Oh (seq_const 1))
by A36, A29, A35;
verum end;
hence
( h in F to_power (Big_Oh (seq_const 1)) iff ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ) ) )
; verum