= N.i holds ||. Sq.j - Sq.(N.i) .|| < 2 to_power (-i) proof let X be RealNormSpace, Sq be sequence of X; assume A1: Sq is Cauchy_sequence_by_Norm; 1 =2 to_power (-0) by POWER:24; then consider N0 be Nat such that A2: for j,i be Nat st j >= N0 & i >= N0 holds ||. Sq.j - Sq.i .|| < 2 to_power (-0) by A1,RSSPACE3:8; reconsider N0 as Element of NAT by ORDINAL1:def 12; defpred P[set,set,set] means ex n,x,y be Nat st n=$1 & x=$2 & y=$3 & ( ( for j be Nat st j >= x holds ||.Sq.j -Sq.x.|| < 2 to_power (-n) ) implies x < y & ( for j be Nat st j >= y holds ||.Sq.j -Sq.y.|| < 2 to_power (-(n+1)) ) ); A3:for n being Nat,x being Element of NAT ex y being Element of NAT st P[n,x,y] proof let n be Nat, x be Element of NAT; now assume for j be Nat st j >= x holds ||.Sq.j -Sq.x.|| < 2 to_power (-n); 0 < 2 to_power (-(n+1)) by POWER:34; then consider N2 be Nat such that A4: for j,i be Nat st j >= N2 & i >= N2 holds ||.Sq.j -Sq.i.|| < 2 to_power (-(n+1)) by A1,RSSPACE3:8; set y= max(x,N2)+1; take y; x <= max(x,N2) by XXREAL_0:25; hence x < y by NAT_1:13; N2 <= max(x,N2) by XXREAL_0:25; then A5: N2 < y by NAT_1:13; thus for j be Nat st j >= y holds ||.Sq.j -Sq.y.|| < 2 to_power (-(n+1)) proof let j be Nat; assume j >= y; then j >= N2 & y >=N2 by A5,XXREAL_0:2; hence thesis by A4; end; end; hence thesis; end; consider f being sequence of NAT such that A6: f.0 = N0 & for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A3); defpred Q[Nat] means for j be Nat st j >= f.$1 holds ||. Sq.j - Sq.(f.$1) .|| < 2 to_power (-$1); A7:Q[ 0] by A2,A6; A8:now let i be Nat; assume A9: Q[i]; ex n,x,y be Nat st n=i & x=f.i & y=f.(i+1) & ( (for j be Nat st j >= x holds ||.Sq.j -Sq.x.|| < 2 to_power (-n)) implies x < y & (for j be Nat st j >= y holds ||.Sq.j -Sq.y.|| < 2 to_power (-(n+1)) ) ) by A6; hence Q[i+1] by A9; end; A10:for i be Nat holds Q[i] from NAT_1:sch 2(A7,A8); now let i be Nat; ex n,x,y be Nat st n=i & x=f.i & y=f.(i+1) & ( (for j be Nat st j >= x holds ||.Sq.j -Sq.x.|| < 2 to_power (-n)) implies x < y & (for j be Nat st j >= y holds ||.Sq.j -Sq.y.|| < 2 to_power (-(n+1))) ) by A6; hence f.i < f.(i+1) by A10; end; then f is increasing; hence thesis by A10; end; theorem Th66: for F be Functional_Sequence of X,REAL st (for m be Nat holds F.m in Lp_Functions(M,k)) holds for m be Nat holds (Partial_Sums F).m in Lp_Functions(M,k) proof let F be Functional_Sequence of X,REAL; assume A1: for m be Nat holds F.m in Lp_Functions(M,k); defpred P[Nat] means (Partial_Sums F).$1 in Lp_Functions(M,k); (Partial_Sums F).0 = F.0 by MESFUN9C:def 2; then A2:P[ 0] by A1; A3:now let j be Nat; assume P[j]; then A4:(Partial_Sums F).j in Lp_Functions(M,k) & F.(j+1) in Lp_Functions(M,k) by A1; (Partial_Sums F).(j+1) = (Partial_Sums F).j + F.(j+1) by MESFUN9C:def 2; hence P[j+1] by A4,Th25; end; for j being Nat holds P[j] from NAT_1:sch 2(A2,A3); hence thesis; end; theorem Th67: for F be Functional_Sequence of X,REAL st (for m be Nat holds F.m is nonnegative) holds for m be Nat holds (Partial_Sums F).m is nonnegative proof let F be Functional_Sequence of X,REAL; assume A1: for m be Nat holds F.m is nonnegative; defpred P[Nat] means (Partial_Sums F).$1 is nonnegative; (Partial_Sums F).0 = F.0 by MESFUN9C:def 2; then A2:P[ 0] by A1; A3:now let k be Nat; assume P[k]; then A4:(Partial_Sums F).k is nonnegative & F.(k+1) is nonnegative by A1; (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by MESFUN9C:def 2; hence P[k+1] by A4,MESFUNC6:56; end; for k being Nat holds P[k] from NAT_1:sch 2(A2,A3); hence thesis; end; theorem Th68: for F be Functional_Sequence of X,REAL, x be Element of X, n,m be Nat st F is with_the_same_dom & x in dom(F.0) & (for k be Nat holds F.k is nonnegative) & n <= m holds ((Partial_Sums F).n).x <= ((Partial_Sums F).m).x proof let F be Functional_Sequence of X,REAL, x be Element of X, n,m be Nat; assume A1: F is with_the_same_dom; assume A2: x in dom(F.0); assume A3: for m be Nat holds F.m is nonnegative; assume A4: n <= m; set PF = Partial_Sums F; defpred P[Nat] means (PF.n).x <= (PF.$1).x; A5:for k be Nat holds (PF.k).x <= (PF.(k+1)).x proof let k be Nat; A6:PF.(k+1) = PF.k + F.(k+1) by MESFUN9C:def 2; A7:dom(PF.(k+1)) = dom(F.0) by A1,MESFUN9C:11; F.(k+1) is nonnegative & PF.k is nonnegative by A3,Th67; then 0 <= (F.(k+1)).x & 0 <= (PF.k).x by MESFUNC6:51; then (PF.k).x + 0 <= (PF.k).x + (F.(k+1)).x by XREAL_1:7; hence thesis by A7,A2,A6,VALUED_1:def 1; end; A8:for k be Nat st k >= n & (for l be Nat st l >= n & l < k holds P[l]) holds P[k] proof let k be Nat; assume A9: k >= n & for l be Nat st l >= n & l < k holds P[l]; now assume k > n; then k >= n + 1 by NAT_1:13; then A10: k = n+1 or k > n+1 by XXREAL_0:1; now assume A11: k > n+1; then reconsider l = k-1 as Nat by NAT_1:20; k < k+1 by NAT_1:13; then k > l & l >= n by A11,XREAL_1:19; then A12: (PF.n).x <= (PF.l).x by A9; k = l+1; then (PF.l).x <= (PF.k).x by A5; hence thesis by A12,XXREAL_0:2; end; hence thesis by A10,A5; end; hence thesis by A9,XXREAL_0:1; end; for k being Nat st k >= n holds P[k] from NAT_1:sch 9(A8); hence thesis by A4; end; theorem Th69: for F be Functional_Sequence of X,REAL st F is with_the_same_dom holds (abs F) is with_the_same_dom proof let F be Functional_Sequence of X,REAL; assume A1: F is with_the_same_dom; for n,m be Nat holds dom((abs F).n) = dom((abs F).m) proof let n,m be Nat; (abs F).n = abs(F.n) & (abs F).m = abs(F.m) by SEQFUNC:def 4; then dom((abs F).n) = dom(F.n) & dom((abs F).m) = dom(F.m) by VALUED_1:def 11; hence dom((abs F).n) = dom((abs F).m) by A1,MESFUNC8:def 2; end; hence abs F is with_the_same_dom by MESFUNC8:def 2; end; theorem Th70: for k be geq_than_1 Real, Sq be sequence of Lp-Space(M,k) st Sq is Cauchy_sequence_by_Norm holds Sq is convergent proof let k be geq_than_1 Real; let Sq be sequence of Lp-Space(M,k); A1:1 <= k by Def1; assume A2: Sq is Cauchy_sequence_by_Norm; consider Fsq be with_the_same_dom Functional_Sequence of X,REAL such that A3: for n be Nat holds Fsq.n in Lp_Functions(M,k) & Fsq.n in Sq.n & Sq.n= a.e-eq-class_Lp(Fsq.n,M,k) & ex r be Real st 0<=r & r = Integral(M,(abs (Fsq.n)) to_power k) & ||. Sq.n .|| =r to_power (1/k) by Th63; Fsq.0 in Lp_Functions(M,k) by A3; then A4: ex D be Element of S st M.D` =0 & dom(Fsq.0) = D & (Fsq.0) is D-measurable by Th35; then reconsider E = dom(Fsq.0) as Element of S; consider N be increasing sequence of NAT such that A5: for i,j be Nat st j >= N.i holds ||. Sq.j - Sq.(N.i) .|| < 2 to_power (-i) by Th65,A2; deffunc FsqN(Nat) = Fsq.(N.$1); consider F1 be Functional_Sequence of X,REAL such that A6: for n be Nat holds F1.n = FsqN(n) from SEQFUNC:sch 1; A7: for n be Nat holds dom(F1.n) = E & F1.n in Lp_Functions(M,k) & F1.n is E-measurable & abs(F1.n) in Lp_Functions(M,k) proof let n be Nat; A8: F1.n = Fsq.(N.n) by A6; hence A9: dom(F1.n) = E & F1.n in Lp_Functions(M,k) by A3,MESFUNC8:def 2; then consider F be PartFunc of X,REAL such that Z1: F1.n = F & ex ND be Element of S st M.ND` =0 & dom F = ND & F is ND-measurable & (abs F) to_power k is_integrable_on M; consider ND be Element of S such that Z2: M.ND` =0 & dom F = ND & F is ND-measurable & (abs F) to_power k is_integrable_on M by Z1; ND = E by Z1,Z2,A8,MESFUNC8:def 2; hence F1.n is E-measurable by Z1,Z2; thus abs(F1.n) in Lp_Functions(M,k) by A9,Th28; end; for n,m be Nat holds dom (F1.n) = dom (F1.m) proof let n,m be Nat; dom(F1.n) = E & dom(F1.m) = E by A7; hence thesis; end; then reconsider F1 as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2; deffunc FF(Nat) = F1.($1+1) - F1.$1; consider FMF be Functional_Sequence of X,REAL such that A10: for n be Nat holds FMF.n = FF(n) from SEQFUNC:sch 1; A11: for n be Nat holds dom(FMF.n) = E & FMF.n in Lp_Functions(M,k) proof let n be Nat; A12: dom(F1.n) = E & dom(F1.(n+1)) = E by A7; FMF.n = F1.(n+1) - F1.n by A10; then dom(FMF.n) = dom (F1.(n+1)) /\ dom (F1.n) by VALUED_1:12; hence dom(FMF.n) = E by A12; Fsq.(N.(n+1)) in Lp_Functions(M,k) & Fsq.(N.n) in Lp_Functions(M,k) by A3; then F1.(n+1) in Lp_Functions(M,k) & F1.n in Lp_Functions(M,k) by A6; then F1.(n+1) - F1.n in Lp_Functions(M,k) by Th27; hence FMF.n in Lp_Functions(M,k) by A10; end; for n,m be Nat holds dom(FMF.n) = dom(FMF.m) proof let n,m be Nat; dom(FMF.n) = E & dom(FMF.m) = E by A11; hence thesis; end; then reconsider FMF as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2; set AbsFMF = abs FMF; A13: for n be Nat holds AbsFMF.n is nonnegative & dom(AbsFMF.n) = E & abs(AbsFMF.n) = AbsFMF.n & AbsFMF.n in Lp_Functions(M,k) & AbsFMF.n is E-measurable proof let n be Nat; A14: AbsFMF.n = abs (FMF.n) by SEQFUNC:def 4; hence AbsFMF.n is nonnegative; A15: dom(FMF.n) = E & FMF.n in Lp_Functions(M,k) by A11; hence dom(AbsFMF.n) = E & abs(AbsFMF.n) = AbsFMF.n by A14,VALUED_1:def 11; thus AbsFMF.n in Lp_Functions(M,k) by A11,A14,Th28; then consider D be Element of S such that Z1: M.D` = 0 & dom(AbsFMF.n) = D & AbsFMF.n is D-measurable by Th35; D = E by Z1,A15,A14,VALUED_1:def 11; hence AbsFMF.n is E-measurable by Z1; end; reconsider AbsFMF as with_the_same_dom Functional_Sequence of X,REAL by Th69; deffunc Gk(Nat) =abs(F1.0) + (Partial_Sums AbsFMF).$1; consider G be Functional_Sequence of X,REAL such that A16: for n be Nat holds G.n = Gk(n) from SEQFUNC:sch 1; A17:for n be Nat holds dom(G.n) = E & G.n in Lp_Functions(M,k) & G.n is nonnegative & G.n is E-measurable & abs(G.n) = G.n proof let n be Nat; A18: G.n = abs(F1.0) + (Partial_Sums AbsFMF).n by A16; then A19: dom(G.n) = dom(abs(F1.0)) /\ dom((Partial_Sums AbsFMF).n) by VALUED_1:def 1 .= dom(F1.0) /\ dom((Partial_Sums AbsFMF).n) by VALUED_1:def 11 .= dom(F1.0) /\ dom(AbsFMF.0) by MESFUN9C:11; A20: (Partial_Sums AbsFMF).n in Lp_Functions(M,k) & (Partial_Sums AbsFMF).n is nonnegative & (Partial_Sums AbsFMF).n is E-measurable by A13,Th66,Th67,MESFUN9C:16; A21: dom(AbsFMF.0) = E by A13; A22: F1.0 in Lp_Functions(M,k) & dom(F1.0) = E & F1.0 is E-measurable by A7; then abs(F1.0) in Lp_Functions(M,k) & abs(F1.0) is nonnegative & abs(F1.0) is E-measurable by Th28,MESFUNC6:48; hence thesis by A19,A22,A21,A18,A20,Th14,Th25,MESFUNC6:26,56; end; deffunc Gpk(Nat) =(G.$1) to_power k; consider Gp be Functional_Sequence of X,REAL such that A23: for n be Nat holds Gp.n = Gpk(n) from SEQFUNC:sch 1; A24:for n be Nat holds ((G.n) to_power k) is nonnegative & ((G.n) to_power k) is E-measurable proof let n be Nat; A25: G.n is nonnegative by A17; hence ((G.n) to_power k) is nonnegative; G.n is E-measurable & dom(G.n) = E by A17; hence ((G.n) to_power k) is E-measurable by A25,MESFUN6C:29; end; reconsider ExtGp = R_EAL Gp as Functional_Sequence of X,ExtREAL; A26:for n be Nat holds dom(ExtGp.n) = E & ExtGp.n is E-measurable & ExtGp.n is nonnegative proof let n be Nat; ExtGp.n = R_EAL((G.n) to_power k) by A23; then dom(ExtGp.n) = dom (G.n) by MESFUN6C:def 4; hence dom(ExtGp.n) = E by A17; ((G.n) to_power k) is E-measurable by A24; then R_EAL((G.n) to_power k) is E-measurable; hence ExtGp.n is E-measurable by A23; ((G.n) to_power k) is nonnegative by A24; hence ExtGp.n is nonnegative by A23; end; then A27:dom(ExtGp.0) = E & ExtGp.0 is nonnegative; for n,m be Nat holds dom (ExtGp.n) = dom (ExtGp.m) proof let n,m be Nat; dom (ExtGp.n) = E & dom(ExtGp.m) = E by A26; hence thesis; end; then reconsider ExtGp as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2; A28:for n,m be Nat st n <=m holds for x be Element of X st x in E holds (ExtGp.n).x <= (ExtGp.m).x proof let n,m be Nat; assume A29:n <=m; let x be Element of X; assume A30:x in E; then A31: x in dom (G.n) & x in dom (G.m) by A17; then x in dom((G.n) to_power k) & x in dom((G.m) to_power k) by MESFUN6C:def 4; then ((G.n).x) to_power k = ((G.n) to_power k).x & ((G.m).x) to_power k = ((G.m) to_power k).x by MESFUN6C:def 4; then A32: ((G.n).x) to_power k = (ExtGp.n).x & ((G.m).x) to_power k = (ExtGp.m).x by A23; dom(AbsFMF.0) = E by A13; then ((Partial_Sums AbsFMF).n).x <= ((Partial_Sums AbsFMF).m).x by Th68,A29,A30,A13; then A33: (abs(F1.0)).x + ((Partial_Sums AbsFMF).n).x <= (abs(F1.0)).x + ((Partial_Sums AbsFMF).m).x by XREAL_1:6; G.m= abs(F1.0) + (Partial_Sums AbsFMF).m & G.n= abs(F1.0) + (Partial_Sums AbsFMF).n by A16; then A34: (G.m).x= (abs(F1.0)).x + ((Partial_Sums AbsFMF).m).x & (G.n).x= (abs(F1.0)).x + ((Partial_Sums AbsFMF).n).x by A31,VALUED_1:def 1 ; G.n is nonnegative by A17; then 0 <= (G.n).x by MESFUNC6:51; hence thesis by A32,A33,A34,HOLDER_1:3; end; A35:for x be Element of X st x in E holds ExtGp#x is non-decreasing proof let x be Element of X; assume A36: x in E; for n,m be Nat st m<=n holds ((ExtGp)#x).m <= ((ExtGp)#x).n proof let n,m be Nat; assume m <= n; then ((ExtGp).m).x <= ((ExtGp).n).x by A28,A36; then ((ExtGp)#x).m <= ((ExtGp).n).x by MESFUNC5:def 13; hence thesis by MESFUNC5:def 13; end; hence ExtGp#x is non-decreasing by RINFSUP2:7; end; A37:for x be Element of X st x in E holds ExtGp#x is convergent proof let x be Element of X; assume x in E; then ExtGp#x is non-decreasing by A35; hence thesis by RINFSUP2:37; end; then consider I be ExtREAL_sequence such that A38: (for n be Nat holds I.n = Integral(M,ExtGp.n)) & I is convergent & Integral(M,lim ExtGp) = lim I by A27,A26,A28,MESFUNC9:52; now let y be object; assume y in rng I; then consider x be Element of NAT such that A39: y = I.x by FUNCT_2:113; A40: y = Integral(M,Gp.x) by A39,A38; G.x = abs(G.x) by A17; then A41: Gp.x = abs(G.x) to_power k by A23; G.x in Lp_Functions(M,k) by A17; hence y in REAL by A40,A41,Th49; end; then rng I c= REAL; then reconsider Ir = I as sequence of REAL by FUNCT_2:6; deffunc KAbsFMF(Nat) = Integral(M,(AbsFMF.$1) to_power k); A42:for x being Element of NAT holds KAbsFMF(x) is Element of REAL proof let x being Element of NAT; (AbsFMF.x) in Lp_Functions(M,k) by A13; then Integral(M,(abs(AbsFMF.x)) to_power k) in REAL by Th49; hence thesis by A13; end; consider KPAbsFMF being sequence of REAL such that A43: for x be Element of NAT holds KPAbsFMF.x = KAbsFMF(x) from FUNCT_2:sch 9(A42); deffunc KKAbsFMF(Nat) = (KPAbsFMF.$1) to_power (1/k); A44:for x being Element of NAT holds KKAbsFMF(x) is Element of REAL by XREAL_0:def 1; consider PAbsFMF being sequence of REAL such that A45: for x be Element of NAT holds PAbsFMF.x = KKAbsFMF(x) from FUNCT_2:sch 9(A44); F1.0 in Lp_Functions(M,k) by A7; then reconsider RF0=Integral(M,(abs(F1.0)) to_power k) as Element of REAL by Th49; deffunc LAbsFMF(Nat) = RF0 to_power (1/k) + (Partial_Sums PAbsFMF).$1; A46:for x being Element of NAT holds LAbsFMF(x) is Element of REAL by XREAL_0:def 1; consider QAbsFMF being sequence of REAL such that A47: for x being Element of NAT holds QAbsFMF.x = LAbsFMF(x) from FUNCT_2:sch 9(A46); A48:for n being Nat holds (Ir.n) to_power (1/k) <= QAbsFMF.n proof defpred PN[Nat] means (Ir.$1) to_power (1/k) <= QAbsFMF.$1; A49: abs(F1.0) in Lp_Functions(M,k) & AbsFMF.0 in Lp_Functions(M,k) by A13,A7; G.0 = abs(F1.0) + (Partial_Sums AbsFMF).0 by A16; then A50: G.0 =abs(F1.0) + AbsFMF.0 by MESFUN9C:def 2; Ir.0 = Integral(M,Gp.0) by A38; then Ir.0 = Integral(M,(G.0) to_power k) by A23; then A51: Ir.0 = Integral(M,abs( abs(F1.0) + AbsFMF.0 ) to_power k) by A17,A50; KPAbsFMF.0 = Integral(M,(AbsFMF.0) to_power k) by A43; then A52: KPAbsFMF.0 = Integral(M,abs(AbsFMF.0) to_power k) by A13; A53: RF0 = Integral(M,abs(abs(F1.0)) to_power k); QAbsFMF.0 = RF0 to_power (1/k) + (Partial_Sums PAbsFMF).0 by A47; then QAbsFMF.0 = RF0 to_power (1/k) + PAbsFMF.0 by SERIES_1:def 1; then QAbsFMF.0 = RF0 to_power (1/k) + (KPAbsFMF.0) to_power (1/k) by A45; then A54: PN[ 0] by A1,A49,A51,A52,A53,Th61; A55: now let n being Nat; A56: n in NAT by ORDINAL1:def 12; assume PN[n]; then A57: (Ir.n) to_power (1/k) + PAbsFMF.(n+1) <= QAbsFMF.n + PAbsFMF.(n+1) by XREAL_1:6; G.(n+1) = abs(F1.0) + (Partial_Sums AbsFMF).(n+1) by A16 .= abs(F1.0) + ((Partial_Sums AbsFMF).n + AbsFMF.(n+1)) by MESFUN9C:def 2 .= abs(F1.0) +(Partial_Sums AbsFMF).n + AbsFMF.(n+1) by RFUNCT_1:8; then A58: G.(n+1) = G.n + AbsFMF.(n+1) by A16; A59: AbsFMF.(n+1) in Lp_Functions(M,k) & G.n in Lp_Functions(M,k) by A13,A17; KPAbsFMF.(n+1) = Integral(M,(AbsFMF.(n+1)) to_power k) by A43; then A60: KPAbsFMF.(n+1) = Integral(M,abs (AbsFMF.(n+1)) to_power k) by A13; A61: PAbsFMF.(n+1) = (KPAbsFMF.(n+1)) to_power (1/k) by A45; Ir.n = Integral(M,Gp.n) & Ir.(n+1) = Integral(M,Gp.(n+1)) by A38; then Ir.n = Integral(M,(G.n) to_power k) & Ir.(n+1) = Integral(M,(G.(n+1)) to_power k) by A23; then Ir.n = Integral(M,abs (G.n) to_power k) & Ir.(n+1) =Integral(M,abs (G.n + AbsFMF.(n+1)) to_power k) by A58,A17; then (Ir.(n+1)) to_power (1/k) <= (Ir.n) to_power (1/k) + PAbsFMF.(n+1) by A1,A59,A60,A61,Th61; then A62: (Ir.(n+1)) to_power (1/k) <= QAbsFMF.n + PAbsFMF.(n+1) by A57,XXREAL_0:2 ; QAbsFMF.n + PAbsFMF.(n+1) = RF0 to_power (1/k) + (Partial_Sums PAbsFMF).n + PAbsFMF.(n+1) by A47,A56 .= RF0 to_power (1/k) + ((Partial_Sums PAbsFMF).n + PAbsFMF.(n+1)) .= RF0 to_power (1/k) + (Partial_Sums PAbsFMF).(n+1) by SERIES_1:def 1; hence PN[n+1] by A62,A47; end; for n be Nat holds PN[n] from NAT_1:sch 2(A54,A55); hence thesis; end; A63:for n be Nat holds PAbsFMF.n = ||. Sq.(N.(n+1))-Sq.(N.n) .|| proof let n be Nat; A64: n in NAT by ORDINAL1:def 12; set m = N.n; set m1 = N.(n+1); A65: F1.(n+1) = Fsq.(N.(n+1)) & F1.n = Fsq.(N.n) by A6; AbsFMF.n = abs (FMF.n) by SEQFUNC:def 4; then A66: AbsFMF.n = abs( Fsq.(N.(n+1)) - Fsq.(N.n) ) by A65,A10; A67: Fsq.(N.(n+1)) in Lp_Functions(M,k) & Fsq.(N.(n+1)) in Sq.(N.(n+1)) & Fsq.(N.n) in Lp_Functions(M,k) & Fsq.(N.n) in Sq.m by A3; then (-1)(#)(Fsq.m) in (-1)*(Sq.m) by Th54; then Fsq.m1 - Fsq.m in Sq.m1 + (-1)*(Sq.m) by Th54,A67; then Fsq.m1 - Fsq.m in Sq.m1 - Sq.m by RLVECT_1:16; then A68: ex r be Real st 0<=r & r = Integral(M,(abs (Fsq.m1 - Fsq.m)) to_power k) & ||. Sq.m1 - Sq.m .|| = r to_power (1/k) by Th53; PAbsFMF.n = (KPAbsFMF.n) to_power (1/k) by A45,A64; hence thesis by A68,A66,A43,A64; end; 1/2 < 1; then |.1/2.| < 1 by ABSVALUE:def 1; then A69:(1/2) GeoSeq is summable & Sum((1/2) GeoSeq) = 1/(1-(1/2)) by SERIES_1:24; for n be Nat holds 0<=PAbsFMF.n & PAbsFMF.n <= ((1/2) GeoSeq).n proof let n be Nat; A70: PAbsFMF.n = ||. Sq.(N.(n+1)) - Sq.(N.n) .|| by A63; hence 0 <= PAbsFMF.n; ((1/2) GeoSeq).n = (1/2) |^n by PREPOWER:def 1 .= (1/2) to_power n by POWER:41; then A71: ((1/2) GeoSeq).n = 2 to_power (-n) by POWER:32; N is Real_Sequence by FUNCT_2:7,NUMBERS:19; then N.n < N.(n+1) by SEQM_3:def 6; hence PAbsFMF.n <= ((1/2) GeoSeq).n by A5,A70,A71; end; then PAbsFMF is summable & Sum(PAbsFMF) <= Sum((1/2) GeoSeq) by A69,SERIES_1:20; then Partial_Sums(PAbsFMF) is convergent by SERIES_1:def 2; then Partial_Sums(PAbsFMF) is bounded; then consider Br be Real such that A72: for n be Nat holds Partial_Sums(PAbsFMF).n < Br by SEQ_2:def 3; for n being Nat holds Ir.n < (RF0 to_power (1/k) + Br) to_power k proof let n being Nat; A73: n in NAT by ORDINAL1:def 12; (Ir.n) to_power (1/k) <= QAbsFMF.n by A48; then A74: (Ir.n) to_power (1/k) <= RF0 to_power (1/k) + (Partial_Sums PAbsFMF).n by A47,A73; RF0 to_power (1/k) + (Partial_Sums PAbsFMF).n < RF0 to_power (1/k) + Br by A72,XREAL_1:8; then A75: (Ir.n) to_power (1/k) < RF0 to_power (1/k) + Br by A74,XXREAL_0:2; Ir.n = Integral(M,Gp.n) by A38; then Ir.n = Integral(M,(G.n) to_power k) by A23; then A76:Ir.n = Integral(M,abs(G.n) to_power k) by A17; A77: G.n in Lp_Functions(M,k) by A17; then 0 <= (Ir.n) to_power (1/k) by Th49,A76,Th4; then ((Ir.n) to_power (1/k)) to_power k < (RF0 to_power (1/k) + Br) to_power k by A75,Th3; then (Ir.n) to_power ((1/k)*k) < (RF0 to_power (1/k) + Br) to_power k by A77,Th49,A76,HOLDER_1:2; then (Ir.n) to_power 1 < (RF0 to_power (1/k) + Br) to_power k by XCMPLX_1:106; hence thesis by POWER:25; end; then A78:Ir is bounded_above by SEQ_2:def 3; for n,m be Nat st n <=m holds Ir.n <= Ir.m proof let n,m be Nat; assume n <=m; then A79: for x be Element of X st x in E holds (ExtGp.n).x <= (ExtGp.m).x by A28; A80: ExtGp.n is E-measurable & ExtGp.m is E-measurable & ExtGp.n is nonnegative & ExtGp.m is nonnegative by A26; A81: dom(ExtGp.n) = E & dom(ExtGp.m) = E by A26; then A82: (ExtGp.n)|E = ExtGp.n & (ExtGp.m)|E = ExtGp.m by RELAT_1:68; I.n = Integral(M,ExtGp.n) & I.m = Integral(M,ExtGp.m) by A38; hence thesis by A79,A81,A80,A82,MESFUNC9:15; end; then Ir is non-decreasing by SEQM_3:6; then A83:I is convergent_to_finite_number & lim I = lim Ir by A78,RINFSUP2:14; reconsider LExtGp = lim ExtGp as PartFunc of X,ExtREAL; A84:E = dom LExtGp & LExtGp is E-measurable by A26,A27,A37,MESFUNC8:25,def 9; A85:for x be object st x in dom LExtGp holds 0 <= LExtGp.x proof let x be object; assume A86: x in dom LExtGp; then reconsider x1 = x as Element of X; A87: x1 in E by A27,A86,MESFUNC8:def 9; now let k1 being Nat; reconsider k=k1 as Nat; ExtGp#x1 is non-decreasing by A35,A87; then A88: (ExtGp#x1).0 <= (ExtGp#x1).k by RINFSUP2:7; 0 <= (ExtGp.0).x1 by A27,SUPINF_2:39; hence 0 <= (ExtGp#x1).k1 by A88,MESFUNC5:def 13; end; then 0 <= lim (ExtGp#x1) by A87,A37,MESFUNC9:10; hence thesis by A86,MESFUNC8:def 9; end; A89:eq_dom(LExtGp,+infty) = E /\ eq_dom(LExtGp,+infty) by A84,RELAT_1:132,XBOOLE_1:28; then reconsider EE=eq_dom(LExtGp,+infty) as Element of S by A84,MESFUNC1:33; reconsider E0= E \ EE as Element of S; E0` = (X \ E) \/ (X /\ EE) by XBOOLE_1:52; then A90:E0` = E` \/ EE by XBOOLE_1:28; M.EE = 0 by A38,A83,A84,A85,A89,MESFUNC9:13,SUPINF_2:52; then A91:EE is measure_zero of M by MEASURE1:def 7; E` is Element of S by MEASURE1:34; then E` is measure_zero of M by A4,MEASURE1:def 7; then E0` is measure_zero of M by A90,A91,MEASURE1:37; then A92:M.E0` = 0 by MEASURE1:def 7; A93:for x be Element of X st x in E0 holds LExtGp.x in REAL proof let x be Element of X; assume x in E0; then x in E & not x in EE by XBOOLE_0:def 5; then LExtGp.x <> +infty & 0<= LExtGp.x by A84,A85,MESFUNC1:def 15; hence LExtGp.x in REAL by XXREAL_0:14; end; A94:for x be Element of X st x in E0 holds Gp#x is convergent & lim (Gp#x)= lim (ExtGp#x) proof let x be Element of X; assume A95: x in E0; then A96: x in E by XBOOLE_0:def 5; then LExtGp.x = lim((ExtGp)#x) by A84,MESFUNC8:def 9; then A97: lim((ExtGp)#x) in REAL by A93,A95; (ExtGp)#x is convergent by A37,A96; then A98: ex g be Real st lim((ExtGp)#x) = g & (for p be Real st 0

0; then consider m be Nat such that A177: n=m+1 by NAT_1:6; reconsider m as Nat; (F1#x).(m+1) = (F1#x).0 + (Partial_Sums(FMF#x)).m by A119,A171; then A178: |.(F1#x).(m+1) qua Complex.| to_power k <= (Gp#x).m by A165,A171; x in E by A171,XBOOLE_0:def 5; then A179: ExtGp#x is non-decreasing by A35; A180: ((ExtGp)#x).m <= ((ExtGp)#x).(m+1) by A179; ExtGp#x = Gp#x by MESFUN7C:1; hence |.((F2#x).n) qua Complex.| to_power k <= (Gp#x).n by A172,A177,A178,A180, XXREAL_0:2; end; end; A181:for x be Element of X st x in E0 holds |.((abs F) to_power k).x qua Complex .| <= gp.x proof let x be Element of X; assume A182: x in E0; then A183: Gp#x is convergent by A94; deffunc ABSF2(set) = (abs(F2#x).$1 ) to_power k; consider s be Real_Sequence such that A184: for n be Nat holds s.n=ABSF2(n) from SEQ_1:sch 1; A185: gp.x = lim (Gp#x) by A152,A182; A186: ((abs F) to_power k).x = ((abs F).x) to_power k by A159,A182, MESFUN6C:def 4 .= (|.F.x qua Complex.|) to_power k by A158,A182,VALUED_1:def 11 .= |.lim (F2#x) qua Complex.| to_power k by A182,A147 .= (lim (abs (F2#x))) to_power k by A134,A182,SEQ_4:14; A187: now let n be Nat; 0 <= |.(F2#x).n.| by COMPLEX1:46; hence 0 <=(abs(F2#x)).n by VALUED_1:18; end; abs (F2#x) is convergent by A182,A134,SEQ_4:13; then A188: s is convergent & (lim (abs (F2#x))) to_power k = lim s by A187,A184,HOLDER_1:10; now let n be Nat; |.(F2#x).n qua Complex.| to_power k <= (Gp#x).n by A170,A182; then (abs(F2#x).n) to_power k <= (Gp#x).n by VALUED_1:18; hence s.n <=(Gp#x).n by A184; end; then A189: ((abs F) to_power k).x <= gp.x by A188,A185,A186,A183,SEQ_2:18; 0 <= ((abs F) to_power k).x by MESFUNC6:51; hence |.((abs F) to_power k).x qua Complex.| <= gp.x by A189,ABSVALUE:def 1; end; R_EAL F is E0-measurable by A138,A156,A134,MESFUN7C:21; then A190:F is E0-measurable; then A191:(abs F) is E0-measurable by A157,MESFUNC6:48; dom abs F = E0 by A157,VALUED_1:def 11; then (abs F) to_power k is E0-measurable by A191,MESFUN6C:29; then (abs F) to_power k is_integrable_on M by A150,A155,A159,A181,MESFUNC6:96; then A192:F in Lp_Functions(M,k) by A92,A157,A190; A193:for x be Element of X, n,m be Nat st x in E0 & m <= n holds |. (F1#x).n -(F1#x).m qua Complex.| to_power k <= (Gp#x).n proof let x be Element of X, n1,m1 be Nat; assume A194: x in E0 & m1 <= n1; now per cases; suppose A195: m1= 0; now per cases; suppose A196: n1=0; ((G.n1) to_power k) is nonnegative by A24; then Gp.n1 is nonnegative by A23; then 0 <= (Gp.n1).x by MESFUNC6:51; then 0 <= (Gp#x).n1 by SEQFUNC:def 10; hence |. (F1#x).n1-(F1#x).m1 qua Complex .| to_power k <= (Gp#x).n1 by A195,A196,COMPLEX1:44,POWER:def 2; end; suppose n1<> 0; then consider n be Nat such that A197: n1=n+1 by NAT_1:6; reconsider n as Nat; A198: (F1#x).(n+1) = (F1#x).0 + (Partial_Sums (FMF#x)).n by A194,A119; A199: |.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.| <= (G#x).n by A160 ,A194; 0 <= |.(F1#x).0 .| by COMPLEX1:46; then |.(Partial_Sums (FMF#x)).n qua Complex.| + 0 <= |.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.| by XREAL_1:6; then A200: |.(Partial_Sums (FMF#x)).n qua Complex.| <= (G#x).n by A199,XXREAL_0:2; 0 <= |.(Partial_Sums (FMF#x)).n.| by COMPLEX1:46; then A201: |. (Partial_Sums(FMF#x)).n qua Complex .| to_power k <= ((G#x).n) to_power k by A200,HOLDER_1:3; A202: (Gp#x).n = (((G#x)).n) to_power k by A194,A99; x in E by A194,XBOOLE_0:def 5; then A203: ExtGp#x is non-decreasing by A35; A204: ((ExtGp)#x).n <= ((ExtGp)#x).(n+1) by A203; ExtGp#x = Gp#x by MESFUN7C:1; hence |. (F1#x).n1 -(F1#x).m1 qua Complex .| to_power k <= (Gp#x).n1 by A195,A197,A204,A201,A202,A198,XXREAL_0:2; end; end; hence |. (F1#x).n1-(F1#x).m1 qua Complex .| to_power k <= (Gp#x).n1; end; suppose A205: m1<> 0; then consider m be Nat such that A206: m1=m+1 by NAT_1:6; reconsider m as Nat; 0 < n1 by A194,A205; then consider n be Nat such that A207: n1=n+1 by NAT_1:6; reconsider n as Element of NAT by ORDINAL1:def 12; A208: m1-1 <= n1-1 by A194,XREAL_1:9; x in E by A194,XBOOLE_0:def 5; then A209: x in dom(G.n) by A17; then A210: x in dom ((G.n) to_power k) by MESFUN6C:def 4; (Gp#x).n = (Gp.n).x by SEQFUNC:def 10; then (Gp#x).n = ((G.n) to_power k).x by A23; then A211: (Gp#x).n = ((G.n).x) to_power k by A210,MESFUN6C:def 4; G.n = abs(F1.0) + (Partial_Sums AbsFMF).n by A16; then (G.n).x = abs(F1.0).x + ((Partial_Sums AbsFMF).n).x by A209,VALUED_1:def 1 .= |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF).n).x by VALUED_1:18; then A212 : (G.n).x = |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF)#x).n by SEQFUNC:def 10; A213: (F1#x).(n+1) = (F1#x).0 + (Partial_Sums (FMF#x)).n & (F1#x).(m+1) = (F1#x).0 + (Partial_Sums (FMF#x)).m by A194,A119; A214: |. (Partial_Sums (FMF#x)).n - (Partial_Sums (FMF#x)).m .| <= (Partial_Sums abs(FMF#x)).n by Th10,A206,A207,A208; A215: (Partial_Sums abs(FMF#x)).n = ((Partial_Sums AbsFMF)#x).n by A111,A194 ; 0 <= |.(F1.0).x.| by COMPLEX1:46; then 0 + (Partial_Sums abs(FMF#x)).n <= |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF)#x).n by A215,XREAL_1:6; then A216: |. (F1#x).(n+1)-(F1#x).(m+1) .| <= (G.n).x by A212,A213,A214,XXREAL_0:2 ; 0 <= |. (F1#x).(n+1)-(F1#x).(m+1) .| by COMPLEX1:46; then A217: (|. (F1#x).(n+1)-(F1#x).(m+1) qua Complex .|) to_power k <= (Gp#x).n by A211,A216,HOLDER_1:3; x in E by A194,XBOOLE_0:def 5; then A218: ExtGp#x is non-decreasing by A35; A219: ((ExtGp)#x).n <= ((ExtGp)#x).(n+1) by A218; ExtGp#x = Gp#x by MESFUN7C:1; hence (|. (F1#x).(n1)-(F1#x).(m1) qua Complex .|) to_power k <= (Gp#x).n1 by A206,A207,A219,A217,XXREAL_0:2; end; end; hence thesis; end; A220:for x be Element of X, n be Nat st x in E0 holds |. F.x -(F2#x).n qua Complex .| to_power k <= gp.x proof let x be Element of X, n1 be Nat; assume A221: x in E0; then A222: Gp#x is convergent by A94; A223: F1#x = F2#x by A136,A221; A224: F2#x is convergent by A221,A134; reconsider n=n1 as Nat; deffunc AF2F20(Nat) = (F2#x).$1 -(F2#x).n; consider s0 be Real_Sequence such that A225: for j be Nat holds s0.j=AF2F20(j) from SEQ_1:sch 1; A226: now let p be Real; assume 0

= 0 proof let n; ||. Sq0-Sq.(N.n) .|| to_power k >= 0 by Th4; hence Ip.n >= 0 by A260; end; A267: for n be Nat holds Iq.n = (Ip.n) to_power (1/k) proof let n be Nat; thus (Ip.n) to_power (1/k) = ( ||.Sq0-Sq.(N.n).|| to_power k) to_power (1/k) by A260 .= ||.Sq0-Sq.(N.n).|| to_power (k*(1/k)) by HOLDER_1:2 .= (||.Sq0-Sq.(N.n).||) to_power 1 by XCMPLX_1:106 .= ||.Sq0-Sq.(N.n).|| by POWER:25 .= Iq.n by A265; end; hence Iq is convergent by A266,A252,A251,HOLDER_1:10; lim Iq = (lim Ip) to_power (1/k) by A252,A251,A266,A267,HOLDER_1:10; then lim Iq = 0 to_power (1/k) by A252,A251,A257,A242,LPSPACE1:22; hence lim Iq = 0 by POWER:def 2; end; hence thesis by A2,A265,Lm7; end; registration let X,S,M; let k be geq_than_1 Real; cluster Lp-Space (M,k) -> complete; coherence proof for Sq be sequence of Lp-Space(M,k) st Sq is Cauchy_sequence_by_Norm holds Sq is convergent by Th70; hence thesis by LOPBAN_1:def 15; end; end; begin :: Relations between L1 Space and Lp Space Lm8: f in L1_Functions M implies f is_integrable_on M & (ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable) proof assume f in L1_Functions M; then ex f2 be PartFunc of X,REAL st f = f2 & ex E be Element of S st M.E=0 & dom f2 = E` & f2 is_integrable_on M; then consider D be Element of S such that A1: M.D = 0 & dom f = D` & f is_integrable_on M; thus f is_integrable_on M by A1; reconsider E=D` as Element of S by MEASURE1:34; take E; thus M.E` = 0 & dom f = E by A1; R_EAL f is_integrable_on M by A1; then ex B be Element of S st B = dom (R_EAL f) & (R_EAL f) is B-measurable; hence f is E-measurable by A1; end; Lm9: f in Lp_Functions(M,k) implies (abs f) to_power k is_integrable_on M proof assume f in Lp_Functions(M,k); then ex f2 be PartFunc of X,REAL st f = f2 & ex E be Element of S st M.E` = 0 & dom f2 = E & f2 is E-measurable & (abs f2) to_power k is_integrable_on M; hence thesis; end; Lm10: (ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable) implies a.e-eq-class_Lp(f,M,1) c= a.e-eq-class(f,M) proof assume A1: ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable; let x be object; assume x in a.e-eq-class_Lp(f,M,1); then consider h be PartFunc of X,REAL such that A2: x = h & h in Lp_Functions(M,1) & f a.e.= h,M; A3: ex g be PartFunc of X,REAL st h = g & (ex E be Element of S st M.E`=0 & dom g = E & g is E-measurable & (abs g) to_power 1 is_integrable_on M) by A2; then consider Eh be Element of S such that A4: M.(Eh`) = 0 & dom h = Eh & h is Eh-measurable & (abs h) to_power 1 is_integrable_on M; A5: dom((abs h) to_power 1) = dom(abs h) by MESFUN6C:def 4; for x be Element of X st x in dom((abs h) to_power 1) holds ((abs h) to_power 1).x = (abs h).x proof let x be Element of X; assume x in dom((abs h) to_power 1); then ((abs h) to_power 1).x = ((abs h).x) to_power 1 by MESFUN6C:def 4; hence thesis by POWER:25; end; then (abs h) to_power 1 = abs h by A5,PARTFUN1:5; then A6: h is_integrable_on M by A3,MESFUNC6:94; reconsider ND = Eh` as Element of S by MEASURE1:34; M.ND = 0 & dom h = ND` by A4; then A7: h in L1_Functions M by A6; ex E be Element of S st M.E = 0 & dom f = E` & f is_integrable_on M proof consider Ef be Element of S such that A8: M.(Ef`)=0 & Ef = dom f & f is Ef-measurable by A1; reconsider E = Ef` as Element of S by MEASURE1:34; take E; consider EE be Element of S such that A9: M.EE = 0 & f|EE` = h|EE` by A2; reconsider E1 = ND \/ EE as Element of S; ND is measure_zero of M & EE is measure_zero of M by A4,A9,MEASURE1:def 7; then E1 is measure_zero of M by MEASURE1:37; then A10: M.E1 = 0 by MEASURE1:def 7; EE c= E1 by XBOOLE_1:7; then E1` c= EE` by SUBSET_1:12; then A11: f|E1` = (f|EE`)|E1` & h|E1` = (h|EE`)|E1` by FUNCT_1:51; A12: dom max+(R_EAL f) = Ef & dom max-(R_EAL f) = Ef by A8,MESFUNC2:def 2,def 3; A13: Ef = dom(R_EAL f) & (R_EAL f) is Ef-measurable by A8; then A14: max+(R_EAL f) is Ef-measurable & max-(R_EAL f) is Ef-measurable by MESFUNC2:25,26; (for x being Element of X holds 0. <= (max+(R_EAL f)).x) & (for x being Element of X holds 0. <= (max-(R_EAL f)).x) by MESFUNC2:12,13; then A15: max+(R_EAL f) is nonnegative & max-(R_EAL f) is nonnegative by SUPINF_2:39; A16: Ef = (Ef /\ E1) \/ (Ef \ E1) by XBOOLE_1:51; reconsider E0 = Ef /\ E1 as Element of S; A17: Ef \ E1 = Ef /\ E1` by SUBSET_1:13; reconsider E2 = Ef \ E1 as Element of S; max+(R_EAL f) = (max+(R_EAL f))|(dom(max+(R_EAL f))) & max-(R_EAL f) = (max-(R_EAL f))|(dom(max-(R_EAL f))) by RELAT_1:69; then A18: integral+(M,max+(R_EAL f)) = integral+(M,(max+(R_EAL f))|E0) + integral+(M,(max+(R_EAL f))|E2) & integral+(M,max-(R_EAL f)) = integral+(M,(max-(R_EAL f))|E0) + integral+(M,(max-(R_EAL f))|E2) by A12,A15,A16,A14,MESFUNC5:81,XBOOLE_1:89; A19: integral+(M,(max+(R_EAL f))|E0) >= 0 & integral+(M,(max-(R_EAL f))|E0) >= 0 by A15,A14,A12,MESFUNC5:80; integral+(M,(max+(R_EAL f))|E1) = 0 & integral+(M,(max-(R_EAL f))|E1) = 0 by A10,A12,A15,A14,MESFUNC5:82; then integral+(M,(max+(R_EAL f))|E0) = 0 & integral+(M,(max-(R_EAL f))|E0) = 0 by A19,A12,A15,A14,MESFUNC5:83,XBOOLE_1:17; then A20: integral+(M,max+(R_EAL f)) = integral+(M,(max+(R_EAL f))|E2) & integral+(M,max-(R_EAL f)) = integral+(M,(max-(R_EAL f))|E2) by A18,XXREAL_3:4; A21: E2 c= E1` by A17,XBOOLE_1:17; then f|E2 = (h|E1`)|E2 by A9,A11,FUNCT_1:51; then A22: (R_EAL f)|E2 = (R_EAL h)|E2 by A21,FUNCT_1:51; A23: max+(R_EAL f)|E2 = max+((R_EAL f)|E2) & max+(R_EAL h)|E2 = max+((R_EAL h)|E2) & max-(R_EAL f)|E2 = max-((R_EAL f)|E2) & max-(R_EAL h)|E2 = max-((R_EAL h)|E2) by MESFUNC5:28; A24: R_EAL h is_integrable_on M by A6; then A25: integral+(M,max+(R_EAL h)) < +infty & integral+(M,max-(R_EAL h)) < +infty; integral+(M,max+((R_EAL h)|E2)) <= integral+(M,max+(R_EAL h)) & integral+(M,max-((R_EAL h)|E2)) <= integral+(M,max-(R_EAL h)) by A24,MESFUNC5:97; then integral+(M,max+(R_EAL f)) < +infty & integral+(M,max-(R_EAL f)) < +infty by A20,A25,A23,A22,XXREAL_0:2; then (R_EAL f) is_integrable_on M by A13; hence thesis by A8; end; then f in L1_Functions M; hence x in a.e-eq-class(f,M) by A2,A7; end; Lm11: a.e-eq-class(f,M) c= a.e-eq-class_Lp(f,M,1) proof let x be object; assume x in a.e-eq-class(f,M); then consider g be PartFunc of X,REAL such that A1: x = g & g in L1_Functions M & f in L1_Functions M & f a.e.= g,M; A2: ex h be PartFunc of X,REAL st g = h & ex D be Element of S st M.D=0 & dom h = D` & h is_integrable_on M by A1; then R_EAL g is_integrable_on M; then consider A be Element of S such that A3: A = dom(R_EAL g) & R_EAL g is A-measurable; A4: A = dom g & g is A-measurable by A3; A5: M.A` = 0 by A2,A3; (abs g) to_power 1 = abs g by Th8; then (abs g) to_power 1 is_integrable_on M by A2,A4,MESFUNC6:94; then g in {p where p is PartFunc of X,REAL : ex Ep be Element of S st M.(Ep`)=0 & dom p = Ep & p is Ep-measurable & (abs p) to_power 1 is_integrable_on M} by A4,A5; hence x in a.e-eq-class_Lp(f,M,1) by A1; end; Lm12: (ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable) implies a.e-eq-class_Lp(f,M,1) = a.e-eq-class(f,M) by Lm10,Lm11; theorem Th71: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds CosetSet M = CosetSet(M,1) proof let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; now let x be object; assume x in CosetSet M; then consider g be PartFunc of X,REAL such that A1: x = a.e-eq-class(g,M) & g in L1_Functions M; A2: g is_integrable_on M & ex E be Element of S st M.E`=0 & E = dom g & g is E-measurable by A1,Lm8; then A3: x = a.e-eq-class_Lp(g,M,1) by A1,Lm12; (abs g) to_power 1 = abs g by Th8; then (abs g) to_power 1 is_integrable_on M by A2,MESFUNC6:94; then g in Lp_Functions(M,1) by A2; hence x in CosetSet(M,1) by A3; end; then A4:CosetSet M c= CosetSet(M,1); now let x be object; assume x in CosetSet(M,1); then consider g be PartFunc of X,REAL such that A5: x = a.e-eq-class_Lp(g,M,1) & g in Lp_Functions(M,1); consider E be Element of S such that A6: M.E` = 0 & dom g = E & g is E-measurable by A5,Th35; A7: x = a.e-eq-class(g,M) by A5,A6,Lm12; reconsider D = E` as Element of S by MEASURE1:34; A8: M.D = 0 & dom g = D` by A6; (abs g) to_power 1 is_integrable_on M by A5,Lm9; then abs g is_integrable_on M by Th8; then g is_integrable_on M by A6,MESFUNC6:94; then g in L1_Functions M by A8; hence x in CosetSet M by A7; end; then CosetSet(M,1) c= CosetSet M; hence thesis by A4; end; theorem Th72: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds addCoset M = addCoset(M,1) proof let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; A1:CosetSet M = CosetSet(M,1) by Th71; now let A,B be Element of CosetSet M; A in {a.e-eq-class(f,M) where f is PartFunc of X,REAL : f in L1_Functions M}; then consider a be PartFunc of X,REAL such that A2: A = a.e-eq-class(a,M) & a in L1_Functions M; B in {a.e-eq-class(f,M) where f is PartFunc of X,REAL : f in L1_Functions M}; then consider b be PartFunc of X,REAL such that A3: B = a.e-eq-class(b,M) & b in L1_Functions M; A4: A is Element of CosetSet(M,1) & B is Element of CosetSet(M,1) by Th71; A5: a in a.e-eq-class(a,M) & b in a.e-eq-class(b,M) by A2,A3,LPSPACE1:38; then A6: (addCoset M).(A,B) = a.e-eq-class(a+b,M) by A2,A3,LPSPACE1:def 15; a+b in L1_Functions M by A2,A3,LPSPACE1:23; then ex E be Element of S st M.E`=0 & E = dom(a+b) & (a+b) is E-measurable by Lm8; then (addCoset M).(A,B) = a.e-eq-class_Lp(a+b,M,1) by A6,Lm12; hence (addCoset M).(A,B) = (addCoset(M,1)).(A,B) by A4,A5,A2,A3,Def8; end; hence addCoset M = addCoset(M,1) by A1,BINOP_1:2; end; theorem Th73: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds zeroCoset M = zeroCoset(M,1) proof let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; reconsider z = zeroCoset(M,1) as Element of CosetSet M by Th71; X-->0 in Lp_Functions(M,1) by Th23; then ex E be Element of S st M.E`=0 & dom (X-->0) = E & (X-->0) is E-measurable by Th35; then A1:z = a.e-eq-class(X-->0,M) by Lm12; X-->0 in L1_Functions M by Th56; hence thesis by A1,LPSPACE1:def 16; end; theorem Th74: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds lmultCoset M = lmultCoset(M,1) proof let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; A1:CosetSet M = CosetSet(M,1) by Th71; now let z be Element of REAL, A be Element of CosetSet M; A in {a.e-eq-class(f,M) where f is PartFunc of X,REAL : f in L1_Functions M}; then consider a be PartFunc of X,REAL such that A2: A = a.e-eq-class(a,M) & a in L1_Functions M; A3: A is Element of CosetSet(M,1) by Th71; A4: a in A by A2,LPSPACE1:38; then A5: (lmultCoset M).(z,A) = a.e-eq-class(z(#)a,M) by LPSPACE1:def 17; z(#)a in L1_Functions M by A2,LPSPACE1:24; then ex E be Element of S st M.E`=0 & E = dom(z(#)a) & (z(#)a) is E-measurable by Lm8; then (lmultCoset M).(z,A) = a.e-eq-class_Lp(z(#)a,M,1) by A5,Lm12; hence (lmultCoset M).(z,A) = (lmultCoset(M,1)).(z,A) by A3,A4,Def10; end; hence lmultCoset M = lmultCoset(M,1) by A1,BINOP_1:2; end; theorem Th75: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds Pre-L-Space M = Pre-Lp-Space(M,1) proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; A1:the carrier of Pre-L-Space M = CosetSet M & the addF of Pre-L-Space M = addCoset M & 0.(Pre-L-Space M) = zeroCoset M & the Mult of Pre-L-Space M = lmultCoset M by LPSPACE1:def 18; CosetSet M = CosetSet(M,1) & addCoset M = addCoset(M,1) & zeroCoset M = zeroCoset(M,1) & lmultCoset M = lmultCoset(M,1) by Th71,Th72,Th73,Th74; hence thesis by A1,Def11; end; theorem Th76: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds L-1-Norm M = Lp-Norm(M,1) proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; A1:the carrier of Pre-L-Space M = the carrier of Pre-Lp-Space(M,1) by Th75; now let x be Element of the carrier of Pre-L-Space M; x in the carrier of Pre-L-Space M; then x in CosetSet M by LPSPACE1:def 18; then consider g be PartFunc of X,REAL such that A2: x = a.e-eq-class(g,M) & g in L1_Functions M; consider a be PartFunc of X,REAL such that A3: a in x & (L-1-Norm M).x = Integral(M,|.a.|) by LPSPACE1:def 19; A4: ex p be PartFunc of X,REAL st a = p & p in L1_Functions M & g in L1_Functions M & g a.e.= p,M by A2,A3; consider b be PartFunc of X,REAL such that A5: b in x & ex r be Real st r = Integral(M,(|.b.|) to_power 1) & (Lp-Norm(M,1)).x = r to_power (1/1) by A1,Def12; A6: ex q be PartFunc of X,REAL st b = q & q in L1_Functions M & g in L1_Functions M & g a.e.= q,M by A2,A5; a a.e.= g,M by A4; then a a.e.= b,M by A6,LPSPACE1:30; then A7: Integral(M,|.a.|) = Integral(M,|.b.|) by A2,A3,A5,LPSPACE1:45; (|.b.|) to_power 1 = |.b.| by Th8; hence (L-1-Norm M).x = (Lp-Norm(M,1)).x by A3,A5,A7,POWER:25; end; hence thesis by A1,FUNCT_2:63; end; theorem for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds L-1-Space M = Lp-Space(M,1) proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; Pre-L-Space M = Pre-Lp-Space(M,1) by Th75; hence thesis by Th76; end;