let p be Real; :: thesis: ( 1 <= p implies the_set_of_RealSequences_l^ p is linearly-closed )
assume A1: p >= 1 ; :: thesis:
set W = the_set_of_RealSequences_l^ p;
A2: for v, u being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_RealSequences_l^ p & u in the_set_of_RealSequences_l^ p holds
v + u in the_set_of_RealSequences_l^ p
proof
let v, u be VECTOR of Linear_Space_of_RealSequences; :: thesis:
assume that
A3: v in the_set_of_RealSequences_l^ p and
A4: u in the_set_of_RealSequences_l^ p ; :: thesis:
A5: (seq_id (v + u)) rto_power p is summable
proof
reconsider vq = v as Real_Sequence by FUNCT_2:66;
set up = () rto_power p;
set vp = () rto_power p;
set p1 = 1 / p;
A7: now :: thesis: for n being Nat holds
( (() rto_power p) . n = |.(() . n).| to_power p & (() rto_power p) . n = |.(() . n).| to_power p & 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n & 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
let n be Nat; :: thesis: ( (() rto_power p) . n = |.(() . n).| to_power p & (() rto_power p) . n = |.(() . n).| to_power p & 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n & 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
thus A8: ((seq_id v) rto_power p) . n = |.(() . n).| to_power p by Def1; :: thesis: ( (() rto_power p) . n = |.(() . n).| to_power p & 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n & 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
thus A9: ((seq_id u) rto_power p) . n = |.(() . n).| to_power p by Def1; :: thesis: ( 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n & 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
thus 0 <= |.(() . n).| by COMPLEX1:46; :: thesis: ( ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n & 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
thus ( 0 < |.(() . n).| or 0 = |.(() . n).| ) by COMPLEX1:46; :: thesis: ( 0 <= (() rto_power p) . n & 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
hence 0 <= (() rto_power p) . n by ; :: thesis: ( 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
thus 0 <= |.(() . n).| by COMPLEX1:46; :: thesis: ( ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
thus ( 0 < |.(() . n).| or 0 = |.(() . n).| ) by COMPLEX1:46; :: thesis: 0 <= (() rto_power p) . n
hence 0 <= (() rto_power p) . n by ; :: thesis: verum
end;
(seq_id v) rto_power p is summable by A1, A3, Def2;
then Partial_Sums (() rto_power p) is bounded_above by ;
then consider r being Real such that
A10: for n being object st n in dom (Partial_Sums (() rto_power p)) holds
(Partial_Sums (() rto_power p)) . n < r by SEQ_2:def 1;
A11: 1 / p > 0 by ;
reconsider r = r as Real ;
A12: Partial_Sums (() rto_power p) is V45() by ;
now :: thesis: for n being set st n in dom (Partial_Sums (() rto_power p)) holds
((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < r to_power (1 / p)
let n be set ; :: thesis: ( n in dom (Partial_Sums (() rto_power p)) implies ((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < r to_power (1 / p) )
assume A13: n in dom (Partial_Sums (() rto_power p)) ; :: thesis: ((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < r to_power (1 / p)
reconsider n1 = n as Nat by A13;
0 <= (() rto_power p) . 0 by A7;
then A14: 0 <= (Partial_Sums (() rto_power p)) . 0 by SERIES_1:def 1;
(Partial_Sums (() rto_power p)) . 0 <= (Partial_Sums (() rto_power p)) . n1 by ;
hence ((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < r to_power (1 / p) by A11, A10, A13, A14, Th1; :: thesis: verum
end;
then consider q being Real such that
A15: for n being set st n in dom (Partial_Sums (() rto_power p)) holds
((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < q ;
reconsider uq = u as Real_Sequence by FUNCT_2:66;
A17: (seq_id v) + () = seq_id (v + u) by RSSPACE:2;
(seq_id u) rto_power p is summable by A1, A4, Def2;
then Partial_Sums (() rto_power p) is bounded_above by ;
then consider r1 being Real such that
A18: for n being object st n in dom (Partial_Sums (() rto_power p)) holds
(Partial_Sums (() rto_power p)) . n < r1 by SEQ_2:def 1;
reconsider r1 = r1 as Real ;
A19: Partial_Sums (() rto_power p) is V45() by ;
now :: thesis: for n being set st n in dom (Partial_Sums (() rto_power p)) holds
((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < r1 to_power (1 / p)
let n be set ; :: thesis: ( n in dom (Partial_Sums (() rto_power p)) implies ((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < r1 to_power (1 / p) )
assume A20: n in dom (Partial_Sums (() rto_power p)) ; :: thesis: ((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < r1 to_power (1 / p)
reconsider n1 = n as Nat by A20;
0 <= (() rto_power p) . 0 by A7;
then A21: 0 <= (Partial_Sums (() rto_power p)) . 0 by SERIES_1:def 1;
(Partial_Sums (() rto_power p)) . 0 <= (Partial_Sums (() rto_power p)) . n1 by ;
hence ((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < r1 to_power (1 / p) by A11, A18, A20, A21, Th1; :: thesis: verum
end;
then consider q1 being Real such that
A22: for n being set st n in dom (Partial_Sums (() rto_power p)) holds
((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < q1 ;
set g = q + q1;
A24: p * (1 / p) = (p * 1) / p by XCMPLX_1:74
.= 1 by ;
now :: thesis: for n being Nat holds
( ( for n being Nat holds
( ( 0 < |.((vq + uq) . n).| or 0 = |.((vq + uq) . n).| ) & 0 <= ((vq + uq) rto_power p) . n ) ) & (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p )
let n be Nat; :: thesis: ( ( for n being Nat holds
( ( 0 < |.((vq + uq) . n).| or 0 = |.((vq + uq) . n).| ) & 0 <= ((vq + uq) rto_power p) . n ) ) & (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p )

A25: n in NAT by ORDINAL1:def 12;
A26: now :: thesis: ( (Partial_Sums ((vq + uq) rto_power p)) . n > 0 implies (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = (Partial_Sums ((vq + uq) rto_power p)) . n )
assume (Partial_Sums ((vq + uq) rto_power p)) . n > 0 ; :: thesis: (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = (Partial_Sums ((vq + uq) rto_power p)) . n
hence (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power ((1 / p) * p) by POWER:33
.= (Partial_Sums ((vq + uq) rto_power p)) . n by ;
:: thesis: verum
end;
NAT = dom (Partial_Sums (() rto_power p)) by SEQ_1:2;
then A27: ((Partial_Sums (() rto_power p)) . n) to_power (1 / p) < q1 by ;
NAT = dom (Partial_Sums (() rto_power p)) by SEQ_1:2;
then A28: (((Partial_Sums (() rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (() rto_power p)) . n) to_power (1 / p)) < q + q1 by ;
((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (() rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (() rto_power p)) . n) to_power (1 / p)) by ;
then A29: ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p) < q + q1 by ;
A30: now :: thesis: ( (Partial_Sums ((vq + uq) rto_power p)) . n = 0 implies (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = (Partial_Sums ((vq + uq) rto_power p)) . n )
assume A31: (Partial_Sums ((vq + uq) rto_power p)) . n = 0 ; :: thesis: (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = (Partial_Sums ((vq + uq) rto_power p)) . n
hence (((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p)) to_power p = 0 to_power p by
.= (Partial_Sums ((vq + uq) rto_power p)) . n by ;
:: thesis: verum
end;
hereby :: thesis: (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p
let n be Nat; :: thesis: ( ( 0 < |.((vq + uq) . n).| or 0 = |.((vq + uq) . n).| ) & 0 <= ((vq + uq) rto_power p) . n )
thus A33: ( 0 < |.((vq + uq) . n).| or 0 = |.((vq + uq) . n).| ) by COMPLEX1:46; :: thesis: 0 <= ((vq + uq) rto_power p) . n
((vq + uq) rto_power p) . n = |.((vq + uq) . n).| to_power p by Def1;
hence 0 <= ((vq + uq) rto_power p) . n by ; :: thesis: verum
end;
then A34: 0 <= ((vq + uq) rto_power p) . 0 ;
A35: (Partial_Sums ((vq + uq) rto_power p)) . 0 <= (Partial_Sums ((vq + uq) rto_power p)) . n by ;
then 0 <= (Partial_Sums ((vq + uq) rto_power p)) . n by ;
then ((Partial_Sums ((vq + uq) rto_power p)) . n) to_power (1 / p) >= 0 by ;
hence (Partial_Sums ((vq + uq) rto_power p)) . n < (q + q1) to_power p by ; :: thesis: verum
end;
then for n being Nat holds
( Partial_Sums ((vq + uq) rto_power p) is bounded_above & 0 <= ((vq + uq) rto_power p) . n ) by SEQ_2:def 3;
hence (seq_id (v + u)) rto_power p is summable by ; :: thesis: verum
end;
thus v + u in the_set_of_RealSequences_l^ p by A1, A5, Def2; :: thesis: verum
end;
for a being Real
for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_RealSequences_l^ p holds
a * v in the_set_of_RealSequences_l^ p
proof
let a be Real; :: thesis:
let v be VECTOR of Linear_Space_of_RealSequences; :: thesis:
assume A37: v in the_set_of_RealSequences_l^ p ; :: thesis:
(seq_id (a * v)) rto_power p is summable
proof
set vp = () rto_power p;
A38: now :: thesis: for n being Nat holds
( 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
let n be Nat; :: thesis: ( 0 <= |.(() . n).| & ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
thus 0 <= |.(() . n).| by COMPLEX1:46; :: thesis: ( ( 0 < |.(() . n).| or 0 = |.(() . n).| ) & 0 <= (() rto_power p) . n )
thus A39: ( 0 < |.(() . n).| or 0 = |.(() . n).| ) by COMPLEX1:46; :: thesis: 0 <= (() rto_power p) . n
((seq_id v) rto_power p) . n = |.(() . n).| to_power p by Def1;
hence 0 <= (() rto_power p) . n by ; :: thesis: verum
end;
(seq_id v) rto_power p is summable by ;
then Partial_Sums (() rto_power p) is bounded_above by ;
then consider r being Real such that
A40: for n being object st n in dom (Partial_Sums (() rto_power p)) holds
(Partial_Sums (() rto_power p)) . n < r by SEQ_2:def 1;
A41: seq_id (a * v) = a (#) () by RSSPACE:3;
A42: for n being Nat holds (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = () * ((Partial_Sums (() rto_power p)) . n)
proof
let n be Nat; :: thesis: (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = () * ((Partial_Sums (() rto_power p)) . n)
now :: thesis: for n being Nat holds ((seq_id (a * v)) rto_power p) . n = (() (#) (() rto_power p)) . n
let n be Nat; :: thesis: ((seq_id (a * v)) rto_power p) . n = (() (#) (() rto_power p)) . n
A43: |.a.| >= 0 by COMPLEX1:46;
A44: |.(() . n).| >= 0 by COMPLEX1:46;
A45: (a (#) ()) . n = a * (() . n) by SEQ_1:9;
((a (#) ()) rto_power p) . n = |.((a (#) ()) . n).| to_power p by Def1
.= (|.a.| * |.(() . n).|) to_power p by
.= () * (|.(() . n).| to_power p) by A1, A43, A44, Lm2 ;
hence ((seq_id (a * v)) rto_power p) . n = () * ((() rto_power p) . n) by
.= (() (#) (() rto_power p)) . n by SEQ_1:9 ;
:: thesis: verum
end;
then for n being object st n in NAT holds
((seq_id (a * v)) rto_power p) . n = (() (#) (() rto_power p)) . n ;
then A46: (seq_id (a * v)) rto_power p = () (#) (() rto_power p) by FUNCT_2:12;
Partial_Sums (() (#) (() rto_power p)) = () (#) (Partial_Sums (() rto_power p)) by SERIES_1:9;
hence (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = () * ((Partial_Sums (() rto_power p)) . n) by ; :: thesis: verum
end;
A47: ( 0 < |.a.| to_power p or 0 = |.a.| to_power p ) by ;
A48: now :: thesis: for n being set st n in dom (Partial_Sums (() rto_power p)) holds
( n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) & ( () * ((Partial_Sums (() rto_power p)) . n) < () * r or () * ((Partial_Sums (() rto_power p)) . n) = () * r ) )
let n be set ; :: thesis: ( n in dom (Partial_Sums (() rto_power p)) implies ( n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) & ( () * ((Partial_Sums (() rto_power p)) . n) < () * r or () * ((Partial_Sums (() rto_power p)) . n) = () * r ) ) )
assume A49: n in dom (Partial_Sums (() rto_power p)) ; :: thesis: ( n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) & ( () * ((Partial_Sums (() rto_power p)) . n) < () * r or () * ((Partial_Sums (() rto_power p)) . n) = () * r ) )
dom (Partial_Sums (() rto_power p)) = NAT by SEQ_1:1;
hence n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) by ; :: thesis: ( () * ((Partial_Sums (() rto_power p)) . n) < () * r or () * ((Partial_Sums (() rto_power p)) . n) = () * r )
thus ( (|.a.| to_power p) * ((Partial_Sums (() rto_power p)) . n) < () * r or () * ((Partial_Sums (() rto_power p)) . n) = () * r ) by ; :: thesis: verum
end;
A50: for n being set holds
( not n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < () * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = () * r )
proof
let n be set ; :: thesis: ( not n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < () * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = () * r )
assume A51: n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) ; :: thesis: ( (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < () * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = () * r )
reconsider n1 = n as Nat by A51;
n in NAT by ;
then n in dom (Partial_Sums (() rto_power p)) by SEQ_1:1;
then ( (|.a.| to_power p) * ((Partial_Sums (() rto_power p)) . n) < () * r or () * ((Partial_Sums (() rto_power p)) . n) = () * r ) by A48;
then ( (Partial_Sums ((seq_id (a * v)) rto_power p)) . n1 < () * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n1 = () * r ) by A42;
hence ( (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < () * r or (Partial_Sums ((seq_id (a * v)) rto_power p)) . n = () * r ) ; :: thesis: verum
end;
ex r1 being Real st
for n being object st n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) holds
(Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1
proof
take r1 = (() * r) + 1; :: thesis: for n being object st n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) holds
(Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1

reconsider r1 = r1 as Real ;
for n being object st n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) holds
(Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1
proof
A52: (|.a.| to_power p) * r < (() * r) + 1 by XREAL_1:29;
let n be object ; :: thesis: ( n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) implies (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1 )
assume n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) ; :: thesis: (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1
hence (Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1 by ; :: thesis: verum
end;
hence for n being object st n in dom (Partial_Sums ((seq_id (a * v)) rto_power p)) holds
(Partial_Sums ((seq_id (a * v)) rto_power p)) . n < r1 ; :: thesis: verum
end;
then A53: Partial_Sums ((seq_id (a * v)) rto_power p) is bounded_above by SEQ_2:def 1;
for n being Nat holds ((seq_id (a * v)) rto_power p) . n >= 0
proof
set b = a (#) ();
let n be Nat; :: thesis: ((seq_id (a * v)) rto_power p) . n >= 0
(a (#) ()) . n = a * (() . n) by SEQ_1:9;
then ((a (#) ()) rto_power p) . n = |.(a * (() . n)).| to_power p by Def1;
hence ((seq_id (a * v)) rto_power p) . n >= 0 by ; :: thesis: verum
end;
hence (seq_id (a * v)) rto_power p is summable by ; :: thesis: verum
end;
hence a * v in the_set_of_RealSequences_l^ p by ; :: thesis: verum
end;
hence the_set_of_RealSequences_l^ p is linearly-closed by ; :: thesis: verum