let f be eventually-nonnegative Real_Sequence; ( ex b being Element of NAT st
( b >= 2 & f is_smooth_wrt b ) implies f is smooth )
given b being Element of NAT such that A1:
b >= 2
and
A2:
f is_smooth_wrt b
; f is smooth
A3:
f is eventually-nondecreasing
by A2;
then consider N3 being Nat such that
A4:
for n being Nat st n >= N3 holds
f . n <= f . (n + 1)
;
f taken_every b in Big_Oh f
by A2;
then consider t being Element of Funcs (NAT,REAL) such that
A5:
f taken_every b = t
and
A6:
ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) )
;
consider c being Real, N2 being Element of NAT such that
A7:
c > 0
and
A8:
for n being Element of NAT st n >= N2 holds
( t . n <= c * (f . n) & t . n >= 0 )
by A6;
reconsider N = max (N2,N3) as Element of NAT by ORDINAL1:def 12;
A9:
N >= N2
by XXREAL_0:25;
A10:
N >= N3
by XXREAL_0:25;
now for a being Element of NAT st a >= 2 holds
f is_smooth_wrt alet a be
Element of
NAT ;
( a >= 2 implies f is_smooth_wrt a )set i =
[/(log (b,a))\];
A11:
[/(log (b,a))\] >= log (
b,
a)
by INT_1:def 7;
A12:
b > 1
by A1, XXREAL_0:2;
A13:
b <> 1
by A1;
assume A14:
a >= 2
;
f is_smooth_wrt athen
a > 1
by XXREAL_0:2;
then
log (
b,
a)
> log (
b,1)
by A12, POWER:57;
then
log (
b,
a)
> 0
by A1, A13, POWER:51;
then reconsider i =
[/(log (b,a))\] as
Element of
NAT by A11, INT_1:3;
reconsider i1 =
b |^ i as
Element of
NAT ;
A15:
now for n being Element of NAT st n >= N holds
( (f taken_every a) . n <= (c |^ i) * (f . n) & (f taken_every a) . n >= 0 )let n be
Element of
NAT ;
( n >= N implies ( (f taken_every a) . n <= (c |^ i) * (f . n) & (f taken_every a) . n >= 0 ) )defpred S1[
Nat]
means f . ((b |^ $1) * n) <= (c |^ $1) * (f . n);
a >= 1
by A14, XXREAL_0:2;
then A16:
a * n >= 1
* n
by XREAL_1:64;
b to_power (log (b,a)) <= b to_power i
by A12, A11, PRE_FF:8;
then
a <= b |^ i
by A1, A13, POWER:def 3;
then A17:
a * n <= i1 * n
by XREAL_1:64;
assume A18:
n >= N
;
( (f taken_every a) . n <= (c |^ i) * (f . n) & (f taken_every a) . n >= 0 )then A19:
n >= N2
by A9, XXREAL_0:2;
then A20:
t . n <= c * (f . n)
by A8;
A22:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
f . ((b |^ 0) * n) =
f . ((b to_power 0) * n)
.=
f . (1 * n)
by POWER:24
.=
1
* (f . n)
.=
(c to_power 0) * (f . n)
by POWER:24
;
then A26:
S1[
0 ]
;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A26, A22);
then
f . ((b |^ i) * n) <= (c |^ i) * (f . n)
;
then A27:
(f taken_every i1) . n <= (c |^ i) * (f . n)
by Def15;
A28:
n >= N3
by A10, A18, XXREAL_0:2;
then
a * n >= N3
by A16, XXREAL_0:2;
then
f . (a * n) <= f . (i1 * n)
by A4, A17, Th1;
then
(f taken_every a) . n <= f . (i1 * n)
by Def15;
then
(f taken_every a) . n <= (f taken_every i1) . n
by Def15;
hence
(f taken_every a) . n <= (c |^ i) * (f . n)
by A27, XXREAL_0:2;
(f taken_every a) . n >= 0
f . n <= f . (a * n)
by A4, A28, A16, Th1;
hence
(f taken_every a) . n >= 0
by A21, Def15;
verum end;
c |^ i = c to_power i
;
then
(
f taken_every a is
Element of
Funcs (
NAT,
REAL) &
c |^ i > 0 )
by A7, FUNCT_2:8, POWER:34;
then
f taken_every a in Big_Oh f
by A15;
hence
f is_smooth_wrt a
by A3;
verum end;
hence
f is smooth
; verum