let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for k being geq_than_1 Real
for Sq being sequence of (Lp-Space M,k) st Sq is CCauchy holds
Sq is convergent
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for k being geq_than_1 Real
for Sq being sequence of (Lp-Space M,k) st Sq is CCauchy holds
Sq is convergent
let M be sigma_Measure of S; :: thesis: for k being geq_than_1 Real
for Sq being sequence of (Lp-Space M,k) st Sq is CCauchy holds
Sq is convergent
let k be geq_than_1 Real; :: thesis: for Sq being sequence of (Lp-Space M,k) st Sq is CCauchy holds
Sq is convergent
let Sq be sequence of (Lp-Space M,k); :: thesis: ( Sq is CCauchy implies Sq is convergent )
AKS: 1 <= k by defH;
assume A1: Sq is CCauchy ; :: thesis: Sq is convergent
consider Fsq being with_the_same_dom Functional_Sequence of X,REAL such that
A2: for n being Element of 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 being Real st
( 0 <= r & r = Integral M,((abs (Fsq . n)) to_power k) & ||.(Sq . n).|| = r to_power (1 / k) ) ) by Th004;
Fsq . 0 in Lp_Functions M,k by A2;
then A3: ex D being Element of S st
( M . (D ` ) = 0 & dom (Fsq . 0 ) = D & Fsq . 0 is_measurable_on D ) by EQC00a;
then reconsider E = dom (Fsq . 0 ) as Element of S ;
consider N being V161() sequence of NAT such that
A4: for i, j being Element of NAT st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i) by Th005, A1;
deffunc H₁( Nat) -> Element of bool [:X,REAL :] = Fsq . (N . $1);
consider F1 being Functional_Sequence of X,REAL such that
A5: for n being Nat holds F1 . n = H₁(n) from SEQFUNC:sch 1();
A6: for n being natural number holds
( dom (F1 . n) = E & F1 . n in Lp_Functions M,k & F1 . n is_measurable_on E & abs (F1 . n) in Lp_Functions M,k )

proof

let n be natural number ; :: thesis: ( dom (F1 . n) = E & F1 . n in Lp_Functions M,k & F1 . n is_measurable_on E & abs (F1 . n) in Lp_Functions M,k )
E61: F1 . n = Fsq . (N . n) by A5;
hence B2: ( dom (F1 . n) = E & F1 . n in Lp_Functions M,k ) by A2, MESFUNC8:def 2; :: thesis: ( F1 . n is_measurable_on E & abs (F1 . n) in Lp_Functions M,k )
then ex F being PartFunc of X,REAL st
( F1 . n = F & ex ND being Element of S st
( M . (ND ` ) = 0 & dom F = ND & F is_measurable_on ND & (abs F) to_power k is_integrable_on M ) ) ;
hence F1 . n is_measurable_on E by E61, MESFUNC8:def 2; :: thesis: abs (F1 . n) in Lp_Functions M,k
thus abs (F1 . n) in Lp_Functions M,k by B2, Th01dLp; :: thesis: verum

end;

for n, m being natural number holds dom (F1 . n) = dom (F1 . m)

proof

let n, m be natural number ; :: thesis: dom (F1 . n) = dom (F1 . m)
( dom (F1 . n) = E & dom (F1 . m) = E ) by A6;
hence dom (F1 . n) = dom (F1 . m) ; :: thesis: verum

end;

then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
deffunc H₂( Nat) -> Element of bool [:X,REAL :] = (F1 . ($1 + 1)) - (F1 . $1);
consider FMF being Functional_Sequence of X,REAL such that
A7: for n being Nat holds FMF . n = H₂(n) from SEQFUNC:sch 1();
A8: for n being natural number holds
( dom (FMF . n) = E & FMF . n in Lp_Functions M,k )

proof

let n be natural number ; :: thesis: ( dom (FMF . n) = E & FMF . n in Lp_Functions M,k )
B1: ( dom (F1 . n) = E & dom (F1 . (n + 1)) = E ) by A6;
FMF . n = (F1 . (n + 1)) - (F1 . n) by A7;
then dom (FMF . n) = (dom (F1 . (n + 1))) /\ (dom (F1 . n)) by VALUED_1:12;
hence dom (FMF . n) = E by B1; :: thesis: FMF . n in Lp_Functions M,k
( Fsq . (N . (n + 1)) in Lp_Functions M,k & Fsq . (N . n) in Lp_Functions M,k ) by A2;
then ( F1 . (n + 1) in Lp_Functions M,k & F1 . n in Lp_Functions M,k ) by A5;
then (F1 . (n + 1)) - (F1 . n) in Lp_Functions M,k by Th01cLp;
hence FMF . n in Lp_Functions M,k by A7; :: thesis: verum

end;

for n, m being natural number holds dom (FMF . n) = dom (FMF . m)

proof

let n, m be natural number ; :: thesis: dom (FMF . n) = dom (FMF . m)
( dom (FMF . n) = E & dom (FMF . m) = E ) by A8;
hence dom (FMF . n) = dom (FMF . m) ; :: thesis: verum

end;

then reconsider FMF = FMF as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
set AbsFMF = abs FMF;
reconsider ExtAbsFMF = R_EAL (abs FMF) as Functional_Sequence of X,ExtREAL ;
A9: for n being natural number holds
( (abs FMF) . n is nonnegative & dom ((abs FMF) . n) = E & abs ((abs FMF) . n) = (abs FMF) . n & (abs FMF) . n in Lp_Functions M,k & (abs FMF) . n is_measurable_on E )

proof

