set g = seq_n^ 1;
set h = seq_n^ 2;
let f be Real_Sequence; :: thesis: ( f in Big_Oh (seq_n^ 1) implies f (#) f in Big_Oh (seq_n^ 2) )
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: max c,(c * c) > 0 by A3, XXREAL_0:25;
A6: t (#) t is Element of Funcs NAT ,REAL by FUNCT_2:11;
A7: 0 to_power 1 = 0 by POWER:def 2;
now
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 n >= N ; :: thesis: ( (t (#) t) . n <= (max c,(c * c)) * ((seq_n^ 2) . n) & (t (#) t) . n >= 0 )
then A8: ( t . n <= c * ((seq_n^ 1) . n) & t . n >= 0 ) by A4;
A9: (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:30 ;
hence (seq_n^ 1) . n >= 0 ; :: thesis: verum
end;
end;
end;
A10: 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 A11: 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 A11, Def3; :: thesis: verum
end;
suppose n > 0 ; :: thesis: (seq_n^ 1) . n <= (seq_n^ 2) . n
then A12: n >= 0 + 1 by NAT_1:13;
thus (seq_n^ 1) . n <= (seq_n^ 2) . n :: thesis: verum
proof
per cases ( n = 1 or n > 1 ) by A12, XXREAL_0:1;
suppose A13: n = 1 ; :: thesis: (seq_n^ 1) . n <= (seq_n^ 2) . n
( 1 to_power 1 = 1 & 1 to_power 2 = 1 ) by POWER:31;
then (seq_n^ 1) . n = 1 to_power 2 by A13, Def3;
hence (seq_n^ 1) . n <= (seq_n^ 2) . n by A13, Def3; :: thesis: verum
end;
end;
end;
end;
end;
end;
A15: (t . n) * (t . n) <= (c * ((seq_n^ 1) . n)) * (c * ((seq_n^ 1) . n)) by A8, Lm26;
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 A7, 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:32; :: 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;
(seq_n^ 2) . n >= (seq_n^ 1) . n by A10;
then (c * c) * ((seq_n^ 2) . n) <= (max c,(c * c)) * ((seq_n^ 2) . n) by A9, XREAL_1:66, XXREAL_0:25;
then (t . n) * (t . n) <= (max c,(c * c)) * ((seq_n^ 2) . n) by A15, A17, XXREAL_0:2;
hence (t (#) t) . n <= (max c,(c * c)) * ((seq_n^ 2) . n) by SEQ_1:12; :: thesis: (t (#) t) . n >= 0
(t . n) * (t . n) >= (t . n) * 0 by A8;
hence (t (#) t) . n >= 0 by SEQ_1:12; :: thesis: verum
end;
hence f (#) f in Big_Oh (seq_n^ 2) by A1, A5, A6; :: thesis: verum