let f be Real_Sequence; :: thesis: ( f in Big_Oh (seq_n^ 1) implies f (#) f in Big_Oh (seq_n^ 2) )
set h = seq_n^ 2;
set g = seq_n^ 1;
assume f in Big_Oh (seq_n^ 1) ; :: thesis: f (#) f in Big_Oh (seq_n^ 2)
then consider t being Element of Funcs (NAT,REAL) such that
A1: t = f and
A2: 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 * ((seq_n^ 1) . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A3: c > 0 and
A4: for n being Element of NAT st n >= N holds
( t . n <= c * ((seq_n^ 1) . n) & t . n >= 0 ) by A2;
set d = max (c,(c * c));
A5: 0 to_power 1 = 0 by POWER:def 2;
A6: now :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
( (t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n) & (t (#) t) . n >= 0 )
take N = N; :: thesis: for n being Element of NAT st n >= N holds
( (t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n) & (t (#) t) . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= N implies ( (t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n) & (t (#) t) . n >= 0 ) )
assume A7: n >= N ; :: thesis: ( (t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n) & (t (#) t) . n >= 0 )
then A8: t . n >= 0 by A4;
for n being Element of NAT holds (seq_n^ 1) . n <= (seq_n^ 2) . n
proof
let n be Element of NAT ; :: thesis: (seq_n^ 1) . n <= (seq_n^ 2) . n
per cases ( n = 0 or n > 0 ) ;
suppose A9: n = 0 ; :: thesis: (seq_n^ 1) . n <= (seq_n^ 2) . n
then (seq_n^ 1) . n = 0 by Def3;
hence (seq_n^ 1) . n <= (seq_n^ 2) . n by A9, Def3; :: thesis: verum
end;
end;
end;
then A14: (seq_n^ 2) . n >= (seq_n^ 1) . n ;
(seq_n^ 1) . n >= 0
proof
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: (seq_n^ 1) . n >= 0
hence (seq_n^ 1) . n >= 0 by Def3; :: thesis: verum
end;
suppose n > 0 ; :: thesis: (seq_n^ 1) . n >= 0
then (seq_n^ 1) . n = n to_power 1 by Def3
.= n by POWER:25 ;
hence (seq_n^ 1) . n >= 0 ; :: thesis: verum
end;
end;
end;
then A15: (c * c) * ((seq_n^ 2) . n) <= (max (c,(c * c))) * ((seq_n^ 2) . n) by A14, XREAL_1:64, XXREAL_0:25;
A16: (n to_power 1) * (n to_power 1) = n to_power (1 + 1)
proof
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: (n to_power 1) * (n to_power 1) = n to_power (1 + 1)
hence (n to_power 1) * (n to_power 1) = n to_power (1 + 1) by A5, POWER:def 2; :: thesis: verum
end;
suppose n > 0 ; :: thesis: (n to_power 1) * (n to_power 1) = n to_power (1 + 1)
hence (n to_power 1) * (n to_power 1) = n to_power (1 + 1) by POWER:27; :: thesis: verum
end;
end;
end;
A17: ((seq_n^ 1) . n) * ((seq_n^ 1) . n) = (seq_n^ 2) . n
proof
per cases ( n = 0 or n > 0 ) ;
suppose A18: n = 0 ; :: thesis: ((seq_n^ 1) . n) * ((seq_n^ 1) . n) = (seq_n^ 2) . n
hence ((seq_n^ 1) . n) * ((seq_n^ 1) . n) = 0 * ((seq_n^ 1) . n) by Def3
.= (seq_n^ 2) . n by A18, Def3 ;
:: thesis: verum
end;
suppose A19: n > 0 ; :: thesis: ((seq_n^ 1) . n) * ((seq_n^ 1) . n) = (seq_n^ 2) . n
hence ((seq_n^ 1) . n) * ((seq_n^ 1) . n) = (n to_power 1) * ((seq_n^ 1) . n) by Def3
.= n to_power (1 + 1) by A16, A19, Def3
.= (seq_n^ 2) . n by A19, Def3 ;
:: thesis: verum
end;
end;
end;
t . n <= c * ((seq_n^ 1) . n) by A4, A7;
then (t . n) * (t . n) <= (c * ((seq_n^ 1) . n)) * (c * ((seq_n^ 1) . n)) by A8, Lm20;
then (t . n) * (t . n) <= (max (c,(c * c))) * ((seq_n^ 2) . n) by A17, A15, XXREAL_0:2;
hence (t (#) t) . n <= (max (c,(c * c))) * ((seq_n^ 2) . n) by SEQ_1:8; :: thesis: (t (#) t) . n >= 0
(t . n) * (t . n) >= (t . n) * 0 by A8;
hence (t (#) t) . n >= 0 by SEQ_1:8; :: thesis: verum
end;
A20: t (#) t is Element of Funcs (NAT,REAL) by FUNCT_2:8;
max (c,(c * c)) > 0 by A3, XXREAL_0:25;
hence f (#) f in Big_Oh (seq_n^ 2) by A1, A20, A6; :: thesis: verum