let n be natural number ; :: thesis: ( (abs FMF) . n is nonnegative & dom ((abs FMF) . n) = E & abs ((abs FMF) . n) = (abs FMF) . n & (abs FMF) . n in Lp_Functions M,k & (abs FMF) . n is_measurable_on E )
PQ: (abs FMF) . n = abs (FMF . n) by SEQFUNC:def 5;
hence (abs FMF) . n is nonnegative ; :: thesis: ( dom ((abs FMF) . n) = E & abs ((abs FMF) . n) = (abs FMF) . n & (abs FMF) . n in Lp_Functions M,k & (abs FMF) . n is_measurable_on E )
PP: ( dom (FMF . n) = E & FMF . n in Lp_Functions M,k ) by A8;
hence ( dom ((abs FMF) . n) = E & abs ((abs FMF) . n) = (abs FMF) . n ) by PQ, VALUED_1:def 11; :: thesis: ( (abs FMF) . n in Lp_Functions M,k & (abs FMF) . n is_measurable_on E )
thus (abs FMF) . n in Lp_Functions M,k by A8, PQ, Th01dLp; :: thesis: (abs FMF) . n is_measurable_on E
then ex D being Element of S st
( M . (D ` ) = 0 & dom ((abs FMF) . n) = D & (abs FMF) . n is_measurable_on D ) by EQC00a;
hence (abs FMF) . n is_measurable_on E by PP, PQ, VALUED_1:def 11; :: thesis: verum

end;

reconsider AbsFMF = abs FMF as with_the_same_dom Functional_Sequence of X,REAL by C938;
deffunc H₃( Nat) -> Element of bool [:X,REAL :] = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . $1);
consider G being Functional_Sequence of X,REAL such that
A10: for n being Nat holds G . n = H₃(n) from SEQFUNC:sch 1();
A11: for n being natural number holds
( dom (G . n) = E & G . n in Lp_Functions M,k & G . n is nonnegative & G . n is_measurable_on E & abs (G . n) = G . n )

proof

let n be natural number ; :: thesis: ( dom (G . n) = E & G . n in Lp_Functions M,k & G . n is nonnegative & G . n is_measurable_on E & abs (G . n) = G . n )
H2: G . n = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . n) by A10;
then P0: 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 ;
P1: ( (Partial_Sums AbsFMF) . n in Lp_Functions M,k & (Partial_Sums AbsFMF) . n is nonnegative & (Partial_Sums AbsFMF) . n is_measurable_on E ) by A9, C935, C936, MESFUN9C:16;
T1: dom (AbsFMF . 0 ) = E by A9;
P2: ( F1 . 0 in Lp_Functions M,k & dom (F1 . 0 ) = E & F1 . 0 is_measurable_on E ) by A6;
then ( abs (F1 . 0 ) in Lp_Functions M,k & abs (F1 . 0 ) is nonnegative & abs (F1 . 0 ) is_measurable_on E ) by Th01dLp, MESFUNC6:48;
hence ( dom (G . n) = E & G . n in Lp_Functions M,k & G . n is nonnegative & G . n is_measurable_on E & abs (G . n) = G . n ) by P0, P2, T1, H2, P1, Lm002b, Th01aLp, MESFUNC6:26, MESFUNC6:56; :: thesis: verum

end;

deffunc H₄( Nat) -> Element of bool [:X,REAL :] = (G . $1) to_power k;
consider Gp being Functional_Sequence of X,REAL such that
A12: for n being Nat holds Gp . n = H₄(n) from SEQFUNC:sch 1();
A13: for n being Nat holds
( (G . n) to_power k is nonnegative & (G . n) to_power k is_measurable_on E )

proof

let n be Nat; :: thesis: ( (G . n) to_power k is nonnegative & (G . n) to_power k is_measurable_on E )
L0: G . n is nonnegative by A11;
hence (G . n) to_power k is nonnegative ; :: thesis: (G . n) to_power k is_measurable_on E
( G . n is_measurable_on E & dom (G . n) = E ) by A11;
hence (G . n) to_power k is_measurable_on E by L0, MESFUN6C:29; :: thesis: verum

end;

reconsider ExtGp = R_EAL Gp as Functional_Sequence of X,ExtREAL ;
A14: for n being natural number holds
( dom (ExtGp . n) = E & ExtGp . n is_measurable_on E & ExtGp . n is nonnegative )

proof

let n be natural number ; :: thesis: ( dom (ExtGp . n) = E & ExtGp . n is_measurable_on E & ExtGp . n is nonnegative )
ExtGp . n = R_EAL ((G . n) to_power k) by A12;
then dom (ExtGp . n) = dom (G . n) by MESFUN6C:def 6;
hence dom (ExtGp . n) = E by A11; :: thesis: ( ExtGp . n is_measurable_on E & ExtGp . n is nonnegative )
(G . n) to_power k is_measurable_on E by A13;
then R_EAL ((G . n) to_power k) is_measurable_on E by MESFUNC6:def 6;
hence ExtGp . n is_measurable_on E by A12; :: thesis: ExtGp . n is nonnegative
(G . n) to_power k is nonnegative by A13;
hence ExtGp . n is nonnegative by A12; :: thesis: verum

end;

then A15: ( dom (ExtGp . 0 ) = E & ExtGp . 0 is nonnegative ) ;
for n, m being natural number holds dom (ExtGp . n) = dom (ExtGp . m)

proof

let n, m be natural number ; :: thesis: dom (ExtGp . n) = dom (ExtGp . m)
( dom (ExtGp . n) = E & dom (ExtGp . m) = E ) by A14;
hence dom (ExtGp . n) = dom (ExtGp . m) ; :: thesis: verum

end;

then reconsider ExtGp = ExtGp as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
A16: for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(ExtGp . n) . x <= (ExtGp . m) . x

proof

let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in E holds
(ExtGp . n) . x <= (ExtGp . m) . x )
assume AS1: n <= m ; :: thesis: for x being Element of X st x in E holds
(ExtGp . n) . x <= (ExtGp . m) . x
let x be Element of X; :: thesis: ( x in E implies (ExtGp . n) . x <= (ExtGp . m) . x )
assume AS2: x in E ; :: thesis: (ExtGp . n) . x <= (ExtGp . m) . x
then B1: ( x in dom (G . n) & x in dom (G . m) ) by A11;
then ( x in dom ((G . n) to_power k) & x in dom ((G . m) to_power k) ) by MESFUN6C:def 6;
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 6;
then B2: ( ((G . n) . x) to_power k = (ExtGp . n) . x & ((G . m) . x) to_power k = (ExtGp . m) . x ) by A12;
dom (AbsFMF . 0 ) = E by A9;
then ((Partial_Sums AbsFMF) . n) . x <= ((Partial_Sums AbsFMF) . m) . x by C937, AS1, AS2, A9;
then B3: ((abs (F1 . 0 )) . x) + (((Partial_Sums AbsFMF) . n) . x) <= ((abs (F1 . 0 )) . x) + (((Partial_Sums AbsFMF) . m) . x) by XREAL_1:8;
( G . m = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . m) & G . n = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . n) ) by A10;
then B4: ( (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 B1, VALUED_1:def 1;
G . n is nonnegative by A11;
then 0 <= (G . n) . x by MESFUNC6:51;
hence (ExtGp . n) . x <= (ExtGp . m) . x by B2, B3, B4, HOLDER_1:3; :: thesis: verum

end;

A17: for x being Element of X st x in E holds
ExtGp # x is V163()

proof

let x be Element of X; :: thesis: ( x in E implies ExtGp # x is V163() )
assume AS: x in E ; :: thesis: ExtGp # x is V163()
for n, m being Element of NAT st m <= n holds
(ExtGp # x) . m <= (ExtGp # x) . n

proof

let n, m be Element of NAT ; :: thesis: ( m <= n implies (ExtGp # x) . m <= (ExtGp # x) . n )
assume m <= n ; :: thesis: (ExtGp # x) . m <= (ExtGp # x) . n
then (ExtGp . m) . x <= (ExtGp . n) . x by A16, AS;
then (ExtGp # x) . m <= (ExtGp . n) . x by MESFUNC5:def 13;
hence (ExtGp # x) . m <= (ExtGp # x) . n by MESFUNC5:def 13; :: thesis: verum

end;

hence ExtGp # x is V163() by RINFSUP2:7; :: thesis: verum

end;

A18: for x being Element of X st x in E holds
ExtGp # x is convergent

proof

let x be Element of X; :: thesis: ( x in E implies ExtGp # x is convergent )
assume x in E ; :: thesis: ExtGp # x is convergent
then ExtGp # x is V163() by A17;
hence ExtGp # x is convergent by RINFSUP2:37; :: thesis: verum

end;

then consider I being ExtREAL_sequence such that
A19: ( ( for n being Nat holds I . n = Integral M,(ExtGp . n) ) & I is convergent & Integral M,(lim ExtGp) = lim I ) by A15, A14, A16, MESFUNC9:52;

now

let y be set ; :: thesis: ( y in rng I implies y in REAL )
assume y in rng I ; :: thesis: y in REAL
then consider x being Element of NAT such that
B1: y = I . x by FUNCT_2:190;
B2: y = Integral M,(Gp . x) by B1, A19;
G . x = abs (G . x) by A11;
then B3: Gp . x = (abs (G . x)) to_power k by A12;
G . x in Lp_Functions M,k by A11;
hence y in REAL by B2, B3, Lm15; :: thesis: verum

end;

then rng I c= REAL by TARSKI:def 3;
then reconsider Ir = I as Function of NAT ,REAL by FUNCT_2:8;
deffunc H₅( Nat) -> Element of ExtREAL = Integral M,((AbsFMF . $1) to_power k);
A20: for x being Element of NAT holds H₅(x) is Element of REAL

proof

let x be Element of NAT ; :: thesis: H₅(x) is Element of REAL
AbsFMF . x in Lp_Functions M,k by A9;
then Integral M,((abs (AbsFMF . x)) to_power k) in REAL by Lm15;
hence H₅(x) is Element of REAL by A9; :: thesis: verum

end;

consider KPAbsFMF being Function of NAT ,REAL such that
A21: for x being Element of NAT holds KPAbsFMF . x = H₅(x) from FUNCT_2:sch 9(A20);
deffunc H₆( Nat) -> Element of REAL = (KPAbsFMF . $1) to_power (1 / k);
A22: for x being Element of NAT holds H₆(x) is Element of REAL ;
consider PAbsFMF being Function of NAT ,REAL such that
A23: for x being Element of NAT holds PAbsFMF . x = H₆(x) from FUNCT_2:sch 9(A22);
F1 . 0 in Lp_Functions M,k by A6;
then reconsider RF0 = Integral M,((abs (F1 . 0 )) to_power k) as Element of REAL by Lm15;
deffunc H₇( Element of NAT ) -> Element of REAL = (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . $1);
A24: for x being Element of NAT holds H₇(x) is Element of REAL ;
consider QAbsFMF being Function of NAT ,REAL such that
A25: for x being Element of NAT holds QAbsFMF . x = H₇(x) from FUNCT_2:sch 9(A24);
A26: for n being Element of NAT holds (Ir . n) to_power (1 / k) <= QAbsFMF . n

proof

defpred S₁[ Nat] means (Ir . $1) to_power (1 / k) <= QAbsFMF . $1;
B1: ( abs (F1 . 0 ) in Lp_Functions M,k & AbsFMF . 0 in Lp_Functions M,k ) by A9, A6;
G . 0 = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . 0 ) by A10;
then B2: G . 0 = (abs (F1 . 0 )) + (AbsFMF . 0 ) by MESFUN9C:def 2;
Ir . 0 = Integral M,(Gp . 0 ) by A19;
then Ir . 0 = Integral M,((G . 0 ) to_power k) by A12;
then B3: Ir . 0 = Integral M,((abs ((abs (F1 . 0 )) + (AbsFMF . 0 ))) to_power k) by A11, B2;
KPAbsFMF . 0 = Integral M,((AbsFMF . 0 ) to_power k) by A21;
then B4: KPAbsFMF . 0 = Integral M,((abs (AbsFMF . 0 )) to_power k) by A9;
B5: RF0 = Integral M,((abs (abs (F1 . 0 ))) to_power k) ;
QAbsFMF . 0 = (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . 0 ) by A25;
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 A23;
then P1: S₁[ 0 ] by AKS, B1, B3, B4, B5, Th002X;

P2: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then B0: ((Ir . n) to_power (1 / k)) + (PAbsFMF . (n + 1)) <= (QAbsFMF . n) + (PAbsFMF . (n + 1)) by XREAL_1:8;
G . (n + 1) = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . (n + 1)) by A10
.= (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:19 ;
then B1: G . (n + 1) = (G . n) + (AbsFMF . (n + 1)) by A10;
B2: ( AbsFMF . (n + 1) in Lp_Functions M,k & G . n in Lp_Functions M,k ) by A9, A11;
KPAbsFMF . (n + 1) = Integral M,((AbsFMF . (n + 1)) to_power k) by A21;
then B3: KPAbsFMF . (n + 1) = Integral M,((abs (AbsFMF . (n + 1))) to_power k) by A9;
B4: PAbsFMF . (n + 1) = (KPAbsFMF . (n + 1)) to_power (1 / k) by A23;
( Ir . n = Integral M,(Gp . n) & Ir . (n + 1) = Integral M,(Gp . (n + 1)) ) by A19;
then ( Ir . n = Integral M,((G . n) to_power k) & Ir . (n + 1) = Integral M,((G . (n + 1)) to_power k) ) by A12;
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 B1, A11;
then (Ir . (n + 1)) to_power (1 / k) <= ((Ir . n) to_power (1 / k)) + (PAbsFMF . (n + 1)) by AKS, B2, B3, B4, Th002X;
then B6: (Ir . (n + 1)) to_power (1 / k) <= (QAbsFMF . n) + (PAbsFMF . (n + 1)) by B0, XXREAL_0:2;
(QAbsFMF . n) + (PAbsFMF . (n + 1)) = ((RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . n)) + (PAbsFMF . (n + 1)) by A25
.= (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 S₁[n + 1] by B6, A25; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(P1, P2);
hence for n being Element of NAT holds (Ir . n) to_power (1 / k) <= QAbsFMF . n ; :: thesis: verum

end;

A27: for n being Element of NAT holds PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).||

proof

let n be Element of NAT ; :: thesis: PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).||
set m = N . n;
set m1 = N . (n + 1);
B4: ( F1 . (n + 1) = Fsq . (N . (n + 1)) & F1 . n = Fsq . (N . n) ) by A5;
AbsFMF . n = abs (FMF . n) by SEQFUNC:def 5;
then B5: AbsFMF . n = abs ((Fsq . (N . (n + 1))) - (Fsq . (N . n))) by B4, A7;
B6: ( 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 . (N . n) ) by A2;
then (- 1) (#) (Fsq . (N . n)) in (- 1) * (Sq . (N . n)) by Lm17Y;
then (Fsq . (N . (n + 1))) - (Fsq . (N . n)) in (Sq . (N . (n + 1))) + ((- 1) * (Sq . (N . n))) by Lm17Y, B6;
then (Fsq . (N . (n + 1))) - (Fsq . (N . n)) in (Sq . (N . (n + 1))) - (Sq . (N . n)) by RLVECT_1:29;
then B9: ex r being Real st
( 0 <= r & r = Integral M,((abs ((Fsq . (N . (n + 1))) - (Fsq . (N . n)))) to_power k) & ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).|| = r to_power (1 / k) ) by Lm17x;
PAbsFMF . n = (KPAbsFMF . n) to_power (1 / k) by A23;
hence PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).|| by B9, B5, A21; :: thesis: verum

end;

1 / 2 < 1 ;
then abs (1 / 2) < 1 by ABSVALUE:def 1;
then A28: ( (1 / 2) GeoSeq is summable & Sum ((1 / 2) GeoSeq ) = 1 / (1 - (1 / 2)) ) by SERIES_1:28;
for n being Element of NAT holds
( 0 <= PAbsFMF . n & PAbsFMF . n <= ((1 / 2) GeoSeq ) . n )

proof

let n be Element of NAT ; :: thesis: ( 0 <= PAbsFMF . n & PAbsFMF . n <= ((1 / 2) GeoSeq ) . n )
LL1: PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).|| by A27;
hence 0 <= PAbsFMF . n by NORMSP_1:8; :: thesis: PAbsFMF . n <= ((1 / 2) GeoSeq ) . n
((1 / 2) GeoSeq ) . n = (1 / 2) |^ n by PREPOWER:def 1
.= (1 / 2) to_power n by POWER:46 ;
then LL2: ((1 / 2) GeoSeq ) . n = 2 to_power (- n) by POWER:37;
N is Real_Sequence by FUNCT_2:9;
then N . n < N . (n + 1) by SEQM_3:def 11;
hence PAbsFMF . n <= ((1 / 2) GeoSeq ) . n by A4, LL1, LL2; :: thesis: verum

end;

then ( PAbsFMF is summable & Sum PAbsFMF <= Sum ((1 / 2) GeoSeq ) ) by A28, SERIES_1:24;
then Partial_Sums PAbsFMF is convergent by SERIES_1:def 2;
then Partial_Sums PAbsFMF is bounded by SEQ_2:27;
then consider Br being real number such that
A29: for n being Element of NAT holds (Partial_Sums PAbsFMF) . n < Br by SEQ_2:def 3;
for n being Element of NAT holds Ir . n < ((RF0 to_power (1 / k)) + Br) to_power k

proof

let n be Element of NAT ; :: thesis: Ir . n < ((RF0 to_power (1 / k)) + Br) to_power k
(Ir . n) to_power (1 / k) <= QAbsFMF . n by A26;
then D1: (Ir . n) to_power (1 / k) <= (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . n) by A25;
(RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . n) < (RF0 to_power (1 / k)) + Br by A29, XREAL_1:10;
then R10: (Ir . n) to_power (1 / k) < (RF0 to_power (1 / k)) + Br by D1, XXREAL_0:2;
Ir . n = Integral M,(Gp . n) by A19;
then Ir . n = Integral M,((G . n) to_power k) by A12;
then R110: Ir . n = Integral M,((abs (G . n)) to_power k) by A11;
R11: G . n in Lp_Functions M,k by A11;
then 0 <= (Ir . n) to_power (1 / k) by Lm15, R110, LmPW001;
then ((Ir . n) to_power (1 / k)) to_power k < ((RF0 to_power (1 / k)) + Br) to_power k by R10, HOLDER13;
then (Ir . n) to_power ((1 / k) * k) < ((RF0 to_power (1 / k)) + Br) to_power k by R11, Lm15, R110, HOLDER_1:2;
then (Ir . n) to_power 1 < ((RF0 to_power (1 / k)) + Br) to_power k by XCMPLX_1:107;
hence Ir . n < ((RF0 to_power (1 / k)) + Br) to_power k by POWER:30; :: thesis: verum

end;

then A30: Ir is bounded_above by SEQ_2:def 3;
for n, m being Element of NAT st n <= m holds
Ir . n <= Ir . m

proof

let n, m be Element of NAT ; :: thesis: ( n <= m implies Ir . n <= Ir . m )
assume n <= m ; :: thesis: Ir . n <= Ir . m
then D2: for x being Element of X st x in E holds
(ExtGp . n) . x <= (ExtGp . m) . x by A16;
D7: ( ExtGp . n is_measurable_on E & ExtGp . m is_measurable_on E & ExtGp . n is nonnegative & ExtGp . m is nonnegative ) by A14;
D5: ( dom (ExtGp . n) = E & dom (ExtGp . m) = E ) by A14;
then D11: ( (ExtGp . n) | E = ExtGp . n & (ExtGp . m) | E = ExtGp . m ) by RELAT_1:97;
( I . n = Integral M,(ExtGp . n) & I . m = Integral M,(ExtGp . m) ) by A19;
hence Ir . n <= Ir . m by D2, D5, D7, D11, MESFUNC9:15; :: thesis: verum

end;

then Ir is V163() by SEQM_3:12;
then A31: ( I is convergent_to_finite_number & lim I = lim Ir ) by A30, RINFSUP2:14;
reconsider LExtGp = lim ExtGp as PartFunc of X,ExtREAL ;
A32: ( E = dom LExtGp & LExtGp is_measurable_on E ) by A14, A15, A18, MESFUNC8:25, MESFUNC8:def 10;
A33: for x being set st x in dom LExtGp holds
0 <= LExtGp . x

proof

let x be set ; :: thesis: ( x in dom LExtGp implies 0 <= LExtGp . x )
assume B0: x in dom LExtGp ; :: thesis: 0 <= LExtGp . x
then reconsider x1 = x as Element of X ;
B1: x1 in E by A15, B0, MESFUNC8:def 10;

now

let k1 be Nat; :: thesis: 0 <= (ExtGp # x1) . k1
reconsider k = k1 as Element of NAT by ORDINAL1:def 13;
ExtGp # x1 is V163() by A17, B1;
then C23: (ExtGp # x1) . 0 <= (ExtGp # x1) . k by RINFSUP2:7;
0 <= (ExtGp . 0 ) . x1 by A15, SUPINF_2:58;
hence 0 <= (ExtGp # x1) . k1 by C23, MESFUNC5:def 13; :: thesis: verum

end;

then 0 <= lim (ExtGp # x1) by B1, A18, MESFUNC9:10;
hence 0 <= LExtGp . x by B0, MESFUNC8:def 10; :: thesis: verum

end;

A34: eq_dom LExtGp,+infty = E /\ (eq_dom LExtGp,+infty ) by A32, RELAT_1:167, XBOOLE_1:28;
then reconsider EE = eq_dom LExtGp,+infty as Element of S by A32, MESFUNC1:37;
reconsider E0 = E \ EE as Element of S ;
E0 ` = (X \ E) \/ (X /\ EE) by XBOOLE_1:52;
then A35: E0 ` = (E ` ) \/ EE by XBOOLE_1:28;
M . EE = 0 by A19, A31, A32, A33, A34, MESFUNC9:13, SUPINF_2:71;
then A36: EE is measure_zero of M by MEASURE1:def 13;
E ` is Element of S by MEASURE1:66;
then E ` is measure_zero of M by A3, MEASURE1:def 13;
then E0 ` is measure_zero of M by A35, A36, MEASURE1:70;
then A37: M . (E0 ` ) = 0 by MEASURE1:def 13;
A38: for x being Element of X st x in E0 holds
LExtGp . x in REAL

