:: The Banach Space $l^p$
:: by Yasumasa Suzuki
::
:: Received September 25, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SEQ_1, REAL_1, SUBSET_1, FUNCT_1, COMPLEX1, POWER,
XXREAL_0, XBOOLE_0, RSSPACE, SERIES_1, CARD_1, TARSKI, RELAT_1, ARYTM_3,
CARD_3, RLVECT_1, RSSPACE3, NORMSP_1, RLSUB_1, XXREAL_2, VALUED_0,
VALUED_1, ALGSTR_0, ZFMISC_1, STRUCT_0, SUPINF_2, REALSET1, ARYTM_1,
SEQ_2, ORDINAL2, PRE_TOPC, NAT_1, LOPBAN_1, LP_SPACE, NORMSP_0, METRIC_1,
RELAT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1,
REALSET1, PARTFUN1, FUNCT_2, PRE_TOPC, DOMAIN_1, XXREAL_0, XREAL_0,
XCMPLX_0, ORDINAL1, NUMBERS, RLVECT_1, COMPLEX1, REAL_1, NAT_1, STRUCT_0,
ALGSTR_0, RLSUB_1, NORMSP_0, NORMSP_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1,
POWER, RSSPACE, RSSPACE3, LOPBAN_1;
constructors REAL_1, COMPLEX1, SEQ_2, PREPOWER, SERIES_1, REALSET1, RLSUB_1,
RSSPACE3, LOPBAN_1, RELSET_1, BINOP_2, COMSEQ_2, BINOP_1, FUNCSDOM,
SEQ_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
XREAL_0, MEMBERED, REALSET1, STRUCT_0, RLVECT_1, LOPBAN_1, VALUED_0,
RSSPACE, VALUED_1, FUNCT_2, SERIES_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, NORMSP_0;
equalities REALSET1, BINOP_1, RLVECT_1, STRUCT_0, ALGSTR_0, VALUED_1,
NORMSP_0, RSSPACE, SEQ_1, FUNCSDOM;
expansions NORMSP_0;
theorems XBOOLE_0, RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1, SEQM_3,
SERIES_1, COMSEQ_3, FUNCT_1, NAT_1, SEQ_2, FUNCT_2, RLVECT_1, RLSUB_1,
NORMSP_1, XREAL_0, RSSPACE2, XCMPLX_1, SEQ_4, POWER, RSSPACE, RSSPACE3,
LOPBAN_1, HOLDER_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1;
schemes NAT_1, SEQ_1, FUNCT_2, XBOOLE_0;
begin :: The Real Norm Space of l^p Real Sequences
definition
let x be Real_Sequence;
let p be Real;
func x rto_power p -> Real_Sequence means
:Def1:
for n be Nat holds it.n = |.x.n.| to_power p;
existence
proof
deffunc F(set)= |.x.$1.| to_power p;
ex q1 be Real_Sequence st for n be Nat holds q1.n=F(n) from
SEQ_1:sch 1;
then consider q1 be Real_Sequence such that
A1: for n be Nat holds q1.n= |.x.n.| to_power p;
take q1;
thus thesis by A1;
end;
uniqueness
proof
let a1,a2 be Real_Sequence;
assume that
A2: for n be Nat holds a1.n = |.x.n.| to_power p and
A3: for n be Nat holds a2.n = |.x.n.| to_power p;
for s be object st s in NAT holds a1.s = a2.s
proof
let s be object such that
A4: s in NAT;
a1.s = |.x.s.| to_power p by A2,A4
.= a2.s by A3,A4;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
definition
let p be Real;
assume
A1: p >= 1;
func the_set_of_RealSequences_l^p -> non empty Subset of
Linear_Space_of_RealSequences means
:Def2:
for x being set holds x in it iff x
in the_set_of_RealSequences & seq_id(x) rto_power p is summable;
existence
proof
defpred P[object] means seq_id($1) rto_power p is summable;
consider IT being set such that
A2: for x being object holds x in IT iff x in the_set_of_RealSequences &
P[x] from XBOOLE_0:sch 1;
for x be object st x in IT holds x in the_set_of_RealSequences by A2;
then
A3: IT is Subset of the_set_of_RealSequences by TARSKI:def 3;
seq_id(Zeroseq) rto_power p is absolutely_summable
proof
reconsider rseq=seq_id(Zeroseq) rto_power p as Real_Sequence;
now
let n be Nat;
thus rseq.n =|.(seq_id(Zeroseq)).n.| to_power p by Def1
.=0 to_power p by ABSVALUE:2,RSSPACE:4
.=0 by A1,POWER:def 2;
end;
hence thesis by COMSEQ_3:3;
end;
then IT is non empty by A2;
then reconsider IT as non empty Subset of
Linear_Space_of_RealSequences by A3;
take IT;
thus thesis by A2;
end;
uniqueness
proof
let X1,X2 be non empty Subset of Linear_Space_of_RealSequences;
assume that
A4: for x being set holds x in X1 iff x in the_set_of_RealSequences &
seq_id(x) rto_power p is summable and
A5: for x being set holds x in X2 iff x in the_set_of_RealSequences &
seq_id(x) rto_power p is summable;
A6: X2 c= X1
proof
let x be object;
assume
A7: x in X2;
then
A8: seq_id(x) rto_power p is summable by A5;
x in the_set_of_RealSequences by A7;
hence thesis by A4,A8;
end;
X1 c= X2
proof
let x be object;
assume
A9: x in X1;
then
A10: seq_id(x) rto_power p is summable by A4;
x in the_set_of_RealSequences by A9;
hence thesis by A5,A10;
end;
hence thesis by A6,XBOOLE_0:def 10;
end;
end;
reserve x1,x2,y1,a,b,c for Real;
Lm1: x1 >= 0 & y1 > 0 implies x1 to_power y1 >= 0
proof
assume that
A1: x1 >= 0 and
A2: y1 > 0;
x1>0 or x1=0 by A1;
hence thesis by A2,POWER:34,def 2;
end;
Lm2: y1>0 & x1>=0 & x2>=0 implies (x1*x2) to_power y1 = (x1 to_power y1) * (x2
to_power y1)
proof
assume that
A1: y1>0 and
A2: x1>=0 and
A3: x2>=0;
per cases by A2,A3;
suppose
x1>0 & x2>0;
hence thesis by POWER:30;
end;
suppose
A4: x1>0 & x2=0;
then x2 to_power y1 = 0 by A1,POWER:def 2;
hence thesis by A4;
end;
suppose
A5: x1=0 & x2>0;
then x1 to_power y1 = 0 by A1,POWER:def 2;
hence thesis by A5;
end;
suppose
A6: x1=0 & x2=0;
then x2 to_power y1 = 0 by A1,POWER:def 2;
hence thesis by A6;
end;
end;
theorem Th1:
a >= 0 & a < b & c > 0 implies a to_power c < b to_power c
proof
a = 0 & c > 0 implies a to_power c = 0 by POWER:def 2;
hence thesis by POWER:34,37;
end;
Lm3: for p be Real st 1 = p for a,b be Real_Sequence for n be Nat
holds (Partial_Sums((a + b) rto_power p).n) to_power (1/p) <= (Partial_Sums(a
rto_power p).n) to_power (1/p) + (Partial_Sums(b rto_power p).n) to_power (1/p)
proof
let p be Real such that
A1: p=1;
let a,b be Real_Sequence;
let n be Nat;
A2: now
let n be Nat;
thus ((a + b) rto_power p).n = |.(a + b).n.| to_power p by Def1
.=|.(a + b).n.| by A1,POWER:25;
thus (a rto_power p).n = |.a .n.| to_power p by Def1
.=|.a .n.| by A1,POWER:25;
thus (b rto_power p).n = |.b .n.| to_power p by Def1
.=|.b .n.| by A1,POWER:25;
end;
then (a + b) rto_power p = |.a + b.| by SEQ_1:12;
then
A3: (Partial_Sums((a + b) rto_power p).n) to_power (1/p) =(Partial_Sums(abs(
a + b)).n) by A1,POWER:25;
a rto_power p = |.a.| by A2,SEQ_1:12;
then
A4: (Partial_Sums(a rto_power p).n) to_power (1/p) =(Partial_Sums(|.a.|).n
) by A1,POWER:25;
deffunc F(Nat) =|.a .($1).| + |.b .($1).|;
consider c be Real_Sequence such that
A5: for n be Nat holds c.n= F(n) from SEQ_1:sch 1;
A6: for n be Nat holds |.(a + b).n.| <= |.b .n.| + |.a .n.|
proof
let n be Nat;
|.(a + b).n.|=|.a.n + b.n.| by SEQ_1:7;
hence thesis by COMPLEX1:56;
end;
now
let n be Nat;
A7: |.(a + b).n.|=abs(a+b).n by SEQ_1:12;
|.(a + b).n.| <= |.b .n.| + |.a .n.| by A6;
hence abs(a+b).n <= c.n by A5,A7;
end;
then
A8: Partial_Sums(abs(a+b)).n<=Partial_Sums(c).n by SERIES_1:14;
now
let n be Nat;
A9: |.a.n.|=abs (a).n by SEQ_1:12;
|.b.n.|=abs (b).n by SEQ_1:12;
hence c.n=abs (a).n + abs (b).n by A5,A9
.=(abs a + abs b).n by SEQ_1:7;
end;
then for n be object st n in NAT holds c.n = (abs (a) + abs (b)).n;
then
A10: c = abs a + abs b by FUNCT_2:12;
b rto_power p = |.b.| by A2,SEQ_1:12;
then
A11: (Partial_Sums(b rto_power p).n) to_power (1/p) =(Partial_Sums(|.b.|).n
) by A1,POWER:25;
Partial_Sums(abs (a) + abs (b)) = Partial_Sums(abs a) + Partial_Sums(
|.b.|) by SERIES_1:5;
hence thesis by A3,A4,A11,A10,A8,SEQ_1:7;
end;
theorem Th2:
for p be Real st 1 <= p for a,b be Real_Sequence
for n be Nat
holds (Partial_Sums((a + b) rto_power p).n) to_power (1/p) <= (
Partial_Sums(a rto_power p).n) to_power (1/p) + (Partial_Sums(b rto_power p).n)
to_power (1/p)
proof
let p be Real such that
A1: 1<=p;
reconsider p as Real;
let a,b be Real_Sequence;
set ap = a rto_power p;
set bp = b rto_power p;
set ab= ((a + b) rto_power p);
let n be Nat;
now
per cases by A1,XXREAL_0:1;
case
A2: p > 1;
now
let n be Nat;
thus ap.n = |.a .n.| to_power p by Def1;
thus bp.n = |.b .n.| to_power p by Def1;
((a + b) rto_power p).n =|.(a + b).n.| to_power p by Def1
.=|.a.n+b.n.| to_power p by SEQ_1:7;
hence ab.n = |.a.n+b.n.| to_power p;
end;
hence thesis by A2,HOLDER_1:7;
end;
case
p=1;
hence thesis by Lm3;
end;
end;
hence thesis;
end;
Lm4: for a,b be Real_Sequence for p be Real st 1 = p & (a rto_power p) is
summable & (b rto_power p) is summable holds ((a+b) rto_power p) is summable &
(Sum((a + b) rto_power p)) to_power (1/p) <= (Sum(a rto_power p)) to_power (1/p
) + (Sum(b rto_power p)) to_power (1/p)
proof
let a,b be Real_Sequence;
let p be Real such that
A1: p=1 and
A2: a rto_power p is summable and
A3: b rto_power p is summable;
A4: now
let n be Nat;
thus ((a + b) rto_power p).n = |.(a + b).n.| to_power p by Def1
.=|.(a + b).n.| by A1,POWER:25;
thus (a rto_power p).n = |.a .n.| to_power p by Def1
.=|.a .n.| by A1,POWER:25;
thus (b rto_power p).n = |.b .n.| to_power p by Def1
.=|.b .n.| by A1,POWER:25;
end;
then
A5: (a + b) rto_power p = abs(a + b) by SEQ_1:12;
A6: a = seq_id (a);
A7: a rto_power p = |.a.| by A4,SEQ_1:12;
then a is absolutely_summable by A2,SERIES_1:def 4;
then reconsider a1=a as VECTOR of l1_Space by A6,RSSPACE3:6;
|.b.| is summable by A3,A4,SEQ_1:12;
then
A8: |.a.| + |.b.| is summable by A2,A7,SERIES_1:7;
A9: b rto_power p = |.b.| by A4,SEQ_1:12;
then
A10: (Sum((b) rto_power p)) to_power (1/p) =Sum(|.b.|) by A1,POWER:25;
A11: b = seq_id (b);
b is absolutely_summable by A3,A9,SERIES_1:def 4;
then reconsider b1=b as VECTOR of l1_Space by A11,RSSPACE3:6;
A12: ||.b1.|| = Sum(abs(seq_id(b1))) by RSSPACE3:def 2,def 3;
deffunc F(Nat) =|.a .($1).| + |.b .($1).|;
consider c be Real_Sequence such that
A14: for n be Nat holds c.n= F(n) from SEQ_1:sch 1;
A15: now
let n be Nat;
A16: abs(a+b).n=|.(a+b).n.| by SEQ_1:12;
hence abs(a+b).n>= 0 by COMPLEX1:46;
thus c.n=|.a.n.|+|.b.n.| by A14;
|.a.n.|+|.b.n.| = |.a.|.n+|.b.n.| by SEQ_1:12
.=|.a.|.n+|.b.|.n by SEQ_1:12;
hence c.n =|.a.|.n+|.b.|.n by A14;
|.(a+b).n.| =|.(a.n)+(b.n).| by SEQ_1:7;
then |.a+b.|.n <= |.a.n.|+|.b.n.| by A16,COMPLEX1:56;
hence abs(a+b).n <= c.n by A14;
end;
then c = |.a.| + |.b.| by SEQ_1:7;
hence (a + b) rto_power p is summable by A5,A8,A15,SERIES_1:20;
A17: ||.a1.|| = Sum(abs(seq_id(a1))) by RSSPACE3:def 2,def 3;
A19: ||.a1+b1.|| =Sum(abs(seq_id(a1+b1))) by RSSPACE3:def 2,def 3
.=Sum(abs(seq_id(seq_id(a1)+seq_id(b1)))) by RSSPACE3:6
.=Sum(abs(seq_id(a1)+seq_id(b1)));
A20: ||.a1+b1.|| <= ||.a1.|| + ||.b1.|| by RSSPACE3:7;
(Sum((a) rto_power p)) to_power (1/p) =Sum(|.a.|) by A1,A7,POWER:25;
hence thesis by A1,A5,A10,A20,A19,A17,A12,POWER:25;
end;
theorem Th3:
for a,b be Real_Sequence for p be Real st 1 <= p & (a rto_power p
) is summable & (b rto_power p) is summable holds ((a+b) rto_power p) is
summable & (Sum((a + b) rto_power p)) to_power (1/p) <= (Sum(a rto_power p))
to_power (1/p) + (Sum(b rto_power p)) to_power (1/p)
proof
let a,b be Real_Sequence;
let p be Real such that
A1: 1<=p and
A2: (a rto_power p) is summable and
A3: (b rto_power p) is summable;
set ab= ((a + b) rto_power p);
set bp = b rto_power p;
set ap = a rto_power p;
A4: now
let n be Nat;
thus ap.n= |.a .n.| to_power p by Def1;
thus bp.n= |.b .n.| to_power p by Def1;
((a + b) rto_power p).n =|.(a + b).n.| to_power p by Def1
.=|.a.n+b.n.| to_power p by SEQ_1:7;
hence ab.n= |.a.n+b.n.| to_power p;
end;
reconsider p as Real;
now
per cases by A1,XXREAL_0:1;
case
p > 1;
hence Sum(ab) to_power (1/p) <= Sum ap to_power (1/p) + Sum(bp) to_power
(1/p) & ab is summable by A2,A3,A4,HOLDER_1:13;
end;
case
p=1;
hence
Sum(ab) to_power (1/p) <= Sum(ap) to_power (1/p) + Sum(bp) to_power
(1/p) & ab is summable by A2,A3,Lm4;
end;
end;
hence thesis;
end;
theorem Th4:
for p be Real
st 1 <= p holds the_set_of_RealSequences_l^p is linearly-closed
proof
let p be Real such that
A1: p >=1;
set W = the_set_of_RealSequences_l^p;
A2: for v,u be 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 such that
A3: v in W and
A4: u in W;
A5: seq_id(v +u) rto_power p is summable
proof
reconsider vq=v as Real_Sequence by FUNCT_2:66;
set up=seq_id(u) rto_power p;
set vp=seq_id(v) rto_power p;
set p1=1/p;
A7: now
let n be Nat;
thus
A8: vp.n=|.(seq_id(v)).n.| to_power p by Def1;
thus
A9: up.n=|.(seq_id(u)).n.| to_power p by Def1;
thus 0 <= |.(seq_id(v)).n.| by COMPLEX1:46;
thus 0 < |.(seq_id(v)).n.| or 0=|.(seq_id(v)).n.| by COMPLEX1:46;
hence 0 <= vp.n by A1,A8,POWER:34,def 2;
thus 0 <= |.(seq_id(u)).n.| by COMPLEX1:46;
thus 0 < |.(seq_id(u)).n.| or 0=|.(seq_id(u)).n.| by COMPLEX1:46;
hence 0 <= up.n by A1,A9,POWER:34,def 2;
end;
seq_id(v) rto_power p is summable by A1,A3,Def2;
then Partial_Sums(vp) is bounded_above by A7,SERIES_1:17;
then consider r be Real such that
A10: for n be object st n in dom Partial_Sums(vp) holds Partial_Sums(vp
).n<r by SEQ_2:def 1;
A11: 1/p > 0 by A1,XREAL_1:139;
reconsider r as Real;
A12: Partial_Sums(vp) is non-decreasing by A7,SERIES_1:16;
now
let n be set such that
A13: n in dom Partial_Sums(vp);
reconsider n1=n as Nat by A13;
0<=vp.0 by A7;
then
A14: 0<=Partial_Sums(vp).0 by SERIES_1:def 1;
Partial_Sums(vp).0<=Partial_Sums(vp).n1 by A12,SEQM_3:11;
hence (Partial_Sums(vp).n) to_power p1 < r to_power p1 by A11,A10,A13
,A14,Th1;
end;
then consider q be Real such that
A15: for n be set st n in dom Partial_Sums(vp) holds (Partial_Sums(
vp).n) to_power p1 <q;
reconsider uq=u as Real_Sequence by FUNCT_2:66;
A17: seq_id(v)+seq_id(u) =seq_id(v+u) by RSSPACE:2;
seq_id(u) rto_power p is summable by A1,A4,Def2;
then Partial_Sums(up) is bounded_above by A7,SERIES_1:17;
then consider r1 be Real such that
A18: for n be object st n in dom Partial_Sums(up) holds Partial_Sums(up
).n<r1 by SEQ_2:def 1;
reconsider r1 as Real;
A19: Partial_Sums(up) is non-decreasing by A7,SERIES_1:16;
now
let n be set such that
A20: n in dom Partial_Sums(up);
reconsider n1=n as Nat by A20;
0<=up.0 by A7;
then
A21: 0<=Partial_Sums(up).0 by SERIES_1:def 1;
Partial_Sums(up).0<=Partial_Sums(up).n1 by A19,SEQM_3:11;
hence (Partial_Sums(up).n) to_power p1 < r1 to_power p1 by A11,A18,A20
,A21,Th1;
end;
then consider q1 be Real such that
A22: for n be set st n in dom Partial_Sums(up) holds (Partial_Sums(
up).n) to_power p1 <q1;
set g = q + q1;
A24: p * (1/p) = (p*1)/p by XCMPLX_1:74
.= 1 by A1,XCMPLX_1:60;
now
let n be Nat;
A25: n in NAT by ORDINAL1:def 12;
A26: now
assume (Partial_Sums((vq + uq) rto_power p).n) > 0;
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 A24,POWER:25;
end;
NAT=dom Partial_Sums(up) by SEQ_1:2;
then
A27: (Partial_Sums(up).n) to_power p1 <q1 by A22,A25;
NAT=dom Partial_Sums(vp) by SEQ_1:2;
then
A28: (Partial_Sums(up).n) to_power (1/p) + (Partial_Sums(vp).n)
to_power (1/p) < g by A15,A27,XREAL_1:8,A25;
(Partial_Sums((vq + uq) rto_power p).n) to_power (1/p) <= (
Partial_Sums(up).n) to_power (1/p) + (Partial_Sums(vp).n) to_power (1/p)
by A1,Th2;
then
A29: (Partial_Sums((vq + uq) rto_power p).n) to_power (1/p) < g by A28,
XXREAL_0:2;
A30: now
assume
A31: (Partial_Sums((vq + uq) rto_power p).n) = 0;
hence
(Partial_Sums((vq + uq) rto_power p).n) to_power (1/p) to_power
p = 0 to_power p by A11,POWER:def 2
.= (Partial_Sums((vq + uq) rto_power p).n) by A1,A31,POWER:def 2;
end;
thus
A32: now
let n be Nat;
thus
A33: 0 < |.(vq + uq).n.| or 0=|.(vq + uq).n.| by COMPLEX1:46;
((vq + uq) rto_power p).n =|.(vq + uq).n.| to_power p by Def1;
hence 0 <= ((vq + uq) rto_power p).n by A1,A33,POWER:34,def 2;
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 A32,SEQM_3:11,SERIES_1:16;
then 0<=Partial_Sums((vq + uq) rto_power p).n by A34,SERIES_1:def 1;
then
(Partial_Sums((vq + uq) rto_power p).n) to_power (1/p) >=0 by A11,Lm1;
hence
(Partial_Sums((vq + uq) rto_power p).n) < g to_power p by A1,A29,A26
,A30,A35,A34,Th1,SERIES_1:def 1;
end;
then for n be 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 thesis by A17,SERIES_1:17;
end;
thus thesis by A1,A5,Def2;
end;
for a be Real
for v be VECTOR of Linear_Space_of_RealSequences st v in
W holds a * v in W
proof
let a be Real;
let v be VECTOR of Linear_Space_of_RealSequences such that
A37: v in W;
seq_id(a*v) rto_power p is summable
proof
set vp = seq_id(v) rto_power p;
A38: now
let n be Nat;
thus 0 <= |.(seq_id(v)).n.| by COMPLEX1:46;
thus
A39: 0 < |.(seq_id(v)).n.| or 0=|.(seq_id(v)).n.| by COMPLEX1:46;
vp.n=|.(seq_id(v)).n.| to_power p by Def1;
hence 0 <= vp.n by A1,A39,POWER:34,def 2;
end;
vp is summable by A1,A37,Def2;
then Partial_Sums(vp) is bounded_above by A38,SERIES_1:17;
then consider r be Real such that
A40: for n be object st n in dom Partial_Sums(seq_id(v) rto_power p)
holds Partial_Sums(vp).n<r by SEQ_2:def 1;
A41: seq_id(a*v)=(a(#)seq_id(v)) by RSSPACE:3;
A42: for n be Nat holds Partial_Sums(seq_id(a*v) rto_power p)
.n = (|.a.| to_power p)* Partial_Sums(seq_id(v) rto_power p).n
proof
let n be Nat;
now
let n be Nat;
A43: |.a.|>=0 by COMPLEX1:46;
A44: |.(seq_id(v)).n.| >= 0 by COMPLEX1:46;
A45: (a(#)seq_id(v)).n = a * (seq_id(v)).n by SEQ_1:9;
((a(#)seq_id(v)) rto_power p).n = |.(a(#)seq_id(v)).n.|
to_power p by Def1
.=((|.a.|* |.(seq_id(v)).n.|)) to_power p by A45,COMPLEX1:65
.=(|.a.| to_power p) * ((|.(seq_id(v)).n.|) to_power p) by A1,A43
,A44,Lm2;
hence
(seq_id(a*v) rto_power p).n = (|.a.| to_power p) * ((seq_id(v)
) rto_power p).n by A41,Def1
.= ((|.a.| to_power p) (#) ((seq_id(v)) rto_power p)).n by SEQ_1:9;
end;
then
for n be object st n in NAT holds (seq_id(a*v) rto_power p).n= ((
|.a.| to_power p) (#) ((seq_id(v)) rto_power p)).n;
then
A46: (seq_id(a*v) rto_power p)= ((|.a.| to_power p) (#) ((seq_id(v))
rto_power p)) by FUNCT_2:12;
Partial_Sums(((|.a.| to_power p) (#) ((seq_id(v)) rto_power p)))
= ((|.a.| to_power p) (#)Partial_Sums( ((seq_id(v)) rto_power p))) by
SERIES_1:9;
hence thesis by A46,SEQ_1:9;
end;
A47: 0<(|.a.| to_power p) or 0=(|.a.| to_power p) by A1,Lm1,COMPLEX1:46;
A48: now
let n be set such that
A49: n in dom Partial_Sums(seq_id(v) rto_power p);
dom Partial_Sums(seq_id(v) rto_power p)= NAT by SEQ_1:1;
hence n in dom Partial_Sums(seq_id(a*v) rto_power p) by A49,SEQ_1:1;
thus (|.a.| to_power p) * Partial_Sums(seq_id(v) rto_power p).n < (
|.a.| to_power p) * r or ((|.a.| to_power p) * Partial_Sums(seq_id(v)
rto_power p).n ) = (|.a.| to_power p) * r by A40,A47,A49,XREAL_1:68;
end;
A50: for n be set st n in dom Partial_Sums(seq_id(a*v) rto_power p)
holds Partial_Sums(seq_id(a*v) rto_power p).n <(|.a.| to_power p) * r or
Partial_Sums(seq_id(a*v) rto_power p).n = (|.a.| to_power p) * r
proof
let n be set such that
A51: n in dom Partial_Sums(seq_id(a*v) rto_power p);
reconsider n1=n as Nat by A51;
n in NAT by A51,SEQ_1:1;
then n in dom Partial_Sums(seq_id(v) rto_power p) by SEQ_1:1;
then (|.a.| to_power p) * Partial_Sums(seq_id(v) rto_power p). n < (
|.a.| to_power p) * r or ((|.a.| to_power p) * Partial_Sums(seq_id(v)
rto_power p).n ) = (|.a.| to_power p) * r by A48;
then Partial_Sums(seq_id(a*v) rto_power p).n1 <(|.a.| to_power p) *
r or Partial_Sums(seq_id(a*v) rto_power p).n1 =(|.a.| to_power p) * r by A42;
hence thesis;
end;
ex r1 be Real st for n be 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 = (|.a.| to_power p) * r + 1;
reconsider r1 as Real;
for n be 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 <(|.a.| to_power p) * r +1 by XREAL_1:29;
let n be object;
assume n in dom Partial_Sums(seq_id(a*v) rto_power p);
hence thesis by A50,A52,XXREAL_0:2;
end;
hence thesis;
end;
then
A53: Partial_Sums(seq_id(a*v) rto_power p) is bounded_above by SEQ_2:def 1;
for n be Nat holds (seq_id(a*v) rto_power p).n >= 0
proof
set b = (a(#)seq_id(v));
let n be Nat;
(a(#)seq_id(v)).n = a * (seq_id(v)).n by SEQ_1:9;
then (b rto_power p).n = |.a * (seq_id(v)).n.| to_power p by Def1;
hence thesis by A1,A41,Lm1,COMPLEX1:46;
end;
hence thesis by A53,SERIES_1:17;
end;
hence thesis by A1,Def2;
end;
hence thesis by A2,RLSUB_1:def 1;
end;
theorem Th5:
for p be Real st 1 <= p holds RLSStruct (#
the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences) #) is Subspace of Linear_Space_of_RealSequences
proof
let p be Real;
assume 1 <= p;
then the_set_of_RealSequences_l^p is linearly-closed by Th4;
hence thesis by RSSPACE:11;
end;
theorem
for p be Real st 1 <= p holds RLSStruct (# the_set_of_RealSequences_l^
p, Zero_(the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences) #) is Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital by Th5;
theorem
for p be Real st 1 <= p holds RLSStruct (# the_set_of_RealSequences_l^
p, Zero_(the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences) #) is
RealLinearSpace by Th5;
definition
let p be Real;
func l_norm^p -> Function of the_set_of_RealSequences_l^p, REAL means
:Def3:
for x be object st x in the_set_of_RealSequences_l^p
holds it.x = ( Sum(seq_id(x) rto_power p) ) to_power (1/p);
existence
proof
deffunc F(object) =( Sum(seq_id($1) rto_power p) ) to_power (1/p);
A1: for z be object st z in the_set_of_RealSequences_l^p holds F(z) in REAL
by XREAL_0:def 1;
ex f being Function of the_set_of_RealSequences_l^p,REAL st for x being
object st x in the_set_of_RealSequences_l^p
holds f.x = F(x) from FUNCT_2:sch 2(A1
);
hence thesis;
end;
uniqueness
proof
let NORM1,NORM2 be Function of the_set_of_RealSequences_l^p, REAL such
that
A2: for x be object st x in the_set_of_RealSequences_l^p holds NORM1.x =
( Sum(seq_id(x) rto_power p) ) to_power (1/p) and
A3: for x be object st x in the_set_of_RealSequences_l^p holds NORM2.x =
( Sum(seq_id(x) rto_power p) ) to_power (1/p);
A4: for z be object st z in the_set_of_RealSequences_l^p
holds NORM1.z = NORM2.z
proof
let z be object such that
A5: z in the_set_of_RealSequences_l^p;
NORM1.z = ( Sum(seq_id(z) rto_power p) ) to_power (1/p) by A2,A5;
hence thesis by A3,A5;
end;
A6: dom NORM2 = the_set_of_RealSequences_l^p by FUNCT_2:def 1;
dom NORM1 = the_set_of_RealSequences_l^p by FUNCT_2:def 1;
hence thesis by A6,A4,FUNCT_1:2;
end;
end;
theorem Th8:
for p be Real st 1 <= p holds NORMSTR (#
the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #) is RealLinearSpace
proof
let p be Real;
assume 1 <= p;
then RLSStruct (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences) #) is
RealLinearSpace by Th5;
hence thesis by RSSPACE3:2;
end;
theorem Th9:
for p be Real st p >= 1 holds NORMSTR (#
the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #) is Subspace of
Linear_Space_of_RealSequences
proof
set V =Linear_Space_of_RealSequences;
let p be Real such that
A1: 1 <= p;
set lSpacep = NORMSTR (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), l_norm^p #);
reconsider lSpacep as RealLinearSpace by A1,Th8;
set w1= the RLSStruct of lSpacep;
A2: w1 is Subspace of V by A1,Th5;
then
A3: the Mult of lSpacep = (the Mult of V) | [:REAL, the carrier of lSpacep
:] by RLSUB_1:def 2;
0.w1 = 0.V by A2,RLSUB_1:def 2;
then
A4: 0.lSpacep = 0.V;
the addF of lSpacep = (the addF of V)||the carrier of lSpacep by A2,
RLSUB_1:def 2;
hence thesis by A4,A3,RLSUB_1:def 2;
end;
begin :: The Banach Space of l^p Real Sequences
theorem Th10:
for p be Real
st 1 <=p holds for lp be non empty NORMSTR st lp =
NORMSTR (# the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #) holds the carrier of lp =
the_set_of_RealSequences_l^p & ( for x be set holds x is VECTOR of lp iff x is
Real_Sequence & seq_id(x) rto_power p is summable ) & 0.lp = Zeroseq & ( for x
be VECTOR of lp holds x =seq_id(x) ) & ( for x,y be VECTOR of lp holds x+y =
seq_id(x)+seq_id(y) ) &
( for r be Real for x be VECTOR of lp holds r*x = r(#)
seq_id(x) ) & ( for x be VECTOR of lp holds -x = -seq_id(x) & seq_id(-x) = -
seq_id(x) ) & ( for x,y be VECTOR of lp holds x-y =seq_id(x)-seq_id(y) ) & (
for x be VECTOR of lp holds seq_id(x) rto_power p is summable ) & for x be
VECTOR of lp holds ||.x.|| = ( Sum(seq_id(x) rto_power p) ) to_power (1/p)
proof
let p be Real such that
A1: 1<= p;
let lp be non empty NORMSTR such that
A2: lp = NORMSTR (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), l_norm^p #);
A3: for x be VECTOR of lp holds ||.x.|| = ( Sum(seq_id(x) rto_power p) )
to_power (1/p) by A2,Def3;
A4: for x,y be VECTOR of lp holds x+y =seq_id(x)+seq_id(y)
proof
let x,y be VECTOR of lp;
A5: lp is Subspace of Linear_Space_of_RealSequences by A1,A2,Th9;
then reconsider x1=x as VECTOR of Linear_Space_of_RealSequences by
RLSUB_1:10;
reconsider y1=y as VECTOR of Linear_Space_of_RealSequences by A5,RLSUB_1:10
;
set L1=Linear_Space_of_RealSequences;
set W = the_set_of_RealSequences_l^p;
dom (the addF of L1) = [:the carrier of L1,the carrier of L1:] by
FUNCT_2:def 1;
then
A6: dom ((the addF of Linear_Space_of_RealSequences)||W) =[:W,W:] by RELAT_1:62
;
W is linearly-closed by A1,Th4;
then x+y= ((the addF of Linear_Space_of_RealSequences)||W).[x,y] by A2,
RSSPACE:def 8
.=x1+y1 by A2,A6,FUNCT_1:47;
hence thesis by RSSPACE:2;
end;
A7: for r be Real for x be VECTOR of lp holds r*x =r(#)seq_id(x)
proof
set W = the_set_of_RealSequences_l^p;
set L1=Linear_Space_of_RealSequences;
let r be Real;
reconsider r as Element of REAL by XREAL_0:def 1;
let x be VECTOR of lp;
dom (the Mult of L1) = [:REAL,the carrier of L1:] by FUNCT_2:def 1;
then
A8: dom ((the Mult of Linear_Space_of_RealSequences) | [:REAL,W:]) =[:
REAL,W:] by RELAT_1:62,ZFMISC_1:96;
lp is Subspace of Linear_Space_of_RealSequences by A1,A2,Th9;
then reconsider x1=x as VECTOR of Linear_Space_of_RealSequences by
RLSUB_1:10;
W is linearly-closed by A1,Th4;
then r*x =((the Mult of Linear_Space_of_RealSequences)|[:REAL,W:]).[r,x]
by A2,RSSPACE:def 9
.=r*x1 by A2,A8,FUNCT_1:47;
hence thesis by RSSPACE:3;
end;
the_set_of_RealSequences_l^p is linearly-closed by A1,Th4;
then
A9: 0.lp = 0.Linear_Space_of_RealSequences by A2,RSSPACE:def 10
.= Zeroseq;
A10: for x be set holds x is Element of lp iff x is Real_Sequence & seq_id(x)
rto_power p is summable
proof
let x be set;
x in the_set_of_RealSequences_l^p iff seq_id(x) rto_power p is
summable & x in the_set_of_RealSequences by A1,Def2;
hence thesis by A2,FUNCT_2:8,66;
end;
A11: for x be set holds x is VECTOR of lp implies x =seq_id(x)
proof
let x be set;
x in the_set_of_RealSequences iff x is Real_Sequence by FUNCT_2:8,66;
hence thesis by A1,A2,Def2;
end;
A12: for x be VECTOR of lp holds -x =-seq_id(x) & seq_id(-x)=-seq_id(x)
proof
let x be VECTOR of lp;
lp is Subspace of Linear_Space_of_RealSequences by A1,A2,Th9;
then -x = (-1)*x by RLVECT_1:16
.= -seq_id(x) by A7;
hence thesis;
end;
for x,y be VECTOR of lp holds x-y =seq_id(x)-seq_id(y)
proof
let x,y be VECTOR of lp;
thus x-y = seq_id(x)+seq_id(-y) by A4
.= seq_id(x)-seq_id(y) by A12;
end;
hence thesis by A2,A10,A11,A9,A4,A7,A12,A3;
end;
theorem Th11:
for p be Real
st p>=1 holds for rseq be Real_Sequence st (for n
be Nat holds rseq.n=0) holds rseq rto_power p is summable & ( Sum(
rseq rto_power p) ) to_power (1/p)=0
proof
let p be Real such that
A1: p>=1;
A2: 1/p > 0 by A1,XREAL_1:139;
let rseq be Real_Sequence such that
A3: for n be Nat holds rseq.n=0;
A4: for n be Nat holds (rseq rto_power p).n=0
proof
let n be Nat;
rseq.n=0 by A3;
then |.(rseq).n.| =0 by ABSVALUE:2;
then |.(rseq).n.| to_power p =0 by A1,POWER:def 2;
hence thesis by Def1;
end;
A5: for m be Nat holds Partial_Sums (rseq rto_power p).m = 0
proof
defpred P[Nat] means
(rseq rto_power p).$1 = (Partial_Sums(rseq rto_power p)).$1;
let m be Nat;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A7: (rseq rto_power p).k = (Partial_Sums (rseq rto_power p)).k;
thus (rseq rto_power p).(k+1) = 0 + (rseq rto_power p).(k+1)
.= (rseq rto_power p).k + (rseq rto_power p).(k+1) by A4
.= (Partial_Sums ((rseq rto_power p))).(k+1) by A7,SERIES_1:def 1;
end;
A8: P[0] by SERIES_1:def 1;
for n be Nat holds P[n] from NAT_1:sch 2(A8,A6);
hence (Partial_Sums ((rseq rto_power p))).m = (rseq rto_power p).m
.= 0 by A4;
end;
A9: for e be Real st 0<e ex n be Nat st
for m be Nat st n<=m holds |.(Partial_Sums (rseq rto_power p)).m-0 .|<e
proof
let e be Real such that
A10: 0<e;
take 0;
let m be Nat such that
0<=m;
|.(Partial_Sums (rseq rto_power p)).m-0 .| = |.0-0 .| by A5
.= 0 by ABSVALUE:def 1;
hence thesis by A10;
end;
then
A11: Partial_Sums (rseq rto_power p) is convergent by SEQ_2:def 6;
then lim (Partial_Sums (rseq rto_power p)) =0 by A9,SEQ_2:def 7;
then Sum(rseq rto_power p) =0 by SERIES_1:def 3;
hence thesis by A2,A11,POWER:def 2,SERIES_1:def 2;
end;
theorem Th12:
for p be Real st 1 <=p for rseq be Real_Sequence st rseq
rto_power p is summable & ( Sum(rseq rto_power p) ) to_power (1/p)=0 holds for
n be Nat holds rseq.n = 0
proof
let p be Real such that
A1: 1 <=p;
A2: 1/p > 0 by A1,XREAL_1:139;
let rseq being Real_Sequence such that
A3: rseq rto_power p is summable and
A4: Sum(rseq rto_power p) to_power (1/p)=0;
A5: for i be Nat holds ((rseq) rto_power p).i >= 0
proof
let i be Nat;
( (rseq) rto_power p).i =|.(rseq).i.| to_power p by Def1;
hence thesis by A1,Lm1,COMPLEX1:46;
end;
then ( (Sum(rseq rto_power p) ) to_power (1/p)) to_power p =(Sum(rseq
rto_power p) ) to_power((1/p)*p) by A1,A2,A3,HOLDER_1:2,SERIES_1:18
.=(Sum(rseq rto_power p) ) to_power(1) by A1,XCMPLX_1:106
.=(Sum(rseq rto_power p) ) by POWER:25;
then
A6: (Sum(rseq rto_power p) ) = 0 by A1,A4,POWER:def 2;
now
let n be Nat;
reconsider n9=n as Nat;
A7: 0 to_power (1/p) =0 by A2,POWER:def 2;
(rseq rto_power p).n9 =|.rseq.n9.| to_power p by Def1;
then
A8: |.rseq.n.| to_power p =0 by A3,A5,A6,RSSPACE:17;
(|.rseq.n.| to_power p) to_power (1/p) =|.rseq.n.| to_power (p*(1/p
)) by A1,A2,COMPLEX1:46,HOLDER_1:2
.=|.rseq.n.| to_power (1) by A1,XCMPLX_1:106
.=|.rseq.n.| by POWER:25;
hence rseq.n =0 by A8,A7,ABSVALUE:2;
end;
hence thesis;
end;
Lm5: for p be Real
st 1 <=p for lp be non empty NORMSTR st lp = NORMSTR (#
the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #)
for x being Point of lp, a be Real
holds (seq_id(a *(x)) rto_power p )= ((|.a.| to_power p)(#)(seq_id(x)
rto_power p))
proof
let p be Real such that
A1: 1<= p;
let lp be non empty NORMSTR such that
A2: lp = NORMSTR (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), l_norm^p #);
let x be Point of lp;
let a be Real;
now
let n1 be object;
assume n1 in NAT;
then reconsider n =n1 as Nat;
A3: |.a.| >=0 by COMPLEX1:46;
A4: |.(seq_id(x)).n.| >=0 by COMPLEX1:46;
(seq_id(a *(x)) rto_power p ).n =|.((seq_id(a*x)).n).| to_power p by Def1
.=|.((seq_id(a(#)seq_id(x))).n).| to_power p by A1,A2,Th10
.=|.a*(seq_id(x)).n .| to_power p by SEQ_1:9
.=(|.a.| * |.(seq_id(x)).n.|) to_power p by COMPLEX1:65
.=|.a.| to_power p * |.(seq_id(x)).n.| to_power p by A1,A3,A4,Lm2
.=|.a.| to_power p*(seq_id(x) rto_power p).n by Def1
.=((|.a.| to_power p)(#)(seq_id(x) rto_power p)).n by SEQ_1:9;
hence (seq_id(a *(x)) rto_power p ).n1= ((|.a.| to_power p)(#)(seq_id(x)
rto_power p)).n1;
end;
hence thesis by FUNCT_2:12;
end;
Lm6: for p be Real
st 1 <=p for lp be non empty NORMSTR st lp = NORMSTR (#
the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #)
for x being Point of lp, a be Real
holds ( Sum(seq_id(a*x) rto_power p) ) =(|.a.| to_power p) * Sum(seq_id(x
) rto_power p)
proof
let p be Real such that
A1: 1<= p;
let lp be non empty NORMSTR such that
A2: lp = NORMSTR (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), l_norm^p #);
let x be Point of lp;
A3: (seq_id(x) rto_power p) is summable by A1,A2,Th10;
let a be Real;
thus ( Sum(seq_id(a*x) rto_power p) ) = ( Sum((|.a.| to_power p)(#)(seq_id(
x) rto_power p)) ) by A1,A2,Lm5
.=(|.a.| to_power p) * Sum(seq_id(x) rto_power p) by A3,SERIES_1:10;
end;
Lm7: for p be Real
st 1 <=p for lp be non empty NORMSTR st lp = NORMSTR (#
the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #)
for x being Point of lp, a be Real
holds ( Sum(seq_id(a*x) rto_power p) ) to_power (1/p) =(|.a.| )*(Sum(
seq_id(x) rto_power p) to_power (1/p))
proof
let p be Real such that
A1: 1<= p;
A2: (1/p)>0 by A1,XREAL_1:139;
let lp be non empty NORMSTR such that
A3: lp = NORMSTR (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), l_norm^p #);
let x be Point of lp;
A4: now
let n be Nat;
(seq_id(x) rto_power p).n =|.(seq_id(x)).n.| to_power p by Def1;
hence (seq_id(x) rto_power p).n >= 0 by A1,Lm1,COMPLEX1:46;
end;
(seq_id(x) rto_power p) is summable by A1,A3,Th10;
then
A5: 0<=Sum(seq_id(x) rto_power p) by A4,SERIES_1:18;
let a be Real;
A6: (|.a.| to_power p) >= 0 by A1,Lm1,COMPLEX1:46;
thus ( Sum(seq_id(a*x) rto_power p) ) to_power (1/p) =((|.a.| to_power p) *
Sum(seq_id(x) rto_power p) ) to_power (1/p) by A1,A3,Lm6
.= ((|.a.| to_power p) to_power (1/p)) * ( Sum(seq_id(x) rto_power p)
to_power (1/p)) by A2,A5,A6,Lm2
.= (|.a.| to_power (p*(1/p))) * ( Sum(seq_id(x) rto_power p) to_power (
1/p)) by A1,A2,COMPLEX1:46,HOLDER_1:2
.= (|.a.| to_power 1) * ( Sum(seq_id(x) rto_power p) to_power (1/p)) by A1
,XCMPLX_1:106
.= |.a.|* ( Sum(seq_id(x) rto_power p) to_power (1/p)) by POWER:25;
end;
theorem Th13:
for p be Real st 1 <= p for lp be non empty NORMSTR st lp =
NORMSTR (# the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #)
for x, y being Point of lp, a be Real
holds ( ||.x.|| = 0 iff x = 0.lp ) & 0 <= ||.x.|| & ||.x+y.|| <= ||.x
.|| + ||.y.|| & ||.(a*x).|| = |.a.| * ||.x.||
proof
let p be Real such that
A1: 1<= p;
A2: 1/p > 0 by A1,XREAL_1:139;
let lp be non empty NORMSTR such that
A3: lp = NORMSTR (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), l_norm^p #);
let x, y be Point of lp;
A4: (seq_id(y) rto_power p) is summable by A1,A3,Th10;
A5: ||.y.|| = ( Sum(seq_id(y) rto_power p) ) to_power (1/p) by A3,Def3;
A6: ||.x.|| = ( Sum(seq_id(x) rto_power p) ) to_power (1/p) by A3,Def3;
A7: now
A8: ||.x.|| = ( Sum(seq_id(x) rto_power p) ) to_power (1/p) by A3,Def3;
A9: x in the_set_of_RealSequences by A1,A3,Def2;
assume
A10: ||.x.|| = 0;
seq_id(x) rto_power p is summable by A1,A3,Th10;
then for n be Nat holds 0 = (seq_id(x)).n by A1,A10,A8,Th12;
hence x = Zeroseq by A9,RSSPACE:5
.=0.lp by A1,A3,Th10;
end;
A11: seq_id(x) rto_power p is summable by A1,A3,Def2;
A12: ( Sum(seq_id(x) rto_power p) ) to_power (1/p) = ||.x.|| by A3,Def3;
A13: now
assume x=0.lp;
then x=Zeroseq by A1,A3,Th10;
then
A14: for n be Nat holds (seq_id(x)).n=0 by RSSPACE:4;
thus ||.x.|| = ( Sum(seq_id(x) rto_power p) ) to_power (1/p) by A3,Def3
.= 0 by A1,A14,Th11;
end;
let a be Real;
A15: for n be Nat holds 0 <= (seq_id(x) rto_power p).n
proof
set xp=seq_id(x) rto_power p;
let n be Nat;
A16: 0 < |.(seq_id(x)).n.| or 0=|.(seq_id(x)).n.| by COMPLEX1:46;
xp.n=|.(seq_id(x)).n.| to_power p by Def1;
hence thesis by A1,A16,POWER:34,def 2;
end;
((seq_id(x))+(seq_id(y))) =seq_id((seq_id(x))+(seq_id(y)))
.=seq_id(x+y) by A1,A3,Th10;
then
A17: Sum((((seq_id(x))+(seq_id(y))) rto_power p)) to_power (1/p)
= ||.x + y.|| by A3,Def3;
(seq_id(x) rto_power p) is summable by A1,A3,Th10;
then
A18: ||.x + y.|| <= ||.x.|| + ||.y.|| by A1,A6,A5,A17,A4,Th3;
A19: ||.x.|| = ( Sum(seq_id(x) rto_power p) ) to_power (1/p) by A3,Def3;
||.(a*x).|| = ( Sum(seq_id(a*x) rto_power p) ) to_power (1/p) by A3,Def3
.=(|.a.|)* ||.x.|| by A1,A3,A19,Lm7;
hence thesis by A2,A7,A13,A15,A11,A12,A18,Lm1,SERIES_1:18;
end;
theorem Th14:
for p be Real st p >= 1 for lp be non empty NORMSTR st lp =
NORMSTR (# the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #) holds lp is
reflexive discerning RealNormSpace-like
proof
let p be Real such that
A1: p >=1;
let lp be non empty NORMSTR;
assume
A2: lp = NORMSTR (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), l_norm^p #);
hence ||.0.lp.|| = 0 by A1,Th13;
for x, y being Point of lp, a be Real
holds ( ||.x.|| = 0 iff x = 0.lp )
& 0 <= ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| & ||.(a*x).|| = |.a.| * ||.x
.|| by A1,Th13,A2;
hence thesis by NORMSP_1:def 1;
end;
theorem
for p be Real st p >= 1 for lp be non empty NORMSTR st lp = NORMSTR (#
the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #) holds lp is RealNormSpace by Th9
,Th14;
Lm8: for p be Real st 0 < p
for c be Real, seq be Real_Sequence st seq is
convergent for rseq be Real_Sequence st ( for i be Nat holds rseq .i
= (|.seq.i -c.|) to_power p ) holds rseq is convergent & lim rseq = (|.lim
seq-c.|) to_power p
proof
let p be Real such that
A1: 0 <p;
let c be Real;
let seq be Real_Sequence such that
A2: seq is convergent;
deffunc F(set) = |.seq.$1-c.|;
consider b be Real_Sequence such that
A3: for n be Nat holds b.n=F(n) from SEQ_1:sch 1;
let rseq be Real_Sequence such that
A4: for i be Nat holds rseq .i = (|.seq.i -c.|) to_power p;
A5: for n be Nat holds rseq.n=(b.n) to_power p
proof
let n be Nat;
rseq.n=(|.seq.n -c.|) to_power p by A4
.=(b.n) to_power p by A3;
hence thesis;
end;
A6: for n be Nat holds 0 <=b.n
proof
let n be Nat;
b.n=|.seq.n-c.| by A3;
hence thesis by COMPLEX1:46;
end;
A7: lim b = |.lim seq - c.| by A2,A3,RSSPACE3:1;
b is convergent by A2,A3,RSSPACE3:1;
hence thesis by A1,A7,A6,A5,HOLDER_1:10;
end;
Lm9: for p be Real st 0 < p
for c be Real, seq, seq1 be Real_Sequence st seq
is convergent & seq1 is convergent for rseq be Real_Sequence st ( for i be
Nat holds rseq .i = (|.seq.i -c.|) to_power p +seq1.i ) holds rseq
is convergent & lim rseq = (|.lim seq-c.|) to_power p + lim seq1
proof
let p be Real such that
A1: 0 < p;
let c be Real;
let seq,seq1 be Real_Sequence such that
A2: seq is convergent and
A3: seq1 is convergent;
deffunc F(set) = |.seq.$1-c.| to_power p;
consider b be Real_Sequence such that
A4: for n be Nat holds b.n=F(n) from SEQ_1:sch 1;
let rseq be Real_Sequence such that
A5: for i be Nat holds rseq .i =( (|.seq.i -c.|) to_power p
) + seq1.i;
now
let n be Nat;
thus rseq .n = ( (|.seq.n -c.|) to_power p ) + seq1.n by A5
.=b.n + seq1.n by A4;
end;
then
A6: rseq = b + seq1 by SEQ_1:7;
A7: b is convergent by A1,A2,A4,Lm8;
hence rseq is convergent by A3,A6,SEQ_2:5;
lim b = (|.lim seq-c.|) to_power p by A1,A2,A4,Lm8;
hence thesis by A3,A7,A6,SEQ_2:6;
end;
Lm10: for a,b be Real_Sequence holds a=a+b-b
proof
let a,b be Real_Sequence;
now
let n be Element of NAT;
(a+(b+(-b))).n=a.n+(b+(-b)).n by SEQ_1:7
.=a.n+(b.n+(-b).n) by SEQ_1:7
.=a.n+(b.n+(-b.n)) by SEQ_1:10
.=a.n;
hence (a+b-b).n=a.n by SEQ_1:13;
end;
hence thesis by FUNCT_2:63;
end;
Lm11: for p be Real st p >= 1
for a,b be Real_Sequence st a rto_power p is
summable & b rto_power p is summable holds (a + b) rto_power p is summable
proof
let p be Real such that
A1: p >= 1;
let a,b be Real_Sequence such that
A2: a rto_power p is summable and
A3: b rto_power p is summable;
reconsider a1=a, b1=b as set;
A4: a1 in the_set_of_RealSequences by FUNCT_2:8;
seq_id(a1) = a;
then
A6: a1 in the_set_of_RealSequences_l^p by A1,A2,A4,Def2;
A7: b1 in the_set_of_RealSequences by FUNCT_2:8;
seq_id(b1) = b;
then
A9: b1 in the_set_of_RealSequences_l^p by A1,A3,A7,Def2;
then reconsider b1 as VECTOR of Linear_Space_of_RealSequences;
reconsider a1 as VECTOR of Linear_Space_of_RealSequences by A6;
A10: seq_id(a1+b1)=seq_id(seq_id(a1)+seq_id(b1)) by RSSPACE:2
.=a+b;
the_set_of_RealSequences_l^p is linearly-closed by A1,Th4;
then a1+b1 in the_set_of_RealSequences_l^p by A6,A9,RLSUB_1:def 1;
hence thesis by A1,A10,Def2;
end;
theorem Th16:
for p be Real st 1 <=p for lp be RealNormSpace st lp = NORMSTR
(# the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #) holds for vseq be sequence of lp st
vseq is Cauchy_sequence_by_Norm holds vseq is convergent
proof
let p be Real such that
A1: 1<= p;
A2: 1/p > 0 by A1,XREAL_1:139;
let lp be RealNormSpace such that
A3: lp = NORMSTR (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), l_norm^p #);
let vseq be sequence of lp such that
A4: vseq is Cauchy_sequence_by_Norm;
defpred P[object,object] means
ex i be Nat st $1=i & ex rseqi be
Real_Sequence st (for n be Nat holds rseqi.n=(seq_id(vseq.n)).i) &
rseqi is convergent & $2 = lim rseqi;
A5: p * (1/p) = (p*1)/p by XCMPLX_1:74
.= 1 by A1,XCMPLX_1:60;
A6: for x be object st x in NAT ex y be object st y in REAL & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
deffunc F(Nat) = (seq_id(vseq.$1)).i;
consider rseqi be Real_Sequence such that
A7: for n be Nat holds rseqi.n= F(n) from SEQ_1:sch 1;
reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;
take lr;
now
let e1 be Real such that
A8: e1 > 0;
reconsider e=e1 as Real;
thus ex k be Nat st for m be Nat st k <= m holds
|.rseqi.m -rseqi.k.| < e1
proof
consider k be Nat such that
A9: for n, m be Nat st n >= k & m >= k holds ||.(vseq.
n) - (vseq.m).|| < e by A4,A8,RSSPACE3:8;
for m being Nat st k <= m holds |.rseqi.m-rseqi.k.| < e
proof
let m be Nat such that
A10: k<=m;
A11: ||.(vseq.m) - (vseq.k).|| =
( Sum(seq_id((vseq.m)-(vseq.k)) rto_power p) ) to_power (1/p)
by A3,Def3;
then
( Sum(seq_id((vseq.m)-(vseq.k)) rto_power p) ) to_power (1/p) <
e by A9,A10;
then
A12: (( Sum(seq_id((vseq.m)-(vseq.k)) rto_power p) ) to_power (1/p))
to_power p < e to_power p by A1,A11,Th1,NORMSP_1:4;
A13: now
let i be Nat;
(seq_id((vseq.m)-(vseq.k)) rto_power p).i =|.(seq_id((vseq.
m)-(vseq.k))).i.| to_power p by Def1;
hence (seq_id((vseq.m)-(vseq.k)) rto_power p).i >= 0 by A1,Lm1,
COMPLEX1:46;
end;
reconsider vsem = (vseq.m), vsek = (vseq.k) as VECTOR of lp;
A14: now
let a,b,c be Real such that
A15: a =0 and
A16: b>0 and
A17: c>0;
b*c >0 by A16,A17,XREAL_1:129;
hence a to_power (b *c) =0 by A15,POWER:def 2;
end;
A18: now
let a,b,c be Real such that
A19: a =0 and
A20: b>0 and
A21: c>0;
a to_power b =0 by A19,A20,POWER:def 2;
hence (a to_power b) to_power c =0 by A21,POWER:def 2;
end;
A22: now
let a,b,c be Real such that
A23: a =0 and
A24: b>0 and
A25: c>0;
thus (a to_power b) to_power c = 0 by A18,A23,A24,A25
.= a to_power (b *c) by A14,A23,A24,A25;
end;
A26: for a,b,c be Real st a>=0 & b>0 & c>0 holds (a to_power b)
to_power c = a to_power (b*c)
proof
let a,b,c be Real such that
A27: a>=0 and
A28: b>0 and
A29: c>0;
a >0 or a=0 by A27;
hence thesis by A22,A28,A29,POWER:33;
end;
(seq_id((vseq.m)-(vseq.k)) rto_power p).i =|.(seq_id((vseq.m)
-(vseq.k))).i.| to_power p by Def1;
then
A30: ((seq_id((vseq.m)-(vseq.k)) rto_power p).i) to_power (1/p) =
|.(seq_id((vseq.m)-(vseq.k))).i.| to_power (1) by A1,A2,A5,A26,COMPLEX1:46
.=|.(seq_id((vseq.m)-(vseq.k))).i.| by POWER:25;
A31: rseqi.m=(seq_id(vseq.m)).i by A7;
A32: (seq_id((vseq.m)-(vseq.k)) rto_power p) is summable by A1,A3,Th10;
then
A33: (seq_id((vseq.m)-(vseq.k)) rto_power p).i <= Sum(seq_id((vseq.m
)-(vseq.k)) rto_power p) by A13,RSSPACE2:3;
(( Sum(seq_id((vseq.m)-(vseq.k)) rto_power p) ) to_power (1/p))
to_power p =( Sum(seq_id((vseq.m)-(vseq.k)) rto_power p) ) to_power ((1/p)*p)
by A1,A2,A32,A13,HOLDER_1:2,SERIES_1:18
.= ( Sum(seq_id((vseq.m)-(vseq.k)) rto_power p) ) by A5,POWER:25;
then
A34: (seq_id((vseq.m)-(vseq.k)) rto_power p).i <e to_power p by A12,A33,
XXREAL_0:2;
A35: rseqi.k=(seq_id(vseq.k)).i by A7;
(vsem)-(vsek) =(seq_id(vsem)) - (seq_id(vsek)) by A1,A3,Th10;
then
A36: |.(seq_id((vseq.m)-(vseq.k))).i.|=
|.(seq_id(vseq.m)).i+(-(seq_id(vseq.k))).i.| by SEQ_1:7
.=|.(seq_id(vseq.m)).i +-(seq_id(vseq.k)).i.| by SEQ_1:10
.=|.rseqi.m -rseqi.k.| by A31,A35;
(e to_power p) to_power (1/p) = e to_power ((1/p) * p) by A8,POWER:33
.= e to_power(1) by A1,XCMPLX_1:106
.=e by POWER:25;
hence thesis by A2,A13,A30,A34,A36,Th1;
end;
hence thesis;
end;
end;
then rseqi is convergent by SEQ_4:41;
hence thesis by A7;
end;
consider f be sequence of REAL such that
A37: for x be object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A6);
reconsider tseq=f as Real_Sequence;
A38: now
let i be Nat;
reconsider x=i as set;
A39: i in NAT by ORDINAL1:def 12;
ex i0 be Nat st x=i0 & ex rseqi be Real_Sequence st ( for
n be Nat holds rseqi.n=(seq_id(vseq.n)).i0 ) & rseqi is convergent &
f.x=lim rseqi by A37,A39;
hence
ex rseqi be Real_Sequence st ( for n be Nat holds rseqi.n=
(seq_id(vseq.n)).i ) & rseqi is convergent & tseq.i=lim rseqi;
end;
A40: for e be Real st e >0
ex k be Nat st for n be Nat
st n >= k holds ((seq_id(tseq)-seq_id(vseq.n)) rto_power p ) is summable & Sum(
(seq_id(tseq)-seq_id(vseq.n)) rto_power p) < e
proof
A41: for n be Nat for i be Nat holds for rseq be
Real_Sequence st ( for m be Nat holds rseq.m = Partial_Sums ((seq_id
((vseq.m)-(vseq.n))) rto_power p).i ) holds rseq is convergent & lim rseq =
Partial_Sums ((seq_id(tseq)-seq_id(vseq.n)) rto_power p) .i
proof
let n be Nat;
defpred P[Nat] means
for rseq be Real_Sequence st for m be
Nat holds rseq.m= Partial_Sums ((seq_id((vseq.m)-(vseq.n)))
rto_power p).$1 holds rseq is convergent & lim rseq = Partial_Sums ((seq_id(
tseq)-seq_id(vseq.n)) rto_power p).$1;
A42: for m,k be Nat holds seq_id((vseq.m) - (vseq.k)) =
seq_id(vseq.m)-seq_id(vseq.k)
proof
let m,k be Nat;
seq_id((vseq.m) - (vseq.k)) = seq_id(seq_id((vseq.m))-seq_id((
vseq.k))) by A1,A3,Th10;
hence thesis;
end;
now
let i be Nat such that
A43: for rseq be Real_Sequence st ( for m be Nat holds
rseq.m= Partial_Sums ((seq_id((vseq.m)-(vseq.n))) rto_power p).i ) holds rseq
is convergent & lim rseq =Partial_Sums ((seq_id(tseq)-seq_id(vseq.n)) rto_power
p).i;
thus for rseq be Real_Sequence st ( for m be Nat holds rseq
.m = Partial_Sums ((seq_id((vseq.m)-(vseq.n))) rto_power p).(i+1) ) holds rseq
is convergent & lim rseq =Partial_Sums ((seq_id(tseq)-seq_id(vseq.n)) rto_power
p).(i+1)
proof
deffunc F(Nat) = Partial_Sums ((seq_id((vseq.$1)-(vseq.n)
)) rto_power p).i;
consider rseqb be Real_Sequence such that
A44: for m be Nat holds rseqb.m = F(m) from SEQ_1:
sch 1;
consider rseq0 be Real_Sequence such that
A45: for m be Nat holds rseq0.m=(seq_id(vseq.m)).(i+ 1) and
A46: rseq0 is convergent and
A47: tseq.(i+1)=lim rseq0 by A38;
let rseq be Real_Sequence such that
A48: for m be Nat holds rseq.m = Partial_Sums ((
seq_id((vseq.m)-(vseq.n))) rto_power p).(i+1);
A49: now
let m be Nat;
thus rseq.m = Partial_Sums ((seq_id((vseq.m)-(vseq.n))) rto_power
p).(i+1) by A48
.=((seq_id((vseq.m)-(vseq.n))) rto_power p).(i+1) +
Partial_Sums((seq_id((vseq.m)-(vseq.n))) rto_power p).i by SERIES_1:def 1
.=((seq_id(vseq.m)-seq_id(vseq.n)) rto_power p).(i+1) +
Partial_Sums((seq_id((vseq.m)-(vseq.n))) rto_power p).i by A42
.=((seq_id(vseq.m)-seq_id(vseq.n)) rto_power p).(i+1) + rseqb.
m by A44
.= |.(seq_id(vseq.m)+-seq_id(vseq.n)).(i+1).| to_power p +
rseqb.m by Def1
.= |.(seq_id(vseq.m)).(i+1)+(-seq_id(vseq.n)).(i+1).|
to_power p + rseqb.m by SEQ_1:7
.= |.(seq_id(vseq.m)).(i+1)+-(seq_id(vseq.n)).(i+1).|
to_power p + rseqb.m by SEQ_1:10
.= |.(seq_id(vseq.m)).(i+1)-(seq_id(vseq.n)).(i+1).| to_power
p + rseqb.m
.= |.rseq0.m-(seq_id(vseq.n)).(i+1).| to_power p + rseqb.m by
A45;
end;
A50: lim rseqb = Partial_Sums ((seq_id(tseq)-seq_id(vseq.n))
rto_power p).i by A43,A44;
A51: rseqb is convergent by A43,A44;
then lim rseq = |.lim rseq0-(seq_id(vseq.n)).(i+1).| to_power p +
lim rseqb by A1,A46,A49,Lm9
.= |.tseq.(i+1)+-(seq_id(vseq.n)).(i+1).| to_power p + lim
rseqb by A47
.= |.tseq.(i+1)+(-seq_id(vseq.n)).(i+1).| to_power p + lim
rseqb by SEQ_1:10
.= (|.(tseq-(seq_id(vseq.n))).(i+1).| to_power p) + lim rseqb
by SEQ_1:7
.= ((tseq-(seq_id(vseq.n))) rto_power p).(i+1) + Partial_Sums ((
seq_id(tseq)-seq_id(vseq.n)) rto_power p).i by A50,Def1
.=Partial_Sums ((seq_id(tseq)-seq_id(vseq.n)) rto_power p).(i+1)
by SERIES_1:def 1;
hence thesis by A1,A51,A46,A49,Lm9;
end;
end;
then
A52: for i be Nat st P[i] holds P[i+1];
now
let rseq be Real_Sequence such that
A53: for m be Nat holds rseq.m= Partial_Sums ((seq_id((
vseq.m)-(vseq.n))) rto_power p).0;
thus rseq is convergent & lim rseq = Partial_Sums ((seq_id(tseq)-
seq_id(vseq.n)) rto_power p).0
proof
consider rseq0 be Real_Sequence such that
A54: for m be Nat holds rseq0.m=(seq_id(vseq.m)).0 and
A55: rseq0 is convergent and
A56: tseq.0=lim rseq0 by A38;
A57: for m being Nat holds rseq.m = |.rseq0.m -(seq_id(
vseq.n)).0 .| to_power p
proof
let m be Nat;
rseq.m =Partial_Sums ((seq_id((vseq.m)-(vseq.n))) rto_power p
).0 by A53
.= ((seq_id((vseq.m)-(vseq.n))) rto_power p).0 by SERIES_1:def 1
.= ((seq_id(vseq.m)-seq_id(vseq.n)) rto_power p).0 by A42
.=|.(seq_id(vseq.m)+-seq_id(vseq.n)).0 .| to_power p by Def1
.=|.(seq_id(vseq.m)).0+(-seq_id(vseq.n)).0 .| to_power p by
SEQ_1:7
.=|.(seq_id(vseq.m)).0+-(seq_id(vseq.n)).0 .| to_power p by
SEQ_1:10
.=|.(seq_id(vseq.m)).0-(seq_id(vseq.n)).0 .| to_power p;
hence thesis by A54;
end;
then lim rseq = |.lim(rseq0) -(seq_id(vseq.n)).0 .| to_power p by A1
,A55,Lm8
.= |.tseq.0+-(seq_id(vseq.n)).0 .| to_power p by A56
.=|.tseq.0+(-(seq_id(vseq.n))).0 .| to_power p by SEQ_1:10
.=|.(tseq-(seq_id((vseq.n)))).0 .| to_power p by SEQ_1:7
.=((seq_id(tseq)+-(seq_id(vseq.n))) rto_power p).0 by Def1
.=Partial_Sums ((seq_id(tseq)-(seq_id(vseq.n))) rto_power p).0
by SERIES_1:def 1;
hence thesis by A1,A55,A57,Lm8;
end;
end;
then
A58: P[0];
for i be Nat holds P[i] from NAT_1:sch 2(A58,A52);
hence thesis;
end;
let e2 be Real such that
A59: e2 >0;
set e=e2/2;
reconsider e1=e to_power (1/p) as Real;
e >0 by A59,XREAL_1:215;
then e1>0 by POWER:34;
then consider k be Nat such that
A60: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e1 by A4,RSSPACE3:8;
A61: for m,n be Nat st n >= k & m >= k holds ((seq_id((vseq.m)-
(vseq.n)) rto_power p) is summable & Sum( (seq_id((vseq.m)-(vseq.n)) rto_power
p) ) < e & for i be Nat holds 0 <= ((seq_id((vseq.m)-(vseq.n)))
rto_power p).i)
proof
let m,n be Nat such that
A62: n >= k and
A63: m >= k;
||.(vseq.m) - (vseq.n).|| < e1 by A60,A62,A63;
then (the normF of lp).((vseq.m)-(vseq.n))<e1;
then
A64: (( Sum(seq_id((vseq.m)-(vseq.n)) rto_power p) ) to_power (1/p)) <
e1 by A3,Def3;
A65: for i be Nat holds (seq_id((vseq.m)-(vseq.n)) rto_power
p).i >= 0
proof
let i be Nat;
(seq_id((vseq.m)-(vseq.n)) rto_power p).i =|.(seq_id((vseq.m)-(
vseq.n))).i.| to_power p by Def1;
hence thesis by A1,Lm1,COMPLEX1:46;
end;
A66: (seq_id((vseq.m)-(vseq.n)) rto_power p) is summable by A1,A3,Th10;
then
A67: (( Sum(seq_id((vseq.m)-(vseq.n)) rto_power p) ) to_power (1/p)) >=0
by A2,A65,Lm1,SERIES_1:18;
A68: e1 to_power p = e to_power ((1/p) * p) by A59,POWER:33,XREAL_1:215
.= e to_power(1) by A1,XCMPLX_1:106
.= e by POWER:25;
(( Sum(seq_id((vseq.m)-(vseq.n)) rto_power p) ) to_power (1/p))
to_power p =( Sum(seq_id((vseq.m)-(vseq.n)) rto_power p) ) to_power ((1/p)*p)
by A1,A2,A65,A66,HOLDER_1:2,SERIES_1:18
.= ( Sum(seq_id((vseq.m)-(vseq.n)) rto_power p) ) by A5,POWER:25;
hence thesis by A1,A3,A65,A64,A68,A67,Th1,Th10;
end;
A69: e2 >e by A59,XREAL_1:216;
for n be Nat st n >= k holds ((seq_id(tseq)-seq_id(vseq.n
)) rto_power p ) is summable & Sum ((seq_id(tseq)-seq_id(vseq.n)) rto_power p )
< e2
proof
let n be Nat such that
A70: n >= k;
A71: for i be Nat st 0 <= i holds Partial_Sums ((seq_id(tseq
)-seq_id(vseq.n)) rto_power p).i <=e
proof
let i be Nat such that
0 <=i;
deffunc F(Nat)= Partial_Sums ((seq_id((vseq.$1)-(vseq.n)))
rto_power p).i;
consider rseq be Real_Sequence such that
A72: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1;
A73: for m be Nat st m >= k holds rseq.m <= e
proof
let m be Nat;
A74: rseq.m = Partial_Sums ((seq_id((vseq.m)-(vseq.n))) rto_power p
). i by A72;
assume
A75: m >= k;
then
A76: for i be Nat holds 0 <= ((seq_id((vseq.m)-(vseq.n))
) rto_power p).i by A61,A70;
(seq_id((vseq.m)-(vseq.n)) rto_power p) is summable by A61,A70,A75;
then
A77: Partial_Sums ((seq_id((vseq.m)-(vseq.n))) rto_power p) .i <=
Sum( (seq_id((vseq.m)-(vseq.n)) rto_power p) ) by A76,RSSPACE2:3;
Sum( (seq_id((vseq.m)-(vseq.n)) rto_power p) ) < e by A61,A70,A75;
hence thesis by A77,A74,XXREAL_0:2;
end;
A78: lim rseq = Partial_Sums ((seq_id(tseq)-seq_id(vseq.n)) rto_power
p) .i by A41,A72;
rseq is convergent by A41,A72;
hence thesis by A78,A73,RSSPACE2:5;
end;
now
take e2=e+1;
A79: e2>e by XREAL_1:29;
let i be Nat;
Partial_Sums ((seq_id(tseq)-seq_id(vseq.n)) rto_power p) .i <=e
by A71,NAT_1:2;
hence Partial_Sums ((seq_id(tseq)-seq_id(vseq.n)) rto_power p) .i <e2
by A79,XXREAL_0:2;
end;
then
A80: Partial_Sums ((seq_id(tseq)-seq_id(vseq.n)) rto_power p) is
bounded_above by SEQ_2:def 3;
A81: Sum ((seq_id(tseq)-seq_id(vseq.n)) rto_power p) = lim Partial_Sums
((seq_id(tseq)-seq_id(vseq.n)) rto_power p) by SERIES_1:def 3;
A82: for i be Nat holds 0 <= ((seq_id(tseq)-seq_id(vseq.n))
rto_power p) .i
proof
let i be Nat;
((seq_id(tseq)-seq_id(vseq.n)) rto_power p) .i =(|.(seq_id(
tseq)-seq_id(vseq.n)).i.|) to_power p by Def1;
hence thesis by A1,Lm1,COMPLEX1:46;
end;
then ((seq_id(tseq)-seq_id(vseq.n)) rto_power p) is summable by A80,
SERIES_1:17;
then Partial_Sums((seq_id(tseq)-seq_id(vseq.n)) rto_power p) is
convergent by SERIES_1:def 2;
then lim Partial_Sums ((seq_id(tseq)-seq_id(vseq.n)) rto_power p) <= e
by A71,RSSPACE2:5;
hence thesis by A69,A82,A80,A81,SERIES_1:17,XXREAL_0:2;
end;
hence thesis;
end;
(seq_id(tseq)) rto_power p is summable
proof
consider m be Nat such that
A83: for n be Nat st n >= m holds ((seq_id(tseq)-seq_id(
vseq.n)) rto_power p ) is summable & Sum((seq_id(tseq)-seq_id(vseq.n))
rto_power p) < 1 by A40;
A84: ((seq_id(tseq)-seq_id(vseq.m)) rto_power p ) is summable by A83;
set d=(seq_id(tseq));
set b=(seq_id(vseq.m));
set a=(seq_id(tseq) -seq_id(vseq.m));
A85: a +b =(seq_id(tseq)+seq_id(vseq.m))+(-seq_id(vseq.m)) by SEQ_1:13
.=seq_id(tseq)+seq_id(vseq.m)-seq_id(vseq.m)
.=d by Lm10;
seq_id( (vseq.m) ) rto_power p is summable by A1,A3,Def2;
hence thesis by A1,A84,A85,Lm11;
end;
then reconsider tv=tseq as Point of lp by A1,A3,Th10;
for e be Real st e > 0 ex m be Nat st
for n be Nat st n >= m holds ||.(vseq.n) - tv.|| < e
proof
let e be Real such that
A86: e > 0;
set e1=e to_power p;
consider m be Nat such that
A87: for n be Nat st n >= m holds ((seq_id(tseq)-seq_id(
vseq.n)) rto_power p ) is summable & Sum((seq_id(tseq)-seq_id(vseq.n))
rto_power p) < e1 by A40,A86,POWER:34;
now
let n be Nat such that
A88: n >= m;
A89: Sum((seq_id(tseq)-seq_id(vseq.n)) rto_power p) < e1 by A87,A88;
for i be Nat holds ((seq_id(tseq)-seq_id(vseq.n))
rto_power p).i >= 0
proof
let i be Nat;
((seq_id(tseq)-seq_id(vseq.n)) rto_power p).i =|.(seq_id(tseq)
-seq_id(vseq.n)).i.| to_power p by Def1;
hence thesis by A1,Lm1,COMPLEX1:46;
end;
then
A90: Sum((seq_id(tseq)-seq_id(vseq.n)) rto_power p) >=0 by A87,A88,SERIES_1:18
;
A91: e1 to_power(1/p) = e to_power (p * (1/p)) by A86,POWER:33
.= e to_power 1 by A1,XCMPLX_1:106
.= e by POWER:25;
(Sum((seq_id(tv)-seq_id(vseq.n)) rto_power p)) to_power (1/p ) =(
Sum(seq_id(seq_id(tv)-seq_id(vseq.n)) rto_power p)) to_power (1/p )
.=(Sum(seq_id((tv)-(vseq.n)) rto_power p)) to_power (1/p ) by A1,A3
,Th10
.= ||.(tv)+(-(vseq.n)).|| by A3,Def3
.=||.-(vseq.n-tv).|| by RLVECT_1:33
.=||.vseq.n-tv.|| by NORMSP_1:2;
hence ||.vseq.n-tv.|| <e by A2,A90,A89,A91,Th1;
end;
hence thesis;
end;
hence thesis by NORMSP_1:def 6;
end;
::$L https://en.wikipedia.org/wiki/Quartic_equation The Solution of the General Quartic Equation
definition
let p be Real such that
A1: 1 <= p;
func l_Space^p -> RealBanachSpace equals
NORMSTR (#
the_set_of_RealSequences_l^p, Zero_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Add_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), Mult_(the_set_of_RealSequences_l^p,
Linear_Space_of_RealSequences), l_norm^p #);
coherence
proof
set lp= NORMSTR (# the_set_of_RealSequences_l^p, Zero_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Add_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), Mult_(
the_set_of_RealSequences_l^p,Linear_Space_of_RealSequences), l_norm^p #);
reconsider lp as RealNormSpace by A1,Th9,Th14;
for vseq be sequence of lp st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent by A1,Th16;
hence thesis by LOPBAN_1:def 15;
end;
end;