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 )
A1: 1 <= k by Def1;
assume A2: Sq is CCauchy ; :: thesis: Sq is convergent
consider Fsq being with_the_same_dom Functional_Sequence of X,REAL such that
A3: 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 Th64;
Fsq . 0 in Lp_Functions (M,k) by A3;
then A4: ex D being Element of S st
( M . (D `) = 0 & dom (Fsq . 0) = D & Fsq . 0 is_measurable_on D ) by Th35;
then reconsider E = dom (Fsq . 0) as Element of S ;
consider N being V162() sequence of NAT such that
A5: for i, j being Element of NAT st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i) by Th66, A2;
deffunc H1( Nat) -> Element of bool [:X,REAL:] = Fsq . (N . $1);
consider F1 being Functional_Sequence of X,REAL such that
A6: for n being Nat holds F1 . n = H1(n) from SEQFUNC:sch 1();
 A7: 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) )
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; :: 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 A8, MESFUNC8:def 2; :: thesis: abs (F1 . n) in Lp_Functions (M,k)
thus abs (F1 . n) in Lp_Functions (M,k) by A9, Th28; :: 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 A7;
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 H2( Nat) -> Element of bool [:X,REAL:] = (F1 . ($1 + 1)) - (F1 . $1);
consider FMF being Functional_Sequence of X,REAL such that
A10: for n being Nat holds FMF . n = H2(n) from SEQFUNC:sch 1();
 A11: 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) )
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; :: 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 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; :: 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 A11;
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;
A13: 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 )
A14: (abs FMF) . n = abs (FMF . n) by SEQFUNC:def 4;
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 )
A15: ( dom (FMF . n) = E & FMF . n in Lp_Functions (M,k) ) by A11;
hence ( dom ((abs FMF) . n) = E & abs ((abs FMF) . n) = (abs FMF) . n ) by A14, 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 A11, A14, Th28; :: 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 Th35;
hence (abs FMF) . n is_measurable_on E by A15, A14, VALUED_1:def 11; :: thesis: verum
end;
reconsider AbsFMF = abs FMF as with_the_same_dom Functional_Sequence of X,REAL by Th70;
deffunc H3( Nat) -> Element of bool [:X,REAL:] = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . $1);
consider G being Functional_Sequence of X,REAL such that
A16: for n being Nat holds G . n = H3(n) from SEQFUNC:sch 1();
 A17: 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 )
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_measurable_on E ) by A13, Th67, Th68, MESFUN9C:16;
A21: dom (AbsFMF . 0) = E by A13;
A22: ( F1 . 0 in Lp_Functions (M,k) & dom (F1 . 0) = E & F1 . 0 is_measurable_on E ) by A7;
then ( abs (F1 . 0) in Lp_Functions (M,k) & abs (F1 . 0) is nonnegative & abs (F1 . 0) is_measurable_on E ) by Th28, 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 A19, A22, A21, A18, A20, Th14, Th25, MESFUNC6:26, MESFUNC6:56; :: thesis: verum
end;
deffunc H4( Nat) -> Element of bool [:X,REAL:] = (G . $1) to_power k;
consider Gp being Functional_Sequence of X,REAL such that
A23: for n being Nat holds Gp . n = H4(n) from SEQFUNC:sch 1();
 A24: 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 )
A25: G . n is nonnegative by A17;
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 A17;
hence (G . n) to_power k is_measurable_on E by A25, MESFUN6C:29; :: thesis: verum
end;
reconsider ExtGp = R_EAL Gp as Functional_Sequence of X,ExtREAL ;
A26: 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 A23;
then dom (ExtGp . n) = dom (G . n) by MESFUN6C:def 4;
hence dom (ExtGp . n) = E by A17; :: thesis: ( ExtGp . n is_measurable_on E & ExtGp . n is nonnegative )
(G . n) to_power k is_measurable_on E by A24;
then R_EAL ((G . n) to_power k) is_measurable_on E by MESFUNC6:def 1;
hence ExtGp . n is_measurable_on E by A23; :: thesis: ExtGp . n is nonnegative
(G . n) to_power k is nonnegative by A24;
hence ExtGp . n is nonnegative by A23; :: thesis: verum
end;
then A27: ( 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 A26;
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;
A28: 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 A29: 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 A30: x in E ; :: thesis: (ExtGp . n) . x <= (ExtGp . m) . x
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 Th69, 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 (ExtGp . n) . x <= (ExtGp . m) . x by A32, A33, A34, HOLDER_1:3; :: thesis: verum
end;
A35: for x being Element of X st x in E holds
ExtGp # x is V164()
proof
let x be Element of X; :: thesis: ( x in E implies ExtGp # x is V164() )
assume A36: x in E ; :: thesis: ExtGp # x is V164()
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 A28, A36;
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 V164() by RINFSUP2:7; :: thesis: verum
end;
A37: 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 V164() by A35;
hence ExtGp # x is convergent by RINFSUP2:37; :: thesis: verum
end;
then consider I being ExtREAL_sequence such that
A38: ( ( for n being 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 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
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; :: thesis: verum
end;
then rng I c= REAL by TARSKI:def 3;
then reconsider Ir = I as Function of NAT,REAL by FUNCT_2:6;
deffunc H5( Nat) -> Element of ExtREAL = Integral (M,((AbsFMF . $1) to_power k));
A42: for x being Element of NAT holds H5(x) is Element of REAL
proof
let x be Element of NAT ; :: thesis: H5(x) is Element of REAL
AbsFMF . x in Lp_Functions (M,k) by A13;
then Integral (M,((abs (AbsFMF . x)) to_power k)) in REAL by Th49;
hence H5(x) is Element of REAL by A13; :: thesis: verum
end;
consider KPAbsFMF being Function of NAT,REAL such that
A43: for x being Element of NAT holds KPAbsFMF . x = H5(x) from FUNCT_2:sch 9(A42);
 deffunc H6( Nat) -> Element of REAL = (KPAbsFMF . $1) to_power (1 / k);
A44: for x being Element of NAT holds H6(x) is Element of REAL ;
consider PAbsFMF being Function of NAT,REAL such that
A45: for x being Element of NAT holds PAbsFMF . x = H6(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 H7( Element of NAT ) -> Element of REAL = (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . $1);
A46: for x being Element of NAT holds H7(x) is Element of REAL ;
consider QAbsFMF being Function of NAT,REAL such that
A47: for x being Element of NAT holds QAbsFMF . x = H7(x) from FUNCT_2:sch 9(A46);
 A48: for n being Element of NAT holds (Ir . n) to_power (1 / k) <= QAbsFMF . n
proof
defpred S1[ 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: S1[ 0 ] by A1, A49, A51, A52, A53, Th62;
A55: now
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; :: thesis: S1[n + 1]
then A56: ((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 A57: G . (n + 1) = (G . n) + (AbsFMF . (n + 1)) by A16;
A58: ( 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 A59: KPAbsFMF . (n + 1) = Integral (M,((abs (AbsFMF . (n + 1))) to_power k)) by A13;
A60: 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 A57, A17;
then (Ir . (n + 1)) to_power (1 / k) <= ((Ir . n) to_power (1 / k)) + (PAbsFMF . (n + 1)) by A1, A58, A59, A60, Th62;
then A61: (Ir . (n + 1)) to_power (1 / k) <= (QAbsFMF . n) + (PAbsFMF . (n + 1)) by A56, XXREAL_0:2;
(QAbsFMF . n) + (PAbsFMF . (n + 1)) = ((RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . n)) + (PAbsFMF . (n + 1)) by A47
.= (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 S1[n + 1] by A61, A47; :: thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A54, A55);
 hence for n being Element of NAT holds (Ir . n) to_power (1 / k) <= QAbsFMF . n ; :: thesis: verum
end;
A62: 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);
A63: ( F1 . (n + 1) = Fsq . (N . (n + 1)) & F1 . n = Fsq . (N . n) ) by A6;
AbsFMF . n = abs (FMF . n) by SEQFUNC:def 4;
then A64: AbsFMF . n = abs ((Fsq . (N . (n + 1))) - (Fsq . (N . n))) by A63, A10;
A65: ( 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 A3;
then (- 1) (#) (Fsq . (N . n)) in (- 1) * (Sq . (N . n)) by Th55;
then (Fsq . (N . (n + 1))) - (Fsq . (N . n)) in (Sq . (N . (n + 1))) + ((- 1) * (Sq . (N . n))) by Th55, A65;
then (Fsq . (N . (n + 1))) - (Fsq . (N . n)) in (Sq . (N . (n + 1))) - (Sq . (N . n)) by RLVECT_1:16;
then A66: 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 Th54;
PAbsFMF . n = (KPAbsFMF . n) to_power (1 / k) by A45;
hence PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).|| by A66, A64, A43; :: thesis: verum
end;
1 / 2 < 1 ;
then abs (1 / 2) < 1 by ABSVALUE:def 1;
then A67: ( (1 / 2) GeoSeq is summable & Sum ((1 / 2) GeoSeq) = 1 / (1 - (1 / 2)) ) by SERIES_1:24;
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 )
A68: PAbsFMF . n = ||.((Sq . (N . (n + 1))) - (Sq . (N . n))).|| by A62;
hence 0 <= PAbsFMF . n ; :: 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:41 ;
then A69: ((1 / 2) GeoSeq) . n = 2 to_power (- n) by POWER:32;
N is Real_Sequence by FUNCT_2:7;
then N . n < N . (n + 1) by SEQM_3:def 6;
hence PAbsFMF . n <= ((1 / 2) GeoSeq) . n by A5, A68, A69; :: thesis: verum
end;
then ( PAbsFMF is summable & Sum PAbsFMF <= Sum ((1 / 2) GeoSeq) ) by A67, SERIES_1:20;
then Partial_Sums PAbsFMF is convergent by SERIES_1:def 2;
then Partial_Sums PAbsFMF is bounded ;
then consider Br being real number such that
A70: 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 A48;
then A71: (Ir . n) to_power (1 / k) <= (RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . n) by A47;
(RF0 to_power (1 / k)) + ((Partial_Sums PAbsFMF) . n) < (RF0 to_power (1 / k)) + Br by A70, XREAL_1:8;
then A72: (Ir . n) to_power (1 / k) < (RF0 to_power (1 / k)) + Br by A71, XXREAL_0:2;
Ir . n = Integral (M,(Gp . n)) by A38;
then Ir . n = Integral (M,((G . n) to_power k)) by A23;
then A73: Ir . n = Integral (M,((abs (G . n)) to_power k)) by A17;
A74: G . n in Lp_Functions (M,k) by A17;
then 0 <= (Ir . n) to_power (1 / k) by Th49, A73, Th4;
then ((Ir . n) to_power (1 / k)) to_power k < ((RF0 to_power (1 / k)) + Br) to_power k by A72, Th3;
then (Ir . n) to_power ((1 / k) * k) < ((RF0 to_power (1 / k)) + Br) to_power k by A74, Th49, A73, HOLDER_1:2;
then (Ir . n) to_power 1 < ((RF0 to_power (1 / k)) + Br) to_power k by XCMPLX_1:106;
hence Ir . n < ((RF0 to_power (1 / k)) + Br) to_power k by POWER:25; :: thesis: verum
end;
then A75: 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 A76: for x being Element of X st x in E holds
(ExtGp . n) . x <= (ExtGp . m) . x by A28;
A77: ( ExtGp . n is_measurable_on E & ExtGp . m is_measurable_on E & ExtGp . n is nonnegative & ExtGp . m is nonnegative ) by A26;
A78: ( dom (ExtGp . n) = E & dom (ExtGp . m) = E ) by A26;
then A79: ( (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 Ir . n <= Ir . m by A76, A78, A77, A79, MESFUNC9:15; :: thesis: verum
end;
then Ir is V164() by SEQM_3:6;
then A80: ( I is convergent_to_finite_number & lim I = lim Ir ) by A75, RINFSUP2:14;
reconsider LExtGp = lim ExtGp as PartFunc of X,ExtREAL ;
A81: ( E = dom LExtGp & LExtGp is_measurable_on E ) by A26, A27, A37, MESFUNC8:25, MESFUNC8:def 9;
A82: 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 A83: x in dom LExtGp ; :: thesis: 0 <= LExtGp . x
then reconsider x1 = x as Element of X ;
A84: x1 in E by A27, A83, MESFUNC8:def 9;
now
let k1 be Nat; :: thesis: 0 <= (ExtGp # x1) . k1
reconsider k = k1 as Element of NAT by ORDINAL1:def 12;
ExtGp # x1 is V164() by A35, A84;
then A85: (ExtGp # x1) . 0 <= (ExtGp # x1) . k by RINFSUP2:7;
0 <= (ExtGp . 0) . x1 by A27, SUPINF_2:39;
hence 0 <= (ExtGp # x1) . k1 by A85, MESFUNC5:def 13; :: thesis: verum
end;
then 0 <= lim (ExtGp # x1) by A84, A37, MESFUNC9:10;
hence 0 <= LExtGp . x by A83, MESFUNC8:def 9; :: thesis: verum
end;
A86: eq_dom (LExtGp,+infty) = E /\ (eq_dom (LExtGp,+infty)) by A81, RELAT_1:132, XBOOLE_1:28;
then reconsider EE = eq_dom (LExtGp,+infty) as Element of S by A81, MESFUNC1:33;
reconsider E0 = E \ EE as Element of S ;
E0 ` = (X \ E) \/ (X /\ EE) by XBOOLE_1:52;
then A87: E0 ` = (E `) \/ EE by XBOOLE_1:28;
M . EE = 0 by A38, A80, A81, A82, A86, MESFUNC9:13, SUPINF_2:52;
then A88: 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 A87, A88, MEASURE1:37;
then A89: M . (E0 `) = 0 by MEASURE1:def 7;
A90: 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 A81, A82, MESFUNC1:def 15;
hence LExtGp . x in REAL by XXREAL_0:14; :: thesis: verum
end;
A91: 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 A92: x in E0 ; :: thesis: ( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) )
then A93: x in E by XBOOLE_0:def 5;
then LExtGp . x = lim (ExtGp # x) by A81, MESFUNC8:def 9;
then A94: lim (ExtGp # x) in REAL by A90, A92;
ExtGp # x is convergent by A37, A93;
then A95: 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 A94, MESFUNC5:def 12;
ExtGp # x = Gp # x by MESFUN7C:1;
hence ( Gp # x is convergent & lim (Gp # x) = lim (ExtGp # x) ) by A95, RINFSUP2:15; :: thesis: verum
end;
A96: 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 A97: 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 A97, XBOOLE_0:def 5;
then x in dom (G . n) by A17;
then A98: x in dom ((G . n) to_power k) by MESFUN6C:def 4;
(Gp # x) . n = (Gp . n) . x by SEQFUNC:def 10
.= ((G . n) to_power k) . x by A23
.= ((G . n) . x) to_power k by A98, MESFUN6C:def 4 ;
hence (Gp # x) . n = ((G # x) . n) to_power k by SEQFUNC:def 10; :: thesis: verum
end;
end;
A99: 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 A100: x in E0 ; :: thesis: (Partial_Sums AbsFMF) # x is convergent
then A101: Gp # x is convergent by A91;
A102: now
let n be Element of NAT ; :: thesis: 0 <= (G # x) . n
G . n is nonnegative by A17;
then 0 <= (G . n) . x by MESFUNC6:51;
hence 0 <= (G # x) . n by SEQFUNC:def 10; :: thesis: verum
end;
for n being Element of NAT holds (Gp # x) . n = ((G # x) . n) to_power k by A100, A96;
then A103: G # x is convergent by A101, A102, Th9;
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
A104: for m being Element of NAT st n <= m holds
abs (((G # x) . m) - ((G # x) . n)) < s by A103, SEQ_4:41;
now
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)) < s )
assume A105: n <= m ; :: thesis: abs ((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)) < s
x in E by A100, XBOOLE_0:def 5;
then A106: ( x in dom (G . n) & x in dom (G . m) ) by A17;
( G . m = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . m) & G . n = (abs (F1 . 0)) + ((Partial_Sums AbsFMF) . n) ) by A16;
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 A106, 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 10;
then A107: ((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 10;
hence abs ((((Partial_Sums AbsFMF) # x) . m) - (((Partial_Sums AbsFMF) # x) . n)) < s by A104, A105, A107; :: 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:41; :: thesis: verum
end;
A108: 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 A109: x in E by XBOOLE_0:def 5;
defpred S1[ 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 10
.= (abs (FMF . 0)) . x by VALUED_1:18
.= (AbsFMF . 0) . x by SEQFUNC:def 4
.= ((Partial_Sums AbsFMF) . 0) . x by MESFUN9C:def 2
.= ((Partial_Sums AbsFMF) # x) . 0 by SEQFUNC:def 10 ;
then A110: S1[ 0 ] ;
A111: now
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A112: S1[n] ; :: thesis: S1[n + 1]
A113: (Partial_Sums AbsFMF) . (n + 1) = ((Partial_Sums AbsFMF) . n) + (AbsFMF . (n + 1)) by MESFUN9C:def 2;
dom (AbsFMF . 0) = E by A13;
then A114: x in dom ((Partial_Sums AbsFMF) . (n + 1)) by A109, MESFUN9C:11;
A115: (abs (FMF # x)) . (n + 1) = abs ((FMF # x) . (n + 1)) by VALUED_1:18
.= abs ((FMF . (n + 1)) . x) by SEQFUNC:def 10
.= (abs (FMF . (n + 1))) . x by VALUED_1:18
.= (AbsFMF . (n + 1)) . x by SEQFUNC:def 4 ;
(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 A112, A115, SEQFUNC:def 10
.= ((Partial_Sums AbsFMF) . (n + 1)) . x by A113, A114, VALUED_1:def 1
.= ((Partial_Sums AbsFMF) # x) . (n + 1) by SEQFUNC:def 10 ;
hence S1[n + 1] ; :: thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A110, A111);
 hence Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x by FUNCT_2:63; :: thesis: verum
end;
A116: 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 A117: x in E by XBOOLE_0:def 5;
defpred S1[ Nat] means (F1 # x) . ($1 + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . $1);
dom (FMF . 0) = E by A11;
then A118: x in dom ((F1 . (0 + 1)) - (F1 . 0)) by A10, A117;
(Partial_Sums (FMF # x)) . 0 = (FMF # x) . 0 by SERIES_1:def 1
.= (FMF . 0) . x by SEQFUNC:def 10
.= ((F1 . (0 + 1)) - (F1 . 0)) . x by A10 ;
then A119: (Partial_Sums (FMF # x)) . 0 = ((F1 . (0 + 1)) . x) - ((F1 . 0) . x) by A118, VALUED_1:13;
((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . 0) = ((F1 . 0) . x) + ((Partial_Sums (FMF # x)) . 0) by SEQFUNC:def 10;
then A120: S1[ 0 ] by A119, SEQFUNC:def 10;
A121: now
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A122: S1[n] ; :: thesis: S1[n + 1]
dom (FMF . (n + 1)) = E by A11;
then A123: x in dom ((F1 . ((n + 1) + 1)) - (F1 . (n + 1))) by A10, A117;
(FMF # x) . (n + 1) = (FMF . (n + 1)) . x by SEQFUNC:def 10
.= ((F1 . ((n + 1) + 1)) - (F1 . (n + 1))) . x by A10 ;
then A124: (FMF # x) . (n + 1) = ((F1 . ((n + 1) + 1)) . x) - ((F1 . (n + 1)) . x) by A123, 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 A122, SEQFUNC:def 10 ;
hence S1[n + 1] by A124, SEQFUNC:def 10; :: thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A120, A121);
 hence for n being Element of NAT holds (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n) ; :: thesis: verum
end;
A125: 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 A126: x in E0 ; :: thesis: F1 # x is convergent
then Partial_Sums (abs (FMF # x)) = (Partial_Sums AbsFMF) # x by A108;
then Partial_Sums (abs (FMF # x)) is convergent by A126, A99;
then abs (FMF # x) is summable by SERIES_1:def 2;
then FMF # x is absolutely_summable by SERIES_1:def 4;
then FMF # x is summable by SERIES_1:35;
then A127: 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
A128: for m being Element of NAT st n <= m holds
abs (((Partial_Sums (FMF # x)) . m) - ((Partial_Sums (FMF # x)) . n)) < s by A127, SEQ_4:41;
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 A129: 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 A129, NAT_1:21, XXREAL_0:2;
(n + 1) - 1 <= m1 - 1 by A129, XREAL_1:9;
then A130: abs (((Partial_Sums (FMF # x)) . m) - ((Partial_Sums (FMF # x)) . n)) < s by A128;
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 A116, A126;
hence abs (((F1 # x) . m1) - ((F1 # x) . (n + 1))) < s by A130; :: 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:41; :: thesis: verum
end;
set F2 = F1 || E0;
A131: 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 A132: x in E0 ; :: thesis: (F1 || E0) # x is convergent
then F1 # x is convergent by A125;
hence (F1 || E0) # x is convergent by A132, MESFUN9C:1; :: thesis: verum
end;
A133: 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 A134: 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 10
.= ((F1 . n) | E0) . x by MESFUN9C:def 1
.= (F1 . n) . x by A134, FUNCT_1:49 ;
hence ((F1 || E0) # x) . n = (F1 # x) . n by SEQFUNC:def 10; :: thesis: verum
end;
hence (F1 || E0) # x = F1 # x by FUNCT_2:63; :: thesis: verum
end;
A135: 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 )
A136: dom (F1 . 0) = E by A7;
dom ((F1 || E0) . n) = dom ((F1 . n) | E0) by MESFUN9C:def 1;
then dom ((F1 || E0) . n) = (dom (F1 . n)) /\ E0 by RELAT_1:61;
then dom ((F1 || E0) . n) = E /\ E0 by A7;
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 A7;
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 A136, 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;
A137: 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 Th13;
then A138: ((abs (F1 . n1)) to_power k) | E0 = (abs (F2 . n1)) to_power k by Th20;
A139: ( F2 . n1 is_measurable_on E0 & dom (F2 . n1) = E0 ) by A135;
F1 . n1 in Lp_Functions (M,k) by A7;
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 A138, MESFUNC6:91;
hence A140: F2 . n1 in Lp_Functions (M,k) by A139, A89; :: thesis: F2 . n1 in Sq . (N . n1)
reconsider n = n1 as Element of NAT by ORDINAL1:def 12;
set m = N . n;
F1 . n = Fsq . (N . n) by A6;
then A141: ( F1 . n in Sq . (N . n) & Sq . (N . n) = a.e-eq-class_Lp ((F1 . n),M,k) ) by A3;
reconsider EB = E0 ` as Element of S by MEASURE1:34;
(F2 . n) | (EB `) = F2 . n by A139, RELAT_1:68;
then (F2 . n) | (EB `) = (F1 . n) | (EB `) by MESFUN9C:def 1;
then F2 . n a.e.= F1 . n,M by A89, LPSPACE1:def 10;
hence F2 . n1 in Sq . (N . n1) by A140, A141, Th36; :: thesis: verum
end;
A142: dom (lim F2) = dom (F2 . 0) by MESFUNC8:def 9;
then A143: dom (lim F2) = E0 by A135;
A144: 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 A143, A131, 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
A145: ( x in dom (lim F2) & y = (lim F2) . x ) by PARTFUN1:3;
y = lim (F2 # x) by A145, A143, A144;
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 A142, RELSET_1:4;
A146: dom (LExtGp | E0) = E /\ E0 by A81, RELAT_1:61;
then A147: 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
A148: ( x in dom (LExtGp | E0) & y = (LExtGp | E0) . x ) by PARTFUN1:3;
y = LExtGp . x by A147, A148, FUNCT_1:49;
hence y in REAL by A147, A148, A90; :: thesis: verum
end;
then rng (LExtGp | E0) c= REAL by TARSKI:def 3;
then reconsider gp = LExtGp | E0 as PartFunc of X,REAL by A146, RELSET_1:4;
A149: 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 A150: x in E0 ; :: thesis: gp . x = lim (Gp # x)
then x in dom LExtGp by A81, XBOOLE_0:def 5;
then LExtGp . x = lim (ExtGp # x) by MESFUNC8:def 9;
then gp . x = lim (ExtGp # x) by A150, FUNCT_1:49;
hence gp . x = lim (Gp # x) by A91, A150; :: thesis: verum
end;
LExtGp is nonnegative by A82, SUPINF_2:52;
then LExtGp is_integrable_on M by A80, A38, A81, Th2;
then R_EAL gp is_integrable_on M by MESFUNC5:97;
then A151: gp is_integrable_on M by MESFUNC6:def 4;
A152: dom (F2 . 0) = E0 by A135;
then A153: dom F = E0 by MESFUNC8:def 9;
then A154: E0 = dom (abs F) by VALUED_1:def 11;
then A155: E0 = dom ((abs F) to_power k) by MESFUN6C:def 4;
A156: 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 A157: 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 A158: x in dom (G . n) by A17;
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 A158, VALUED_1:def 1;
then A159: (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 10
.= (abs ((F1 . 0) . x)) + (((Partial_Sums AbsFMF) # x) . n) by A159, SEQFUNC:def 10
.= (abs ((F1 # x) . 0)) + (((Partial_Sums AbsFMF) # x) . n) by SEQFUNC:def 10 ;
then A160: (G # x) . n = (abs ((F1 # x) . 0)) + ((Partial_Sums (abs (FMF # x))) . n) by A108, A157;
abs ((Partial_Sums (FMF # x)) . n) <= (Partial_Sums (abs (FMF # x))) . n by Lm1;
hence (abs ((F1 # x) . 0)) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by A160, XREAL_1:6; :: thesis: verum
end;
A161: 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 A162: x in E0 ; :: thesis: (abs (((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n))) to_power k <= (Gp # x) . n
then A163: (Gp # x) . n = ((G # x) . n) to_power k by A96;
A164: (abs ((F1 # x) . 0)) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by A156, A162;
abs (((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)) <= (abs ((F1 # x) . 0)) + (abs ((Partial_Sums (FMF # x)) . n)) by COMPLEX1:56;
then A165: abs (((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by A164, XXREAL_0:2;
0 <= abs (((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n)) by COMPLEX1:46;
hence (abs (((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n))) to_power k <= (Gp # x) . n by A163, A165, HOLDER_1:3; :: thesis: verum
end;
A166: 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 A167: x in E0 ; :: thesis: (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n
then A168: F1 # x = F2 # x by A133;
per cases ( n = 0 or n <> 0 ) ;
suppose A169: n = 0 ; :: thesis: (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n
A170: (Gp # x) . n = ((G # x) . n) to_power k by A167, A96;
A171: (abs ((F1 # x) . 0)) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by A156, A167;
0 <= abs ((Partial_Sums (FMF # x)) . n) by COMPLEX1:46;
then 0 + (abs ((F1 # x) . 0)) <= (abs ((F1 # x) . 0)) + (abs ((Partial_Sums (FMF # x)) . n)) by XREAL_1:6;
then A172: abs ((F1 # x) . 0) <= (G # x) . n by A171, XXREAL_0:2;
0 <= abs ((F1 # x) . 0) by COMPLEX1:46;
hence (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n by A168, A169, A170, A172, 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
A173: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
(F1 # x) . (m + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . m) by A116, A167;
then A174: (abs ((F1 # x) . (m + 1))) to_power k <= (Gp # x) . m by A161, A167;
x in E by A167, XBOOLE_0:def 5;
then A175: ExtGp # x is V164() by A35;
m <= m + 1 by NAT_1:11;
then A176: (ExtGp # x) . m <= (ExtGp # x) . (m + 1) by A175, RINFSUP2:7;
ExtGp # x = Gp # x by MESFUN7C:1;
hence (abs ((F2 # x) . n)) to_power k <= (Gp # x) . n by A168, A173, A174, A176, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A177: 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 A178: x in E0 ; :: thesis: abs (((abs F) to_power k) . x) <= gp . x
then A179: Gp # x is convergent by A91;
deffunc H8( set ) -> Element of REAL = ((abs (F2 # x)) . $1) to_power k;
consider s being Real_Sequence such that
A180: for n being Element of NAT holds s . n = H8(n) from SEQ_1:sch 1();
 A181: gp . x = lim (Gp # x) by A149, A178;
A182: ((abs F) to_power k) . x = ((abs F) . x) to_power k by A155, A178, MESFUN6C:def 4
.= (abs (F . x)) to_power k by A154, A178, VALUED_1:def 11
.= (abs (lim (F2 # x))) to_power k by A178, A144
.= (lim (abs (F2 # x))) to_power k by A131, A178, SEQ_4:14 ;
A183: now
let n be Element of NAT ; :: thesis: 0 <= (abs (F2 # x)) . n
0 <= abs ((F2 # x) . n) by COMPLEX1:46;
hence 0 <= (abs (F2 # x)) . n by VALUED_1:18; :: thesis: verum
end;
abs (F2 # x) is convergent by A178, A131, SEQ_4:13;
then A184: ( s is convergent & (lim (abs (F2 # x))) to_power k = lim s ) by A183, A180, 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 A166, A178;
then ((abs (F2 # x)) . n) to_power k <= (Gp # x) . n by VALUED_1:18;
hence s . n <= (Gp # x) . n by A180; :: thesis: verum
end;
then A185: ((abs F) to_power k) . x <= gp . x by A184, A181, A182, A179, SEQ_2:18;
0 <= ((abs F) to_power k) . x by MESFUNC6:51;
hence abs (((abs F) to_power k) . x) <= gp . x by A185, ABSVALUE:def 1; :: thesis: verum
end;
R_EAL F is_measurable_on E0 by A135, A152, A131, MESFUN7C:21;
then A186: F is_measurable_on E0 by MESFUNC6:def 1;
then A187: abs F is_measurable_on E0 by A153, MESFUNC6:48;
dom (abs F) = E0 by A153, VALUED_1:def 11;
then (abs F) to_power k is_measurable_on E0 by A187, MESFUN6C:29;
then (abs F) to_power k is_integrable_on M by A147, A151, A155, A177, MESFUNC6:96;
then A188: F in Lp_Functions (M,k) by A89, A153, A186;
A189: 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 A190: ( 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 A191: m1 = 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1
now
per cases ( n1 = 0 or n1 <> 0 ) ;
suppose A192: n1 = 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1
(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)).| to_power k <= (Gp # x) . n1 by A191, A192, COMPLEX1:44, 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
A193: n1 = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A194: (F1 # x) . (n + 1) = ((F1 # x) . 0) + ((Partial_Sums (FMF # x)) . n) by A190, A116;
A195: (abs ((F1 # x) . 0)) + (abs ((Partial_Sums (FMF # x)) . n)) <= (G # x) . n by A156, A190;
0 <= abs ((F1 # x) . 0) by COMPLEX1:46;
then (abs ((Partial_Sums (FMF # x)) . n)) + 0 <= (abs ((F1 # x) . 0)) + (abs ((Partial_Sums (FMF # x)) . n)) by XREAL_1:6;
then A196: abs ((Partial_Sums (FMF # x)) . n) <= (G # x) . n by A195, XXREAL_0:2;
0 <= abs ((Partial_Sums (FMF # x)) . n) by COMPLEX1:46;
then A197: |.((Partial_Sums (FMF # x)) . n).| to_power k <= ((G # x) . n) to_power k by A196, HOLDER_1:3;
A198: (Gp # x) . n = ((G # x) . n) to_power k by A190, A96;
x in E by A190, XBOOLE_0:def 5;
then A199: ExtGp # x is V164() by A35;
n <= n + 1 by NAT_1:11;
then A200: (ExtGp # x) . n <= (ExtGp # x) . (n + 1) by A199, RINFSUP2:7;
ExtGp # x = Gp # x by MESFUN7C:1;
hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 by A191, A193, A200, A197, A198, A194, 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 A201: m1 <> 0 ; :: thesis: |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1
then consider m being Nat such that
A202: m1 = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
0 < n1 by A190, A201;
then consider n being Nat such that
A203: n1 = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A204: m1 - 1 <= n1 - 1 by A190, XREAL_1:9;
x in E by A190, XBOOLE_0:def 5;
then A205: x in dom (G . n) by A17;
then A206: 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 A207: (Gp # x) . n = ((G . n) . x) to_power k by A206, 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 A205, VALUED_1:def 1
.= (abs ((F1 . 0) . x)) + (((Partial_Sums AbsFMF) . n) . x) by VALUED_1:18 ;
then A208: (G . n) . x = (abs ((F1 . 0) . x)) + (((Partial_Sums AbsFMF) # x) . n) by SEQFUNC:def 10;
A209: ( (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 A190, A116;
A210: |.(((Partial_Sums (FMF # x)) . n) - ((Partial_Sums (FMF # x)) . m)).| <= (Partial_Sums (abs (FMF # x))) . n by Th10, A202, A203, A204;
A211: (Partial_Sums (abs (FMF # x))) . n = ((Partial_Sums AbsFMF) # x) . n by A108, A190;
0 <= abs ((F1 . 0) . x) by COMPLEX1:46;
then 0 + ((Partial_Sums (abs (FMF # x))) . n) <= (abs ((F1 . 0) . x)) + (((Partial_Sums AbsFMF) # x) . n) by A211, XREAL_1:6;
then A212: |.(((F1 # x) . (n + 1)) - ((F1 # x) . (m + 1))).| <= (G . n) . x by A208, A209, A210, XXREAL_0:2;
0 <= |.(((F1 # x) . (n + 1)) - ((F1 # x) . (m + 1))).| by COMPLEX1:46;
then A213: |.(((F1 # x) . (n + 1)) - ((F1 # x) . (m + 1))).| to_power k <= (Gp # x) . n by A207, A212, HOLDER_1:3;
x in E by A190, XBOOLE_0:def 5;
then A214: ExtGp # x is V164() by A35;
n <= n + 1 by NAT_1:11;
then A215: (ExtGp # x) . n <= (ExtGp # x) . (n + 1) by A214, RINFSUP2:7;
ExtGp # x = Gp # x by MESFUN7C:1;
hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 by A202, A203, A215, A213, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence |.(((F1 # x) . n1) - ((F1 # x) . m1)).| to_power k <= (Gp # x) . n1 ; :: thesis: verum
end;
A216: 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 A217: x in E0 ; :: thesis: |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x
then A218: Gp # x is convergent by A91;
A219: F1 # x = F2 # x by A133, A217;
A220: F2 # x is convergent by A217, A131;
reconsider n = n1 as Element of NAT by ORDINAL1:def 12;
deffunc H8( Element of NAT ) -> Element of REAL = ((F2 # x) . $1) - ((F2 # x) . n);
consider s0 being Real_Sequence such that
A221: for j being Element of NAT holds s0 . j = H8(j) from SEQ_1:sch 1();
A222: 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
A223: for m being Element of NAT st n1 <= m holds
abs (((F2 # x) . m) - (lim (F2 # x))) < p by A220, 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 A224: 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 A221;
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 A224, A223; :: thesis: verum
end;
end;
then A225: s0 is convergent by SEQ_2:def 6;
then lim s0 = (lim (F2 # x)) - ((F2 # x) . n) by A222, SEQ_2:def 7;
then A226: lim (abs s0) = abs ((lim (F2 # x)) - ((F2 # x) . n)) by A225, SEQ_4:14;
A227: abs s0 is convergent by A225;
deffunc H9( Element of NAT ) -> Element of REAL = |.(((F2 # x) . $1) - ((F2 # x) . n)).| to_power k;
consider s being Real_Sequence such that
A228: for j being Element of NAT holds s . j = H9(j) from SEQ_1:sch 1();
 A229: 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 A219, A217, A189;
hence s . j <= (Gp # x) . j by A228; :: thesis: verum
end;
A230: now
let n be Element of NAT ; :: thesis: 0 <= (abs s0) . n
0 <= abs (s0 . n) by COMPLEX1:46;
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 A228
.= (abs (s0 . j)) to_power k by A221
.= ((abs s0) . j) to_power k by VALUED_1:18 ; :: thesis: verum
end;
then A231: ( s is convergent & lim s = (lim (abs s0)) to_power k ) by A230, A227, HOLDER_1:10;
then A232: ( s ^\ n is convergent & lim (s ^\ n) = lim s ) by SEQ_4:20;
gp . x = lim (Gp # x) by A149, A217;
then A233: ( (Gp # x) ^\ n is convergent & lim ((Gp # x) ^\ n) = gp . x ) by A218, SEQ_4:20;
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 A229, NAT_1:11; :: thesis: verum
end;
then lim s <= gp . x by A232, A233, SEQ_2:18;
hence |.((F . x) - ((F2 # x) . n1)).| to_power k <= gp . x by A226, A231, A144, A217; :: thesis: verum
end;
deffunc H8( Nat) -> Element of bool [:X,REAL:] = |.(F - (F2 . $1)).| to_power k;
consider FP being Functional_Sequence of X,REAL such that
A234: for n being Nat holds FP . n = H8(n) from SEQFUNC:sch 1();
 A235: 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 12;
A236: dom (F2 . n) = E0 by A135;
dom (FP . n1) = dom ((abs (F - (F2 . n))) to_power k) by A234;
then dom (FP . n1) = dom (abs (F - (F2 . n))) by MESFUN6C:def 4;
then dom (FP . n1) = dom (F - (F2 . n)) by VALUED_1:def 11;
then dom (FP . n1) = E0 /\ E0 by A236, A143, VALUED_1:12;
hence dom (FP . n1) = E0 ; :: thesis: verum
end;
then A237: E0 = dom (FP . 0) ;
then A238: dom (lim FP) = E0 by MESFUNC8:def 9;
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 A235
.= dom (FP . m) by A235 ; :: thesis: verum
end;
then reconsider FP = FP as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2;
A239: 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 12;
dom (F2 . n) = E0 by A135;
then A240: dom (F - (F2 . n)) = E0 /\ E0 by A143, VALUED_1:12;
( F2 . n is_measurable_on E0 & dom (F2 . n) = E0 ) by A135;
then F - (F2 . n) is_measurable_on E0 by A186, MESFUNC6:29;
then A241: abs (F - (F2 . n)) is_measurable_on E0 by A240, MESFUNC6:48;
dom (abs (F - (F2 . n))) = E0 by A240, VALUED_1:def 11;
then (abs (F - (F2 . n))) to_power k is_measurable_on E0 by A241, MESFUN6C:29;
hence FP . n1 is_measurable_on E0 by A234; :: 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 12;
assume A242: x in E0 ; :: thesis: |.(FP . n1).| . x <= gp . x
then A243: x in dom (FP . n) by A235;
then x in dom (|.(F - (F2 . n)).| to_power k) by A234;
then x in dom |.(F - (F2 . n)).| by MESFUN6C:def 4;
then A244: x in dom (F - (F2 . n)) by VALUED_1:def 11;
A245: FP . n1 = |.(F - (F2 . n1)).| to_power k by A234;
A246: 0 <= |.((F . x) - ((F2 . n1) . x)).| to_power k by Th4, COMPLEX1:46;
|.(FP . n).| . x = |.((FP . n) . x).| by VALUED_1:18
.= |.((|.(F - (F2 . n1)).| . x) to_power k).| by A243, A245, MESFUN6C:def 4
.= |.(|.((F - (F2 . n1)) . x).| to_power k).| by VALUED_1:18
.= |.(|.((F . x) - ((F2 . n1) . x)).| to_power k).| by A244, VALUED_1:13
.= |.((F . x) - ((F2 . n1) . x)).| to_power k by A246, ABSVALUE:def 1
.= |.((F . x) - ((F2 # x) . n)).| to_power k by SEQFUNC:def 10 ;
hence |.(FP . n1).| . x <= gp . x by A216, A242; :: thesis: verum
end;
then consider Ip being Real_Sequence such that
A247: ( ( 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 A147, A151, A237, A239, MESFUN9C:48;
A248: 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 A249: x in E0 ; :: thesis: ( FP # x is convergent & lim (FP # x) = 0 )
A250: 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 A249, A235;
then A251: x in dom (|.(F - (F2 . n)).| to_power k) by A234;
then x in dom |.(F - (F2 . n)).| by MESFUN6C:def 4;
then A252: x in dom (F - (F2 . n)) by VALUED_1:def 11;
thus (FP # x) . n = (FP . n) . x by SEQFUNC:def 10
.= (|.(F - (F2 . n)).| to_power k) . x by A234
.= (|.(F - (F2 . n)).| . x) to_power k by A251, MESFUN6C:def 4
.= |.((F - (F2 . n)) . x).| to_power k by VALUED_1:18
.= |.((F . x) - ((F2 . n) . x)).| to_power k by A252, VALUED_1:13
.= |.((lim (F2 # x)) - ((F2 . n) . x)).| to_power k by A144, A249
.= |.((lim (F2 # x)) - ((F2 # x) . n)).| to_power k by SEQFUNC:def 10 ; :: thesis: verum
end;
F2 # x is convergent by A249, A131;
hence ( FP # x is convergent & lim (FP # x) = 0 ) by A250, Th11; :: thesis: verum
end;
A253: 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 A254: x in dom (lim FP) ; :: thesis: 0 = (lim FP) . x
then A255: ( lim (FP # x) = 0 & FP # x is convergent ) by A248, A238;
(lim FP) . x = lim (R_EAL (FP # x)) by A254, MESFUN7C:14;
hence 0 = (lim FP) . x by A255, RINFSUP2:14; :: thesis: verum
end;
a.e-eq-class_Lp (F,M,k) in CosetSet (M,k) by A188;
then reconsider Sq0 = a.e-eq-class_Lp (F,M,k) as Point of (Lp-Space (M,k)) by Def11;
A256: 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 ;
A257: FP . n = (abs (F - (F2 . n1))) to_power k by A234;
A258: ( F in Lp_Functions (M,k) & F in Sq0 ) by A188, Th38;
( F2 . n1 in Lp_Functions (M,k) & F2 . n1 in Sq . (N . n) ) by A137;
then (- 1) (#) (F2 . n1) in (- 1) * (Sq . (N . n)) by Th55;
then F - (F2 . n1) in Sq0 + ((- 1) * (Sq . (N . n))) by Th55, A258;
then F - (F2 . n1) in Sq0 - (Sq . (N . n)) by RLVECT_1:16;
then consider r being Real such that
A259: ( 0 <= r & r = Integral (M,((abs (F - (F2 . n1))) to_power k)) & ||.(Sq0 - (Sq . (N . n))).|| = r to_power (1 / k) ) by Th54;
||.(Sq0 - (Sq . (N . n))).|| to_power k = r to_power ((1 / k) * k) by A259, HOLDER_1:2
.= r to_power 1 by XCMPLX_1:106
.= r by POWER:25 ;
hence Ip . n = ||.(Sq0 - (Sq . (N . n))).|| to_power k by A259, A257, A247; :: thesis: verum
end;
deffunc H9( Element of NAT ) -> Element of REAL = ||.(Sq0 - (Sq . (N . $1))).||;
consider Iq being Real_Sequence such that
A260: for n being Element of NAT holds Iq . n = H9(n) from SEQ_1:sch 1();
A261: now
let n be Nat; :: thesis: Iq . n = ||.(Sq0 - (Sq . (N . n))).||
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
Iq . n = ||.(Sq0 - (Sq . (N . n0))).|| by A260;
hence Iq . n = ||.(Sq0 - (Sq . (N . n))).|| ; :: thesis: verum
end;
( Iq is convergent & lim Iq = 0 )
proof
A262: 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 Th4;
hence Ip . n >= 0 by A256; :: thesis: verum
end;
A263: 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 A256
.= ||.(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 A261 ; :: thesis: verum
end;
hence Iq is convergent by A262, A248, A247, HOLDER_1:10; :: thesis: lim Iq = 0
lim Iq = (lim Ip) to_power (1 / k) by A248, A247, A262, A263, HOLDER_1:10;
then lim Iq = 0 to_power (1 / k) by A248, A247, A253, A238, LPSPACE1:22;
hence lim Iq = 0 by POWER:def 2; :: thesis: verum
end;
hence Sq is convergent by A2, A261, Lm7; :: thesis: verum