proof

let x be Element of X; :: thesis: ( x in E0 implies LExtGp . x in REAL )
assume x in E0 ; :: thesis: LExtGp . x in REAL
then ( x in E & not x in EE ) by XBOOLE_0:def 5;
then ( LExtGp . x <> +infty & 0 <= LExtGp . x ) by A32, A33, MESFUNC1:def 16;
hence LExtGp . x in REAL by XXREAL_0:14; :: thesis: verum

end;

A39: for x being 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; :: thesis: ( x in E0 implies ( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) ) )
assume B1: x in E0 ; :: thesis: ( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) )
then B2: x in E by XBOOLE_0:def 5;
then LExtGp . x = lim (ExtGp # x) by A32, MESFUNC8:def 10;
then B3: lim (ExtGp # x) in REAL by A38, B1;
ExtGp # x is convergent by A18, B2;
then B4: ex g being real number st
( lim (ExtGp # x) = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((ExtGp # x) . m) - (lim (ExtGp # x))).| < p ) & ExtGp # x is convergent_to_finite_number ) by B3, MESFUNC5:def 12;
ExtGp # x = Gp # x by MESFUN7C:1;
hence ( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) ) by B4, RINFSUP2:15; :: thesis: verum

end;

A40: for x being Element of X st x in E0 holds
for n being Element of NAT holds (Gp # x) . n = ((G # x) . n) to_power k

proof

let x be Element of X; :: thesis: ( x in E0 implies for n being Element of NAT holds (Gp # x) . n = ((G # x) . n) to_power k )
assume B1: x in E0 ; :: thesis: for n being Element of NAT holds (Gp # x) . n = ((G # x) . n) to_power k

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: (Gp # x) . n = ((G # x) . n) to_power k
x in E by B1, XBOOLE_0:def 5;
then x in dom (G . n) by A11;
then B2: x in dom ((G . n) to_power k) by MESFUN6C:def 6;
(Gp # x) . n = (Gp . n) . x by SEQFUNC:def 11
.= ((G . n) to_power k) . x by A12
.= ((G . n) . x) to_power k by B2, MESFUN6C:def 6 ;
hence (Gp # x) . n = ((G # x) . n) to_power k by SEQFUNC:def 11; :: thesis: verum

end;

end;

A41: for x being Element of X st x in E0 holds
(Partial_Sums AbsFMF) # x is convergent

proof

let x be Element of X; :: thesis: ( x in E0 implies (Partial_Sums AbsFMF) # x is convergent )
assume B1: x in E0 ; :: thesis: (Partial_Sums AbsFMF) # x is convergent
then B2: Gp # x is convergent by A39;

B3: now

let n be Element of NAT ; :: thesis: 0 <= (G # x) . n
G . n is nonnegative by A11;
then 0 <= (G . n) . x by MESFUNC6:51;
hence 0 <= (G # x) . n by SEQFUNC:def 11; :: thesis: verum

end;

for n being Element of NAT holds (Gp # x) . n = ((G # x) . n) to_power k by B1, A40;
then B4: G # x is convergent by B2, B3, LMSQ1;

now

let s be real number ; :: thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)) < s )
assume 0 < s ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)) < s
then consider n being Element of NAT such that
B5: for m being Element of NAT st n <= m holds
abs (((G # x) . m) - ((G # x) . n)) < s by B4, SEQ_4:58;

now

let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)) < s )
assume B6: n <= m ; :: thesis: abs ((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)) < s
x in E by B1, XBOOLE_0:def 5;
then B7: ( x in dom (G . n) & x in dom (G . m) ) by A11;
( G . m = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . m) & G . n = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . n) ) by A10;
then ( (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 B7, VALUED_1:def 1;
then ( (G # x) . m = ((abs (F1 . 0 )) . x) + (((Partial_Sums AbsFMF) . m) . x) & (G # x) . n = ((abs (F1 . 0 )) . x) + (((Partial_Sums AbsFMF) . n) . x) ) by SEQFUNC:def 11;
then B8: ((G # x) . m) - ((G # x) . n) = (((Partial_Sums AbsFMF) . m) . x) - (((Partial_Sums AbsFMF) . n) . x) ;
( ((Partial_Sums AbsFMF) # x) . m = ((Partial_Sums AbsFMF) . m) . x & ((Partial_Sums AbsFMF) # x) . n = ((Partial_Sums AbsFMF) . n) . x ) by SEQFUNC:def 11;
hence abs ((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)) < s by B5, B6, B8; :: thesis: verum

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)) < s ; :: thesis: verum

end;

hence (Partial_Sums AbsFMF) # x is convergent by SEQ_4:58; :: thesis: verum

end;

A42: for x being Element of X st x in E0 holds
Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x

proof

let x be Element of X; :: thesis: ( x in E0 implies Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x )
assume x in E0 ; :: thesis: Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x
then B0: x in E by XBOOLE_0:def 5;
defpred S₁[ Nat] means (Partial_Sums (abs (FMF # x))) . $1 = ((Partial_Sums AbsFMF) # x) . $1;
(Partial_Sums (abs (FMF # x))) . 0 = (abs (FMF # x)) . 0 by SERIES_1:def 1
.= abs ((FMF # x) . 0 ) by VALUED_1:18
.= abs ((FMF . 0 ) . x) by SEQFUNC:def 11
.= (abs (FMF . 0 )) . x by VALUED_1:18
.= (AbsFMF . 0 ) . x by SEQFUNC:def 5
.= ((Partial_Sums AbsFMF) . 0 ) . x by MESFUN9C:def 2
.= ((Partial_Sums AbsFMF) # x) . 0 by SEQFUNC:def 11 ;
then P0: S₁[ 0 ] ;

P1: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume D1: S₁[n] ; :: thesis: S₁[n + 1]
D0: (Partial_Sums AbsFMF) . (n + 1) = ((Partial_Sums AbsFMF) . n) + (AbsFMF . (n + 1)) by MESFUN9C:def 2;
dom (AbsFMF . 0 ) = E by A9;
then D5: x in dom ((Partial_Sums AbsFMF) . (n + 1)) by B0, MESFUN9C:11;
D2: (abs (FMF # x)) . (n + 1) = abs ((FMF # x) . (n + 1)) by VALUED_1:18
.= abs ((FMF . (n + 1)) . x) by SEQFUNC:def 11
.= (abs (FMF . (n + 1))) . x by VALUED_1:18
.= (AbsFMF . (n + 1)) . x by SEQFUNC:def 5 ;
(Partial_Sums (abs (FMF # x))) . (n + 1) = ((Partial_Sums (abs (FMF # x))) . n) + ((abs (FMF # x)) . (n + 1)) by SERIES_1:def 1
.= (((Partial_Sums AbsFMF) . n) . x) + ((AbsFMF . (n + 1)) . x) by D1, D2, SEQFUNC:def 11
.= ((Partial_Sums AbsFMF) . (n + 1)) . x by D0, D5, VALUED_1:def 1
.= ((Partial_Sums AbsFMF) # x) . (n + 1) by SEQFUNC:def 11 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(P0, P1);
hence Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x by FUNCT_2:113; :: thesis: verum

end;

A43: for x being Element of X st x in E0 holds
for n being Element of NAT holds (F1 # x) . (n + 1) = ((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n)

proof

let x be Element of X; :: thesis: ( x in E0 implies for n being Element of NAT holds (F1 # x) . (n + 1) = ((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n) )
assume x in E0 ; :: thesis: for n being Element of NAT holds (F1 # x) . (n + 1) = ((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n)
then A252: x in E by XBOOLE_0:def 5;
defpred S₁[ Nat] means (F1 # x) . ($1 + 1) = ((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . $1);
dom (FMF . 0 ) = E by A8;
then D4: x in dom ((F1 . (0 + 1)) - (F1 . 0 )) by A7, A252;
(Partial_Sums (FMF # x)) . 0 = (FMF # x) . 0 by SERIES_1:def 1
.= (FMF . 0 ) . x by SEQFUNC:def 11
.= ((F1 . (0 + 1)) - (F1 . 0 )) . x by A7 ;
then D1: (Partial_Sums (FMF # x)) . 0 = ((F1 . (0 + 1)) . x) - ((F1 . 0 ) . x) by D4, VALUED_1:13;
((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . 0 ) = ((F1 . 0 ) . x) + ((Partial_Sums (FMF # x)) . 0 ) by SEQFUNC:def 11;
then P0: S₁[ 0 ] by D1, SEQFUNC:def 11;

P1: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume D1: S₁[n] ; :: thesis: S₁[n + 1]
dom (FMF . (n + 1)) = E by A8;
then DN4: x in dom ((F1 . ((n + 1) + 1)) - (F1 . (n + 1))) by A7, A252;
(FMF # x) . (n + 1) = (FMF . (n + 1)) . x by SEQFUNC:def 11
.= ((F1 . ((n + 1) + 1)) - (F1 . (n + 1))) . x by A7 ;
then D2: (FMF # x) . (n + 1) = ((F1 . ((n + 1) + 1)) . x) - ((F1 . (n + 1)) . x) by DN4, VALUED_1:13;
((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . (n + 1)) = ((F1 # x) . 0 ) + (((Partial_Sums (FMF # x)) . n) + ((FMF # x) . (n + 1))) by SERIES_1:def 1
.= (((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n)) + ((FMF # x) . (n + 1))
.= ((F1 . (n + 1)) . x) + ((FMF # x) . (n + 1)) by D1, SEQFUNC:def 11 ;
hence S₁[n + 1] by D2, SEQFUNC:def 11; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(P0, P1);
hence for n being Element of NAT holds (F1 # x) . (n + 1) = ((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n) ; :: thesis: verum

end;

A44: for x being Element of X st x in E0 holds
F1 # x is convergent

proof

let x be Element of X; :: thesis: ( x in E0 implies F1 # x is convergent )
assume A281: x in E0 ; :: thesis: F1 # x is convergent
then Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x by A42;
then Partial_Sums (abs (FMF # x)) is convergent by A281, A41;
then abs (FMF # x) is summable by SERIES_1:def 2;
then FMF # x is absolutely_summable by SERIES_1:def 5;
then FMF # x is summable by SERIES_1:40;
then A285: Partial_Sums (FMF # x) is convergent by SERIES_1:def 2;

now

let s be real number ; :: thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((F1 # x) . m) - ((F1 # x) . n)) < s )
assume 0 < s ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((F1 # x) . m) - ((F1 # x) . n)) < s
then consider n being Element of NAT such that
A286: for m being Element of NAT st n <= m holds
abs (((Partial_Sums (FMF # x)) . m) - ((Partial_Sums (FMF # x)) . n)) < s by A285, SEQ_4:58;
set n1 = n + 1;

now

let m1 be Element of NAT ; :: thesis: ( n + 1 <= m1 implies abs (((F1 # x) . m1) - ((F1 # x) . (n + 1))) < s )
assume AD2: n + 1 <= m1 ; :: thesis: abs (((F1 # x) . m1) - ((F1 # x) . (n + 1))) < s
1 <= n + 1 by NAT_1:11;
then reconsider m = m1 - 1 as Element of NAT by AD2, NAT_1:21, XXREAL_0:2;
(n + 1) - 1 <= m1 - 1 by AD2, XREAL_1:11;
then AD3: abs (((Partial_Sums (FMF # x)) . m) - ((Partial_Sums (FMF # x)) . n)) < s by A286;
m1 = m + 1 ;
then ( (F1 # x) . (n + 1) = ((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n) & (F1 # x) . m1 = ((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . m) ) by A43, A281;
hence abs (((F1 # x) . m1) - ((F1 # x) . (n + 1))) < s by AD3; :: thesis: verum

end;

hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((F1 # x) . m) - ((F1 # x) . n)) < s ; :: thesis: verum

end;

hence F1 # x is convergent by SEQ_4:58; :: thesis: verum

end;

set F2 = F1 || E0;
A59: for x being Element of X st x in E0 holds
(F1 || E0) # x is convergent

proof

let x be Element of X; :: thesis: ( x in E0 implies (F1 || E0) # x is convergent )
assume AA0: x in E0 ; :: thesis: (F1 || E0) # x is convergent
then F1 # x is convergent by A44;
hence (F1 || E0) # x is convergent by AA0, MESFUN9C:1; :: thesis: verum

end;

A45: for x being Element of X st x in E0 holds
(F1 || E0) # x = F1 # x

proof

let x be Element of X; :: thesis: ( x in E0 implies (F1 || E0) # x = F1 # x )
assume A281: x in E0 ; :: thesis: (F1 || E0) # x = F1 # x

now

let n be Element of NAT ; :: thesis: ((F1 || E0) # x) . n = (F1 # x) . n
((F1 || E0) # x) . n = ((F1 || E0) . n) . x by SEQFUNC:def 11
.= ((F1 . n) | E0) . x by MESFUN9C:def 1
.= (F1 . n) . x by A281, FUNCT_1:72 ;
hence ((F1 || E0) # x) . n = (F1 # x) . n by SEQFUNC:def 11; :: thesis: verum

end;

hence (F1 || E0) # x = F1 # x by FUNCT_2:113; :: thesis: verum

end;

A46: for n being natural number holds
( dom ((F1 || E0) . n) = E0 & (F1 || E0) . n is_measurable_on E0 )

proof

let n be natural number ; :: thesis: ( dom ((F1 || E0) . n) = E0 & (F1 || E0) . n is_measurable_on E0 )
DD0: dom (F1 . 0 ) = E by A6;
dom ((F1 || E0) . n) = dom ((F1 . n) | E0) by MESFUN9C:def 1;
then dom ((F1 || E0) . n) = (dom (F1 . n)) /\ E0 by RELAT_1:90;
then dom ((F1 || E0) . n) = E /\ E0 by A6;
hence dom ((F1 || E0) . n) = E0 by XBOOLE_1:28, XBOOLE_1:36; :: thesis: (F1 || E0) . n is_measurable_on E0
for m being Nat holds F1 . m is_measurable_on E0

proof

let m be Nat; :: thesis: F1 . m is_measurable_on E0
F1 . m is_measurable_on E by A6;
hence F1 . m is_measurable_on E0 by MESFUNC6:16, XBOOLE_1:36; :: thesis: verum

end;

hence (F1 || E0) . n is_measurable_on E0 by DD0, MESFUN9C:4, XBOOLE_1:36; :: thesis: verum

end;

reconsider F2 = F1 || E0 as with_the_same_dom Functional_Sequence of X,REAL by MESFUN9C:2;
A47: for n being Nat holds
( F2 . n in Lp_Functions M,k & F2 . n in Sq . (N . n) )

proof

let n1 be Nat; :: thesis: ( F2 . n1 in Lp_Functions M,k & F2 . n1 in Sq . (N . n1) )
F2 . n1 = (F1 . n1) | E0 by MESFUN9C:def 1;
then abs (F2 . n1) = (abs (F1 . n1)) | E0 by Lm001x;
then DY6: ((abs (F1 . n1)) to_power k) | E0 = (abs (F2 . n1)) to_power k by Lm001g;
L1: ( F2 . n1 is_measurable_on E0 & dom (F2 . n1) = E0 ) by A46;
F1 . n1 in Lp_Functions M,k by A6;
then ex FMF being PartFunc of X,REAL st
( F1 . n1 = FMF & ex ND being Element of S st
( M . (ND ` ) = 0 & dom FMF = ND & FMF is_measurable_on ND & (abs FMF) to_power k is_integrable_on M ) ) ;
then (abs (F2 . n1)) to_power k is_integrable_on M by DY6, MESFUNC6:91;
hence D1: F2 . n1 in Lp_Functions M,k by L1, A37; :: thesis: F2 . n1 in Sq . (N . n1)
reconsider n = n1 as Element of NAT by ORDINAL1:def 13;
set m = N . n;
F1 . n = Fsq . (N . n) by A5;
then L2: ( F1 . n in Sq . (N . n) & Sq . (N . n) = a.e-eq-class_Lp (F1 . n),M,k ) by A2;
reconsider EB = E0 ` as Element of S by MEASURE1:66;
(F2 . n) | (EB ` ) = F2 . n by L1, RELAT_1:97;
then (F2 . n) | (EB ` ) = (F1 . n) | (EB ` ) by MESFUN9C:def 1;
then F2 . n a.e.= F1 . n,M by A37, LPSPACE1:def 10;
hence F2 . n1 in Sq . (N . n1) by D1, L2, EQC00b; :: thesis: verum

end;

A48: dom (lim F2) = dom (F2 . 0 ) by MESFUNC8:def 10;
then A49: dom (lim F2) = E0 by A46;
A50: for x being Element of X st x in E0 holds
(lim F2) . x = lim (F2 # x)

proof

let x be Element of X; :: thesis: ( x in E0 implies (lim F2) . x = lim (F2 # x) )
assume x in E0 ; :: thesis: (lim F2) . x = lim (F2 # x)
then ( (lim F2) . x = lim (R_EAL (F2 # x)) & F2 # x is convergent ) by A49, A59, MESFUN7C:14;
hence (lim F2) . x = lim (F2 # x) by RINFSUP2:14; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in rng (lim F2) implies y in REAL )
assume y in rng (lim F2) ; :: thesis: y in REAL
then consider x being Element of X such that
D1: ( x in dom (lim F2) & y = (lim F2) . x ) by PARTFUN1:26;
y = lim (F2 # x) by D1, A49, A50;
hence y in REAL ; :: thesis: verum

end;

then rng (lim F2) c= REAL by TARSKI:def 3;
then reconsider F = lim F2 as PartFunc of X,REAL by A48, RELSET_1:11;
A51: dom (LExtGp | E0) = E /\ E0 by A32, RELAT_1:90;
then A52: dom (LExtGp | E0) = E0 by XBOOLE_1:28, XBOOLE_1:36;

now

let y be set ; :: thesis: ( y in rng (LExtGp | E0) implies y in REAL )
assume y in rng (LExtGp | E0) ; :: thesis: y in REAL
then consider x being Element of X such that
AA2: ( x in dom (LExtGp | E0) & y = (LExtGp | E0) . x ) by PARTFUN1:26;
y = LExtGp . x by A52, AA2, FUNCT_1:72;
hence y in REAL by A52, AA2, A38; :: thesis: verum

end;

then rng (LExtGp | E0) c= REAL by TARSKI:def 3;
then reconsider gp = LExtGp | E0 as PartFunc of X,REAL by A51, RELSET_1:11;
A53: for x being Element of X st x in E0 holds
gp . x = lim (Gp # x)

proof

let x be Element of X; :: thesis: ( x in E0 implies gp . x = lim (Gp # x) )
assume AA01: x in E0 ; :: thesis: gp . x = lim (Gp # x)
then x in dom LExtGp by A32, XBOOLE_0:def 5;
then LExtGp . x = lim (ExtGp # x) by MESFUNC8:def 10;
then gp . x = lim (ExtGp # x) by AA01, FUNCT_1:72;
hence gp . x = lim (Gp # x) by A39, AA01; :: thesis: verum

end;

LExtGp is nonnegative by A33, SUPINF_2:71;
then LExtGp is_integrable_on M by A31, A19, A32, MPreLm8;
then R_EAL gp is_integrable_on M by MESFUNC5:103;
then A54: gp is_integrable_on M by MESFUNC6:def 9;
A55: dom (F2 . 0 ) = E0 by A46;
then A56: dom F = E0 by MESFUNC8:def 10;
then A58: E0 = dom (abs F) by VALUED_1:def 11;
then A57: E0 = dom ((abs F) to_power k) by MESFUN6C:def 6;
A61: for x being Element of X
for n being Element of NAT st x in E0 holds
(abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n

proof

let x be Element of X; :: thesis: for n being Element of NAT st x in E0 holds
(abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n
let n be Element of NAT ; :: thesis: ( x in E0 implies (abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n )
assume ASP: x in E0 ; :: thesis: (abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n
then x in E by XBOOLE_0:def 5;
then P1: x in dom (G . n) by A11;
G . n = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . n) by A10;
then (G . n) . x = ((abs (F1 . 0 )) . x) + (((Partial_Sums AbsFMF) . n) . x) by P1, VALUED_1:def 1;
then P6: (G . n) . x = (abs ((F1 . 0 ) . x)) + (((Partial_Sums AbsFMF) . n) . x) by VALUED_1:18;
(G # x) . n = (G . n) . x by SEQFUNC:def 11
.= (abs ((F1 . 0 ) . x)) + (((Partial_Sums AbsFMF) # x) . n) by P6, SEQFUNC:def 11
.= (abs ((F1 # x) . 0 )) + (((Partial_Sums AbsFMF) # x) . n) by SEQFUNC:def 11 ;
then P9: (G # x) . n = (abs ((F1 # x) . 0 )) + ((Partial_Sums (abs (FMF # x))) . n) by A42, ASP;
abs ((Partial_Sums (FMF # x)) . n) <= (Partial_Sums (abs (FMF # x))) . n by LMSQ6;
hence (abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by P9, XREAL_1:8; :: thesis: verum

end;

A62: for x being Element of X
for n being Element of NAT st x in E0 holds
(abs (((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n))) to_power k <= (Gp # x) . n

proof

let x be Element of X; :: thesis: for n being Element of NAT st x in E0 holds
(abs (((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n))) to_power k <= (Gp # x) . n
let n be Element of NAT ; :: thesis: ( x in E0 implies (abs (((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n))) to_power k <= (Gp # x) . n )
assume A281: x in E0 ; :: thesis: (abs (((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n))) to_power k <= (Gp # x) . n
then P1: (Gp # x) . n = ((G # x) . n) to_power k by A40;
P11: (abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by A61, A281;
abs (((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n)) <= (abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) by COMPLEX1:142;
then P12: abs (((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by P11, XXREAL_0:2;
0 <= abs (((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n)) by COMPLEX1:132;
hence (abs (((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n))) to_power k <= (Gp # x) . n by P1, P12, HOLDER_1:3; :: thesis: verum

end;

A63: for x being Element of X
for n being Element of NAT st x in E0 holds
(abs ((F2 # x) . n)) to_power k <= (Gp # x) . n

proof

let x be Element of X; :: thesis: for n being Element of NAT st x in E0 holds
(abs ((F2 # x) . n)) to_power k <= (Gp # x) . n
let n be Element of NAT ; :: thesis: ( x in E0 implies (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n )
assume B1: x in E0 ; :: thesis: (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n
then B2: F1 # x = F2 # x by A45;

per cases ( n = 0 or n <> 0 ) ;

suppose C1: n = 0 ; :: thesis: (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n

C2: (Gp # x) . n = ((G # x) . n) to_power k by B1, A40;
C3: (abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by A61, B1;
0 <= abs ((Partial_Sums (FMF # x)) . n) by COMPLEX1:132;
then 0 + (abs ((F1 # x) . 0 )) <= (abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) by XREAL_1:8;
then C4: abs ((F1 # x) . 0 ) <= (G # x) . n by C3, XXREAL_0:2;
0 <= abs ((F1 # x) . 0 ) by COMPLEX1:132;
hence (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n by B2, C1, C2, C4, HOLDER_1:3; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n

then consider m being Nat such that
P1: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
(F1 # x) . (m + 1) = ((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . m) by A43, B1;
then P3: (abs ((F1 # x) . (m + 1))) to_power k <= (Gp # x) . m by A62, B1;
x in E by B1, XBOOLE_0:def 5;
then P4: ExtGp # x is V163() by A17;
m <= m + 1 by NAT_1:11;
then P5: (ExtGp # x) . m <= (ExtGp # x) . (m + 1) by P4, RINFSUP2:7;
ExtGp # x = Gp # x by MESFUN7C:1;
hence (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n by B2, P1, P3, P5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A64: for x being Element of X st x in E0 holds
abs (((abs F) to_power k) . x) <= gp . x

proof

let x be Element of X; :: thesis: ( x in E0 implies abs (((abs F) to_power k) . x) <= gp . x )
assume PY61: x in E0 ; :: thesis: abs (((abs F) to_power k) . x) <= gp . x
then L0: Gp # x is convergent by A39;
deffunc H₈( set ) -> Element of REAL = ((abs (F2 # x)) . $1) to_power k;
consider s being Real_Sequence such that
D0: for n being Element of NAT holds s . n = H₈(n) from SEQ_1:sch 1();
D2: gp . x = lim (Gp # x) by A53, PY61;
D6: ((abs F) to_power k) . x = ((abs F) . x) to_power k by A57, PY61, MESFUN6C:def 6
.= (abs (F . x)) to_power k by A58, PY61, VALUED_1:def 11
.= (abs (lim (F2 # x))) to_power k by PY61, A50
.= (lim (abs (F2 # x))) to_power k by A59, PY61, SEQ_4:27 ;

D71: now

let n be Element of NAT ; :: thesis: 0 <= (abs (F2 # x)) . n
0 <= abs ((F2 # x) . n) by COMPLEX1:132;
hence 0 <= (abs (F2 # x)) . n by VALUED_1:18; :: thesis: verum

end;

abs (F2 # x) is convergent by PY61, A59, SEQ_4:26;
then D7: ( s is convergent & (lim (abs (F2 # x))) to_power k = lim s ) by D71, D0, HOLDER_1:10;

now

let n be Element of NAT ; :: thesis: s . n <= (Gp # x) . n
(abs ((F2 # x) . n)) to_power k <= (Gp # x) . n by A63, PY61;
then ((abs (F2 # x)) . n) to_power k <= (Gp # x) . n by VALUED_1:18;
hence s . n <= (Gp # x) . n by D0; :: thesis: verum

end;

then Q1: ((abs F) to_power k) . x <= gp . x by D7, D2, D6, L0, SEQ_2:32;
0 <= ((abs F) to_power k) . x by MESFUNC6:51;
hence abs (((abs F) to_power k) . x) <= gp . x by Q1, ABSVALUE:def 1; :: thesis: verum

end;

R_EAL F is_measurable_on E0 by A46, A55, A59, MESFUN7C:21;
then A65: F is_measurable_on E0 by MESFUNC6:def 6;
then A66: abs F is_measurable_on E0 by A56, MESFUNC6:48;
dom (abs F) = E0 by A56, VALUED_1:def 11;
then (abs F) to_power k is_measurable_on E0 by A66, MESFUN6C:29;
then (abs F) to_power k is_integrable_on M by A52, A54, A57, A64, MESFUNC6:96;
then A67: F in Lp_Functions M,k by A37, A56, A65;
A68: for x being Element of X
for n, m being Element of NAT st x in E0 & m <= n holds
|.(((F1 # x) . n) - ((F1 # x) . m)).| to_power k <= (Gp # x) . n

proof

let x be Element of X; :: thesis: for n, m being Element of NAT st x in E0 & m <= n holds
|.(((F1 # x) . n) - ((F1 # x) . m)).| to_power k <= (Gp # x) . n
let n1, m1 be Element of NAT ; :: thesis: ( x in E0 & m1 <= n1 implies |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 )
assume ASP: ( x in E0 & m1 <= n1 ) ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

now

per cases ( m1 = 0 or m1 <> 0 ) ;

suppose C1: m1 = 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

now

per cases ( n1 = 0 or n1 <> 0 ) ;

suppose C11: n1 = 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

(G . n1) to_power k is nonnegative by A13;
then Gp . n1 is nonnegative by A12;
then 0 <= (Gp . n1) . x by MESFUNC6:51;
then 0 <= (Gp # x) . n1 by SEQFUNC:def 11;
hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 by C1, C11, COMPLEX1:130, POWER:def 2; :: thesis: verum

end;

suppose n1 <> 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

then consider n being Nat such that
C111: n1 = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
LLL0: (F1 # x) . (n + 1) = ((F1 # x) . 0 ) + ((Partial_Sums (FMF # x)) . n) by ASP, A43;
Q2: (abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by A61, ASP;
0 <= abs ((F1 # x) . 0 ) by COMPLEX1:132;
then (abs ((Partial_Sums (FMF # x)) . n)) + 0 <= (abs ((F1 # x) . 0 )) + (abs ((Partial_Sums (FMF # x)) . n)) by XREAL_1:8;
then Q3: abs ((Partial_Sums (FMF # x)) . n) <= (G # x) . n by Q2, XXREAL_0:2;
0 <= abs ((Partial_Sums (FMF # x)) . n) by COMPLEX1:132;
then AAA1: |.((Partial_Sums (FMF # x)) . n).| to_power k <= ((G # x) . n) to_power k by Q3, HOLDER_1:3;
LLL1: (Gp # x) . n = ((G # x) . n) to_power k by ASP, A40;
x in E by ASP, XBOOLE_0:def 5;
then PPP2: ExtGp # x is V163() by A17;
n <= n + 1 by NAT_1:11;
then PPP3: (ExtGp # x) . n <= (ExtGp # x) . (n + 1) by PPP2, RINFSUP2:7;
ExtGp # x = Gp # x by MESFUN7C:1;
hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 by C1, C111, PPP3, AAA1, LLL1, LLL0, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 ; :: thesis: verum

end;

suppose C1: m1 <> 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1

then consider m being Nat such that
C11: m1 = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
0 < n1 by ASP, C1;
then consider n being Nat such that
C12: n1 = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
C13: m1 - 1 <= n1 - 1 by ASP, XREAL_1:11;
x in E by ASP, XBOOLE_0:def 5;
then P11: x in dom (G . n) by A11;
then A284: x in dom ((G . n) to_power k) by MESFUN6C:def 6;
(Gp # x) . n = (Gp . n) . x by SEQFUNC:def 11;
then (Gp # x) . n = ((G . n) to_power k) . x by A12;
then P100: (Gp # x) . n = ((G . n) . x) to_power k by A284, MESFUN6C:def 6;
G . n = (abs (F1 . 0 )) + ((Partial_Sums AbsFMF) . n) by A10;
then (G . n) . x = ((abs (F1 . 0 )) . x) + (((Partial_Sums AbsFMF) . n) . x) by P11, VALUED_1:def 1
.= (abs ((F1 . 0 ) . x)) + (((Partial_Sums AbsFMF) . n) . x) by VALUED_1:18 ;
then P61: (G . n) . x = (abs ((F1 . 0 ) . x)) + (((Partial_Sums AbsFMF) # x) . n) by SEQFUNC:def 11;
Q1: ( (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 ASP, A43;
Q3: |.(((Partial_Sums (FMF # x)) . n) - ((Partial_Sums (FMF # x)) . m)).| <= (Partial_Sums (abs (FMF # x))) . n by LMSQ4, C11, C12, C13;
Q5: (Partial_Sums (abs (FMF # x))) . n = ((Partial_Sums AbsFMF) # x) . n by A42, ASP;
0 <= abs ((F1 . 0 ) . x) by COMPLEX1:132;
then 0 + ((Partial_Sums (abs (FMF # x))) . n) <= (abs ((F1 . 0 ) . x)) + (((Partial_Sums AbsFMF) # x) . n) by Q5, XREAL_1:8;
then Q71: |.(((F1 # x) . (n + 1)) - ((F1 # x) . (m + 1))).| <= (G . n) . x by P61, Q1, Q3, XXREAL_0:2;
0 <= |.(((F1 # x) . (n + 1)) - ((F1 # x) . (m + 1))).| by COMPLEX1:132;
then FF1: |.(((F1 # x) . (n + 1)) - ((F1 # x) . (m + 1))).| to_power k <= (Gp # x) . n by P100, Q71, HOLDER_1:3;
x in E by ASP, XBOOLE_0:def 5;
then PPP2: ExtGp # x is V163() by A17;
n <= n + 1 by NAT_1:11;
then PPP3: (ExtGp # x) . n <= (ExtGp # x) . (n + 1) by PPP2, RINFSUP2:7;
ExtGp # x = Gp # x by MESFUN7C:1;
hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 by C11, C12, PPP3, FF1, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 ; :: thesis: verum

end;

A69: for x being Element of X
for n being Nat st x in E0 holds
|.((F . x) - ((F2 # x) . n)).| to_power k <= gp . x

proof

let x be Element of X; :: thesis: for n being Nat st x in E0 holds
|.((F . x) - ((F2 # x) . n)).| to_power k <= gp . x
let n1 be Nat; :: thesis: ( x in E0 implies |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x )
assume PY61: x in E0 ; :: thesis: |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x
then L0: Gp # x is convergent by A39;
E1: F1 # x = F2 # x by A45, PY61;
L1: F2 # x is convergent by PY61, A59;
reconsider n = n1 as Element of NAT by ORDINAL1:def 13;
deffunc H₈( Element of NAT ) -> Element of REAL = ((F2 # x) . $1) - ((F2 # x) . n);
consider s0 being Real_Sequence such that
D00: for j being Element of NAT holds s0 . j = H₈(j) from SEQ_1:sch 1();

JJ0: now

let p be real number ; :: thesis: ( 0 < p implies ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))) < p )
assume 0 < p ; :: thesis: ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
abs ((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))) < p
then consider n1 being Element of NAT such that
J2: for m being Element of NAT st n1 <= m holds
abs (((F2 # x) . m) - (lim (F2 # x))) < p by L1, SEQ_2:def 7;
take n1 = n1; :: thesis: for m being Element of NAT st n1 <= m holds
abs ((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))) < p
thus for m being Element of NAT st n1 <= m holds
abs ((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))) < p :: thesis: verum

proof

let m be Element of NAT ; :: thesis: ( n1 <= m implies abs ((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))) < p )
assume J3: n1 <= m ; :: thesis: abs ((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))) < p
(s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n)) = (((F2 # x) . m) - ((F2 # x) . n)) - ((lim (F2 # x)) - ((F2 # x) . n)) by D00;
then (s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n)) = ((F2 # x) . m) - (lim (F2 # x)) ;
hence abs ((s0 . m) - ((lim (F2 # x)) - ((F2 # x) . n))) < p by J3, J2; :: thesis: verum

end;

end;

then F00: s0 is convergent by SEQ_2:def 6;
then lim s0 = (lim (F2 # x)) - ((F2 # x) . n) by JJ0, SEQ_2:def 7;
then F03: lim (abs s0) = abs ((lim (F2 # x)) - ((F2 # x) . n)) by F00, SEQ_4:27;
F02: abs s0 is convergent by F00, SEQ_4:26;
deffunc H₉( Element of NAT ) -> Element of REAL = |.(((F2 # x) . $1) - ((F2 # x) . n)).| to_power k;
consider s being Real_Sequence such that
D0: for j being Element of NAT holds s . j = H₉(j) from SEQ_1:sch 1();
E21: for j being Element of NAT st n <= j holds
s . j <= (Gp # x) . j

proof

let j be Element of NAT ; :: thesis: ( n <= j implies s . j <= (Gp # x) . j )
assume n <= j ; :: thesis: s . j <= (Gp # x) . j
then |.(((F2 # x) . j) - ((F2 # x) . n)).| to_power k <= (Gp # x) . j by E1, PY61, A68;
hence s . j <= (Gp # x) . j by D0; :: thesis: verum

end;

D71: now

let n be Element of NAT ; :: thesis: 0 <= (abs s0) . n
0 <= abs (s0 . n) by COMPLEX1:132;
hence 0 <= (abs s0) . n by VALUED_1:18; :: thesis: verum

end;

now

let j be Element of NAT ; :: thesis: s . j = ((abs s0) . j) to_power k
thus s . j = |.(((F2 # x) . j) - ((F2 # x) . n)).| to_power k by D0
.= (abs (s0 . j)) to_power k by D00
.= ((abs s0) . j) to_power k by VALUED_1:18 ; :: thesis: verum

end;

then D72: ( s is convergent & lim s = (lim (abs s0)) to_power k ) by D71, F02, HOLDER_1:10;
then D73: ( s ^\ n is convergent & lim (s ^\ n) = lim s ) by SEQ_4:33;
gp . x = lim (Gp # x) by A53, PY61;
then D74: ( (Gp # x) ^\ n is convergent & lim ((Gp # x) ^\ n) = gp . x ) by L0, SEQ_4:33;
for j being Element of NAT holds (s ^\ n) . j <= ((Gp # x) ^\ n) . j

proof

let j be Element of NAT ; :: thesis: (s ^\ n) . j <= ((Gp # x) ^\ n) . j
( (s ^\ n) . j = s . (n + j) & ((Gp # x) ^\ n) . j = (Gp # x) . (n + j) ) by NAT_1:def 3;
hence (s ^\ n) . j <= ((Gp # x) ^\ n) . j by E21, NAT_1:11; :: thesis: verum

end;

then lim s <= gp . x by D73, D74, SEQ_2:32;
hence |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x by F03, D72, A50, PY61; :: thesis: verum

end;

deffunc H₈( Nat) -> Element of bool [:X,REAL :] = |.(F - (F2 . $1)).| to_power k;
consider FP being Functional_Sequence of X,REAL such that
A70: for n being Nat holds FP . n = H₈(n) from SEQFUNC:sch 1();
A71: for n being natural number holds dom (FP . n) = E0

proof

let n1 be natural number ; :: thesis: dom (FP . n1) = E0
reconsider n = n1 as Element of NAT by ORDINAL1:def 13;
B1: dom (F2 . n) = E0 by A46;
dom (FP . n1) = dom ((abs (F - (F2 . n))) to_power k) by A70;
then dom (FP . n1) = dom (abs (F - (F2 . n))) by MESFUN6C:def 6;
then dom (FP . n1) = dom (F - (F2 . n)) by VALUED_1:def 11;
then dom (FP . n1) = E0 /\ E0 by B1, A49, VALUED_1:12;
hence dom (FP . n1) = E0 ; :: thesis: verum

end;

then A72: E0 = dom (FP . 0 ) ;
then A74: dom (lim FP) = E0 by MESFUNC8:def 10;
for n, m being natural number holds dom (FP . n) = dom (FP . m)

proof

let n, m be natural number ; :: thesis: dom (FP . n) = dom (FP . m)
thus dom (FP . n) = E0 by A71
.= dom (FP . m) by A71 ; :: thesis: verum

end;

then reconsider FP = FP as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
A73: for n being Nat holds FP . n is_measurable_on E0

proof

let n1 be Nat; :: thesis: FP . n1 is_measurable_on E0
reconsider n = n1 as Element of NAT by ORDINAL1:def 13;
dom (F2 . n) = E0 by A46;
then D0: dom (F - (F2 . n)) = E0 /\ E0 by A49, VALUED_1:12;
( F2 . n is_measurable_on E0 & dom (F2 . n) = E0 ) by A46;
then F - (F2 . n) is_measurable_on E0 by A65, MESFUNC6:29;
then Y621: abs (F - (F2 . n)) is_measurable_on E0 by D0, MESFUNC6:48;
dom (abs (F - (F2 . n))) = E0 by D0, VALUED_1:def 11;
then (abs (F - (F2 . n))) to_power k is_measurable_on E0 by Y621, MESFUN6C:29;
hence FP . n1 is_measurable_on E0 by A70; :: thesis: verum

end;

for x being Element of X
for n being Nat st x in E0 holds
|.(FP . n).| . x <= gp . x

proof

let x be Element of X; :: thesis: for n being Nat st x in E0 holds
|.(FP . n).| . x <= gp . x
let n1 be Nat; :: thesis: ( x in E0 implies |.(FP . n1).| . x <= gp . x )
reconsider n = n1 as Element of NAT by ORDINAL1:def 13;
assume ASP: x in E0 ; :: thesis: |.(FP . n1).| . x <= gp . x
then D1: x in dom (FP . n) by A71;
then x in dom (|.(F - (F2 . n)).| to_power k) by A70;
then x in dom |.(F - (F2 . n)).| by MESFUN6C:def 6;
then D3: x in dom (F - (F2 . n)) by VALUED_1:def 11;
DD2: FP . n1 = |.(F - (F2 . n1)).| to_power k by A70;
DD21: 0 <= |.((F . x) - ((F2 . n1) . x)).| to_power k by LmPW001, COMPLEX1:132;
|.(FP . n).| . x = |.((FP . n) . x).| by VALUED_1:18
.= |.((|.(F - (F2 . n1)).| . x) to_power k).| by D1, DD2, MESFUN6C:def 6
.= |.(|.((F - (F2 . n1)) . x).| to_power k).| by VALUED_1:18
.= |.(|.((F . x) - ((F2 . n1) . x)).| to_power k).| by D3, VALUED_1:13
.= |.((F . x) - ((F2 . n1) . x)).| to_power k by DD21, ABSVALUE:def 1
.= |.((F . x) - ((F2 # x) . n)).| to_power k by SEQFUNC:def 11 ;
hence |.(FP . n1).| . x <= gp . x by A69, ASP; :: thesis: verum

end;

then consider Ip being Real_Sequence such that
A75: ( ( for n being Nat holds Ip . n = Integral M,(FP . n) ) & ( ( for x being Element of X st x in E0 holds
FP # x is convergent ) implies ( Ip is convergent & lim Ip = Integral M,(lim FP) ) ) ) by A52, A54, A72, A73, MESFUN9C:48;
A76: for x being Element of X st x in E0 holds
( FP # x is convergent & lim (FP # x) = 0 )

proof

let x be Element of X; :: thesis: ( x in E0 implies ( FP # x is convergent & lim (FP # x) = 0 ) )
assume ASP1: x in E0 ; :: thesis: ( FP # x is convergent & lim (FP # x) = 0 )
D1: for n being Element of NAT holds (FP # x) . n = |.((lim (F2 # x)) - ((F2 # x) . n)).| to_power k

proof

let n be Element of NAT ; :: thesis: (FP # x) . n = |.((lim (F2 # x)) - ((F2 # x) . n)).| to_power k
x in dom (FP . n) by ASP1, A71;
then D0: x in dom (|.(F - (F2 . n)).| to_power k) by A70;
then x in dom |.(F - (F2 . n)).| by MESFUN6C:def 6;
then D3: x in dom (F - (F2 . n)) by VALUED_1:def 11;
thus (FP # x) . n = (FP . n) . x by SEQFUNC:def 11
.= (|.(F - (F2 . n)).| to_power k) . x by A70
.= (|.(F - (F2 . n)).| . x) to_power k by D0, MESFUN6C:def 6
.= |.((F - (F2 . n)) . x).| to_power k by VALUED_1:18
.= |.((F . x) - ((F2 . n) . x)).| to_power k by D3, VALUED_1:13
.= |.((lim (F2 # x)) - ((F2 . n) . x)).| to_power k by A50, ASP1
.= |.((lim (F2 # x)) - ((F2 # x) . n)).| to_power k by SEQFUNC:def 11 ; :: thesis: verum

end;

F2 # x is convergent by ASP1, A59;
hence ( FP # x is convergent & lim (FP # x) = 0 ) by D1, LMSQ5; :: thesis: verum

end;

A77: for x being Element of X st x in dom (lim FP) holds
0 = (lim FP) . x

proof

let x be Element of X; :: thesis: ( x in dom (lim FP) implies 0 = (lim FP) . x )
assume ASP: x in dom (lim FP) ; :: thesis: 0 = (lim FP) . x
then AA1: ( lim (FP # x) = 0 & FP # x is convergent ) by A76, A74;
(lim FP) . x = lim (R_EAL (FP # x)) by ASP, MESFUN7C:14;
hence 0 = (lim FP) . x by AA1, RINFSUP2:14; :: thesis: verum

end;

a.e-eq-class_Lp F,M,k in CosetSet M,k by A67;
then reconsider Sq0 = a.e-eq-class_Lp F,M,k as Point of (Lp-Space M,k) by VSPDef6X;
Y21: for n being Element of NAT holds Ip . n = ||.(Sq0 - (Sq . (N . n))).|| to_power k

proof

let n be Element of NAT ; :: thesis: Ip . n = ||.(Sq0 - (Sq . (N . n))).|| to_power k
set m = N . n;
reconsider n1 = n as Nat ;
B5: FP . n = (abs (F - (F2 . n1))) to_power k by A70;
B6: ( F in Lp_Functions M,k & F in Sq0 ) by A67, EQC01;
( F2 . n1 in Lp_Functions M,k & F2 . n1 in Sq . (N . n) ) by A47;
then (- 1) (#) (F2 . n1) in (- 1) * (Sq . (N . n)) by Lm17Y;
then F - (F2 . n1) in Sq0 + ((- 1) * (Sq . (N . n))) by Lm17Y, B6;
then F - (F2 . n1) in Sq0 - (Sq . (N . n)) by RLVECT_1:29;
then consider r being Real such that
B9: ( 0 <= r & r = Integral M,((abs (F - (F2 . n1))) to_power k) & ||.(Sq0 - (Sq . (N . n))).|| = r to_power (1 / k) ) by Lm17x;
||.(Sq0 - (Sq . (N . n))).|| to_power k = r to_power ((1 / k) * k) by B9, HOLDER_1:2
.= r to_power 1 by XCMPLX_1:107
.= r by POWER:30 ;
hence Ip . n = ||.(Sq0 - (Sq . (N . n))).|| to_power k by B9, B5, A75; :: thesis: verum

end;

deffunc H₉( Element of NAT ) -> Element of REAL = ||.(Sq0 - (Sq . (N . $1))).||;
consider Iq being Real_Sequence such that
Y221: for n being Element of NAT holds Iq . n = H₉(n) from SEQ_1:sch 1();

Y22: now

let n be Nat; :: thesis: Iq . n = ||.(Sq0 - (Sq . (N . n))).||
reconsider n0 = n as Element of NAT by ORDINAL1:def 13;
Iq . n = ||.(Sq0 - (Sq . (N . n0))).|| by Y221;
hence Iq . n = ||.(Sq0 - (Sq . (N . n))).|| ; :: thesis: verum

end;

( Iq is convergent & lim Iq = 0 )

proof

A1a: for n being Element of NAT holds Ip . n >= 0

proof

let n be Element of NAT ; :: thesis: Ip . n >= 0
||.(Sq0 - (Sq . (N . n))).|| to_power k >= 0 by LmPW001, NORMSP_1:8;
hence Ip . n >= 0 by Y21; :: thesis: verum

end;

A3: for n being Element of NAT holds Iq . n = (Ip . n) to_power (1 / k)

proof

let n be Element of NAT ; :: thesis: Iq . n = (Ip . n) to_power (1 / k)
thus (Ip . n) to_power (1 / k) = (||.(Sq0 - (Sq . (N . n))).|| to_power k) to_power (1 / k) by Y21
.= ||.(Sq0 - (Sq . (N . n))).|| to_power (k * (1 / k)) by HOLDER_1:2, NORMSP_1:8
.= ||.(Sq0 - (Sq . (N . n))).|| to_power 1 by XCMPLX_1:107
.= ||.(Sq0 - (Sq . (N . n))).|| by POWER:30
.= Iq . n by Y22 ; :: thesis: verum

end;

hence Iq is convergent by A1a, A76, A75, HOLDER_1:10; :: thesis: lim Iq = 0
lim Iq = (lim Ip) to_power (1 / k) by A76, A75, A1a, A3, HOLDER_1:10;
then lim Iq = 0 to_power (1 / k) by A76, A75, A77, A74, LPSPACE1:22;
hence lim Iq = 0 by POWER:def 2; :: thesis: verum

end;

hence Sq is convergent by A1, Y22, LM005X; :: thesis: verum