:: On $L^p$ Space Formed by Real-valued Partial Functions
:: by Yasushige Watase , Noboru Endou and Yasunari Shidama
::
:: Received February 4, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, COMPLEX1, XBOOLE_0, XXREAL_0, VALUED_1, NAT_1, PARTFUN1,
SEQ_1, ARYTM_1, ORDINAL2, ZFMISC_1, NUMBERS, CARD_1, RELAT_1, SEQFUNC,
ARYTM_3, PBOOLE, RLVECT_1, SUPINF_2, RSSPACE, STRUCT_0, ALGSTR_0,
VECTSP10, REALSET1, FUNCOP_1, PRE_TOPC, LPSPACE1, BINOP_1, NORMSP_1,
PROB_1, MEASURE1, MEASURE2, MEASURE6, MESFUNC1, TARSKI, RFUNCT_3,
SETFAM_1, MESFUNC5, MESFUNC8, IDEAL_1, SUBSET_1, FUNCT_7, PREPOWER,
POWER, LPSPACE2, RSSPACE3, SEQ_2, SERIES_1, REAL_1, INTEGRA5, VALUED_0,
CARD_3, REWRITE1, NEWTON, XXREAL_2, METRIC_1, RELAT_2, XCMPLX_0,
SUPINF_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3,
XCMPLX_0, COMPLEX1, XXREAL_0, XREAL_0, SUPINF_1, SUPINF_2, EXTREAL1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_1, RFUNCT_3, BINOP_1,
REAL_1, NAT_1, STRUCT_0, ALGSTR_0, RLVECT_1, IDEAL_1, SETFAM_1, PRE_TOPC,
NORMSP_0, NORMSP_1, PROB_1, MEASURE1, MEASURE2, MEASURE3, MEASURE6,
SEQFUNC, MESFUNC1, MESFUNC2, MESFUNC5, MESFUNC6, FUNCT_7, MESFUNC8,
NEWTON, PREPOWER, POWER, MESFUN6C, SEQ_1, SEQ_2, RECDEF_1, SERIES_1,
RSSPACE3, LOPBAN_1, MESFUN7C, MESFUN9C, LPSPACE1;
constructors EXTREAL1, REAL_1, IDEAL_1, NEWTON, MEASURE3, MEASURE6, MESFUNC2,
MESFUNC6, MESFUNC9, MESFUN6C, MESFUN7C, MESFUN9C, RECDEF_1, RINFSUP2,
FUNCT_7, SERIES_1, PREPOWER, LPSPACE1, SUPINF_1, SEQFUNC, MESFUNC5,
RSSPACE3, LOPBAN_1, MESFUNC1, RELSET_1, BINOP_2, COMSEQ_2, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, MEMBERED, VALUED_0, NAT_1,
SUBSET_1, PARTFUN1, RLVECT_1, STRUCT_0, NORMSP_1, MEASURE1, SEQ_4, SEQ_2,
MESFUN6C, MESFUNC8, LPSPACE1, XCMPLX_0, XREAL_0, XXREAL_0, VALUED_1,
FUNCT_2, MESFUN7C, SERIES_1, XXREAL_3, EXTREAL1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, ALGSTR_0, RLVECT_1, NORMSP_0;
equalities STRUCT_0, ALGSTR_0, RLVECT_1, MESFUN7C, MESFUNC5, MESFUNC6,
SUBSET_1, LPSPACE1, XBOOLE_0, VALUED_1, RELAT_1, XCMPLX_0, NORMSP_0;
expansions TARSKI, RLVECT_1, MESFUNC5, MESFUNC6, LPSPACE1, XBOOLE_0, VALUED_1,
NORMSP_0;
theorems FUNCT_1, FUNCT_2, PARTFUN1, COMPLEX1, MESFUN9C, RINFSUP2, SEQ_2,
SETFAM_1, LOPBAN_1, PREPOWER, XBOOLE_0, TARSKI, RELAT_1, SEQM_3,
VALUED_1, SERIES_1, IDEAL_1, RLVECT_1, FUNCOP_1, XBOOLE_1, BINOP_1,
SUPINF_2, MESFUNC5, MESFUNC2, EXTREAL1, MEASURE1, MESFUNC6, RFUNCT_1,
XXREAL_0, ABSVALUE, MESFUNC1, MEASURE2, RSSPACE3, NORMSP_1, XREAL_1,
HOLDER_1, POWER, XREAL_0, SUBSET_1, LPSPACE1, MESFUN6C, MESFUN7C,
MESFUNC8, ORDINAL1, NAT_1, XCMPLX_0, XCMPLX_1, VALUED_0, XXREAL_3,
SEQFUNC, MESFUNC9, SEQ_4, RELSET_1, COMSEQ_3, SEQ_1, SERIES_3, LOPBAN_3,
NAGATA_2, NORMSP_0, NUMBERS;
schemes NAT_1, RECDEF_1, BINOP_1, FUNCT_2, SEQ_1, SEQFUNC;
begin :: Preliminaries of Powers of Numbers and Operations of Real Sequences.
reserve X for non empty set,
x for Element of X,
S for SigmaField of X,
M for sigma_Measure of S,
f,g,f1,g1 for PartFunc of X,REAL,
l,m,n,n1,n2 for Nat,
a,b,c for Real;
theorem Th1:
for m,n be positive Real st 1/m + 1/n = 1 holds m > 1
proof
let m,n be positive Real;
assume 1/m +1/n =1; then
A1:1/n = 1-1/m;
assume m <=1; then
1<= 1/m by XREAL_1:181;
hence contradiction by A1,XREAL_1:47;
end;
theorem Th2:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
A be Element of S, f be PartFunc of X,ExtREAL st
A = dom f & f is A-measurable & f is nonnegative holds
Integral(M,f) in REAL iff f is_integrable_on M
proof
let X be non empty set,
S be SigmaField of X,
M be sigma_Measure of S,
A be Element of S,
f be PartFunc of X,ExtREAL;
assume A1: A = dom f & f is A-measurable & f is nonnegative;
A2:now assume f is_integrable_on M; then
-infty < Integral(M,f) & Integral(M,f) < +infty by MESFUNC5:96;
hence Integral(M,f) in REAL by XXREAL_0:14;
end;
now assume A3: Integral(M,f) in REAL;
A4: dom (max-f) = A & max-f is A-measurable by A1,MESFUNC2:26,def 3;
A5: dom (max+f) = A & max+f is A-measurable by A1,MESFUNC2:25,def 2;
for x being Element of X holds 0 <= (max+f).x by MESFUNC2:12; then
max+f is nonnegative by SUPINF_2:39; then
A6: Integral(M,max+f) = integral+(M,max+f) by A5,MESFUNC5:88;
A7:for x be Element of X st x in dom f holds (max+f).x = f.x
proof
let x be Element of X;
A8: f.x >= 0 by A1,SUPINF_2:39;
assume x in dom f; then
(max+f).x = max(f.x,0) by A1,A5,MESFUNC2:def 2;
hence thesis by A8,XXREAL_0:def 10;
end; then
max+f = f by A1,A5,PARTFUN1:5; then
A9: Integral(M,max+f) < +infty by A3,XXREAL_0:9;
for x being Element of X holds 0 <= (max-f).x by MESFUNC2:13; then
max-f is nonnegative by SUPINF_2:39; then
A10: Integral(M,max-f) = integral+(M,max-f) by A4,MESFUNC5:88;
for x be Element of X st x in dom (max-f) holds 0= (max-f).x
proof
let x be Element of X;
assume x in dom (max-f);
max+f.x = f.x by A1,A5,A7,PARTFUN1:5;
hence 0= max-f.x by MESFUNC2:19;
end; then
Integral(M,max-f) = 0 by A4,LPSPACE1:22;
hence f is_integrable_on M by A1,A6,A9,A10;
end;
hence thesis by A2;
end;
definition
let r be Real;
attr r is geq_than_1 means :Def1:
1 <= r;
end;
registration
cluster geq_than_1 -> positive for Real;
coherence;
end;
reconsider jj=1 as Real;
registration
cluster geq_than_1 for Real;
existence
by Def1;
end;
registration
cluster geq_than_1 for Real;
existence
by Def1;
end;
reserve k for positive Real;
theorem Th3:
for a,b,p be Real
st 0 < p & 0 <= a & a < b holds a to_power p < b to_power p
proof
let a,b,p be Real;
assume A1: 0 < p & 0 <= a & a< b;
now assume a = 0; then
a to_power p = 0 by A1,POWER:def 2;
hence a to_power p < b to_power p by A1,POWER:34;
end;
hence thesis by A1,POWER:37;
end;
theorem Th4:
a >= 0 & b > 0 implies a to_power b >= 0
proof
assume A1: a >= 0;
assume b > 0; then
a = 0 implies a to_power b >= 0 by POWER:def 2;
hence thesis by A1,POWER:34;
end;
theorem Th5:
a >= 0 & b >= 0 & c > 0 implies (a*b) to_power c = a to_power c * b to_power c
proof
assume that
A1: a >= 0 & b >= 0 and
A2: c > 0;
now assume A3: a = 0 or b = 0; then
(a*b) to_power c = 0 by A2,POWER:def 2;
hence (a*b) to_power c = a to_power c * b to_power c by A3;
end;
hence thesis by A1,POWER:30;
end;
theorem Th6:
for a,b be Real, f st f is nonnegative & a > 0 & b > 0 holds
(f to_power a) to_power b = f to_power (a*b)
proof
let a,b be Real;
let f;
assume A1: f is nonnegative & a > 0 & b > 0;
A2:dom (f to_power a) = dom f &
dom((f to_power a) to_power b) = dom (f to_power a) &
dom(f to_power (a*b)) = dom f by MESFUN6C:def 4;
for x be object st x in dom((f to_power a) to_power b) holds
((f to_power a) to_power b).x = (f to_power (a*b)).x
proof
let x be object;
assume A3: x in dom ((f to_power a) to_power b); then
A4: ((f to_power a) to_power b).x
= ((f to_power a).x) to_power b by MESFUN6C:def 4
.= ((f.x) to_power a) to_power b by A2,A3,MESFUN6C:def 4;
A5: (f to_power (a*b)).x = (f.x) to_power (a*b) by A2,A3,MESFUN6C:def 4; then
A6: f.x > 0 implies ((f to_power a) to_power b).x = (f to_power (a*b)).x
by A4,POWER:33;
now assume A7: f.x = 0; then
((f to_power a) to_power b).x = 0 to_power b by A1,A4,POWER:def 2; then
((f to_power a) to_power b).x = 0 by A1,POWER:def 2;
hence ((f to_power a) to_power b).x = (f to_power (a*b)).x
by A1,A7,A5,POWER:def 2;
end;
hence thesis by A6,A1,MESFUNC6:51;
end;
hence thesis by A2,FUNCT_1:2;
end;
theorem Th7:
for a,b be Real, f st f is nonnegative & a > 0 & b > 0 holds
(f to_power a)(#)(f to_power b) = f to_power (a+b)
proof
let a,b be Real; let f;
assume A1: f is nonnegative & a >0 & b >0;
A2:dom(f to_power a) = dom f & dom(f to_power b) = dom f by MESFUN6C:def 4;
A3:dom((f to_power a)(#)(f to_power b))
= dom (f to_power a) /\ dom (f to_power b) by VALUED_1:def 4; then
A4:dom ((f to_power a)(#)(f to_power b)) = dom(f to_power (a+b))
by A2,MESFUN6C:def 4;
for x be object st x in dom((f to_power a)(#)(f to_power b)) holds
((f to_power a)(#)(f to_power b)).x = (f to_power (a+b)).x
proof
let x be object;
assume A5: x in dom((f to_power a)(#)(f to_power b));
then (f to_power a).x = ((f.x) to_power a) &
(f to_power b).x = ((f.x) to_power b) by A2,A3,MESFUN6C:def 4; then
A6: ((f to_power a)(#)(f to_power b)).x
= ((f.x) to_power a) * ((f.x) to_power b) by A5,VALUED_1:def 4;
A7: (f to_power (a+b)).x = (f.x) to_power (a+b) by A4,A5,MESFUN6C:def 4;
then
A8: f.x > 0 implies ((f to_power a)(#)(f to_power b)).x = (f to_power (a+b)).x
by A6,POWER:27;
now assume A9: f.x = 0; then
((f to_power a)(#)(f to_power b)).x = 0 * (0 to_power b)
by A1,A6,POWER:def 2;
hence ((f to_power a)(#)(f to_power b)).x = (f to_power (a+b)).x
by A7,A1,A9,POWER:def 2;
end;
hence thesis by A1,A8,MESFUNC6:51;
end;
hence thesis by A4,FUNCT_1:2;
end;
theorem Th8:
f to_power 1 = f
proof
A1:dom (f to_power 1) = dom f by MESFUN6C:def 4;
for x be object st x in dom (f to_power 1) holds (f to_power 1).x = f.x
proof
let x be object;
assume x in dom(f to_power 1); then
(f to_power 1).x = (f.x) to_power 1 by MESFUN6C:def 4;
hence thesis by POWER:25;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th9:
for seq1,seq2 be Real_Sequence, k be positive Real st
for n be Nat holds seq1.n = (seq2.n) to_power k & seq2.n >= 0
holds (seq1 is convergent iff seq2 is convergent)
proof
let seq1,seq2 be Real_Sequence, k be positive Real;
assume
A1: for n be Nat holds seq1.n = (seq2.n) to_power k & seq2.n >= 0;
A2:for n holds seq1.n >= 0
proof
let n;
(seq2.n) to_power k >= 0 by A1,Th4;
hence thesis by A1;
end;
thus seq1 is convergent implies seq2 is convergent
proof
assume A3: seq1 is convergent;
for n be Nat holds seq2.n = (seq1.n) to_power (1/k)
proof
let n be Nat;
(seq1.n) to_power (1/k) = (seq2.n) to_power k to_power (1/k) by A1
.= (seq2.n) to_power (k*(1/k)) by A1,HOLDER_1:2
.= (seq2.n) to_power 1 by XCMPLX_1:106;
hence thesis by POWER:25;
end;
hence thesis by A2,A3,HOLDER_1:10;
end;
assume seq2 is convergent;
hence thesis by A1,HOLDER_1:10;
end;
theorem Th10:
for seq be Real_Sequence, n,m be Nat st m <= n holds
|.(Partial_Sums seq).n - (Partial_Sums seq).m.|
<= (Partial_Sums abs seq).n - (Partial_Sums abs seq).m &
|.(Partial_Sums seq).n - (Partial_Sums seq).m.|
<= (Partial_Sums abs seq).n
proof
let seq be Real_Sequence;
let n, m be Nat;
assume A1: m<= n;
A2:for n holds abs(seq).n >= 0
proof
let n;
|.seq.n.|=abs(seq).n by SEQ_1:12;
hence thesis by COMPLEX1:46;
end; then
A3: |.(Partial_Sums abs seq).n - (Partial_Sums abs seq).m.|
= (Partial_Sums abs seq).n - (Partial_Sums abs seq).m by A1,COMSEQ_3:9;
(Partial_Sums abs seq).m >= 0 by A2,SERIES_3:34; then
|.(Partial_Sums seq).n - (Partial_Sums seq).m.|
<= (Partial_Sums abs seq).n - (Partial_Sums abs seq).m
+ (Partial_Sums abs seq).m by A3,A1,SERIES_1:34,XREAL_1:38;
hence thesis by A3,A1,SERIES_1:34;
end;
theorem Th11:
for seq,seq2 be Real_Sequence, k be positive Real st seq is convergent &
for n be Nat holds
seq2.n = |. lim seq - seq.n qua Complex .| to_power k
holds seq2 is convergent & lim seq2 = 0
proof
let seq, seq2 be Real_Sequence, k be positive Real;
set r = lim seq;
assume
A1: seq is convergent &
for n be Nat holds seq2.n = |. r -seq.n qua Complex .| to_power k;
deffunc U(Nat) = |.r -seq.$1 qua Complex.|;
consider seq1 be Real_Sequence such that
A2: for n holds seq1.n = U(n) from SEQ_1:sch 1;
deffunc U(Nat) = r;
consider seq0 be Real_Sequence such that
A3: for n holds seq0.n = U(n) from SEQ_1:sch 1;
reconsider r as Element of REAL by XREAL_0:def 1;
for n be Nat holds seq0.n = r
by A3; then
A4:seq0 is constant by VALUED_0:def 18; then
A5:seq0 - seq is convergent by A1;
A6:dom seq0 = NAT & dom seq = NAT & dom (seq0 - seq)= NAT
& dom seq1 = NAT by FUNCT_2:def 1;
A7:dom abs(seq0 - seq) = dom (seq0 - seq) by VALUED_1:def 11;
for n be Element of NAT holds abs(seq0 - seq).n = seq1.n
proof
let n be Element of NAT;
seq1.n = |. r - seq.n .| by A2; then
seq1.n = |. seq0.n - seq.n .| by A3; then
seq1.n = |.(seq0-seq).n.| by A6,VALUED_1:13;
hence thesis by A6,A7,VALUED_1:def 11;
end; then
A8:abs(seq0 - seq) = seq1 by FUNCT_2:63; then
A9:seq1 is convergent by A5;
lim (seq0-seq) = seq0.0 - lim seq by A4,A1,SEQ_4:42; then
lim (seq0-seq) = r - lim seq by A3; then
A10:lim seq1 = 0 by A5,A8,COMPLEX1:44,SEQ_4:14;
for n holds seq2.n = (seq1.n) to_power k & seq1.n >= 0
proof
let n;
|. r -seq.n .| = seq1.n by A2;
hence thesis by A1,COMPLEX1:46;
end; then
seq2 is convergent & lim seq2 = (lim seq1) to_power k by A9,HOLDER_1:10;
hence thesis by A10,POWER:def 2;
end;
Lm1:
for seq be Real_Sequence, n be Nat holds
|.(Partial_Sums seq).n qua Complex.| <= (Partial_Sums abs seq).n
by NAGATA_2:13;
begin :: Real Linear Space of Lp Integrable Functions
theorem Th12:
for k be positive Real,
X be non empty set holds (X -->0) to_power k = X --> 0
proof
let k be positive Real, X be non empty set;
A1:dom ((X -->0) to_power k) = dom (X-->0) by MESFUN6C:def 4;
now let x be Element of X;
assume x in dom((X -->0) to_power k); then
((X -->0) to_power k).x = ((X -->0).x) to_power k by MESFUN6C:def 4; then
((X -->0) to_power k).x = 0 to_power k by FUNCOP_1:7; then
((X -->0) to_power k).x = 0 by POWER:def 2;
hence ((X -->0) to_power k).x = (X --> 0).x by FUNCOP_1:7;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th13:
for f be PartFunc of X,REAL, D be set holds abs(f|D) = (abs f)|D
proof
let f be PartFunc of X,REAL;
let D be set;
A1:dom abs(f|D) = dom (f|D) by VALUED_1:def 11; then
dom abs(f|D) = dom f /\ D by RELAT_1:61; then
dom abs(f|D) = dom abs f /\ D by VALUED_1:def 11; then
A2:dom abs(f|D) = dom((abs f)|D) by RELAT_1:61;
for x be Element of X st x in dom abs(f|D) holds
(abs(f|D)).x = ((abs f)|D).x
proof
let x be Element of X;
assume A3: x in dom abs(f|D); then
x in dom f by A1,RELAT_1:57; then
A4: x in dom abs f by VALUED_1:def 11;
(abs(f|D)).x = |.(f|D).x.| by A3,VALUED_1:def 11; then
(abs(f|D)).x = |.f.x.| by A3,A1,FUNCT_1:47; then
(abs(f|D)).x = (abs f).x by A4,VALUED_1:def 11;
hence (abs(f|D)).x = ((abs f)|D).x by A3,A2,FUNCT_1:47;
end;
hence thesis by A2,PARTFUN1:5;
end;
registration
let X; let f be PartFunc of X,REAL;
cluster abs f -> nonnegative;
coherence
proof
now let x be object;
assume x in dom abs f; then
(abs f).x = |.f.x.| by VALUED_1:def 11;
hence 0 <= (abs f).x by COMPLEX1:46;
end;
hence thesis by MESFUNC6:52;
end;
end;
theorem Th14:
for f be PartFunc of X,REAL st f is nonnegative holds abs f = f
proof
let f be PartFunc of X,REAL;
A1:dom f = dom (abs f) by VALUED_1:def 11;
assume A2: f is nonnegative;
now let x be Element of X;
A3: f.x >= 0 by A2,MESFUNC6:51;
assume x in dom f; then
x in dom abs f by VALUED_1:def 11; then
(abs f).x = |.f.x.| by VALUED_1:def 11;
hence (abs f).x = f.x by A3,ABSVALUE:def 1;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th15:
(X = dom f & for x st x in dom f holds 0 = f.x) implies
f is_integrable_on M & Integral(M,f) =0
proof
assume A1:X=dom f & for x st x in dom f holds 0 = f.x;
X is Element of S by MEASURE1:7; then
R_EAL f is_integrable_on M & Integral(M,R_EAL f) = 0 by A1,LPSPACE1:22;
hence thesis;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
k be positive Real;
func Lp_Functions(M,k) -> non empty Subset of RLSp_PFunct X equals
{f where f is PartFunc of X,REAL :
ex Ef be Element of S st M.(Ef`)=0 & dom f = Ef &
f is Ef-measurable & (abs f) to_power k is_integrable_on M};
correctness
proof
set V = {f where f is PartFunc of X,REAL :
ex Ef be Element of S st M.(Ef`)=0 & dom f = Ef &
f is Ef-measurable & (abs f) to_power k is_integrable_on M};
A1:V c= PFuncs(X,REAL)
proof
let x be object;
assume x in V; then
ex f be PartFunc of X,REAL st x = f &
ex Ef be Element of S st M.(Ef`)=0 & dom f = Ef &
f is Ef-measurable & (abs f) to_power k is_integrable_on M;
hence x in PFuncs(X,REAL) by PARTFUN1:45;
end;
reconsider g = X--> In(0,REAL) as Function of X,REAL by FUNCOP_1:46;
reconsider Ef = X as Element of S by MEASURE1:34;
set h = (abs g) to_power k;
A2:dom g = X by FUNCOP_1:13;
for x be set st x in dom g holds g.x = 0 by FUNCOP_1:7; then
A3:g is Ef-measurable by A2,LPSPACE1:52;
Ef` = {} by XBOOLE_1:37; then
A4:M.(Ef`) = 0 by VALUED_0:def 19;
for x be object st x in dom (X-->0) holds 0 <= (X-->0).x; then
abs g = X-->0 by Th14,MESFUNC6:52; then
A5:h = g by Th12; then
for x be Element of X st x in dom h holds h.x = 0 by FUNCOP_1:7; then
h is_integrable_on M by Th15,A5,A2; then
g in V by A3,A4,A2;
hence thesis by A1;
end;
end;
theorem Th16:
for a,b,k be Real st k > 0 holds
|.a+b qua Complex.| to_power k
<= (|.a qua Complex.| + |.b qua Complex.|) to_power k &
(|.a qua Complex.| + |.b qua Complex.|) to_power k
<= (2 * max(|.a qua Complex.|,|.b qua Complex.|)) to_power k &
|.a+b qua Complex.| to_power k
<= (2*max(|.a qua Complex.|,|.b qua Complex.|)) to_power k
proof
let a,b,k be Real;
assume A1: k > 0;
A2:|.a+b qua Complex.| <= |.a qua Complex.| + |.b qua Complex.| by ABSVALUE:9;
|.a.| <= max(|.a.|,|.b.|) & |.b.| <= max(|.a.|,|.b.|) by XXREAL_0:25; then
A3:|.a qua Complex.| + |.b qua Complex.|
<= max(|.a qua Complex.|,|.b qua Complex.|) +
max(|.a qua Complex.|,|.b qua Complex.|) by XREAL_1:7; then
A4:|.a+b qua Complex.| <= 2*max(|.a qua Complex.|,|.b qua Complex.|)
by A2,XXREAL_0:2;
0 <= |.a+b qua Complex.| by COMPLEX1:46;
hence thesis by A1,A2,A3,A4,HOLDER_1:3;
end;
theorem Th17:
for a, b, k be Real st a >= 0 & b >= 0 & k > 0 holds
max(a,b) to_power k <= a to_power k + b to_power k
proof
let a,b,k be Real;
assume A1: a >= 0 & b >= 0 & k > 0;
per cases;
suppose a <> 0 & b <> 0; then
A2: a to_power k >= 0 & b to_power k >= 0 by A1,POWER:34;
max(a,b) = a or max(a,b) = b by XXREAL_0:def 10;
hence max(a,b) to_power k <= a to_power k + b to_power k by A2,XREAL_1:40;
end;
suppose A3: a = 0; then
a to_power k = 0 by A1,POWER:def 2;
hence max(a,b) to_power k <= a to_power k + b to_power k
by A1,A3,XXREAL_0:def 10;
end;
suppose A4: b =0; then
b to_power k = 0 by A1,POWER:def 2;
hence (max(a,b)) to_power k <= a to_power k + b to_power k
by A1,A4,XXREAL_0:def 10;
end;
end;
theorem Th18:
for f be PartFunc of X,REAL, a,b be Real st b > 0 holds
(|.a qua Complex.| to_power b)(#)((abs f) to_power b) = (abs(a(#)f)) to_power b
proof
let f be PartFunc of X,REAL;
let a,b be Real;
assume A1: b >0;
A2:dom((|.a qua Complex.| to_power b)(#)((abs f) to_power b))
= dom((abs f) to_power b) &
dom(a(#)f) = dom f by VALUED_1:def 5;
A3:dom((abs f) to_power b) = dom (abs f) &
dom abs(a(#)f) = dom ((abs (a(#)f)) to_power b) by MESFUN6C:def 4;
A4:dom (abs f) = dom f & dom abs(a(#)f) = dom (a(#)f) by VALUED_1:def 11;
for x be Element of X st
x in dom ((|.a qua Complex.| to_power b)(#)((abs f) to_power b)) holds
((|.a qua Complex.| to_power b)(#)((abs f) to_power b)).x
= ((abs(a(#)f)) to_power b).x
proof
let x be Element of X;
assume
A5: x in dom ((|.a qua Complex.| to_power b)(#)((abs f) to_power b));
A6:|.f.x.| >= 0 & |.a.| >= 0 by COMPLEX1:46;
((|.a qua Complex.| to_power b)(#)((abs f) to_power b)).x
= (|.a qua Complex.| to_power b) * ((abs f) to_power b).x
by A5,VALUED_1:def 5
.= (|.a qua Complex.| to_power b) * (((abs f).x) to_power b)
by A2,A5,MESFUN6C:def 4
.= (|.a qua Complex.| to_power b) * ((|.f.x qua Complex.|) to_power b)
by VALUED_1:18
.= (|.a qua Complex.| * |.f.x qua Complex.|) to_power b by A1,A6,Th5
.= |.a * f.x qua Complex.| to_power b by COMPLEX1:65
.= |.(a(#)f).x qua Complex.| to_power b by VALUED_1:6
.= ((abs(a(#)f)).x) to_power b by VALUED_1:18;
hence thesis by A2,A3,A4,A5,MESFUN6C:def 4;
end;
hence thesis by A2,A3,A4,PARTFUN1:5;
end;
theorem Th19:
for f be PartFunc of X,REAL, a,b be Real st a > 0 & b > 0 holds
(a to_power b)(#)((abs f) to_power b) = (a(#)(abs f)) to_power b
proof
let f be PartFunc of X,REAL;
let a,b be Real;
assume A1: a > 0 & b > 0; then
A2:|.a.| = a by COMPLEX1:43; then
(a to_power b)(#)((abs f) to_power b)
= (abs(a(#)f)) to_power b by A1,Th18;
hence thesis by A2,RFUNCT_1:25;
end;
theorem Th20:
for f be PartFunc of X,REAL, k be Real, E be set holds
(f|E) to_power k = (f to_power k)|E
proof
let f be PartFunc of X,REAL;
let k be Real;
let E be set;
A1:dom((f|E) to_power k) = dom(f|E) by MESFUN6C:def 4; then
dom((f|E) to_power k) = dom f /\ E by RELAT_1:61; then
A2:dom((f|E) to_power k) = dom(f to_power k) /\ E by MESFUN6C:def 4; then
A3:dom((f|E) to_power k) = dom((f to_power k)|E) by RELAT_1:61;
now let x be Element of X;
assume A4: x in dom((f|E) to_power k); then
((f|E) to_power k).x = ((f|E).x) to_power k by MESFUN6C:def 4; then
A5: ((f|E) to_power k).x = (f.x) to_power k by A1,A4,FUNCT_1:47;
x in dom(f to_power k) by A2,A4,XBOOLE_0:def 4; then
((f|E) to_power k).x = (f to_power k).x by A5,MESFUN6C:def 4;
hence ((f|E) to_power k).x = ((f to_power k)|E).x by A4,A3,FUNCT_1:47;
end;
hence thesis by A3,PARTFUN1:5;
end;
theorem Th21:
for a,b,k be Real st k > 0 holds (|.a+b qua Complex.|) to_power k
<= (2 to_power k)*(|.a qua Complex.| to_power k +
(|.b qua Complex.|) to_power k)
proof
let a,b,k be Real;
assume A1: k > 0; then
A2:(|.a+b qua Complex.|) to_power k
<= (2*max(|.a qua Complex.|,|.b qua Complex.|)) to_power k by Th16;
A3:|.a.| >= 0 & |.b.| >= 0 by COMPLEX1:46; then
A4:(max(|.a qua Complex.|,|.b qua Complex.|)) to_power k
<= |.a qua Complex.| to_power k + |.b qua Complex.| to_power k by A1,Th17;
max(|.a.|,|.b.|) = |.a.| or max(|.a.|,|.b.|)= |.b.| by XXREAL_0:16; then
A5:(2*max(|.a qua Complex.|,|.b qua Complex.|)) to_power k
= (2 to_power k)*(max(|.a qua Complex.|,|.b qua Complex.|)) to_power k
by A1,A3,Th5;
(2 to_power k) > 0 by POWER:34; then
(2 to_power k) *(max(|.a qua Complex.|,|.b qua Complex.|)) to_power k
<= (2 to_power k)*(|.a qua Complex.| to_power k
+ |.b qua Complex.| to_power k) by A4,XREAL_1:64;
hence thesis by A2,A5,XXREAL_0:2;
end;
theorem Th22:
for k be positive Real, f,g be PartFunc of X,REAL st
f in Lp_Functions(M,k) & g in Lp_Functions (M,k) holds
(abs f) to_power k is_integrable_on M &
(abs g) to_power k is_integrable_on M &
(abs f) to_power k + (abs g) to_power k is_integrable_on M
proof
let k be positive Real;
let f,g be PartFunc of X,REAL;
assume A1: f in Lp_Functions (M,k) & g in Lp_Functions (M,k); then
A2:ex f1 be PartFunc of X,REAL st
f=f1 & ex Ev be Element of S st M.(Ev`) = 0 & dom f1 = Ev &
f1 is Ev-measurable & (abs f1) to_power k is_integrable_on M;
ex g1 be PartFunc of X, REAL st
g = g1 & ex Eu be Element of S st M.(Eu`) = 0 & dom g1 = Eu &
g1 is Eu-measurable & (abs g1) to_power k is_integrable_on M by A1;
hence thesis by A2,MESFUNC6:100;
end;
theorem Th23:
X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions(M,k)
proof
reconsider g = X --> In(0,REAL) as Function of X,REAL by FUNCOP_1:46;
reconsider ND = X as Element of S by MEASURE1:34;
ND` = {} by XBOOLE_1:37; then
A1:M.ND` = 0 by VALUED_0:def 19;
A2:dom g = X by FUNCT_2:def 1;
for x be Element of X st x in dom g holds g.x = 0 by FUNCOP_1:7; then
A3:g is_integrable_on M by A2,Th15;
for x be object st x in dom g holds 0 <= g.x; then
abs g = g by Th14,MESFUNC6:52; then
A4:(abs g) to_power k = g by Th12;
for x be set st x in dom g holds g.x = 0 by FUNCOP_1:7; then
g is ND-measurable by A2,LPSPACE1:52;
hence thesis by A1,A2,A3,A4;
end;
theorem Th24:
for k be Real st k > 0 for f,g be PartFunc of X,REAL holds
for x be Element of X st x in dom f /\ dom g holds
(abs(f + g) to_power k).x <=
((2 to_power k)(#)((abs f) to_power k + (abs g) to_power k)).x
proof
let k be Real;
assume A1: k > 0;
let f,g be PartFunc of X,REAL;
let x be Element of X;
assume A2: x in dom f /\ dom g;
A3:dom(f + g) = dom f /\ dom g by VALUED_1:def 1; then
dom abs(f + g) = dom f /\ dom g by VALUED_1:def 11; then
x in dom (abs(f + g) to_power k) by A2,MESFUN6C:def 4; then
A4:(abs(f + g) to_power k).x = ((abs(f + g)).x) to_power k by MESFUN6C:def 4
.= |.(f+g).x qua Complex.| to_power k by VALUED_1:18
.= |.f.x + g.x qua Complex.| to_power k by A3,A2,VALUED_1:def 1;
dom (abs f) = dom f & dom (abs g) = dom g by VALUED_1:def 11; then
x in dom (abs f) & x in dom (abs g) by A2,XBOOLE_0:def 4; then
A5:x in dom ((abs f) to_power k) & x in dom ((abs g) to_power k)
by MESFUN6C:def 4;
|.f.x qua Complex.| to_power k = ((abs f).x) to_power k &
|.g.x qua Complex.| to_power k = ((abs g).x) to_power k by VALUED_1:18; then
A6:|.f.x qua Complex.| to_power k = ((abs f) to_power k).x &
|.g.x qua Complex.| to_power k = ((abs g) to_power k).x
by A5,MESFUN6C:def 4;
dom ((abs f) to_power k + (abs g) to_power k) =
dom ((abs f) to_power k) /\ dom ((abs g) to_power k) by VALUED_1:def 1;then
x in dom((abs f) to_power k + (abs g) to_power k) by A5,XBOOLE_0:def 4; then
(2 to_power k)*(|.f.x qua Complex.| to_power k
+ |.g.x qua Complex.| to_power k)
= (2 to_power k) * ((abs f) to_power k + (abs g) to_power k).x
by A6,VALUED_1:def 1
.= ((2 to_power k)(#)((abs f) to_power k + (abs g) to_power k)).x
by VALUED_1:6;
hence thesis by A1,A4,Th21;
end;
theorem Th25:
f in Lp_Functions(M,k) & g in Lp_Functions(M,k) implies
f + g in Lp_Functions(M,k)
proof
set W = Lp_Functions(M,k);
assume A1: f in W & g in W;
then consider f1 be PartFunc of X,REAL such that
A2: f1=f & ex Ef1 be Element of S st M.(Ef1`) = 0 & dom f1 = Ef1 &
f1 is Ef1-measurable & (abs f1) to_power k is_integrable_on M;
consider Ef be Element of S such that
A3: M.(Ef`) = 0 & dom f1 = Ef &
f1 is Ef-measurable & (abs f1) to_power k is_integrable_on M by A2;
consider g1 be PartFunc of X,REAL such that
A4: g1=g & ex Eg1 be Element of S st M.(Eg1`) = 0 & dom g1 = Eg1 &
g1 is Eg1-measurable & (abs g1) to_power k is_integrable_on M by A1;
consider Eg be Element of S such that
A5: M.(Eg`) = 0 & dom g1 = Eg &
g1 is Eg-measurable & (abs g1) to_power k is_integrable_on M by A4;
A6:dom (f1+g1)= Ef /\ Eg by A3,A5,VALUED_1:def 1;
set Efg = Ef /\ Eg;
set s = abs(f1 + g1) to_power k;
set t = (2 to_power k)(#)((abs f1) to_power k + (abs g1) to_power k);
A7:Efg` = (X \ Ef) \/ (X \ Eg) by XBOOLE_1:54;
Ef` is Element of S & Eg` is Element of S by MEASURE1:34; then
Ef` is measure_zero of M & Eg` is measure_zero of M
by A3,A5,MEASURE1:def 7; then
Ef` \/ Eg` is measure_zero of M by MEASURE1:37; then
A8:M.(Efg`) = 0 by A7,MEASURE1:def 7;
f1 is Efg-measurable & g1 is Efg-measurable
by A3,A5,MESFUNC6:16,XBOOLE_1:17; then
A9: f1 + g1 is Efg-measurable by MESFUNC6:26; then
A10: abs(f1 + g1) is Efg-measurable by A6,MESFUNC6:48;
(abs f1) to_power k + (abs g1) to_power k is_integrable_on M
by A1,A2,A4,Th22; then
A11: t is_integrable_on M by MESFUNC6:102;
A12:dom abs f1 = dom f1 & dom abs g1 = dom g1 &
dom abs(f1 + g1) = dom (f1+g1) by VALUED_1:def 11; then
A13: s is Efg-measurable by A6,A10,MESFUN6C:29;
A14: abs s = (abs(f1 + g1) to_power k) by Th14;
A15: dom s = Efg by A6,A12,MESFUN6C:def 4;
A16:dom t = dom ((abs f1) to_power k + (abs g1) to_power k) by VALUED_1:def 5
.= dom((abs f1) to_power k) /\ dom((abs g1) to_power k) by VALUED_1:def 1
.= dom (abs f1) /\ dom ((abs g1) to_power k) by MESFUN6C:def 4
.= dom (abs f1) /\ dom (abs g1) by MESFUN6C:def 4
.= dom (f1+g1) by A12,VALUED_1:def 1
.= dom s by A12,MESFUN6C:def 4;
now let x be Element of X;
assume x in dom s; then
(abs s).x <= t.x by A14,Th24,A3,A5,A15;
hence |.s.x qua Complex.| <= t.x by VALUED_1:18;
end; then
s is_integrable_on M by A13,A15,A16,A11,MESFUNC6:96;
hence thesis by A2,A4,A8,A6,A9;
end;
theorem Th26:
f in Lp_Functions(M,k) implies a(#)f in Lp_Functions(M,k)
proof
assume f in Lp_Functions(M,k); then
consider f1 be PartFunc of X,REAL such that
A1: f1=f & ex Ef1 be Element of S st M.(Ef1`) = 0 & dom f1 = Ef1 &
f1 is Ef1-measurable & (abs f1) to_power k is_integrable_on M;
consider Ef be Element of S such that
A2: M.(Ef`) = 0 & dom f1 = Ef &
f1 is Ef-measurable & (abs f1) to_power k is_integrable_on M by A1;
A3:dom(a(#)f1) = Ef & a(#)f1 is Ef-measurable
by A2,MESFUNC6:21,VALUED_1:def 5;
(|.a qua Complex.| to_power k)(#)((abs f1) to_power k) is_integrable_on M
by A1,MESFUNC6:102; then
(abs(a(#)f1)) to_power k is_integrable_on M by Th18;
hence thesis by A1,A2,A3;
end;
theorem Th27:
f in Lp_Functions(M,k) & g in Lp_Functions(M,k) implies
f - g in Lp_Functions(M,k)
proof
assume A1: f in Lp_Functions(M,k) & g in Lp_Functions(M,k); then
(-1)(#)g in Lp_Functions(M,k) by Th26;
hence thesis by Th25,A1;
end;
theorem Th28:
f in Lp_Functions(M,k) implies abs f in Lp_Functions(M,k)
proof
set W = Lp_Functions(M,k);
assume f in W; then
consider f1 be PartFunc of X,REAL such that
A1: f1=f & ex Ef1 be Element of S st M.(Ef1`) = 0 & dom f1 = Ef1 &
f1 is Ef1-measurable & (abs f1) to_power k is_integrable_on M;
consider Ef be Element of S such that
A2: M.(Ef`) = 0 & dom f1 = Ef &
f1 is Ef-measurable & (abs f1) to_power k is_integrable_on M by A1;
dom (abs f1) = Ef by A2,VALUED_1:def 11; then
Z1: M.(Ef`) = 0 & dom (abs f1) = Ef &
(abs f1) is Ef-measurable & (abs(abs f1)) to_power k is_integrable_on M
by A2,MESFUNC6:48;
thus thesis by A1,Z1;
end;
Lm2:
Lp_Functions(M,k) is add-closed & Lp_Functions(M,k) is multi-closed
proof
set W = Lp_Functions(M,k);
now let v,u be Element of the carrier of RLSp_PFunctX;
assume A1: v in W & u in W; then
consider v1 be PartFunc of X, REAL such that
A2: v1=v & ex ND be Element of S st M.ND`=0 & dom v1 = ND &
v1 is ND-measurable & (abs v1) to_power k is_integrable_on M;
consider u1 be PartFunc of X, REAL such that
A3: u1=u & ex ND be Element of S st M.ND`=0 & dom u1 = ND &
u1 is ND-measurable & (abs u1) to_power k is_integrable_on M by A1;
reconsider h = v+u as Element of PFuncs(X,REAL);
dom h = dom v1 /\ dom u1 &
for x be object st x in dom h holds h.x = v1.x + u1.x
by A2,A3,LPSPACE1:6; then
v+u=v1+u1 by VALUED_1:def 1;
hence v+u in Lp_Functions(M,k) by A1,A2,A3,Th25;
end;
hence Lp_Functions(M,k) is add-closed by IDEAL_1:def 1;
now let a be Real, u be VECTOR of RLSp_PFunctX;
assume A4: u in W; then
consider u1 be PartFunc of X,REAL such that
A5: u1=u & ex ND be Element of S st M.ND`=0 & dom u1 = ND &
u1 is ND-measurable & (abs u1) to_power k is_integrable_on M;
reconsider h = a*u as Element of PFuncs(X,REAL);
A6: dom h = dom u1 &
for x being Element of X st x in dom u1 holds h.x = a * (u1.x)
by A5,LPSPACE1:9; then
for x be object st x in dom h holds h.x = a*(u1.x); then
a*u=a(#)u1 by A6,VALUED_1:def 5;
hence a*u in Lp_Functions(M,k) by Th26,A4,A5;
end;
hence Lp_Functions(M,k) is multi-closed;
end;
registration
let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
cluster Lp_Functions(M,k) -> multi-closed add-closed;
coherence by Lm2;
end;
Lm3: RLSStruct (# Lp_Functions(M,k),
In(0.(RLSp_PFunct X),Lp_Functions(M,k)),
add|(Lp_Functions(M,k),RLSp_PFunct X),
Mult_(Lp_Functions(M,k)) #)
is Abelian add-associative right_zeroed vector-distributive
scalar-distributive scalar-associative scalar-unital
proof
0.(RLSp_PFunct X) in Lp_Functions(M,k) by Th23;
hence thesis by LPSPACE1:3;
end;
registration
let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
cluster RLSStruct (# Lp_Functions(M,k),
In(0.(RLSp_PFunct X),Lp_Functions(M,k)),
add|(Lp_Functions(M,k),RLSp_PFunct X),
Mult_(Lp_Functions(M,k)) #)
-> Abelian add-associative right_zeroed vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence by Lm3;
end;
definition
let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
func RLSp_LpFunct(M,k) -> strict Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct equals
RLSStruct (# Lp_Functions(M,k),
In(0.(RLSp_PFunct X),Lp_Functions(M,k)),
add|(Lp_Functions(M,k),RLSp_PFunct X),
Mult_(Lp_Functions(M,k)) #);
coherence;
end;
begin :: Preliminaries of Real Normed Space of Lp Integrable Functions
reserve v,u for VECTOR of RLSp_LpFunct(M,k);
theorem Th29:
f = v & g = u implies f+g = v+u
proof
reconsider v2=v, u2=u as VECTOR of RLSp_PFunct(X) by TARSKI:def 3;
reconsider h = v2+u2 as Element of PFuncs(X,REAL);
reconsider v2,u2 as Element of PFuncs(X,REAL);
assume A1:f=v & g=u;
A2:dom h= dom v2 /\ dom u2 &
for x being Element of X st x in dom h holds h.x = v2.x + u2.x
by LPSPACE1:6;
for x be object st x in dom h holds h.x = f.x + g.x by A1,LPSPACE1:6; then
h= f+g by A1,A2,VALUED_1:def 1;
hence thesis by LPSPACE1:4;
end;
theorem Th30:
f = u implies a(#)f = a*u
proof
reconsider u2=u as VECTOR of RLSp_PFunct X by TARSKI:def 3;
reconsider h = a*u2 as Element of PFuncs(X,REAL);
assume A1:f=u; then
A2:dom h = dom f by LPSPACE1:9; then
for x be object st x in dom h holds h.x = a*(f.x) by A1,LPSPACE1:9; then
h= a(#)f by A2,VALUED_1:def 5;
hence thesis by LPSPACE1:5;
end;
theorem Th31:
f=u implies u + (-1)*u = (X --> 0)|dom f & ex v,g be PartFunc of X,REAL st
v in Lp_Functions(M,k) & g in Lp_Functions(M,k) &
v = u + (-1)*u & g = X --> 0 & v a.e.= g,M
proof
reconsider u2=u as VECTOR of RLSp_PFunct X by TARSKI:def 3;
assume A1: f=u;
(-1)*u =(-1)*u2 by LPSPACE1:5; then
A2:u+(-1)*u =u2+(-1)*u2 by LPSPACE1:4;
hence u+(-1)*u = (X --> 0)|dom f by A1,LPSPACE1:16;
u+(-1)*u in Lp_Functions(M,k); then
consider v be PartFunc of X,REAL such that
A3: v=u+(-1)*u &
ex ND be Element of S st M.ND`= 0 & dom v = ND & v is ND-measurable &
(abs v)to_power k is_integrable_on M;
u in Lp_Functions(M,k); then
ex uu1 be PartFunc of X,REAL st
uu1=u & ex ND be Element of S st M.ND`=0 & dom uu1 = ND &
uu1 is ND-measurable & (abs uu1) to_power k is_integrable_on M; then
consider ND be Element of S such that
A4: M.ND`=0 & dom f = ND & f is ND-measurable &
(abs f) to_power k is_integrable_on M by A1;
set g = X-->0;
A5:ND` is Element of S & (ND`)`= ND by MEASURE1:34;
A6:g in Lp_Functions(M,k) by Th23;
v|ND = g|ND|ND by A2,A3,A4,A1,LPSPACE1:16; then
v|ND = g|ND by FUNCT_1:51; then
v a.e.= g,M by A4,A5;
hence thesis by A3,A6;
end;
definition
let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
func AlmostZeroLpFunctions(M,k) ->
non empty Subset of RLSp_LpFunct(M,k) equals
{ f where f is PartFunc of X,REAL :
f in Lp_Functions(M,k) & f a.e.= X-->0,M };
coherence
proof
A1:now let x be object;
assume x in { f where f is PartFunc of X,REAL: f in Lp_Functions(M,k) &
f a.e.= X-->0,M }; then
ex f be PartFunc of X,REAL st
x=f & f in Lp_Functions(M,k) & f a.e.= X-->0,M;
hence x in the carrier of RLSp_LpFunct(M,k);
end;
A2:X-->0 a.e.= X-->0,M by LPSPACE1:28;
X-->0 in Lp_Functions(M,k) by Th23; then
X-->0 in { f where f is PartFunc of X,REAL :
f in Lp_Functions (M,k) & f a.e.= X-->0,M } by A2;
hence thesis by A1,TARSKI:def 3;
end;
end;
Lm4:
AlmostZeroLpFunctions(M,k) is add-closed &
AlmostZeroLpFunctions(M,k) is multi-closed
proof
set Z = AlmostZeroLpFunctions(M,k);
set V = RLSp_LpFunct(M,k);
now let v,u be VECTOR of V;
assume A1: v in Z & u in Z; then
consider v1 be PartFunc of X,REAL such that
A2: v1=v & v1 in Lp_Functions(M,k) & v1 a.e.= X-->0,M;
consider u1 be PartFunc of X,REAL such that
A3: u1=u & u1 in Lp_Functions(M,k) & u1 a.e.= X-->0,M by A1;
A4: v+u=v1+u1 by Th29,A2,A3;
(X-->0)+(X-->0)=X-->0 by LPSPACE1:33; then
v1+u1 in Lp_Functions(M,k) & v1+u1 a.e.=X-->0,M by A4,A2,A3,LPSPACE1:31;
hence v+u in Z by A4;
end;
hence Z is add-closed by IDEAL_1:def 1;
now let a be Real, u be VECTOR of V;
assume u in Z; then
consider u1 be PartFunc of X,REAL such that
A5: u1=u & u1 in Lp_Functions(M,k) & u1 a.e.= X-->0,M;
A6:a*u=a(#)u1 by Th30,A5;
a(#)(X-->0)=X-->0 by LPSPACE1:33; then
a(#)u1 in Lp_Functions(M,k) & a(#)u1 a.e.=X-->0,M by A6,A5,LPSPACE1:32;
hence a*u in Z by A6;
end;
hence Z is multi-closed;
end;
registration
let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
cluster AlmostZeroLpFunctions(M,k) -> add-closed multi-closed;
coherence by Lm4;
end;
theorem
0.(RLSp_LpFunct(M,k)) = X-->0 &
0.(RLSp_LpFunct(M,k)) in AlmostZeroLpFunctions(M,k)
proof
thus 0.(RLSp_LpFunct(M,k)) = X --> 0 by Th23,SUBSET_1:def 8;
A1:X-->0 a.e.= X-->0,M & X --> 0 in Lp_Functions(M,k) by Th23,LPSPACE1:28;
0.(RLSp_LpFunct(M,k)) = 0.(RLSp_PFunctX) by Th23,SUBSET_1:def 8;
hence 0.(RLSp_LpFunct(M,k)) in AlmostZeroLpFunctions(M,k) by A1;
end;
definition
let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
func RLSp_AlmostZeroLpFunct(M,k) -> non empty RLSStruct equals
RLSStruct (# AlmostZeroLpFunctions(M,k),
In(0.(RLSp_LpFunct(M,k)),AlmostZeroLpFunctions(M,k)),
add|(AlmostZeroLpFunctions(M,k),RLSp_LpFunct(M,k)),
Mult_(AlmostZeroLpFunctions(M,k)) #);
coherence;
end;
registration
let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
cluster RLSp_LpFunct(M,k) ->
strict Abelian add-associative right_zeroed vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence;
end;
reserve v,u for VECTOR of RLSp_AlmostZeroLpFunct(M,k);
theorem
f=v & g=u implies f+g=v+u
proof
reconsider v2=v, u2=u as VECTOR of RLSp_LpFunct(M,k) by TARSKI:def 3;
assume A1: f=v & g=u;
v+u=v2+u2 by LPSPACE1:4;
hence v+u = f+g by Th29,A1;
end;
theorem
f=u implies a(#)f=a*u
proof
reconsider u2=u as VECTOR of RLSp_LpFunct(M,k) by TARSKI:def 3;
assume A1: f=u;
a*u=a*u2 by LPSPACE1:5;
hence a*u = a(#)f by Th30,A1;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,REAL, k be positive Real;
func a.e-eq-class_Lp(f,M,k) -> Subset of Lp_Functions(M,k) equals
{h where h is PartFunc of X,REAL : h in Lp_Functions(M,k) & f a.e.= h,M};
correctness
proof
now let x be object;
assume x in {g where g is PartFunc of X,REAL :
g in Lp_Functions (M,k) & f a.e.= g,M }; then
ex g be PartFunc of X,REAL st x=g & g in Lp_Functions (M,k) & f a.e.= g,M;
hence x in Lp_Functions(M,k);
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th35:
f in Lp_Functions(M,k) implies
ex E be Element of S st M.(E`) = 0 & dom f = E & f is E-measurable
proof
assume f in Lp_Functions(M,k); then
ex f1 be PartFunc of X,REAL st f = f1 &
(ex E be Element of S st M.(E`) = 0 & dom f1 = E &
f1 is E-measurable & (abs f1) to_power k is_integrable_on M);
hence thesis;
end;
theorem Th36:
g in Lp_Functions(M,k) & g a.e.= f,M implies g in a.e-eq-class_Lp(f,M,k)
proof
assume that
A1: g in Lp_Functions(M,k) and
A2: g a.e.= f,M;
f a.e.= g,M by A2;
hence g in a.e-eq-class_Lp(f,M,k) by A1;
end;
theorem Th37:
(ex E be Element of S st M.(E`)=0 & E = dom f & f is E-measurable) &
g in a.e-eq-class_Lp(f,M,k) implies
g a.e.= f,M & f in Lp_Functions(M,k)
proof
assume that
A1: ex E be Element of S st M.(E`)=0 & E = dom f & f is E-measurable and
A2: g in a.e-eq-class_Lp(f,M,k);
A3:ex r be PartFunc of X,REAL st g=r & r in Lp_Functions (M,k) &
f a.e.= r,M by A2;
hence g a.e.= f,M;
g in Lp_Functions(M,k) by A2; then
consider g1 be PartFunc of X,REAL such that
A4: g = g1 & ex E be Element of S st M.(E`)=0 & dom g1 = E &
g1 is E-measurable & (abs g1) to_power k is_integrable_on M;
consider Eh be Element of S such that
A5: M.(Eh`) = 0 & dom g = Eh &
g is Eh-measurable & (abs g) to_power k is_integrable_on M by A4;
reconsider ND = Eh` as Element of S by MEASURE1:34;
ex E be Element of S st M.E` = 0 & dom f = E &
f is E-measurable & (abs f) to_power k is_integrable_on M
proof
set AFK = (abs f) to_power k;
set AGK = (abs g) to_power k;
consider Ef be Element of S such that
A6: M.(Ef`)=0 & Ef = dom f & f is Ef-measurable by A1;
take Ef;
consider EE be Element of S such that
A7: M.EE = 0 & g|EE` = f|EE` by A3;
reconsider E1 = ND \/ EE as Element of S;
EE c= E1 by XBOOLE_1:7; then
E1` c= EE` by SUBSET_1:12; then
A8: f|E1` = (f|EE`)|E1` & g|E1` = (g|EE`)|E1` by FUNCT_1:51;
A9: dom(abs f) = Ef by A6,VALUED_1:def 11; then
dom AFK = Ef by MESFUN6C:def 4; then
A10: dom max+(R_EAL AFK) = Ef & dom max-(R_EAL AFK) = Ef
by MESFUNC2:def 2,def 3;
abs f is Ef-measurable by A6,MESFUNC6:48; then
AFK is Ef-measurable by A9,MESFUN6C:29; then
A11: Ef = dom(R_EAL AFK) & (R_EAL AFK) is Ef-measurable
by A9,MESFUN6C:def 4; then
A12: max+(R_EAL AFK) is Ef-measurable &
max-(R_EAL AFK) is Ef-measurable by MESFUNC2:25,26;
(for x being Element of X holds 0. <= (max+(R_EAL AFK)).x) &
(for x being Element of X holds 0. <= (max-(R_EAL AFK)).x)
by MESFUNC2:12,13; then
A13: max+(R_EAL AFK) is nonnegative &
max-(R_EAL AFK) is nonnegative by SUPINF_2:39;
A14: Ef = (Ef /\ E1) \/ (Ef \ E1) by XBOOLE_1:51;
reconsider E0 = Ef /\ E1 as Element of S;
reconsider E2 = Ef \ E1 as Element of S;
max+(R_EAL AFK) = (max+(R_EAL AFK))|(dom(max+(R_EAL AFK))) &
max-(R_EAL AFK) = (max-(R_EAL AFK))|(dom(max-(R_EAL AFK)))
by RELAT_1:69; then
A15:integral+(M,max+(R_EAL AFK)) = integral+(M,(max+(R_EAL AFK))|E0)
+ integral+(M,(max+(R_EAL AFK))|E2) &
integral+(M,max-(R_EAL AFK)) = integral+(M,(max-(R_EAL AFK))|E0)
+ integral+(M,(max-(R_EAL AFK))|E2)
by A10,A12,A13,A14,MESFUNC5:81,XBOOLE_1:89;
A16:integral+(M,(max+(R_EAL AFK))|E0) >= 0 &
integral+(M,(max-(R_EAL AFK))|E0) >= 0 by A12,A13,A10,MESFUNC5:80;
ND is measure_zero of M & EE is measure_zero of M
by A5,A7,MEASURE1:def 7; then
E1 is measure_zero of M by MEASURE1:37; then
M.E1 = 0 by MEASURE1:def 7; then
integral+(M,(max+(R_EAL AFK))|E1) = 0 &
integral+(M,(max-(R_EAL AFK))|E1) = 0 by A10,A12,A13,MESFUNC5:82; then
integral+(M,(max+(R_EAL AFK))|E0) = 0 &
integral+(M,(max-(R_EAL AFK))|E0) = 0
by A10,A12,A13,A16,MESFUNC5:83,XBOOLE_1:17; then
A17:integral+(M,max+(R_EAL AFK)) = integral+(M,(max+(R_EAL AFK))|E2) &
integral+(M,max-(R_EAL AFK)) = integral+(M,(max-(R_EAL AFK))|E2)
by A15,XXREAL_3:4;
Ef \ E1 = Ef /\ E1` by SUBSET_1:13; then
A18:E2 c= E1` by XBOOLE_1:17; then
f|E2 = (g|E1`)|E2 by A7,A8,FUNCT_1:51; then
A19:f|E2 = g|E2 by A18,FUNCT_1:51;
A20:(abs f)|E2 = abs(f|E2) & (abs g)|E2 = abs(g|E2) by RFUNCT_1:46;
A21:((abs f)|E2) to_power k = AFK|E2 &
((abs g)|E2) to_power k = AGK|E2 by Th20;
A22:max+(R_EAL AFK)|E2 = max+((R_EAL AFK)|E2) &
max+(R_EAL AGK)|E2 = max+((R_EAL AGK)|E2) &
max-(R_EAL AFK)|E2 = max-((R_EAL AFK)|E2) &
max-(R_EAL AGK)|E2 = max-((R_EAL AGK)|E2) by MESFUNC5:28;
A23:R_EAL AGK is_integrable_on M by A5; then
A24:integral+(M,max+(R_EAL AGK)) < +infty &
integral+(M,max-(R_EAL AGK)) < +infty;
integral+(M,max+((R_EAL AGK)|E2)) <= integral+(M,max+(R_EAL AGK)) &
integral+(M,max-((R_EAL AGK)|E2)) <= integral+(M,max-(R_EAL AGK))
by A23,MESFUNC5:97; then
integral+(M,max+(R_EAL AFK)) < +infty &
integral+(M,max-(R_EAL AFK)) < +infty
by A17,A19,A20,A21,A22,A24,XXREAL_0:2; then
(R_EAL((abs f) to_power k)) is_integrable_on M by A11;
hence thesis by A6;
end;
hence f in Lp_Functions(M,k);
end;
theorem Th38:
f in Lp_Functions(M,k) implies f in a.e-eq-class_Lp(f,M,k)
proof
assume A1: f in Lp_Functions(M,k);
f a.e.= f,M by LPSPACE1:28;
hence thesis by A1;
end;
theorem Th39:
(ex E be Element of S st M.(E`)=0 & E = dom g & g is E-measurable) &
a.e-eq-class_Lp(f,M,k) <> {} &
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k) implies
f a.e.= g,M
proof
assume that
A1:(ex E be Element of S st M.(E`)=0 & E = dom g & g is E-measurable) and
A2: a.e-eq-class_Lp(f,M,k) <> {} and
A3: a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k);
consider x be object such that
A4: x in a.e-eq-class_Lp(f,M,k) by A2,XBOOLE_0:def 1;
consider r be PartFunc of X,REAL such that
A5: x = r & r in Lp_Functions(M,k) & f a.e.= r,M by A4;
r a.e.= g,M by A1,A3,A4,A5,Th37;
hence thesis by A5,LPSPACE1:30;
end;
theorem
f in Lp_Functions(M,k) &
(ex E be Element of S st M.(E`)=0 & E = dom g & g is E-measurable) &
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k)
implies f a.e.= g,M
proof
assume that
A1: f in Lp_Functions(M,k) and
A2: (ex E be Element of S st M.(E`)=0 & E = dom g & g is E-measurable) and
A3: a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k);
a.e-eq-class_Lp(f,M,k) is non empty by A1,Th38;
hence thesis by A2,A3,Th39;
end;
theorem Th41:
f a.e.= g,M implies a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k)
proof
assume
A1: f a.e.= g,M;
now let x be object;
assume x in a.e-eq-class_Lp(f,M,k); then
consider r be PartFunc of X,REAL such that
A2: x=r & r in Lp_Functions(M,k) & f a.e.= r,M;
r a.e.= f,M by A2; then
r a.e.= g,M by A1,LPSPACE1:30; then
g a.e.= r,M;
hence x in a.e-eq-class_Lp(g,M,k) by A2;
end; then
A3:a.e-eq-class_Lp(f,M,k) c= a.e-eq-class_Lp(g,M,k);
now let x be object;
assume x in a.e-eq-class_Lp(g,M,k); then
consider r be PartFunc of X,REAL such that
A4: x=r & r in Lp_Functions(M,k) & g a.e.= r,M;
r a.e.= g,M & g a.e.= f,M by A1,A4; then
r a.e.= f,M by LPSPACE1:30; then
f a.e.= r,M;
hence x in a.e-eq-class_Lp(f,M,k) by A4;
end; then
a.e-eq-class_Lp(g,M,k) c= a.e-eq-class_Lp(f,M,k);
hence a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k) by A3;
end;
theorem Th42:
f a.e.= g,M implies a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k) by Th41;
theorem
f in Lp_Functions (M,k) & g in a.e-eq-class_Lp(f,M,k) implies
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k)
proof
assume that
A1: f in Lp_Functions(M,k) and
A2: g in a.e-eq-class_Lp(f,M,k);
ex E be Element of S st M.(E`) = 0 & dom f = E & f is E-measurable
by A1,Th35;
hence thesis by Th41,A2,Th37;
end;
theorem
(ex E be Element of S st M.(E`)=0 & E = dom f & f is E-measurable) &
(ex E be Element of S st M.(E`)=0 & E = dom f1 & f1 is E-measurable) &
(ex E be Element of S st M.(E`)=0 & E = dom g & g is E-measurable) &
(ex E be Element of S st M.(E`)=0 & E = dom g1 & g1 is E-measurable) &
a.e-eq-class_Lp(f,M,k) is non empty &
a.e-eq-class_Lp(g,M,k) is non empty &
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(f1,M,k) &
a.e-eq-class_Lp(g,M,k) = a.e-eq-class_Lp(g1,M,k)
implies a.e-eq-class_Lp(f+g,M,k) = a.e-eq-class_Lp(f1+g1,M,k)
proof
assume
(ex E be Element of S st M.(E`)=0 & E = dom f & f is E-measurable) &
(ex E be Element of S st M.(E`)=0 & E = dom f1 & f1 is E-measurable) &
(ex E be Element of S st M.(E`)=0 & E = dom g & g is E-measurable) &
(ex E be Element of S st M.(E`)=0 & E = dom g1 & g1 is E-measurable) &
a.e-eq-class_Lp(f,M,k) is non empty &
a.e-eq-class_Lp(g,M,k) is non empty &
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(f1,M,k) &
a.e-eq-class_Lp(g,M,k) = a.e-eq-class_Lp(g1,M,k);
then f a.e.= f1,M & g a.e.= g1,M by Th39;
hence thesis by Th41,LPSPACE1:31;
end;
theorem Th45:
f in Lp_Functions(M,k) & f1 in Lp_Functions(M,k) &
g in Lp_Functions(M,k) & g1 in Lp_Functions(M,k) &
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(f1,M,k) &
a.e-eq-class_Lp(g,M,k) = a.e-eq-class_Lp(g1,M,k)
implies a.e-eq-class_Lp(f+g,M,k) = a.e-eq-class_Lp(f1+g1,M,k)
proof
assume that
A1:f in Lp_Functions(M,k) and
A2:f1 in Lp_Functions(M,k) and
A3:g in Lp_Functions(M,k) and
A4:g1 in Lp_Functions(M,k) and
A5:a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(f1,M,k) &
a.e-eq-class_Lp(g,M,k) = a.e-eq-class_Lp(g1,M,k);
A6:(ex E be Element of S st M.(E`) = 0 & dom f1 = E & f1 is E-measurable) &
(ex E be Element of S st M.(E`) = 0 & dom g1 = E & g1 is E-measurable)
by A2,A4,Th35;
f in a.e-eq-class_Lp(f,M,k) &
g in a.e-eq-class_Lp(g,M,k) by A1,A3,Th38; then
f a.e.= f1,M & g a.e.= g1,M by A5,A6,Th37;
hence thesis by Th41,LPSPACE1:31;
end;
theorem
(ex E be Element of S st M.(E`) = 0 & dom f = E & f is E-measurable) &
(ex E be Element of S st M.(E`) = 0 & dom g = E & g is E-measurable) &
a.e-eq-class_Lp(f,M,k) is non empty &
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k) implies
a.e-eq-class_Lp(a(#)f,M,k) = a.e-eq-class_Lp(a(#)g,M,k)
proof
assume
(ex E be Element of S st M.(E`) = 0 & dom f = E & f is E-measurable) &
(ex E be Element of S st M.(E`) = 0 & dom g = E & g is E-measurable) &
a.e-eq-class_Lp(f,M,k) is non empty &
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k);
then a(#)f a.e.= a(#)g,M by Th39,LPSPACE1:32;
hence thesis by Th41;
end;
theorem Th47:
f in Lp_Functions(M,k) & g in Lp_Functions(M,k) &
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k) implies
a.e-eq-class_Lp(a(#)f,M,k) = a.e-eq-class_Lp(a(#)g,M,k)
proof
assume A1: f in Lp_Functions (M,k) & g in Lp_Functions (M,k) &
a.e-eq-class_Lp(f,M,k) = a.e-eq-class_Lp(g,M,k); then
A2:(ex E be Element of S st M.(E`) = 0 & dom f = E & f is E-measurable) &
(ex E be Element of S st M.(E`) = 0 & dom g = E & g is E-measurable)
by Th35;
f in a.e-eq-class_Lp(g,M,k) by A1,Th38; then
f a.e.= g,M & a(#)f in Lp_Functions(M,k) &
a(#)g in Lp_Functions(M,k) by A2,Th37,Th26;
hence thesis by Th42,LPSPACE1:32;
end;
definition let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
func CosetSet(M,k) -> non empty Subset-Family of Lp_Functions(M,k) equals
{a.e-eq-class_Lp(f,M,k) where f is PartFunc of X,REAL :
f in Lp_Functions(M,k)};
correctness
proof
set C = {a.e-eq-class_Lp(f,M,k) where f is PartFunc of X,REAL :
f in Lp_Functions(M,k)};
A1:C c= bool Lp_Functions (M,k)
proof
let x be object;assume x in C; then
ex f be PartFunc of X,REAL st
a.e-eq-class_Lp(f,M,k) = x & f in Lp_Functions (M,k);
hence x in bool Lp_Functions (M,k);
end;
X-->0 in Lp_Functions (M,k) by Th23; then
a.e-eq-class_Lp(X-->0,M,k) in C;
hence thesis by A1;
end;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
k be positive Real;
func addCoset(M,k) -> BinOp of CosetSet(M,k) means :Def8:
for A,B be Element of CosetSet(M,k), a,b be PartFunc of X,REAL st
a in A & b in B holds it.(A,B) = a.e-eq-class_Lp(a+b,M,k);
existence
proof
set C = CosetSet(M,k);
defpred P[set,set,set] means
for a,b be PartFunc of X,REAL st a in $1& b in $2 holds
$3 = a.e-eq-class_Lp(a+b,M,k);
A1:now let A,B be Element of C;
A in C; then
consider a be PartFunc of X,REAL such that
A2: A=a.e-eq-class_Lp(a,M,k) & a in Lp_Functions(M,k);
A3: ex E be Element of S st M.E` = 0 & dom a = E & a is E-measurable
by A2,Th35;
B in C; then
consider b be PartFunc of X,REAL such that
A4: B=a.e-eq-class_Lp(b,M,k) & b in Lp_Functions(M,k);
A5: ex E be Element of S st M.E` = 0 & dom b = E & b is E-measurable
by A4,Th35;
set z = a.e-eq-class_Lp(a+b,M,k);
a+b in Lp_Functions(M,k) by Th25,A2,A4; then
z in C; then
reconsider z as Element of C;
take z;
now let a1,b1 be PartFunc of X,REAL;
assume a1 in A & b1 in B; then
a1 a.e.= a,M & b1 a.e.= b,M by A2,A3,A4,A5,Th37;
hence z = a.e-eq-class_Lp(a1+b1,M,k) by Th42,LPSPACE1:31;
end;
hence P[A,B,z];
end;
consider f be Function of [:C,C:],C such that
A6: for A,B be Element of C holds P[A,B, f.(A,B)] from BINOP_1:sch 3(A1);
reconsider f as BinOp of C;
take f;
let A,B be Element of C;
let a,b be PartFunc of X,REAL;
assume a in A & b in B;
hence f.(A,B) = a.e-eq-class_Lp(a+b,M,k) by A6;
end;
uniqueness
proof
let f1,f2 be BinOp of CosetSet(M,k) such that
A7: for A,B be Element of CosetSet(M,k), a,b be PartFunc of X,REAL st
a in A & b in B holds f1.(A,B) = a.e-eq-class_Lp(a+b,M,k) and
A8:for A,B be Element of CosetSet(M,k), a,b be PartFunc of X,REAL st
a in A & b in B holds f2.(A,B) = a.e-eq-class_Lp(a+b,M,k);
now let A,B be Element of CosetSet(M,k);
A in CosetSet(M,k); then
consider a1 be PartFunc of X,REAL such that
A9: A=a.e-eq-class_Lp(a1,M,k) & a1 in Lp_Functions(M,k);
B in CosetSet(M,k); then
consider b1 be PartFunc of X,REAL such that
A10: B=a.e-eq-class_Lp(b1,M,k) & b1 in Lp_Functions(M,k);
A11:a1 in A & b1 in B by A9,A10,Th38; then
f1.(A,B) = a.e-eq-class_Lp(a1+b1,M,k) by A7;
hence f1.(A,B) = f2.(A,B) by A8,A11;
end;
hence thesis by BINOP_1:2;
end;
end;
definition let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
func zeroCoset(M,k) -> Element of CosetSet(M,k) equals
a.e-eq-class_Lp(X-->0,M,k);
correctness
proof
X-->0 in Lp_Functions(M,k) by Th23; then
a.e-eq-class_Lp(X-->0,M,k) in CosetSet(M,k);
hence thesis;
end;
end;
definition let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
func lmultCoset(M,k) -> Function of [:REAL,CosetSet(M,k):],CosetSet(M,k) means
:Def10:
for z be Real, A be Element of CosetSet(M,k),
f be PartFunc of X,REAL st
f in A holds it.(z,A) = a.e-eq-class_Lp(z(#)f,M,k);
existence
proof
set C = CosetSet(M,k);
defpred P[Real,set,set] means
for f be PartFunc of X,REAL st f in $2 holds
$3 = a.e-eq-class_Lp($1(#)f,M,k);
A1:now let z be Element of REAL, A be Element of C;
A in C; then
consider a be PartFunc of X,REAL such that
A2: A = a.e-eq-class_Lp(a,M,k) & a in Lp_Functions(M,k);
A3: ex E be Element of S st M.E`=0 & E = dom a & a is E-measurable
by A2,Th35;
set c = a.e-eq-class_Lp(z(#)a,M,k);
z(#)a in Lp_Functions(M,k) by Th26,A2; then
c in C; then
reconsider c as Element of C;
take c;
now let a1 be PartFunc of X,REAL;
assume a1 in A; then
z(#)a1 a.e.= z(#)a,M by A2,A3,Th37,LPSPACE1:32;
hence c = a.e-eq-class_Lp(z(#)a1,M,k) by Th42;
end;
hence P[z,A,c];
end;
consider f be Function of [:REAL,C:],C such that
A4: for z be Element of REAL, A be Element of C holds P[z,A, f.(z,A)]
from BINOP_1:sch 3(A1);
A5: for z be Real, A be Element of C holds P[z,A, f.(z,A)]
proof let z be Real, A be Element of C;
reconsider z as Element of REAL by XREAL_0:def 1;
P[z,A, f.(z,A)] by A4;
hence thesis;
end;
take f;
let z be Real, A be Element of C, a be PartFunc of X,REAL;
assume a in A;
hence f.(z,A) = a.e-eq-class_Lp(z(#)a,M,k) by A5;
end;
uniqueness
proof
set C = CosetSet(M,k);
let f1,f2 be Function of [:REAL,C:],C such that
A6: for z be Real, A be Element of CosetSet(M,k),
a be PartFunc of X,REAL st a in A holds
f1.(z,A) = a.e-eq-class_Lp(z(#)a,M,k) and
A7: for z be Real, A be Element of CosetSet(M,k),
a be PartFunc of X,REAL st a in A holds
f2.(z,A) = a.e-eq-class_Lp(z(#)a,M,k);
now let z be Element of REAL, A be Element of CosetSet(M,k);
A in C; then
consider a1 be PartFunc of X,REAL such that
A8: A=a.e-eq-class_Lp(a1,M,k) & a1 in Lp_Functions(M,k);
thus f1.(z,A) = a.e-eq-class_Lp(z(#)a1,M,k) by A6,A8,Th38
.= f2.(z,A) by A7,A8,Th38;
end;
hence thesis by BINOP_1:2;
end;
end;
definition let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
func Pre-Lp-Space(M,k) -> strict RLSStruct means :Def11:
the carrier of it = CosetSet(M,k) & the addF of it = addCoset(M,k) &
0.it = zeroCoset(M,k) &
the Mult of it = lmultCoset(M,k);
existence
proof
take
RLSStruct(# CosetSet(M,k),zeroCoset(M,k),addCoset(M,k),lmultCoset(M,k) #);
thus thesis;
end;
uniqueness;
end;
registration let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
cluster Pre-Lp-Space(M,k) -> non empty;
coherence
proof
the carrier of Pre-Lp-Space(M,k) = CosetSet(M,k) by Def11;
hence thesis;
end;
end;
registration let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
cluster Pre-Lp-Space(M,k) -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof
set C = CosetSet(M,k), aC = addCoset(M,k), lC = lmultCoset(M,k);
set A = Pre-Lp-Space(M,k);
A1: the carrier of A = CosetSet(M,k) & the addF of A = addCoset(M,k) &
0.A = zeroCoset(M,k) &
the Mult of A = lmultCoset(M,k) by Def11;
thus A is Abelian
proof
let A1,A2 be Element of A;
A1 in C by A1; then
consider a be PartFunc of X,REAL such that
A2: A1 = a.e-eq-class_Lp(a,M,k) & a in Lp_Functions(M,k);
A2 in C by A1; then
consider b be PartFunc of X,REAL such that
A3: A2 = a.e-eq-class_Lp(b,M,k) & b in Lp_Functions(M,k);
A4: a in A1 & b in A2 by A2,A3,Th38; then
A1+A2 = a.e-eq-class_Lp(a+b,M,k) by A1,Def8;
hence A1+A2 = A2+A1 by A1,A4,Def8;
end;
thus A is add-associative
proof
let A1,A2,A3 be Element of A;
A1 in C by A1; then
consider a be PartFunc of X,REAL such that
A5: A1=a.e-eq-class_Lp(a,M,k) & a in Lp_Functions(M,k);
A2 in C by A1; then
consider b be PartFunc of X,REAL such that
A6: A2=a.e-eq-class_Lp(b,M,k) & b in Lp_Functions(M,k);
A3 in C by A1; then
consider c be PartFunc of X,REAL such that
A7: A3=a.e-eq-class_Lp(c,M,k) & c in Lp_Functions(M,k);
A8: a in A1 & b in A2 & c in A3 by A5,A6,A7,Th38; then
aC.(A1,A2) =a.e-eq-class_Lp(a+b,M,k) &
aC.(A2,A3) =a.e-eq-class_Lp(b+c,M,k) by A1,Def8; then
A9:a+b in A1+A2 & b+c in A2+A3 by A1,Th38,Th25,A5,A6,A7;
reconsider a1=a,b1=b,c1=c as VECTOR of RLSp_LpFunct(M,k) by A5,A6,A7;
A10:a+b = a1+b1 & b+c = b1+c1 by Th29; then
a+(b+c) =a1+(b1+c1) by Th29; then
a+(b+c) =(a1+b1)+c1 by RLVECT_1:def 3; then
a+(b+c) = a+b+c by A10,Th29; then
A1+A2+A3 = a.e-eq-class_Lp(a+(b+c),M,k) by A8,A9,Def8,A1;
hence A1+A2+A3 = A1+(A2+A3) by A8,A9,Def8,A1;
end;
thus A is right_zeroed
proof
let A1 be Element of A;
A1 in C by A1; then
consider a be PartFunc of X,REAL such that
A11: A1=a.e-eq-class_Lp(a,M,k) & a in Lp_Functions(M,k);
A12:a in A1 by A11,Th38;
set z = X-->0;
A13:z in 0.A by A1,Th38,Th23;
reconsider a1=a,z1=z as VECTOR of RLSp_LpFunct(M,k) by A11,Th23;
a+z =a1+z1 by Th29
.=a1+0.RLSp_LpFunct(M,k)
.=a by RLVECT_1:def 4;
hence A1+0.A = A1 by A1,A11,A12,A13,Def8;
end;
thus A is right_complementable
proof
let A1 be Element of A;
A1 in C by A1; then
consider a be PartFunc of X,REAL such that
A14: A1=a.e-eq-class_Lp(a,M,k) & a in Lp_Functions(M,k);
A15:a in A1 by A14,Th38;
reconsider a1=a as VECTOR of RLSp_LpFunct(M,k) by A14;
A16:(-1)(#)a in Lp_Functions (M,k) by A14,Th26;
set A2 = a.e-eq-class_Lp((-1)(#)a,M,k);
A2 in C by A16; then
reconsider A2 as Element of A by A1;
take A2;
A17:(-1)(#)a in A2 by Th38,A14,Th26;
consider v,g be PartFunc of X,REAL such that
A18: v in Lp_Functions (M,k) & g in Lp_Functions (M,k) &
v = a1+(-1)*a1 & g = X --> 0 & v a.e.= g,M by Th31;
(-1)(#)a = (-1)*a1 by Th30; then
a+(-1)(#)a a.e.= g,M by Th29,A18; then
0.A = a.e-eq-class_Lp(a+ (-1)(#)a,M,k) by Th42,A18,A1;
hence A1 + A2 = 0.A by A15,A17,Def8,A1;
end;
now let x0,y0 be Real, A1,A2 be Element of A;
reconsider x=x0,y=y0 as Real;
A1 in C by A1; then
consider a be PartFunc of X,REAL such that
A19: A1=a.e-eq-class_Lp(a,M,k) & a in Lp_Functions(M,k);
A2 in C by A1; then
consider b be PartFunc of X,REAL such that
A20: A2=a.e-eq-class_Lp(b,M,k) & b in Lp_Functions(M,k);
A21:a in A1 & b in A2 by A19,A20,Th38; then
aC.(A1,A2) =a.e-eq-class_Lp(a+b,M,k) by A1,Def8; then
A22:a+b in (A1+A2) by Th38,Th25,A19,A20,A1;
reconsider a1=a,b1=b as VECTOR of RLSp_LpFunct (M,k) by A19,A20;
A23:y(#)a = y*a1 & x(#)a = x*a1 & x(#)b = x*b1 &
(x+y)(#)a = (x+y)*a1 & 1(#)a =1*a1 by Th30;
a+b = a1+b1 by Th29; then
x(#)(a+b) = x*(a1+b1) by Th30; then
x(#)(a+b) = x*a1+x*b1 by RLVECT_1:def 5; then
A24:x(#)(a+b) = x(#)a + x(#)b by A23,Th29;
(x+y)(#)a = x*a1+y*a1 by A23,RLVECT_1:def 6; then
A25:(x+y)(#)a = x(#)a + y(#)a by A23,Th29;
x(#)(y(#)a) =x*(y*a1) by A23,Th30 .= (x*y)*a1
by RLVECT_1:def 7;
then
A26:x(#)(y(#)a) = (x*y)(#)a by Th30;
lC.(x,A1) =a.e-eq-class_Lp(x(#)a,M,k) &
lC.(x,A2) =a.e-eq-class_Lp(x(#)b,M,k) &
lC.(y,A1) =a.e-eq-class_Lp(y(#)a,M,k) by A1,A21,Def10; then
A27:x(#)a in x*A1 & x(#)b in x*A2 & y(#)a in y*A1 by A1,Th38,Th26,A19,A20;
x*(A1+A2) = a.e-eq-class_Lp(x(#)a+x(#)b,M,k) by A1,A24,A22,Def10;
hence x0*(A1+A2) = x0*A1+x0*A2 by A1,A27,Def8;
(x+y)*A1 = a.e-eq-class_Lp(x(#)a+y(#)a,M,k) by A1,A25,A21,Def10;
hence (x0+y0)*A1 = x0*A1+y0*A1 by A27,Def8,A1;
(x0*y0)*A1 = a.e-eq-class_Lp(x(#)(y(#)a),M,k) by A1,A26,A21,Def10;
hence (x0*y0)*A1 =x0*(y0*A1) by A27,Def10,A1;
1(#)a = a by A23,RLVECT_1:def 8;
hence 1*A1 = A1 by A19,A21,Def10,A1;
end;
hence thesis;
end;
end;
begin :: Real Normed Space of Lp Integrable Functions
theorem Th48:
f in Lp_Functions(M,k) & g in Lp_Functions(M,k) & f a.e.= g,M implies
Integral(M,(abs f) to_power k) = Integral(M,(abs g) to_power k)
proof
set t = (abs f) to_power k;
set s = (abs g) to_power k;
assume
A1: f in Lp_Functions (M,k) & g in Lp_Functions (M,k) & f a.e.= g,M;
then ex f1 be PartFunc of X,REAL st
f=f1 & ex E be Element of S st M.E` =0 & dom f1 = E &
f1 is E-measurable & (abs f1) to_power k is_integrable_on M; then
consider Df be Element of S such that
A2: M.Df`=0 & dom f = Df & f is Df-measurable & t is_integrable_on M;
ex g1 be PartFunc of X,REAL st
g=g1 & ex E be Element of S st M.E` =0 & dom g1 = E &
g1 is E-measurable & (abs g1) to_power k is_integrable_on M by A1; then
consider Dg be Element of S such that
A3: M.Dg`=0 & dom g = Dg & g is Dg-measurable & s is_integrable_on M;
A4:dom(abs f) = dom f & dom(abs g) = dom g by VALUED_1:def 11;
consider E1 being Element of S such that
A5: M.E1 = 0 & f|E1` = g|E1` by A1;
reconsider NDf = Df`, NDg = Dg` as Element of S by MEASURE1:34;
set Ef = Df \ (NDg \/ E1);
set Eg = Dg \ (NDf \/ E1);
set E2 = NDf \/ NDg \/ E1;
NDf is measure_zero of M & NDg is measure_zero of M &
E1 is measure_zero of M by A2,A3,A5,MEASURE1:def 7; then
NDf \/ E1 is measure_zero of M & NDg \/ E1 is measure_zero of M
by MEASURE1:37; then
A6:M.(NDf \/ E1) = 0 & M.(NDg \/ E1) = 0 by MEASURE1:def 7;
X \ NDf = X /\ Df & X \ NDg = X /\ Dg by XBOOLE_1:48; then
A7:X \ NDf = Df & X \ NDg = Dg by XBOOLE_1:28;
Ef = (Df \ NDg) \ E1 & Eg = (Dg \ NDf) \ E1 by XBOOLE_1:41; then
A8:Ef = (X \ (NDf \/ NDg)) \ E1 & Eg = (X \ (NDf \/ NDg)) \ E1
by A7,XBOOLE_1:41; then
A9:Ef = X \ E2 & Eg = X \ E2 by XBOOLE_1:41;
(abs f) is Df-measurable & (abs g) is Dg-measurable
by A2,A3,MESFUNC6:48; then
A10:t is Df-measurable & s is Dg-measurable by A2,A3,A4,MESFUN6C:29;
A11:dom t = Df & dom s = Dg by A2,A3,A4,MESFUN6C:def 4; then
A12:Integral(M,t|Ef) = Integral(M,t) &
Integral(M,s|Eg) = Integral(M,s) by A6,A10,MESFUNC6:89;
dom(t|Ef) = dom t /\ Ef & dom(s|Ef) = dom s /\ Ef by RELAT_1:61; then
A13:dom(t|Ef) = (Df /\ Df) \ (NDg \/ E1) &
dom(s|Ef) = (Dg /\ Dg) \ (NDf \/ E1) by A11,A8,XBOOLE_1:49;
now let x be Element of X;
assume A14: x in dom(t|Ef);
A15: dom(t|Ef) c= dom t & dom(s|Ef) c= dom s by RELAT_1:60;
E2` c= E1` by XBOOLE_1:7,34; then
A16: f.x =(f|E1`).x & g.x = (g|E1`).x by A14,A13,A9,FUNCT_1:49;
(t|Ef).x = t.x & (s|Ef).x = s.x by A14,A13,FUNCT_1:49; then
(t|Ef).x = ((abs f).x) to_power k &
(s|Ef).x = ((abs g).x) to_power k by A8,A13,A14,A15,MESFUN6C:def 4; then
(t|Ef).x = (|.f.x qua Complex.|) to_power k &
(s|Ef).x = (|.g.x qua Complex.|) to_power k
by VALUED_1:18;
hence (t|Ef).x = (s|Ef).x by A5,A16;
end;
hence thesis by A12,A13,A8,PARTFUN1:5;
end;
theorem Th49:
f in Lp_Functions(M,k) implies
Integral(M,(abs f) to_power k) in REAL & 0 <= Integral(M,(abs f) to_power k)
proof
assume f in Lp_Functions(M,k); then
A1:ex f1 be PartFunc of X,REAL st
f=f1 & ex ND be Element of S st M.ND` =0 & dom f1 = ND &
f1 is ND-measurable & (abs f1) to_power k is_integrable_on M; then
-infty < Integral(M,(abs f) to_power k) &
Integral(M,(abs f) to_power k) < +infty by MESFUNC6:90;
hence Integral(M,(abs f) to_power k) in REAL by XXREAL_0:14;
R_EAL((abs f) to_power k) is_integrable_on M by A1; then
consider A be Element of S such that
A2: A = dom(R_EAL((abs f) to_power k)) &
R_EAL((abs f) to_power k) is A-measurable;
A = dom((abs f) to_power k) &
(abs f) to_power k is A-measurable by A2;
hence thesis by MESFUNC6:84;
end;
theorem Th50:
(ex x be VECTOR of Pre-Lp-Space(M,k) st f in x & g in x) implies
f a.e.= g,M & f in Lp_Functions(M,k) & g in Lp_Functions(M,k)
proof
assume ex x be VECTOR of Pre-Lp-Space(M,k) st f in x & g in x; then
consider x be VECTOR of Pre-Lp-Space(M,k) such that
A1: f in x & g in x;
x in the carrier of Pre-Lp-Space(M,k); then
x in CosetSet(M,k) by Def11; then
consider h be PartFunc of X,REAL such that
A2: x=a.e-eq-class_Lp(h,M,k) & h in Lp_Functions(M,k);
(ex i be PartFunc of X,REAL st f=i & i in Lp_Functions(M,k) & h a.e.= i,M) &
(ex j be PartFunc of X,REAL st g=j & j in Lp_Functions(M,k) & h a.e.= j,M)
by A1,A2; then
f a.e.= h,M & h a.e.= g,M;
hence thesis by A1,A2,LPSPACE1:30;
end;
reserve x for Point of Pre-Lp-Space(M,k);
theorem Th51:
f in x implies (abs f) to_power k is_integrable_on M & f in Lp_Functions(M,k)
proof
assume A1: f in x;
x in the carrier of Pre-Lp-Space(M,k); then
x in CosetSet(M,k) by Def11; then
consider h be PartFunc of X,REAL such that
A2: x=a.e-eq-class_Lp(h,M,k) & h in Lp_Functions(M,k);
ex g be PartFunc of X,REAL st
f=g & g in Lp_Functions (M,k) & h a.e.= g,M by A1,A2; then
ex f0 be PartFunc of X,REAL st
f=f0 & ex ND be Element of S st M.ND` =0 & dom f0 = ND &
f0 is ND-measurable & (abs f0) to_power k is_integrable_on M;
hence thesis;
end;
theorem Th52:
f in x & g in x implies f a.e.= g,M &
Integral(M,(abs f) to_power k) = Integral(M,(abs g) to_power k)
proof
assume f in x & g in x; then
f a.e.= g,M & f in Lp_Functions(M,k) & g in Lp_Functions(M,k) by Th50;
hence thesis by Th48;
end;
definition let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
func Lp-Norm(M,k) -> Function of the carrier of Pre-Lp-Space (M,k),REAL means
:Def12:
for x be Point of Pre-Lp-Space(M,k) ex f be PartFunc of X,REAL st f in x &
ex r be Real st
r = Integral(M,(abs f) to_power k) & it.x = r to_power (1/k);
existence
proof
defpred P[set,set] means
ex f be PartFunc of X,REAL st
f in $1 &
ex r be Real st
r = Integral(M,(abs f) to_power k) & $2 = r to_power (1/k);
A1:for x be Point of Pre-Lp-Space(M,k) ex y being Element of REAL st P[x,y]
proof
let x be Point of Pre-Lp-Space(M,k);
x in the carrier of Pre-Lp-Space(M,k); then
x in CosetSet(M,k) by Def11; then
consider f be PartFunc of X,REAL such that
A2: x=a.e-eq-class_Lp(f,M,k) & f in Lp_Functions(M,k);
reconsider r1 = Integral(M,(abs f) to_power k)
as Element of REAL by A2,Th49;
r1 to_power (1/k) in REAL by XREAL_0:def 1;
hence thesis by A2,Th38;
end;
consider F being Function of the carrier of Pre-Lp-Space(M,k),REAL such that
A3: for x being Point of Pre-Lp-Space (M,k) holds P[x,F.x]
from FUNCT_2:sch 3(A1);
take F;
thus thesis by A3;
end;
uniqueness
proof
let N1,N2 be Function of the carrier of Pre-Lp-Space (M,k),REAL;
assume
A4: (for x be Point of Pre-Lp-Space(M,k) ex f be PartFunc of X,REAL st
f in x & ex r1 be Real st r1 = Integral(M,(abs f) to_power k) &
N1.x = r1 to_power (1/k)) &
(for x be Point of Pre-Lp-Space(M,k) ex g be PartFunc of X,REAL st
g in x & ex r2 be Real st r2 = Integral(M,(abs g) to_power k) &
N2.x = r2 to_power (1/k));
now let x be Point of Pre-Lp-Space(M,k);
(ex f be PartFunc of X,REAL st f in x & ex r1 be Real st
r1 = Integral(M,(abs f) to_power k) & N1.x = r1 to_power (1/k)) &
(ex g be PartFunc of X,REAL st g in x & ex r2 be Real st
r2 = Integral(M,(abs g) to_power k) & N2.x = r2 to_power (1/k)) by A4;
hence N1.x=N2.x by Th52;
end;
hence N1=N2 by FUNCT_2:63;
end;
end;
definition let X be non empty set, S be SigmaField of X,
M be sigma_Measure of S, k be positive Real;
func Lp-Space(M,k) -> non empty NORMSTR equals
NORMSTR (# the carrier of Pre-Lp-Space(M,k),
the ZeroF of Pre-Lp-Space(M,k),
the addF of Pre-Lp-Space(M,k),
the Mult of Pre-Lp-Space(M,k),
Lp-Norm(M,k) #);
coherence;
end;
reserve x,y for Point of Lp-Space(M,k);
theorem Th53:
(ex f be PartFunc of X,REAL st
f in Lp_Functions(M,k) & x= a.e-eq-class_Lp(f,M,k)) &
for f be PartFunc of X,REAL st f in x holds
ex r be Real st
0<=r & r = Integral(M,(abs f) to_power k) & ||.x.|| =r to_power (1/k)
proof
x in the carrier of Pre-Lp-Space(M,k); then
x in CosetSet(M,k) by Def11; then
ex g be PartFunc of X,REAL st
x=a.e-eq-class_Lp(g,M,k) & g in Lp_Functions(M,k);
hence ex f be PartFunc of X,REAL st f in Lp_Functions(M,k) &
x= a.e-eq-class_Lp(f,M,k);
consider f be PartFunc of X,REAL such that
A1: f in x & ex r be Real st r = Integral(M,(abs f) to_power k) &
(Lp-Norm(M,k)).x = r to_power (1/k) by Def12;
hereby let g be PartFunc of X,REAL;
assume A2: g in x; then
A3: g in Lp_Functions(M,k) by Th50;
Integral(M,(abs g) to_power k) = Integral(M,(abs f) to_power k)
by A1,Th52,A2;
hence ex r be Real st 0 <= r & r = Integral(M,(abs g) to_power k) &
||.x.|| =r to_power (1/k) by A1,A3,Th49;
end;
end;
theorem Th54:
(f in x & g in y implies f+g in x+y) & (f in x implies a(#)f in a*x)
proof
set C = CosetSet(M,k);
hereby assume A1: f in x & g in y;
x in the carrier of Pre-Lp-Space(M,k); then
A2: x in C by Def11; then
consider a be PartFunc of X,REAL such that
A3: x=a.e-eq-class_Lp(a,M,k) & a in Lp_Functions(M,k);
A4: a in x by A3,Th38;
y in the carrier of Pre-Lp-Space(M,k); then
A5: y in C by Def11; then
consider b be PartFunc of X,REAL such that
A6: y=a.e-eq-class_Lp(b,M,k) & b in Lp_Functions(M,k);
b in y by A6,Th38; then
(addCoset(M,k)).(x,y) = a.e-eq-class_Lp(a+b,M,k) by A2,A5,A4,Def8;
then
A7: x+y = a.e-eq-class_Lp(a+b,M,k) by Def11;
ex r be PartFunc of X,REAL st f=r & r in Lp_Functions(M,k) &
a a.e.= r,M by A1,A3; then
A8:a.e-eq-class_Lp(a,M,k) = a.e-eq-class_Lp(f,M,k) by Th42;
ex r be PartFunc of X,REAL st g=r & r in Lp_Functions (M,k) &
b a.e.= r,M by A1,A6; then
a.e-eq-class_Lp(b,M,k) = a.e-eq-class_Lp(g,M,k) by Th42; then
a.e-eq-class_Lp(a+b,M,k) = a.e-eq-class_Lp(f+g,M,k) by A1,A3,A6,A8,Th45;
hence f+g in x+y by Th38,A7,Th25,A3,A1,A6;
end;
hereby assume A9:f in x;
x in the carrier of Pre-Lp-Space (M,k); then
A10:x in C by Def11; then
consider f1 be PartFunc of X,REAL such that
A11: x=a.e-eq-class_Lp(f1,M,k) & f1 in Lp_Functions (M,k);
f1 in x by A11,Th38; then
(lmultCoset(M,k)).(a,x) = a.e-eq-class_Lp(a(#)f1,M,k) by A10,Def10;
then
A12:a*x = a.e-eq-class_Lp(a(#)f1,M,k) by Def11;
ex r be PartFunc of X,REAL st f=r & r in Lp_Functions (M,k) &
f1 a.e.= r,M by A9,A11; then
a.e-eq-class_Lp(f1,M,k) = a.e-eq-class_Lp(f,M,k) by Th42; then
a.e-eq-class_Lp(a(#)f1,M,k) = a.e-eq-class_Lp(a(#)f,M,k) by A11,A9,Th47;
hence a(#)f in a*x by A12,Th26,A9,A11,Th38;
end;
end;
theorem Th55:
f in x implies x= a.e-eq-class_Lp(f,M,k) & ( ex r be Real st
0 <=r & r = Integral(M,(abs f) to_power k) & ||.x.|| = r to_power (1/k) )
proof
assume A1:f in x;
x in the carrier of Pre-Lp-Space(M,k); then
x in CosetSet(M,k) by Def11; then
consider g be PartFunc of X,REAL such that
A2: x=a.e-eq-class_Lp(g,M,k) & g in Lp_Functions(M,k);
g in x by A2,Th38; then
f a.e.= g,M & f in Lp_Functions(M,k) & g in Lp_Functions(M,k) by A1,Th50;
hence thesis by Th53,A1,A2,Th42;
end;
theorem Th56:
X --> 0 in L1_Functions M
proof
reconsider ND = {} as Element of S by MEASURE1:34;
A1:M.ND =0 by VALUED_0:def 19;
X --> In(0,REAL) is Function of X,REAL by FUNCOP_1:46; then
A2:dom (X --> 0) = ND` by FUNCT_2:def 1;
for x be Element of X st x in dom (X --> 0) holds (X --> 0).x = 0
by FUNCOP_1:7; then
X --> 0 is_integrable_on M by A2,Th15;
hence thesis by A1,A2;
end;
theorem Th57:
f in Lp_Functions(M,k) & Integral(M,(abs f) to_power k) = 0 implies
f a.e.= X-->0,M
proof
assume that
A1: f in Lp_Functions(M,k) and
A2: Integral(M,(abs f) to_power k) = 0;
ex h be PartFunc of X,REAL st
f=h & ex ND be Element of S st M.ND` =0 & dom h = ND &
h is ND-measurable & (abs h) to_power k is_integrable_on M by A1; then
consider NDf be Element of S such that
A3: M.NDf`=0 & dom f = NDf & f is NDf-measurable &
(abs f) to_power k is_integrable_on M;
reconsider t = (abs f) to_power k as PartFunc of X,REAL;
reconsider ND = NDf` as Element of S by MEASURE1:34;
A4:dom t = dom (abs f) by MESFUN6C:def 4; then
A5:dom t = NDf by A3,VALUED_1:def 11;
dom t = ND` by A4,A3,VALUED_1:def 11; then
A6:t in L1_Functions M by A3;
abs t = t by Th14; then
t a.e.= X-->0,M by A2,A6,LPSPACE1:53; then
consider ND1 be Element of S such that
A7: M.ND1 = 0 & (abs f) to_power k|ND1` = (X-->0)|ND1`;
set ND2= ND \/ ND1;
ND is measure_zero of M & ND1 is measure_zero of M
by A3,A7,MEASURE1:def 7; then
ND2 is measure_zero of M by MEASURE1:37; then
A8:M.ND2 = 0 by MEASURE1:def 7;
A9:ND2` c= ND` & ND2` c= ND1` by XBOOLE_1:7,34;
dom(X-->0) = X by FUNCOP_1:13; then
A10:dom((X-->0)|ND2`) = ND2` by RELAT_1:62;
A11:dom(f|ND2`) = ND2` by A3,A9,RELAT_1:62;
for x be object st x in dom (f|ND2`) holds (f|ND2`).x = ((X-->0)|ND2`).x
proof
let x be object;
assume A12: x in dom (f|ND2`);
A13: now assume f.x <> 0; then
|.f.x.| > 0 by COMPLEX1:47; then
|.f.x qua Complex.| to_power k <> 0 by POWER:34; then
((abs f).x) to_power k <> 0 by VALUED_1:18; then
A14: ((abs f) to_power k).x <> 0 by A5,A9,A12,A11,MESFUN6C:def 4;
((X-->0)|ND1`).x = (X-->0).x by A9,A12,A11,FUNCT_1:49; then
((X-->0)|ND1`).x = 0 by A12,FUNCOP_1:7;
hence contradiction by A14,A7,A9,A12,A11,FUNCT_1:49;
end;
((X-->0)|ND2`).x =(X-->0).x by A11,A12,FUNCT_1:49; then
((X-->0)|ND2`).x = 0 by A12,FUNCOP_1:7;
hence thesis by A11,A12,A13,FUNCT_1:49;
end; then
f |ND2` = (X-->0)|ND2` by A10,A11,FUNCT_1:def 11;
hence thesis by A8;
end;
theorem Th58:
Integral(M,(abs(X-->0)) to_power k) = 0
proof
A1:for x be object st x in dom (X-->0) holds 0 <= (X-->0).x;
then Integral(M,(abs(X-->0)) to_power k)
= Integral(M,(X-->0) to_power k) by Th14,MESFUNC6:52
.= Integral(M,(X-->0)) by Th12
.= Integral(M,abs(X-->0)) by A1,Th14,MESFUNC6:52;
hence thesis by LPSPACE1:54;
end;
:: lemma for Holder
theorem Th59:
for m,n be positive Real st
1/m +1/n =1 & f in Lp_Functions(M,m) & g in Lp_Functions(M,n) holds
f(#)g in L1_Functions M & f(#)g is_integrable_on M
proof
let m,n be positive Real;
assume that
A1: 1/m +1/n =1 and
A2: f in Lp_Functions(M,m) & g in Lp_Functions(M,n);
A3: m > 1 & n > 1 by A1,Th1;
consider f1 be PartFunc of X,REAL such that
A4: f=f1 & ex NDf be Element of S st M.NDf` =0 & dom f1 = NDf &
f1 is NDf-measurable & (abs f1) to_power m is_integrable_on M by A2;
consider EDf be Element of S such that
A5: M.EDf` =0 & dom f1 = EDf & f1 is EDf-measurable by A4;
consider g1 be PartFunc of X,REAL such that
A6: g=g1 & ex NDg be Element of S st M.NDg` =0 & dom g1 = NDg &
g1 is NDg-measurable & (abs g1) to_power n is_integrable_on M by A2;
consider EDg be Element of S such that
A7: M.EDg` =0 & dom g1 = EDg & g1 is EDg-measurable by A6;
set u =(abs f1) to_power m;
set v =(abs g1) to_power n;
set w = f1(#)g1;
set z = (1/m)(#)u + (1/n)(#)v;
A8: dom f1 = dom(abs f1) & dom g1 = dom(abs g1) by VALUED_1:def 11; then
A9: dom u = dom f1 & dom v = dom g1 by MESFUN6C:def 4; then
A10: dom w = dom u /\ dom v by VALUED_1:def 4;
set Nf = EDf`;
set Ng = EDg`;
set E = EDf /\ EDg;
reconsider Nf,Ng as Element of S by MEASURE1:34;
dom u = Nf` & dom v = Ng` by A5,A7,A8,MESFUN6C:def 4; then
u in L1_Functions M & v in L1_Functions M by A4,A5,A6,A7; then
(1/m)(#)u in L1_Functions M & (1/n)(#)v in L1_Functions M
by LPSPACE1:24; then
z in L1_Functions M by LPSPACE1:23; then
A11:ex h be PartFunc of X,REAL st z = h &
ex ND be Element of S st M.ND=0 & dom h = ND` & h is_integrable_on M;
dom((1/m)(#)u) = dom u & dom((1/n)(#)v) = dom v by VALUED_1:def 5; then
A12:dom z = dom u /\ dom v by VALUED_1:def 1;
A13:E` = EDf` \/ EDg` by XBOOLE_1:54;
Nf is measure_zero of M & Ng is measure_zero of M
by A5,A7,MEASURE1:def 7; then
Nf \/ Ng is measure_zero of M by MEASURE1:37; then
A14:M.E` = 0 by A13,MEASURE1:def 7;
f1 is E-measurable & g1 is E-measurable
by A5,A7,MESFUNC6:16,XBOOLE_1:17; then
A15:w is E-measurable by A5,A7,MESFUN7C:31;
for x be Element of X st x in dom w holds |.w.x qua Complex.| <= z.x
proof
let x be Element of X;
assume A16: x in dom w;
abs(f1(#)g1) = (abs f1)(#)(abs g1) by RFUNCT_1:24; then
abs(f1(#)g1).x = (abs f1).x * (abs g1).x by VALUED_1:5; then
A17: |.(f1(#)g1).x.| = (abs f1).x * (abs g1).x by VALUED_1:18;
A18: (abs f1).x >= 0 & (abs g1).x >= 0 by MESFUNC6:51;
x in dom u & x in dom v by A16,A10,XBOOLE_0:def 4;
then ((abs f1).x) to_power m /m = (1/m)*(((abs f1) to_power m).x) &
((abs g1).x) to_power n /n = (1/n)*(((abs g1) to_power n).x)
by MESFUN6C:def 4; then
((abs f1).x) to_power m /m = ((1/m)(#)((abs f1) to_power m)).x &
((abs g1).x) to_power n /n = ((1/n)(#)((abs g1) to_power n)).x
by VALUED_1:6; then
|.w.x.| <= ((1/m)(#)u).x + ((1/n)(#)v).x by A1,A3,A17,A18,HOLDER_1:5;
hence thesis by A16,A10,A12,VALUED_1:def 1;
end;then
A19:w is_integrable_on M by A5,A7,A9,A10,A11,A15,A12,MESFUNC6:96;
set ND = E`;
reconsider ND as Element of S by MEASURE1:34;
dom w = ND` by A5,A7,VALUED_1:def 4;
hence thesis by A4,A6,A14,A19;
end;
:: Holder
theorem Th60:
for m,n be positive Real st 1/m +1/n =1 &
f in Lp_Functions(M,m) & g in Lp_Functions(M,n) holds
ex r1 be Real st r1 = Integral(M,(abs f) to_power m) &
ex r2 be Real st r2 = Integral(M,(abs g) to_power n) &
Integral(M,abs(f(#)g)) <= r1 to_power (1/m) * r2 to_power (1/n)
proof
let m,n be positive Real;
assume
A1: 1/m +1/n =1 & f in Lp_Functions(M,m) & g in Lp_Functions(M,n);
then A2: m > 1 & n > 1 by Th1;
consider f1 be PartFunc of X,REAL such that
A3: f=f1 & ex NDf be Element of S st M.NDf` =0 & dom f1 = NDf &
f1 is NDf-measurable & (abs f1) to_power m is_integrable_on M by A1;
consider EDf be Element of S such that
A4: M.EDf` =0 & dom f1 = EDf & f1 is EDf-measurable by A3;
consider g1 be PartFunc of X,REAL such that
A5: g=g1 & ex NDg be Element of S st M.NDg` =0 & dom g1 = NDg &
g1 is NDg-measurable & (abs g1) to_power n is_integrable_on M by A1;
consider EDg be Element of S such that
A6: M.EDg` =0 & dom g1 = EDg & g1 is EDg-measurable by A5;
set u =(abs f1) to_power m;
set v =(abs g1) to_power n;
A7: 0 <= Integral(M,u) & 0 <= Integral(M,v) by A3,A5,A1,Th49;
reconsider s1 = Integral(M,u), s2 = Integral(M,v) as Element of REAL
by A3,A5,A1,Th49;
A8: dom f1 = dom (abs f1) & dom g1 = dom (abs g1) by VALUED_1:def 11;
reconsider Nf = EDf`, Ng = EDg` as Element of S by MEASURE1:34;
set t1 = s1 to_power (1/m);
set t2 = s2 to_power (1/n);
set E = EDf /\ EDg;
A9:E` = EDf` \/ EDg` by XBOOLE_1:54;
Nf is measure_zero of M & Ng is measure_zero of M
by A4,A6,MEASURE1:def 7; then
A10:E` is measure_zero of M by A9,MEASURE1:37;
A11:dom (f1(#)g1) = EDf /\ EDg by A4,A6,VALUED_1:def 4;
f1 is E-measurable & g1 is E-measurable
by A4,A6,MESFUNC6:16,XBOOLE_1:17; then
A12:f1(#)g1 is E-measurable by A4,A6,MESFUN7C:31;
A13:f1(#)g1 in L1_Functions M by A1,A3,A5,Th59; then
A14:ex fg1 be PartFunc of X,REAL st
fg1=f1(#)g1 & ex ND be Element of S st M.ND=0 & dom fg1 = ND` &
fg1 is_integrable_on M; then
A15:Integral(M,abs(f1(#)g1)) in REAL & abs(f1(#)g1) is_integrable_on M
by LPSPACE1:44;
per cases by A3,A5,A1,Th49;
suppose A16: s1 = 0 & s2 >= 0;
f1 in Lp_Functions (M,m) by A3; then
f1 a.e.= X-->0,M by A16,Th57; then
consider Nf1 be Element of S such that
A17: M.Nf1 = 0 & f1|Nf1` = (X-->0)|Nf1`;
reconsider Z = (E \ Nf1)` as Element of S by MEASURE1:34;
A18: (E \ Nf1)` = E` \/ Nf1 by SUBSET_1:14;
Nf1 is measure_zero of M by A17,MEASURE1:def 7; then
Z is measure_zero of M by A10,A18,MEASURE1:37; then
A19: M.Z = 0 by MEASURE1:def 7;
dom (X-->0) = X by FUNCOP_1:13; then
A20: dom ((X-->0)|Z`) = Z` by RELAT_1:62;
A21: dom ((f1(#)g1)|Z`) = Z` by A11,RELAT_1:62,XBOOLE_1:36;
for x be object st x in dom((f1(#)g1)|Z`) holds
((f1(#)g1)|Z`).x = ((X-->0)|Z`).x
proof
let x be object;
assume A22: x in dom ((f1(#)g1)|Z`); then
x in X & not x in Nf1 by A21,XBOOLE_0:def 5; then
x in Nf1` by XBOOLE_0:def 5; then
f1.x = (f1|Nf1`).x & (X-->0).x = ((X-->0)|Nf1`).x by FUNCT_1:49; then
A23: f1.x = 0 by A17,A22,FUNCOP_1:7;
A24: dom ((f1(#)g1)|Z`) c= dom(f1(#)g1) by RELAT_1:60;
((f1(#)g1)|Z`).x = (f1(#)g1).x by A22,FUNCT_1:47
.= f1.x * g1.x by A22,A24,VALUED_1:def 4
.= (Z`-->0).x by A22,A21,A23,FUNCOP_1:7
.= (X/\Z`-->0).x by XBOOLE_1:28;
hence thesis by FUNCOP_1:12;
end; then
(f1(#)g1)|Z` =(X-->0)|Z` by A20,A21,FUNCT_1:def 11; then
A25: f1(#)g1 a.e.= X-->0,M by A19;
X-->0 in L1_Functions M by Th56; then
Integral(M,abs(f1(#)g1)) = Integral(M,abs(X-->0))
by A13,A25,LPSPACE1:45; then
A26: Integral(M,abs (f1(#)g1)) = 0 by LPSPACE1:54;
t1 * t2 = 0 * t2 by A16,POWER:def 2;
hence thesis by A3,A5,A26;
end;
suppose A27: s1 > 0 & s2 = 0;
g1 in Lp_Functions(M,n) by A5; then
g1 a.e.= X-->0,M by A27,Th57; then
consider Ng1 be Element of S such that
A28: M.Ng1 = 0 & g1|Ng1` = (X-->0)|Ng1`;
reconsider Z = (E \ Ng1)` as Element of S by MEASURE1:34;
A29: (E \ Ng1)` = E` \/ Ng1 by SUBSET_1:14;
Ng1 is measure_zero of M by A28,MEASURE1:def 7; then
Z is measure_zero of M by A10,A29,MEASURE1:37; then
A30: M.Z = 0 by MEASURE1:def 7;
dom (X-->0) = X by FUNCOP_1:13; then
A31: dom ((X-->0)|Z`) = Z` by RELAT_1:62;
A32: dom ((f1(#)g1)|Z`) = Z` by A11,RELAT_1:62,XBOOLE_1:36;
for x be object st x in dom((f1(#)g1)|Z`) holds
((f1(#)g1)|Z`).x = ((X-->0)|Z`).x
proof
let x be object;
assume A33: x in dom((f1(#)g1)|Z`); then
x in X & not x in Ng1 by A32,XBOOLE_0:def 5; then
x in Ng1` by XBOOLE_0:def 5; then
g1.x = (g1|Ng1`).x & (X-->0).x = ((X-->0)|Ng1`).x by FUNCT_1:49; then
A34: g1.x = 0 by A28,A33,FUNCOP_1:7;
A35: dom ((f1(#)g1)|Z`) c= dom(f1(#)g1) by RELAT_1:60;
((f1(#)g1)|Z`).x = (f1(#)g1).x by A33,FUNCT_1:47
.= f1.x * g1.x by A33,A35,VALUED_1:def 4
.= (Z`-->0).x by A33,A32,A34,FUNCOP_1:7
.= (X/\Z`-->0).x by XBOOLE_1:28;
hence thesis by FUNCOP_1:12;
end; then
(f1(#)g1)|Z` =(X-->0)|Z` by A31,A32,FUNCT_1:def 11; then
A36: f1(#)g1 a.e.= X-->0,M by A30;
X-->0 in L1_Functions M by Th56; then
Integral(M,abs(f1(#)g1))=Integral(M,abs(X-->0))
by A13,A36,LPSPACE1:45; then
A37: Integral(M,abs(f1(#)g1))=0 by LPSPACE1:54;
t1 * t2 = t1 * 0 by A27,POWER:def 2;
hence thesis by A3,A5,A37;
end;
suppose A38: s1 <> 0 & s2 <> 0; then
A39: t1 > 0 & t2 >0 by A7,POWER:34; then
A40: |.1/(t1*t2).| = 1/(t1*t2) by ABSVALUE:def 1;
set w = (1/(t1*t2))(#)(f1(#)g1);
set F = (1/m)(#)((1/t1(#)(abs f1)) to_power m);
set G = (1/n)(#)((1/t2(#)(abs g1)) to_power n);
set z = F + G;
A41: dom (1/t1(#)(abs f1)) = dom abs f1 &
dom (1/t2(#)(abs g1)) = dom abs g1 by VALUED_1:def 5;
dom F = dom ((1/t1(#)(abs f1)) to_power m) &
dom G = dom ((1/t2(#)(abs g1)) to_power n ) by VALUED_1:def 5; then
A42: dom F = dom abs f1 & dom G = dom abs g1 by A41,MESFUN6C:def 4; then
A43: dom z = dom abs f1 /\ dom abs g1 by VALUED_1:def 1;
((1/t1)(#)(abs f1)) to_power m = ((1/t1) to_power m)(#)u &
((1/t2)(#)(abs g1)) to_power n = ((1/t2) to_power n)(#)v
by A39,Th19; then
A44: (1/t1(#)(abs f1)) to_power m is_integrable_on M &
(1/t2(#)(abs g1)) to_power n is_integrable_on M
by A3,A5,MESFUNC6:102;then
A45: F is_integrable_on M & G is_integrable_on M by MESFUNC6:102; then
A46: z is_integrable_on M by MESFUNC6:100;
A47:dom w = dom (f1(#)g1) by VALUED_1:def 5; then
A48:dom w = dom f1 /\ dom g1 by VALUED_1:def 4;
dom((1/(t1*t2))(#)abs(f1(#)g1)) = dom abs(f1(#)g1) by VALUED_1:def 5; then
A49:dom((1/(t1*t2))(#)abs(f1(#)g1)) = dom (f1(#)g1) by VALUED_1:def 11;
A50:w is E-measurable by A11,A12,MESFUNC6:21;
for x be Element of X st x in dom w holds |.w.x qua Complex.| <= z.x
proof
let x be Element of X;
assume A51: x in dom w;
(abs f1).x >= 0 & (abs g1).x >= 0 by MESFUNC6:51;then
A52: (1/t1*(abs f1).x) * (1/t2*(abs g1).x) <=
(1/t1*(abs f1).x) to_power m /m + (1/t2*(abs g1).x)to_power n /n
by A1,A2,A39,HOLDER_1:5;
dom((abs f1)(#)(abs g1)) = dom abs f1 /\ dom abs g1
by VALUED_1:def 4; then
A53: ((abs f1)(#)(abs g1)).x = (abs f1).x * (abs g1).x
by A8,A48,A51,VALUED_1:def 4;
A54: ((1/t1*(abs f1).x) * (1/t2*(abs g1).x))
= ((1/t1)*(1/t2)*(abs f1).x)*((abs g1).x)
.= (1/(t1*t2))*(abs f1).x * (abs g1).x by XCMPLX_1:102
.= (1/(t1*t2))*(((abs f1)(#)(abs g1)).x) by A53
.= (1/(t1*t2))*abs(f1(#)g1).x by RFUNCT_1:24
.= ((1/(t1*t2))(#)abs(f1(#)g1)).x by A47,A51,A49,VALUED_1:def 5
.= (abs w).x by A40,RFUNCT_1:25;
A55: 1/t1*(abs f1).x = (1/t1(#)(abs f1)).x &
1/t2*(abs g1).x = (1/t2(#)(abs g1)).x by VALUED_1:6;
dom((1/t1(#)(abs f1)) to_power m) = dom f1 &
dom((1/t2(#)(abs g1)) to_power n) = dom g1 by A8,A41,MESFUN6C:def 4; then
x in dom ((1/t1(#)(abs f1)) to_power m) &
x in dom ((1/t2(#)(abs g1)) to_power n) by A48,A51,XBOOLE_0:def 4; then
((1/t1(#)(abs f1)).x) to_power m = ((1/t1(#)(abs f1)) to_power m).x &
((1/t2(#)(abs g1)).x) to_power n = ((1/t2(#)(abs g1)) to_power n).x
by MESFUN6C:def 4;
then ((1/t1(#)(abs f1)).x) to_power m /m = F.x &
((1/t2(#)(abs g1)).x) to_power n /n = G.x by VALUED_1:6; then
(1/t1*(abs f1).x) to_power m /m + (1/t2*(abs g1).x)to_power n /n = z.x
by A8,A48,A51,A43,A55,VALUED_1:def 1;
hence thesis by A52,A54,VALUED_1:18;
end; then
A56:Integral(M,abs w) <= Integral(M,z) by A4,A6,A46,A8,A48,A43,A50,MESFUNC6:96;
consider E1 be Element of S such that
A57: E1 = dom F /\ dom G & Integral(M,F+G) =Integral(M,F|E1)+Integral(M,G|E1)
by A45,MESFUNC6:101;
EDf = X /\ EDf & EDg = X /\ EDg by XBOOLE_1:28; then
A58:EDf = X \ Nf & EDg = X \ Ng by XBOOLE_1:48;
A59:EDf \ E = EDf \ EDg by XBOOLE_1:47
.= (X \ Nf) \ X \/ (X \ Nf) /\ Ng by A58,XBOOLE_1:52
.= X \(Nf \/ X) \/ (X \ Nf) /\ Ng by XBOOLE_1:41
.= X \ X \/(X \ Nf)/\ Ng by XBOOLE_1:12
.= {} \/ (X \ Nf) /\ Ng by XBOOLE_1:37;
A60:EDg \ E = EDg \ EDf by XBOOLE_1:47
.= (X \ Ng) \ X \/ (X \ Ng) /\ Nf by A58,XBOOLE_1:52
.= X \(Ng \/ X) \/ (X \ Ng) /\ Nf by XBOOLE_1:41
.= X \ X \/(X \ Ng)/\ Nf by XBOOLE_1:12
.= {} \/ (X \ Ng) /\ Nf by XBOOLE_1:37;
set NF = EDf /\ Ng;
set NG = EDg /\ Nf;
Nf is measure_zero of M & Ng is measure_zero of M
by A4,A6,MEASURE1:def 7; then
NF is measure_zero of M & NG is measure_zero of M
by MEASURE1:36,XBOOLE_1:17; then
A61:M.NF = 0 & M.NG = 0 by MEASURE1:def 7;
E = EDf /\ E & E = EDg /\ E by XBOOLE_1:17,28; then
A62:E = EDf \ NF & E = EDg \ NG by A58,A59,A60,XBOOLE_1:48;
R_EAL F is_integrable_on M by A45; then
ex E being Element of S st
E = dom R_EAL F & R_EAL F is E-measurable; then
A63:F is EDf-measurable by A42,A8,A4;
R_EAL G is_integrable_on M by A45; then
ex E being Element of S st
E = dom R_EAL G & R_EAL G is E-measurable; then
A64:G is EDg-measurable by A42,A8,A6;
(1/t1) to_power m = t1 to_power (-m) by A38,A7,POWER:32,34; then
(1/t1) to_power m = s1 to_power((1/m)*(-m)) by A7,A38,POWER:33; then
(1/t1) to_power m = s1 to_power (-1*(1/m)*m); then
(1/t1) to_power m = s1 to_power (-1) by XCMPLX_1:106; then
(1/t1) to_power m = (1/s1) to_power 1 by A7,A38,POWER:32; then
A65:(1/t1) to_power m = 1/s1 by POWER:25;
A66:(1/s1 qua ExtReal) * s1 = 1 &
(1/s2 qua ExtReal) * s2 = 1
by A38,XCMPLX_1:106;
A67:(1/t2) to_power n = t2 to_power (-n) by A38,A7,POWER:32,34
.= s2 to_power((1/n)*(-n)) by A7,A38,POWER:33
.= s2 to_power (-1*(1/n)*n)
.= s2 to_power (-1) by XCMPLX_1:106
.= (1/s2) to_power 1 by A7,A38,POWER:32
.= 1/s2 by POWER:25;
A68:Integral(M,F|E) = Integral(M,F) by A4,A8,A42,A62,A61,A63,MESFUNC6:89
.= (1/m) *Integral(M,(1/t1(#)(abs f1)) to_power m) by A44,MESFUNC6:102
.= (1/m) *Integral(M,((1/t1) to_power m)(#)((abs f1) to_power m))
by A39,Th19
.= (1/m) * (((1/t1) to_power m) * Integral(M,(abs f1) to_power m))
by A3,MESFUNC6:102
.= 1/m by A65,A66,XXREAL_3:81;
A69:
Integral(M,G|E) = Integral(M,G) by A6,A8,A42,A62,A61,A64,MESFUNC6:89
.= (1/n)*Integral(M,(1/t2(#)(abs g1)) to_power n) by A44,MESFUNC6:102
.= (1/n) * Integral(M,((1/t2) to_power n)(#)((abs g1) to_power n))
by A39,Th19
.= (1/n) * (((1/t2) to_power n) * Integral(M,(abs g1) to_power n))
by A5,MESFUNC6:102
.= 1/n by A66,A67,XXREAL_3:81;
reconsider n1=1/n, m1=1/m as Real;
A70:Integral(M,F+G) = Integral(M,F|E)+Integral(M,G|E)
by A42,A4,A6,A8,A57
.= m1+n1 by A69,A68,SUPINF_2:1
.= jj by A1;
abs w = |.1/(t1*t2) qua Complex.|(#)abs(f1(#)g1) by RFUNCT_1:25; then
abs w = (1/(t1*t2))(#)abs(f1(#)g1) by A39,ABSVALUE:def 1; then
A71:Integral(M,abs w) = (1/(t1*t2)) * Integral(M,abs(f1(#)g1))
by A15,MESFUNC6:102;
reconsider c1 = Integral(M,abs(f1(#)g1)) as Element of REAL
by A14,LPSPACE1:44;
(1/(t1*t2) qua ExtReal) * Integral(M,abs(f1(#)g1))
= (1/(t1*t2) qua ExtReal) * c1;
then
(1/(t1*t2)) * Integral(M,abs(f1(#)g1)) = (1/(t1*t2)) * c1;
then
(t1*t2)*((1/(t1*t2)) * c1) <= (t1*t2)*1 by A39,A56,A71,A70,XREAL_1:64; then
A72:(t1*t2)*(1/(t1*t2)) * c1 <= (t1*t2);
(t1*t2)*(1/(t1*t2)) = 1 by A39,XCMPLX_1:106;
hence thesis by A3,A5,A72;
end;
end;
::Minkowski
Lm5:
for m,n be positive Real st 1/m +1/n =1 &
f in Lp_Functions(M,m) & g in Lp_Functions(M,m) holds
ex r1,r2,r3 be Real st
r1 = Integral(M,(abs f) to_power m) &
r2 = Integral(M,(abs g) to_power m) &
r3 = Integral(M,(abs (f+g)) to_power m) &
r3 to_power (1/m) <= r1 to_power (1/m) + r2 to_power (1/m)
proof
let m,n be positive Real;
assume
A1: 1/m +1/n =1 & f in Lp_Functions(M,m) & g in Lp_Functions(M,m); then
(m+n)*(m*n)"*(m*n) = 1* (m*n) by XCMPLX_1:211;then
(m+n)*((m*n)"*(m*n)) = (m*n); then
(m+n)*1 = (m*n) by XCMPLX_0:def 7; then
A2: m = n*(m-1);
A3: 1-1 < m - 1 by A1,Th1,XREAL_1:14; then
A4:m -1 > 0;
ex f1 be PartFunc of X,REAL st
f=f1 & ex NDf be Element of S st M.NDf` =0 & dom f1 = NDf &
f1 is NDf-measurable & (abs f1) to_power m is_integrable_on M
by A1; then
consider EDf be Element of S such that
A5: M.EDf` =0 & dom f = EDf & f is EDf-measurable;
ex g1 be PartFunc of X,REAL st
g=g1 & ex NDg be Element of S st M.NDg` =0 & dom g1 = NDg &
g1 is NDg-measurable & (abs g1) to_power m is_integrable_on M
by A1; then
consider EDg be Element of S such that
A6: M.EDg` =0 & dom g = EDg & g is EDg-measurable;
set E = EDf /\ EDg;
A7: f + g in Lp_Functions(M,m) by A1,Th25; then
A8: ex h1 be PartFunc of X,REAL st
f+g = h1 & ex NDfg be Element of S st M.NDfg` =0 & dom h1 = NDfg &
h1 is NDfg-measurable & (abs h1) to_power m is_integrable_on M;
A9:dom(f+g) = E by A5,A6,VALUED_1:def 1; then
A10:abs(f+g) is E-measurable by A8,MESFUNC6:48;
reconsider s1 = Integral(M,(abs f) to_power m) as Element of REAL
by A1,Th49;
reconsider s2 = Integral(M,(abs g) to_power m) as Element of REAL
by A1,Th49;
reconsider s3 = Integral(M,(abs(f+g)) to_power m) as Element of REAL
by A7,Th49;
set t = (abs(f+g)) to_power (m-1);
A11:dom t = dom abs(f+g) by MESFUN6C:def 4; then
A12:dom t = E by A9,VALUED_1:def 11; then
A13:t is E-measurable by A3,A10,A11,MESFUN6C:29;
A14:t to_power n = abs(f+g) to_power m by A2,A3,Th6;
A15:abs t = t by Th14,A4; then
A16:t in Lp_Functions(M,n) by A9,A12,A14,A8,A13; then
reconsider s4 = Integral(M,(abs t) to_power n) as Element of REAL
by Th49;
t(#)f is_integrable_on M & t(#)g is_integrable_on M by A1,A16,Th59; then
reconsider u1 = Integral(M,abs(t(#)f)), u2 = Integral(M,abs(t(#)g))
as Element of REAL by LPSPACE1:44;
A17:dom (abs f)= EDf & dom (abs g)= EDg by A5,A6,VALUED_1:def 11;
dom (t(#)abs f) = dom t /\ dom(abs f) &
dom (t(#)abs g) = dom t /\ dom(abs g) by VALUED_1:def 4; then
A18:dom (t(#)abs f) = E & dom (t(#)abs g) = E by A12,A17,XBOOLE_1:17,28;
A19:abs(t(#)f)= t(#)abs f & abs(t(#)g)= t(#)abs g &
abs(t(#)(f+g)) = t(#)abs (f+g) by A15,RFUNCT_1:24;
t(#)f is_integrable_on M & t(#)g is_integrable_on M &
t(#)(f+g) is_integrable_on M by A1,A16,A7,Th59; then
A20:t(#)abs f is_integrable_on M & t(#)abs g is_integrable_on M &
t(#)abs(f+g) is_integrable_on M by A19,LPSPACE1:44;
set F = t(#)abs(f+g);
set G = t(#)abs f + t(#)abs g;
A21:dom F = E /\ E by A11,A12,VALUED_1:def 4;
A22:dom G = E /\ E by A18,VALUED_1:def 1;
R_EAL F is_integrable_on M by A20; then
ex E1 being Element of S st
E1 = dom R_EAL F & R_EAL F is E1-measurable; then
A23:F is E-measurable by A21;
A24:G is_integrable_on M by A20,MESFUNC6:100;
for x be Element of X st x in dom F holds |.F.x qua Complex.| <= G.x
proof
let x be Element of X;
assume A25: x in dom F; then
|.f.x+g.x.| = |.(f+g).x.| by A9,A21,VALUED_1:def 1; then
A26: |.f.x+g.x.| = (abs(f+g)).x &
|.f.x.| = (abs f).x & |.g.x.| = (abs g).x by VALUED_1:18;
A27: |. f.x .| = |.f.x.| & |. g.x .|= |.g.x.| &
|. f.x + g.x .| = |.f.x+g.x.|;
A28: t.x >= 0 & (abs(f+g)).x >= 0 by A3,MESFUNC6:51;
reconsider fx =f.x, gx = g.x as R_eal by XXREAL_0:def 1;
A29: fx+ gx = f.x+ g.x by SUPINF_2:1;
|. fx+ gx.| <= |. fx.| + |. gx.| by EXTREAL1:24; then
|. f.x+ g.x.| <= |. fx.| + |. gx.| by A29; then
|.f.x+g.x.| <= |.f.x qua Complex.| + |.g.x qua Complex.|
by A27,SUPINF_2:1; then
A30: t.x * (abs(f+g)).x <= t.x * (abs(f).x + abs(g).x) by A26,A28,XREAL_1:64;
t.x * abs(f).x = (t(#)abs f).x & t.x * abs(g).x = (t(#)abs(g)).x
by VALUED_1:5; then
t.x * (abs(f).x + abs(g).x) = (t(#)abs f).x + (t(#)abs(g)).x; then
A31: t.x * (abs(f).x + abs(g).x) = G.x by A21,A22,A25,VALUED_1:def 1;
t.x * (abs(f+g)).x = F.x by VALUED_1:5;
hence thesis by A31,A30,A28,ABSVALUE:def 1;
end; then
A32:Integral(M,abs F) <= Integral(M,G) by A21,A22,A23,A24,MESFUNC6:96;
A33:ex E1 be Element of S st E1 = E /\ E &
Integral(M,G) = Integral(M,(t(#)abs f)|E1)+Integral(M,(t(#)abs g)|E1)
by A18,A20,MESFUNC6:101;
Integral(M,(t(#)abs f)|E) = Integral(M,t(#)abs f) &
Integral(M,(t(#)abs g)|E) = Integral(M,t(#)abs g) by A18,RELAT_1:69; then
A34:Integral(M,G) = u1 + u2 by A19,A33,SUPINF_2:1;
set v1 = s4 to_power (1/n) * s1 to_power (1/m);
set v2 = s4 to_power (1/n) * s2 to_power (1/m);
(ex r4 be Real st r4=Integral(M,(abs t) to_power n) &
ex r1 be Real st r1 = Integral(M,(abs f) to_power m) &
Integral(M,abs(t(#)f)) <= r4 to_power (1/n) * r1 to_power (1/m)) &
(ex r4 be Real st r4=Integral(M,(abs t) to_power n) &
ex r2 be Real st r2 = Integral(M,(abs g) to_power m) &
Integral(M,abs(t(#)g)) <= r4 to_power (1/n) * r2 to_power (1/m))
by A1,A16,Th60; then
A35:u1 + u2 <= v1 + v2 by XREAL_1:7;
F = ((abs(f+g)) to_power (m-1))(#)((abs(f+g)) to_power 1) by Th8
.= (abs(f+g)) to_power ((m-1) +1) by Th7,A3; then
Integral(M,abs F)= s3 by Th14; then
A36:s3 <= (s3 to_power (1/n))*(s1 to_power (1/m))
+ (s3 to_power (1/n))*(s2 to_power (1/m))
by A14,A15,A32,A34,A35,XXREAL_0:2;
per cases by A7,Th49;
suppose s3 = 0; then
A37: s3 to_power (1/m)= 0 by POWER:def 2;
s1 to_power (1/m) >= 0 & s2 to_power (1/m) >= 0 by A1,Th49,Th4; then
s3 to_power (1/m) <= s1 to_power (1/m) + s2 to_power (1/m) by A37;
hence thesis;
end;
suppose A38: s3 > 0; then
A39: s3 to_power (1/n) > 0 by POWER:34;
set w1 = s3 to_power (1/n);
(1/w1) * (w1*(s1 to_power (1/m))+w1*(s2 to_power (1/m)))
=(1/w1) * w1*((s1 to_power (1/m)) + (s2 to_power (1/m))); then
A40:(1/w1) * (w1*(s1 to_power (1/m))+w1*(s2 to_power (1/m)))
=1*((s1 to_power (1/m)) + (s2 to_power (1/m))) by A39,XCMPLX_1:106;
(1/w1) * s3 = (s3 to_power (-1/n)) * s3 by A38,POWER:28
.= (s3 to_power (-1/n)) * (s3 to_power 1) by POWER:25
.= s3 to_power ((-1/n)+1) by A38,POWER:27
.= s3 to_power (1/m) by A1;
hence thesis by A39,A40,A36,XREAL_1:64;
end;
end;
:: Minkowski
theorem Th61:
for m be positive Real for r1,r2,r3 be Real st 1 <= m &
f in Lp_Functions(M,m) & g in Lp_Functions(M,m) &
r1 = Integral(M,(abs f) to_power m) &
r2 = Integral(M,(abs g) to_power m) &
r3 = Integral(M,(abs (f+g)) to_power m) holds
r3 to_power (1/m) <= r1 to_power (1/m) + r2 to_power (1/m)
proof
let m be positive Real;
let r1,r2,r3 be Real;
assume
A1: 1 <= m & f in Lp_Functions(M,m) & g in Lp_Functions(M,m) &
r1 = Integral(M,(abs f) to_power m) &
r2 = Integral(M,(abs g) to_power m) &
r3 = Integral(M,(abs (f+g)) to_power m);
per cases;
suppose A2: m=1; then
A3: r1 = Integral(M,(abs f)) & r2 = Integral(M,(abs g)) &
r3 = Integral(M,(abs (f+g))) by A1,Th8;
A4:ex f1 be PartFunc of X,REAL st
f=f1 & ex ND be Element of S st M.ND` =0 & dom f1 = ND &
f1 is ND-measurable & (abs f1) to_power m is_integrable_on M by A1;
A5:ex g1 be PartFunc of X,REAL st
g=g1 & ex ND be Element of S st M.ND` =0 & dom g1 = ND &
g1 is ND-measurable & (abs g1) to_power m is_integrable_on M by A1;
then (abs f) is_integrable_on M &
(abs g) is_integrable_on M by A2,A4,Th8; then
f is_integrable_on M & g is_integrable_on M by A4,A5,MESFUNC6:94; then
Integral(M,abs(f+g)) <= Integral(M,abs f) + Integral(M,abs g)
by LPSPACE1:55; then
A6: r3 <= r1 + r2 by A3,XXREAL_3:def 2;
r1 to_power (1/m) = r1 & r2 to_power (1/m) = r2 by A2,POWER:25;
hence thesis by A6,A2,POWER:25;
end;
suppose A7: m <> 1;
set n1= 1 - 1/m;
1 < m by A1,A7,XXREAL_0:1; then
1/m < 1 by XREAL_1:189; then
0 < n1 by XREAL_1:50; then
reconsider n=1/n1 as positive Real;
1/m +1/n =1; then
ex rr1,rr2,rr3 be Real st rr1 = Integral(M,(abs f) to_power m) &
rr2 = Integral(M,(abs g) to_power m) &
rr3 = Integral(M,(abs (f+g)) to_power m) &
rr3 to_power (1/m) <= rr1 to_power (1/m) + rr2 to_power (1/m) by A1,Lm5;
hence thesis by A1;
end;
end;
Lm6:
for k be geq_than_1 Real holds
Lp-Space(M,k) is reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative
scalar-unital Abelian add-associative right_zeroed right_complementable
proof
let k be geq_than_1 Real;
set x = 0.(Lp-Space(M,k));
x =0.(Pre-Lp-Space(M,k)); then
x = zeroCoset(M,k) by Def11; then
X-->0 in x by Th38,Th23; then
ex r be Real st 0 <=r & r = Integral(M,(abs(X-->0)) to_power k) &
||.x.|| = r to_power (1/k) by Th55; then
consider r0 be Real such that
A1: r0 = Integral(M,(abs(X-->0)) to_power k) &
(Lp-Norm (M,k)).x = r0 to_power (1/k);
r0 = 0 by A1,Th58;
hence ||.x.||=0 by A1,POWER:def 2;
now let x,y be Point of Lp-Space (M,k), a be Real;
A2:1<=k by Def1;
hereby assume A3: ||.x.|| = 0;
consider f be PartFunc of X, REAL such that
A4: f in x & ex r be Real st r = Integral(M,(abs f) to_power k) &
||.x.|| = r to_power (1/k) by Def12;
A5: f in Lp_Functions(M,k) by Th51,A4;
then consider r1 be Real such that
A6: r1 = Integral(M,(abs f) to_power k) & r1 >= 0 &
(Lp-Norm (M,k)).x = r1 to_power (1/k) by A4,Th49;
r1 = 0 by A3,A6,POWER:34; then
zeroCoset(M,k) = a.e-eq-class_Lp(f,M,k) by A5,A6,Th57,Th42; then
0.(Pre-Lp-Space(M,k)) = a.e-eq-class_Lp(f,M,k) by Def11;
hence x =0.(Lp-Space(M,k)) by A4,Th55;
end;
consider f be PartFunc of X,REAL such that
A7: f in x & ex r1 be Real st r1 = Integral(M,(abs f) to_power k) &
||.x.|| = r1 to_power (1/k) by Def12;
A8:
(abs f) to_power k is_integrable_on M & f in Lp_Functions(M,k) by Th51,A7;
consider g be PartFunc of X,REAL such that
A9: g in y & ex r2 be Real st r2 = Integral(M,(abs g) to_power k) &
||.y.|| = r2 to_power (1/k) by Def12;
A10:
(abs g) to_power k is_integrable_on M & g in Lp_Functions (M,k)
by Th51,A9;
consider s1 be Real such that
A11: s1 = Integral(M,(abs f) to_power k) & ||.x.|| = s1 to_power (1/k) by A7;
A12:s1 = 0 implies s1 to_power (1/k) >= 0 by POWER:def 2;
s1 > 0 implies s1 to_power (1/k) >= 0 by POWER:34;
hence 0 <= ||.x.|| by A12,A8,A11,Th49;
set t = f+g;
set w = x + y;
A13: s1 >= 0 by A8,A11,Th49;
consider s2 be Real such that
A14:s2 = Integral(M,(abs g) to_power k) & ||.y.|| = s2 to_power (1/k) by A9;
f+g in x+y by Th54,A7,A9; then
ex r be Real st 0 <= r &
r = Integral(M,(abs t) to_power k) & ||.w.|| =r to_power (1/k) by Th53;
hence ||.x+y.|| <= ||.x.|| + ||.y.|| by Th61,A2,A8,A10,A14,A11;
set t = a(#)f;
set w = a*x;
a(#)f in a*x by Th54,A7; then
ex r be Real st 0 <= r & r = Integral(M, (abs t) to_power k)
& ||.w.|| =r to_power (1/k) by Th53; then
consider s be Real such that
A15: s =Integral(M,(abs t) to_power k) & ||.w.|| =s to_power (1/k);
reconsider r = |.a qua Complex.| to_power k as Real;
A16:s = Integral(M,( r (#) (abs f) to_power k))
by A15,Th18
.= r * Integral(M,(abs f) to_power k) by A8,MESFUNC6:102
.= r * s1 by A11,EXTREAL1:1
.= |.a qua Complex.| to_power k * s1;
|.a qua Complex.| to_power k >=0 by Th4,COMPLEX1:46; then
||.a*x.||
= (|.a qua Complex.| to_power k to_power (1/k)) * s1 to_power (1/k)
by A13,A15,A16,Th5
.= |.a qua Complex.| to_power (k*(1/k)) * s1 to_power (1/k)
by COMPLEX1:46,HOLDER_1:2
.= |.a qua Complex.| to_power 1 * s1 to_power (1/k) by XCMPLX_1:106;
hence ||.a*x.|| = |.a qua Complex.| * ||.x.|| by A11,POWER:25;
end;
hence thesis by NORMSP_1:def 1,RSSPACE3:2;
end;
registration
let k be geq_than_1 Real;
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster Lp-Space (M,k) -> reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence by Lm6;
end;
begin :: Preliminaries of completeness of Lp Space
theorem Th62:
for Sq be sequence of Lp-Space(M,k) holds
ex Fsq be Functional_Sequence of X,REAL st
for n be Nat holds
Fsq.n in Lp_Functions(M,k) & Fsq.n in Sq.n &
Sq.n= a.e-eq-class_Lp(Fsq.n,M,k) &
ex r be Real st
r = Integral(M,(abs (Fsq.n)) to_power k) &
||. Sq.n .|| = r to_power (1/k)
proof
let Sq be sequence of Lp-Space(M,k);
defpred P[Nat,set ] means
ex f be PartFunc of X,REAL st $2=f & f in Lp_Functions(M,k) &
f in Sq.$1 & Sq.$1= a.e-eq-class_Lp(f,M,k) &
ex r be Real st
r = Integral(M,(abs f) to_power k) & ||. Sq.$1 .|| =r to_power (1/k);
A1:for x being Element of NAT ex y being Element of PFuncs(X,REAL) st P[x,y]
proof
let x be Element of NAT;
consider y be PartFunc of X,REAL such that
A2: y in Lp_Functions(M,k) & Sq.x= a.e-eq-class_Lp(y,M,k) by Th53;
ex r be Real st 0 <= r &
r = Integral(M,(abs y) to_power k) & ||. Sq.x .|| =r to_power (1/k)
by Th53,A2,Th38;
hence thesis by A2,Th38;
end;
consider G be sequence of PFuncs(X,REAL) such that
A3: for n be Element of NAT holds P[n,G.n] from FUNCT_2:sch 3(A1);
reconsider G as Functional_Sequence of X,REAL;
now let n be Nat;
n in NAT by ORDINAL1:def 12;
then
ex f be PartFunc of X,REAL st G.n=f & f in Lp_Functions(M,k) & f in Sq.n &
Sq.n= a.e-eq-class_Lp(f,M,k) &
ex r be Real st
r = Integral(M,(abs f) to_power k) &
||. Sq.n .|| =r to_power (1/k) by A3;
hence
G.n in Lp_Functions(M,k) & G.n in Sq.n & Sq.n= a.e-eq-class_Lp(G.n,M,k) &
ex r be Real st
r = Integral(M,(abs (G.n)) to_power k) & ||. Sq.n .|| =r to_power (1/k);
end;
hence thesis;
end;
theorem Th63:
for Sq be sequence of Lp-Space(M,k) holds
ex Fsq be with_the_same_dom Functional_Sequence of X,REAL st
for n be Nat holds
Fsq.n in Lp_Functions(M,k) & Fsq.n in Sq.n &
Sq.n= a.e-eq-class_Lp(Fsq.n,M,k) &
ex r be Real st 0 <= r &
r = Integral(M,(abs (Fsq.n)) to_power k) &
||. Sq.n .|| =r to_power (1/k)
proof
let Sq be sequence of Lp-Space(M,k);
consider Fsq be Functional_Sequence of X,REAL such that
A1: for n be Nat holds Fsq.n in Lp_Functions(M,k) & Fsq.n in Sq.n &
Sq.n= a.e-eq-class_Lp(Fsq.n,M,k) &
ex r be Real st r = Integral(M,(abs (Fsq.n)) to_power k) &
||. Sq.n .|| = r to_power (1/k) by Th62;
defpred P[Nat,set] means
ex DMFSQN be Element of S st $2 = DMFSQN &
ex FSQN be PartFunc of X,REAL st
Fsq.$1 = FSQN & M.DMFSQN` = 0 & dom FSQN = DMFSQN &
FSQN is DMFSQN-measurable &
(abs FSQN) to_power k is_integrable_on M;
A2: for n being Element of NAT ex y being Element of S st P[n,y]
proof
let n be Element of NAT;
Fsq.n in Lp_Functions(M,k) by A1; then
ex FMF be PartFunc of X,REAL st Fsq.n = FMF &
ex ND be Element of S st M.ND` =0 & dom FMF = ND &
FMF is ND-measurable & (abs FMF) to_power k is_integrable_on M;
hence thesis;
end;
consider G be sequence of S such that
A3: for n be Element of NAT holds P[n,G.n] from FUNCT_2:sch 3(A2);
reconsider E0 = meet rng G as Element of S;
A4: for n be Nat holds M.(X \ G.n) =0 & E0 c= dom(Fsq.n)
proof
let n be Nat;
A5: n in NAT by ORDINAL1:def 12;
ex D be Element of S st G.n=D & ex F be PartFunc of X,REAL st
Fsq.n= F & M.D` =0 & dom F = D & F is D-measurable &
(abs F) to_power k is_integrable_on M by A3,A5;
hence M.(X \ (G.n)) =0 & E0 c= dom(Fsq.n) by FUNCT_2:4,SETFAM_1:3,A5;
end;
A6: (X \ rng G) is N_Sub_set_fam of X by MEASURE1:21;
for A be set st A in (X \ rng G) holds A in S & A is measure_zero of M
proof
let A being set;
assume A7: A in (X \ rng G); then
reconsider A0 = A as Subset of X;
A0` in rng G by A7,SETFAM_1:def 7; then
consider n be object such that
A8: n in NAT & A0` = G.n by FUNCT_2:11;
reconsider n as Nat by A8;
A9: (A0`)` = A0; then
A0 = X \ G.n by A8;
hence A in S by MEASURE1:34;
A10: M.A0= 0 by A4,A8,A9;
A0= X \ (G.n) by A8,A9; then
A is Element of S by MEASURE1:34;
hence A is measure_zero of M by A10,MEASURE1:def 7;
end; then
A11: (for A be object st A in (X \ rng G) holds A in S) &
(for A be set st A in (X \ rng G) holds A is measure_zero of M); then
(X \ rng G) c= S; then
(X \ rng G) is N_Measure_fam of S by A6,MEASURE2:def 1; then
A12: union (X \ rng G) is measure_zero of M by A11,MEASURE2:14;
E0` = X \ (X \ (union (X \ rng G))) by MEASURE1:4
.= X /\ union (X \ rng G) by XBOOLE_1:48
.= union (X \ rng G) by XBOOLE_1:28; then
A13: M.E0` =0 by A12,MEASURE1:def 7;
set Fsq2 = Fsq||E0;
A14: for n be Nat holds dom (Fsq2.n) = E0
proof
let n be Nat;
dom (Fsq2.n) = dom((Fsq.n)|E0) by MESFUN9C:def 1; then
dom (Fsq2.n) =dom(Fsq.n) /\ E0 by RELAT_1:61;
hence dom (Fsq2.n) = E0 by A4,XBOOLE_1:28;
end;
now let n,m be Nat;
dom(Fsq2.n) =E0 & dom(Fsq2.m) = E0 by A14;
hence dom(Fsq2.n) = dom(Fsq2.m);
end; then
reconsider Fsq2 as with_the_same_dom Functional_Sequence of X,REAL
by MESFUNC8:def 2;
take Fsq2;
hereby let n be Nat;
Fsq.n in Lp_Functions(M,k) by A1; then
A15: ex FMF be PartFunc of X,REAL st Fsq.n= FMF &
ex ND be Element of S st M.ND` =0 & dom FMF = ND &
FMF is ND-measurable & (abs FMF) to_power k is_integrable_on M;
then reconsider E2 = dom (Fsq.n) as Element of S;
A16: E2 /\ E0 = E0 by A4,XBOOLE_1:28;
R_EAL (Fsq.n) is E2-measurable by A15; then
R_EAL (Fsq.n) is E0-measurable by A4,MESFUNC1:30; then
Fsq.n is E0-measurable; then
(Fsq.n)|E0 is E0-measurable by A16,MESFUNC6:76; then
A17: Fsq2.n is E0-measurable by MESFUN9C:def 1;
A18: dom (Fsq2.n)= E0 by A14;
dom ((abs (Fsq.n)) to_power k) = dom abs (Fsq.n) &
dom ((abs (Fsq2.n)) to_power k) = dom abs (Fsq2.n) by MESFUN6C:def 4; then
A19: dom ((abs (Fsq.n)) to_power k) = dom (Fsq.n) &
dom ((abs (Fsq2.n)) to_power k) = dom (Fsq2.n) by VALUED_1:def 11;
for x be object st x in dom((abs (Fsq2.n)) to_power k) holds
((abs (Fsq2.n)) to_power k ).x = ((abs (Fsq.n)) to_power k).x
proof
let x be object;
assume A20: x in dom((abs (Fsq2.n)) to_power k); then
reconsider x0=x as Element of X;
A21: x in dom((abs (Fsq.n)) to_power k) by A18,A19,A16,A20,XBOOLE_0:def 4;
thus ((abs (Fsq2.n)) to_power k ).x
= ((abs (Fsq2.n)).x0) to_power k by A20,MESFUN6C:def 4
.= |.((Fsq2.n).x0) qua Complex.| to_power k by VALUED_1:18
.= |.(((Fsq.n)|E0).x0) qua Complex.| to_power k by MESFUN9C:def 1
.= |.((Fsq.n).x0) qua Complex.| to_power k by A18,A19,A20,FUNCT_1:49
.= (abs(Fsq.n).x0) to_power k by VALUED_1:18
.= ((abs (Fsq.n)) to_power k).x by A21,MESFUN6C:def 4;
end; then
((abs (Fsq.n)) to_power k)|E0 = (abs (Fsq2.n)) to_power k
by A14,A16,A19,FUNCT_1:46; then
((abs (Fsq2.n)) to_power k) is_integrable_on M by A15,MESFUNC6:91;
hence
A22: Fsq2.n in Lp_Functions(M,k) by A17,A18,A13;
A23: Fsq.n in Sq.n & Sq.n= a.e-eq-class_Lp(Fsq.n,M,k) by A1;
reconsider EB = E0` as Element of S by MEASURE1:34;
(Fsq2.n)|EB` = Fsq2.n by A18,RELAT_1:68; then
(Fsq2.n)|EB` =(Fsq.n)|EB` by MESFUN9C:def 1; then
A24: (Fsq2.n) a.e.= (Fsq.n),M by A13;
hence Fsq2.n in Sq.n by A23,A22,Th36;
a.e-eq-class_Lp((Fsq2.n),M,k) = a.e-eq-class_Lp((Fsq.n),M,k)
by Th42,A24;
hence Sq.n= a.e-eq-class_Lp(Fsq2.n,M,k) by A1;
hence ex r be Real st
0 <= r & r = Integral(M, (abs (Fsq2.n)) to_power k) &
||. Sq.n .|| =r to_power (1/k) by Th53,Th38,A22;
end;
end;
Lm7:
for X be RealNormSpace, Sq be sequence of X, Sq0 be Point of X,
R1 be Real_Sequence, N be increasing sequence of NAT st
Sq is Cauchy_sequence_by_Norm &
(for i be Nat holds R1.i = ||. Sq0-Sq.(N.i) .||) &
R1 is convergent & lim R1=0
holds
Sq is convergent & lim Sq = Sq0 &
||.Sq -Sq0.|| is convergent & lim ||.Sq -Sq0.|| = 0
proof
let X be RealNormSpace, Sq be sequence of X, Sq0 be Point of X,
R1 be Real_Sequence, N be increasing sequence of NAT;
assume that
A1: Sq is Cauchy_sequence_by_Norm and
A2: for i be Nat holds R1.i = ||. Sq0 - Sq.(N.i) .|| and
A3: R1 is convergent & lim R1=0;
A4: now let p be Real;
assume A5: 0<p; then
consider n2 such that
A6: for m,n st n2<=m & n2 <= n holds ||.Sq.m-Sq.n.||< p/2 by A1,RSSPACE3:8;
consider n1 such that
A7: for l st n1<=l holds |.(R1.l)-0 qua Complex .|<p/2 by A3,A5,SEQ_2:def 7;
reconsider n3= max(n1,n2) as Nat by TARSKI:1;
take n3;
thus for n be Nat st n3 <= n holds ||. Sq.n - Sq0 .|| < p
proof
let n be Nat;
assume A8: n3 <= n;
n1 <= n3 by XXREAL_0:25; then
n1 <= n by A8,XXREAL_0:2; then
|.(R1.n)-0 .|<p/2 by A7; then
A9: |. ||.Sq0-Sq.(N.n).|| .| < p/2 by A2;
A10: ||.Sq0-Sq.(N.n).|| < p/2 by A9,ABSVALUE:def 1;
n <= N.n by SEQM_3:14; then
A11: n3 <=N.n by A8,XXREAL_0:2;
n2 <= n3 by XXREAL_0:25; then
n2 <= N.n & n2 <= n by A8,A11,XXREAL_0:2; then
||. Sq.(N.n)-Sq.n .|| < p/2 by A6; then
A12: ||.Sq0-Sq.(N.n).|| + ||. Sq.(N.n)-Sq.n .|| < p/2 + p/2 by A10,XREAL_1:8;
A13: ||.Sq.n-Sq0 .|| = ||. Sq0 - Sq.n .|| by NORMSP_1:7
.= ||. (Sq0 - Sq.(N.n)) + (Sq.(N.n)-Sq.n) .|| by LOPBAN_3:3;
||. (Sq0 - Sq.(N.n)) + (Sq.(N.n)-Sq.n) .||
<= ||.Sq0-Sq.(N.n).|| + ||. Sq.(N.n)-Sq.n .|| by NORMSP_1:def 1;
hence ||.Sq.n-Sq0 .|| < p by A13,A12,XXREAL_0:2;
end;
end;
hence
A14: Sq is convergent by NORMSP_1:def 6;
hence lim Sq = Sq0 by A4,NORMSP_1:def 7;
hence thesis by A14,NORMSP_1:24;
end;
theorem
for X be RealNormSpace, Sq be sequence of X, Sq0 be Point of X st
||.Sq -Sq0.|| is convergent & lim ||.Sq -Sq0.|| =0
holds Sq is convergent & lim Sq = Sq0
proof
let X be RealNormSpace, Sq be sequence of X, Sq0 be Point of X;
assume
A1: ||.Sq -Sq0.|| is convergent & lim ||.Sq -Sq0.|| = 0;
A2:for p be Real st 0 < p ex n be Nat st
for m be Nat st n <= m holds ||. Sq.m - Sq0 .|| < p
proof
let p be Real;
assume 0 < p; then
consider n such that
A3: for m st n<=m holds |. (||.Sq - Sq0.||).m - 0 qua Complex .| < p
by A1,SEQ_2:def 7;
take n;
hereby let m be Nat;
assume n<=m; then
|.(||.Sq -Sq0.||).m-0 .| < p by A3; then
|.||. (Sq -Sq0).m .||.| < p by NORMSP_0:def 4; then
|.||.Sq.m -Sq0.||.| < p by NORMSP_1:def 4;
hence ||.Sq.m -Sq0.|| < p by ABSVALUE:def 1;
end;
end;
hence Sq is convergent by NORMSP_1:def 6;
hence lim Sq =Sq0 by A2,NORMSP_1:def 7;
end;
theorem Th65:
for X be RealNormSpace, Sq be sequence of X st
Sq is Cauchy_sequence_by_Norm holds
ex N be increasing sequence of NAT st
for i,j be Nat st j >= N.i holds
||. Sq.j - Sq.(N.i) .|| < 2 to_power (-i)
proof
let X be RealNormSpace, Sq be sequence of X;
assume A1: Sq is Cauchy_sequence_by_Norm;
1 =2 to_power (-0) by POWER:24; then
consider N0 be Nat such that
A2: for j,i be Nat st j >= N0 & i >= N0 holds
||. Sq.j - Sq.i .|| < 2 to_power (-0) by A1,RSSPACE3:8;
reconsider N0 as Element of NAT by ORDINAL1:def 12;
defpred P[set,set,set] means
ex n,x,y be Nat st n=$1 & x=$2 & y=$3 &
( ( for j be Nat st j >= x holds
||.Sq.j -Sq.x.|| < 2 to_power (-n) ) implies x < y &
( for j be Nat st j >= y holds
||.Sq.j -Sq.y.|| < 2 to_power (-(n+1)) ) );
A3:for n being Nat,x being Element of NAT
ex y being Element of NAT st P[n,x,y]
proof
let n be Nat, x be Element of NAT;
now assume for j be Nat st j >= x
holds ||.Sq.j -Sq.x.|| < 2 to_power (-n);
0 < 2 to_power (-(n+1)) by POWER:34; then
consider N2 be Nat such that
A4: for j,i be Nat st j >= N2 & i >= N2 holds
||.Sq.j -Sq.i.|| < 2 to_power (-(n+1)) by A1,RSSPACE3:8;
set y= max(x,N2)+1;
take y;
x <= max(x,N2) by XXREAL_0:25;
hence x < y by NAT_1:13;
N2 <= max(x,N2) by XXREAL_0:25; then
A5: N2 < y by NAT_1:13;
thus for j be Nat st j >= y holds
||.Sq.j -Sq.y.|| < 2 to_power (-(n+1))
proof
let j be Nat;
assume j >= y; then
j >= N2 & y >=N2 by A5,XXREAL_0:2;
hence thesis by A4;
end;
end;
hence thesis;
end;
consider f being sequence of NAT such that
A6: f.0 = N0 &
for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A3);
defpred Q[Nat] means
for j be Nat st j >= f.$1 holds
||. Sq.j - Sq.(f.$1) .|| < 2 to_power (-$1);
A7:Q[ 0] by A2,A6;
A8:now let i be Nat;
assume A9: Q[i];
ex n,x,y be Nat st n=i & x=f.i & y=f.(i+1) &
( (for j be Nat st j >= x holds
||.Sq.j -Sq.x.|| < 2 to_power (-n))
implies
x < y &
(for j be Nat st j >= y holds
||.Sq.j -Sq.y.|| < 2 to_power (-(n+1)) )
) by A6;
hence Q[i+1] by A9;
end;
A10:for i be Nat holds Q[i] from NAT_1:sch 2(A7,A8);
now let i be Nat;
ex n,x,y be Nat st n=i & x=f.i & y=f.(i+1) &
( (for j be Nat st j >= x holds
||.Sq.j -Sq.x.|| < 2 to_power (-n))
implies
x < y &
(for j be Nat st j >= y holds
||.Sq.j -Sq.y.|| < 2 to_power (-(n+1)))
) by A6;
hence f.i < f.(i+1) by A10;
end; then
f is increasing;
hence thesis by A10;
end;
theorem Th66:
for F be Functional_Sequence of X,REAL st
(for m be Nat holds F.m in Lp_Functions(M,k))
holds
for m be Nat holds (Partial_Sums F).m in Lp_Functions(M,k)
proof
let F be Functional_Sequence of X,REAL;
assume A1: for m be Nat holds F.m in Lp_Functions(M,k);
defpred P[Nat] means (Partial_Sums F).$1 in Lp_Functions(M,k);
(Partial_Sums F).0 = F.0 by MESFUN9C:def 2; then
A2:P[ 0] by A1;
A3:now let j be Nat;
assume P[j]; then
A4:(Partial_Sums F).j in Lp_Functions(M,k) &
F.(j+1) in Lp_Functions(M,k) by A1;
(Partial_Sums F).(j+1) = (Partial_Sums F).j + F.(j+1) by MESFUN9C:def 2;
hence P[j+1] by A4,Th25;
end;
for j being Nat holds P[j] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th67:
for F be Functional_Sequence of X,REAL st
(for m be Nat holds F.m is nonnegative)
holds
for m be Nat holds (Partial_Sums F).m is nonnegative
proof
let F be Functional_Sequence of X,REAL;
assume A1: for m be Nat holds F.m is nonnegative;
defpred P[Nat] means (Partial_Sums F).$1 is nonnegative;
(Partial_Sums F).0 = F.0 by MESFUN9C:def 2; then
A2:P[ 0] by A1;
A3:now let k be Nat;
assume P[k]; then
A4:(Partial_Sums F).k is nonnegative & F.(k+1) is nonnegative by A1;
(Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by MESFUN9C:def 2;
hence P[k+1] by A4,MESFUNC6:56;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th68:
for F be Functional_Sequence of X,REAL, x be Element of X, n,m be Nat st
F is with_the_same_dom & x in dom(F.0) &
(for k be Nat holds F.k is nonnegative) & n <= m holds
((Partial_Sums F).n).x <= ((Partial_Sums F).m).x
proof
let F be Functional_Sequence of X,REAL, x be Element of X, n,m be Nat;
assume A1: F is with_the_same_dom;
assume A2: x in dom(F.0);
assume A3: for m be Nat holds F.m is nonnegative;
assume A4: n <= m;
set PF = Partial_Sums F;
defpred P[Nat] means (PF.n).x <= (PF.$1).x;
A5:for k be Nat holds (PF.k).x <= (PF.(k+1)).x
proof
let k be Nat;
A6:PF.(k+1) = PF.k + F.(k+1) by MESFUN9C:def 2;
A7:dom(PF.(k+1)) = dom(F.0) by A1,MESFUN9C:11;
F.(k+1) is nonnegative & PF.k is nonnegative by A3,Th67; then
0 <= (F.(k+1)).x & 0 <= (PF.k).x by MESFUNC6:51; then
(PF.k).x + 0 <= (PF.k).x + (F.(k+1)).x by XREAL_1:7;
hence thesis by A7,A2,A6,VALUED_1:def 1;
end;
A8:for k be Nat st k >= n &
(for l be Nat st l >= n & l < k holds P[l]) holds P[k]
proof
let k be Nat;
assume
A9: k >= n & for l be Nat st l >= n & l < k holds P[l];
now assume k > n; then
k >= n + 1 by NAT_1:13; then
A10: k = n+1 or k > n+1 by XXREAL_0:1;
now assume A11: k > n+1; then
reconsider l = k-1 as Nat by NAT_1:20;
k < k+1 by NAT_1:13; then
k > l & l >= n by A11,XREAL_1:19; then
A12: (PF.n).x <= (PF.l).x by A9;
k = l+1; then
(PF.l).x <= (PF.k).x by A5;
hence thesis by A12,XXREAL_0:2;
end;
hence thesis by A10,A5;
end;
hence thesis by A9,XXREAL_0:1;
end;
for k being Nat st k >= n holds P[k] from NAT_1:sch 9(A8);
hence thesis by A4;
end;
theorem Th69:
for F be Functional_Sequence of X,REAL st
F is with_the_same_dom holds (abs F) is with_the_same_dom
proof
let F be Functional_Sequence of X,REAL;
assume A1: F is with_the_same_dom;
for n,m be Nat holds dom((abs F).n) = dom((abs F).m)
proof
let n,m be Nat;
(abs F).n = abs(F.n) & (abs F).m = abs(F.m) by SEQFUNC:def 4; then
dom((abs F).n) = dom(F.n) & dom((abs F).m) = dom(F.m) by VALUED_1:def 11;
hence dom((abs F).n) = dom((abs F).m) by A1,MESFUNC8:def 2;
end;
hence abs F is with_the_same_dom by MESFUNC8:def 2;
end;
theorem Th70:
for k be geq_than_1 Real, Sq be sequence of Lp-Space(M,k) st
Sq is Cauchy_sequence_by_Norm holds Sq is convergent
proof
let k be geq_than_1 Real;
let Sq be sequence of Lp-Space(M,k);
A1:1 <= k by Def1;
assume A2: Sq is Cauchy_sequence_by_Norm;
consider Fsq be with_the_same_dom Functional_Sequence of X,REAL such that
A3: for n be Nat holds Fsq.n in Lp_Functions(M,k) & Fsq.n in Sq.n &
Sq.n= a.e-eq-class_Lp(Fsq.n,M,k) &
ex r be Real st 0<=r & r = Integral(M,(abs (Fsq.n)) to_power k) &
||. Sq.n .|| =r to_power (1/k) by Th63;
Fsq.0 in Lp_Functions(M,k) by A3; then
A4: ex D be Element of S st M.D` =0 & dom(Fsq.0) = D &
(Fsq.0) is D-measurable by Th35; then
reconsider E = dom(Fsq.0) as Element of S;
consider N be increasing sequence of NAT such that
A5: for i,j be Nat st j >= N.i holds
||. Sq.j - Sq.(N.i) .|| < 2 to_power (-i) by Th65,A2;
deffunc FsqN(Nat) = Fsq.(N.$1);
consider F1 be Functional_Sequence of X,REAL such that
A6: for n be Nat holds F1.n = FsqN(n) from SEQFUNC:sch 1;
A7: for n be Nat holds dom(F1.n) = E & F1.n in Lp_Functions(M,k) &
F1.n is E-measurable & abs(F1.n) in Lp_Functions(M,k)
proof
let n be Nat;
A8: F1.n = Fsq.(N.n) by A6;
hence
A9: dom(F1.n) = E & F1.n in Lp_Functions(M,k) by A3,MESFUNC8:def 2; then
consider F be PartFunc of X,REAL such that
Z1: F1.n = F &
ex ND be Element of S st M.ND` =0 & dom F = ND &
F is ND-measurable & (abs F) to_power k is_integrable_on M;
consider ND be Element of S such that
Z2: M.ND` =0 & dom F = ND &
F is ND-measurable & (abs F) to_power k is_integrable_on M by Z1;
ND = E by Z1,Z2,A8,MESFUNC8:def 2;
hence F1.n is E-measurable by Z1,Z2;
thus abs(F1.n) in Lp_Functions(M,k) by A9,Th28;
end;
for n,m be Nat holds dom (F1.n) = dom (F1.m)
proof
let n,m be Nat;
dom(F1.n) = E & dom(F1.m) = E by A7;
hence thesis;
end; then
reconsider F1 as with_the_same_dom Functional_Sequence of X,REAL
by MESFUNC8:def 2;
deffunc FF(Nat) = F1.($1+1) - F1.$1;
consider FMF be Functional_Sequence of X,REAL such that
A10: for n be Nat holds FMF.n = FF(n) from SEQFUNC:sch 1;
A11: for n be Nat holds dom(FMF.n) = E & FMF.n in Lp_Functions(M,k)
proof
let n be Nat;
A12: dom(F1.n) = E & dom(F1.(n+1)) = E by A7;
FMF.n = F1.(n+1) - F1.n by A10; then
dom(FMF.n) = dom (F1.(n+1)) /\ dom (F1.n) by VALUED_1:12;
hence dom(FMF.n) = E by A12;
Fsq.(N.(n+1)) in Lp_Functions(M,k) & Fsq.(N.n) in Lp_Functions(M,k)
by A3; then
F1.(n+1) in Lp_Functions(M,k) & F1.n in Lp_Functions(M,k) by A6; then
F1.(n+1) - F1.n in Lp_Functions(M,k) by Th27;
hence FMF.n in Lp_Functions(M,k) by A10;
end;
for n,m be Nat holds dom(FMF.n) = dom(FMF.m)
proof
let n,m be Nat;
dom(FMF.n) = E & dom(FMF.m) = E by A11;
hence thesis;
end; then
reconsider FMF as with_the_same_dom Functional_Sequence of X,REAL
by MESFUNC8:def 2;
set AbsFMF = abs FMF;
A13: for n be Nat holds
AbsFMF.n is nonnegative & dom(AbsFMF.n) = E & abs(AbsFMF.n) = AbsFMF.n &
AbsFMF.n in Lp_Functions(M,k) & AbsFMF.n is E-measurable
proof
let n be Nat;
A14: AbsFMF.n = abs (FMF.n) by SEQFUNC:def 4;
hence AbsFMF.n is nonnegative;
A15: dom(FMF.n) = E & FMF.n in Lp_Functions(M,k) by A11;
hence dom(AbsFMF.n) = E & abs(AbsFMF.n) = AbsFMF.n by A14,VALUED_1:def 11;
thus AbsFMF.n in Lp_Functions(M,k) by A11,A14,Th28; then
consider D be Element of S such that
Z1: M.D` = 0 & dom(AbsFMF.n) = D &
AbsFMF.n is D-measurable by Th35;
D = E by Z1,A15,A14,VALUED_1:def 11;
hence AbsFMF.n is E-measurable by Z1;
end;
reconsider
AbsFMF as with_the_same_dom Functional_Sequence of X,REAL by Th69;
deffunc Gk(Nat) =abs(F1.0) + (Partial_Sums AbsFMF).$1;
consider G be Functional_Sequence of X,REAL such that
A16: for n be Nat holds G.n = Gk(n) from SEQFUNC:sch 1;
A17:for n be Nat holds
dom(G.n) = E & G.n in Lp_Functions(M,k) & G.n is nonnegative &
G.n is E-measurable & abs(G.n) = G.n
proof
let n be Nat;
A18: G.n = abs(F1.0) + (Partial_Sums AbsFMF).n by A16; then
A19: dom(G.n)
= dom(abs(F1.0)) /\ dom((Partial_Sums AbsFMF).n) by VALUED_1:def 1
.= dom(F1.0) /\ dom((Partial_Sums AbsFMF).n) by VALUED_1:def 11
.= dom(F1.0) /\ dom(AbsFMF.0) by MESFUN9C:11;
A20: (Partial_Sums AbsFMF).n in Lp_Functions(M,k) &
(Partial_Sums AbsFMF).n is nonnegative &
(Partial_Sums AbsFMF).n is E-measurable
by A13,Th66,Th67,MESFUN9C:16;
A21: dom(AbsFMF.0) = E by A13;
A22: F1.0 in Lp_Functions(M,k) & dom(F1.0) = E & F1.0 is E-measurable
by A7; then
abs(F1.0) in Lp_Functions(M,k) & abs(F1.0) is nonnegative &
abs(F1.0) is E-measurable by Th28,MESFUNC6:48;
hence thesis by A19,A22,A21,A18,A20,Th14,Th25,MESFUNC6:26,56;
end;
deffunc Gpk(Nat) =(G.$1) to_power k;
consider Gp be Functional_Sequence of X,REAL such that
A23: for n be Nat holds Gp.n = Gpk(n) from SEQFUNC:sch 1;
A24:for n be Nat holds
((G.n) to_power k) is nonnegative & ((G.n) to_power k) is E-measurable
proof
let n be Nat;
A25: G.n is nonnegative by A17;
hence ((G.n) to_power k) is nonnegative;
G.n is E-measurable & dom(G.n) = E by A17;
hence ((G.n) to_power k) is E-measurable by A25,MESFUN6C:29;
end;
reconsider ExtGp = R_EAL Gp as Functional_Sequence of X,ExtREAL;
A26:for n be Nat holds
dom(ExtGp.n) = E & ExtGp.n is E-measurable &
ExtGp.n is nonnegative
proof
let n be Nat;
ExtGp.n = R_EAL((G.n) to_power k) by A23; then
dom(ExtGp.n) = dom (G.n) by MESFUN6C:def 4;
hence dom(ExtGp.n) = E by A17;
((G.n) to_power k) is E-measurable by A24; then
R_EAL((G.n) to_power k) is E-measurable;
hence ExtGp.n is E-measurable by A23;
((G.n) to_power k) is nonnegative by A24;
hence ExtGp.n is nonnegative by A23;
end; then
A27:dom(ExtGp.0) = E & ExtGp.0 is nonnegative;
for n,m be Nat holds dom (ExtGp.n) = dom (ExtGp.m)
proof
let n,m be Nat;
dom (ExtGp.n) = E & dom(ExtGp.m) = E by A26;
hence thesis;
end; then
reconsider ExtGp as with_the_same_dom Functional_Sequence of X,ExtREAL
by MESFUNC8:def 2;
A28:for n,m be Nat st n <=m holds
for x be Element of X st x in E holds (ExtGp.n).x <= (ExtGp.m).x
proof
let n,m be Nat;
assume A29:n <=m;
let x be Element of X;
assume A30:x in E; then
A31: x in dom (G.n) & x in dom (G.m) by A17; then
x in dom((G.n) to_power k) &
x in dom((G.m) to_power k) by MESFUN6C:def 4; then
((G.n).x) to_power k = ((G.n) to_power k).x &
((G.m).x) to_power k = ((G.m) to_power k).x by MESFUN6C:def 4; then
A32: ((G.n).x) to_power k = (ExtGp.n).x &
((G.m).x) to_power k = (ExtGp.m).x by A23;
dom(AbsFMF.0) = E by A13; then
((Partial_Sums AbsFMF).n).x <= ((Partial_Sums AbsFMF).m).x
by Th68,A29,A30,A13; then
A33: (abs(F1.0)).x + ((Partial_Sums AbsFMF).n).x
<= (abs(F1.0)).x + ((Partial_Sums AbsFMF).m).x by XREAL_1:6;
G.m= abs(F1.0) + (Partial_Sums AbsFMF).m &
G.n= abs(F1.0) + (Partial_Sums AbsFMF).n by A16; then
A34: (G.m).x= (abs(F1.0)).x + ((Partial_Sums AbsFMF).m).x &
(G.n).x= (abs(F1.0)).x + ((Partial_Sums AbsFMF).n).x by A31,VALUED_1:def 1
;
G.n is nonnegative by A17; then
0 <= (G.n).x by MESFUNC6:51;
hence thesis by A32,A33,A34,HOLDER_1:3;
end;
A35:for x be Element of X st x in E holds ExtGp#x is non-decreasing
proof
let x be Element of X;
assume A36: x in E;
for n,m be Nat st m<=n holds ((ExtGp)#x).m <= ((ExtGp)#x).n
proof
let n,m be Nat;
assume m <= n; then
((ExtGp).m).x <= ((ExtGp).n).x by A28,A36; then
((ExtGp)#x).m <= ((ExtGp).n).x by MESFUNC5:def 13;
hence thesis by MESFUNC5:def 13;
end;
hence ExtGp#x is non-decreasing by RINFSUP2:7;
end;
A37:for x be Element of X st x in E holds ExtGp#x is convergent
proof
let x be Element of X;
assume x in E; then
ExtGp#x is non-decreasing by A35;
hence thesis by RINFSUP2:37;
end; then
consider I be ExtREAL_sequence such that
A38: (for n be Nat holds I.n = Integral(M,ExtGp.n)) &
I is convergent & Integral(M,lim ExtGp) = lim I
by A27,A26,A28,MESFUNC9:52;
now let y be object;
assume y in rng I; then
consider x be Element of NAT such that
A39: y = I.x by FUNCT_2:113;
A40: y = Integral(M,Gp.x) by A39,A38;
G.x = abs(G.x) by A17; then
A41: Gp.x = abs(G.x) to_power k by A23;
G.x in Lp_Functions(M,k) by A17;
hence y in REAL by A40,A41,Th49;
end; then
rng I c= REAL; then
reconsider Ir = I as sequence of REAL by FUNCT_2:6;
deffunc KAbsFMF(Nat) = Integral(M,(AbsFMF.$1) to_power k);
A42:for x being Element of NAT holds KAbsFMF(x) is Element of REAL
proof
let x being Element of NAT;
(AbsFMF.x) in Lp_Functions(M,k) by A13; then
Integral(M,(abs(AbsFMF.x)) to_power k) in REAL by Th49;
hence thesis by A13;
end;
consider KPAbsFMF being sequence of REAL such that
A43: for x be Element of NAT holds
KPAbsFMF.x = KAbsFMF(x) from FUNCT_2:sch 9(A42);
deffunc KKAbsFMF(Nat) = (KPAbsFMF.$1) to_power (1/k);
A44:for x being Element of NAT holds KKAbsFMF(x) is Element of REAL
by XREAL_0:def 1;
consider PAbsFMF being sequence of REAL such that
A45: for x be Element of NAT holds
PAbsFMF.x = KKAbsFMF(x) from FUNCT_2:sch 9(A44);
F1.0 in Lp_Functions(M,k) by A7; then
reconsider
RF0=Integral(M,(abs(F1.0)) to_power k) as Element of REAL by Th49;
deffunc LAbsFMF(Nat)
= RF0 to_power (1/k) + (Partial_Sums PAbsFMF).$1;
A46:for x being Element of NAT holds LAbsFMF(x) is Element of REAL
by XREAL_0:def 1;
consider QAbsFMF being sequence of REAL such that
A47: for x being Element of NAT holds QAbsFMF.x = LAbsFMF(x)
from FUNCT_2:sch 9(A46);
A48:for n being Nat holds (Ir.n) to_power (1/k) <= QAbsFMF.n
proof
defpred PN[Nat] means (Ir.$1) to_power (1/k) <= QAbsFMF.$1;
A49: abs(F1.0) in Lp_Functions(M,k) & AbsFMF.0 in Lp_Functions(M,k) by A13,A7;
G.0 = abs(F1.0) + (Partial_Sums AbsFMF).0 by A16; then
A50: G.0 =abs(F1.0) + AbsFMF.0 by MESFUN9C:def 2;
Ir.0 = Integral(M,Gp.0) by A38; then
Ir.0 = Integral(M,(G.0) to_power k) by A23; then
A51: Ir.0 = Integral(M,abs( abs(F1.0) + AbsFMF.0 ) to_power k) by A17,A50;
KPAbsFMF.0 = Integral(M,(AbsFMF.0) to_power k) by A43; then
A52: KPAbsFMF.0 = Integral(M,abs(AbsFMF.0) to_power k) by A13;
A53: RF0 = Integral(M,abs(abs(F1.0)) to_power k);
QAbsFMF.0 = RF0 to_power (1/k) + (Partial_Sums PAbsFMF).0 by A47; then
QAbsFMF.0 = RF0 to_power (1/k) + PAbsFMF.0 by SERIES_1:def 1; then
QAbsFMF.0 = RF0 to_power (1/k) + (KPAbsFMF.0) to_power (1/k) by A45; then
A54: PN[ 0] by A1,A49,A51,A52,A53,Th61;
A55: now let n being Nat;
A56: n in NAT by ORDINAL1:def 12;
assume PN[n]; then
A57: (Ir.n) to_power (1/k) + PAbsFMF.(n+1) <= QAbsFMF.n + PAbsFMF.(n+1)
by XREAL_1:6;
G.(n+1) = abs(F1.0) + (Partial_Sums AbsFMF).(n+1) by A16
.= abs(F1.0) + ((Partial_Sums AbsFMF).n + AbsFMF.(n+1)) by MESFUN9C:def 2
.= abs(F1.0) +(Partial_Sums AbsFMF).n + AbsFMF.(n+1) by RFUNCT_1:8; then
A58: G.(n+1) = G.n + AbsFMF.(n+1) by A16;
A59: AbsFMF.(n+1) in Lp_Functions(M,k) & G.n in Lp_Functions(M,k) by A13,A17;
KPAbsFMF.(n+1) = Integral(M,(AbsFMF.(n+1)) to_power k) by A43; then
A60: KPAbsFMF.(n+1) = Integral(M,abs (AbsFMF.(n+1)) to_power k) by A13;
A61: PAbsFMF.(n+1) = (KPAbsFMF.(n+1)) to_power (1/k) by A45;
Ir.n = Integral(M,Gp.n) & Ir.(n+1) = Integral(M,Gp.(n+1)) by A38; then
Ir.n = Integral(M,(G.n) to_power k) &
Ir.(n+1) = Integral(M,(G.(n+1)) to_power k) by A23; then
Ir.n = Integral(M,abs (G.n) to_power k) &
Ir.(n+1) =Integral(M,abs (G.n + AbsFMF.(n+1)) to_power k) by A58,A17;
then
(Ir.(n+1)) to_power (1/k) <= (Ir.n) to_power (1/k) + PAbsFMF.(n+1)
by A1,A59,A60,A61,Th61; then
A62: (Ir.(n+1)) to_power (1/k) <= QAbsFMF.n + PAbsFMF.(n+1) by A57,XXREAL_0:2
;
QAbsFMF.n + PAbsFMF.(n+1)
= RF0 to_power (1/k) + (Partial_Sums PAbsFMF).n + PAbsFMF.(n+1)
by A47,A56
.= RF0 to_power (1/k) + ((Partial_Sums PAbsFMF).n + PAbsFMF.(n+1))
.= RF0 to_power (1/k) + (Partial_Sums PAbsFMF).(n+1) by SERIES_1:def 1;
hence PN[n+1] by A62,A47;
end;
for n be Nat holds PN[n] from NAT_1:sch 2(A54,A55);
hence thesis;
end;
A63:for n be Nat holds PAbsFMF.n = ||. Sq.(N.(n+1))-Sq.(N.n) .||
proof
let n be Nat;
A64: n in NAT by ORDINAL1:def 12;
set m = N.n;
set m1 = N.(n+1);
A65: F1.(n+1) = Fsq.(N.(n+1)) & F1.n = Fsq.(N.n) by A6;
AbsFMF.n = abs (FMF.n) by SEQFUNC:def 4; then
A66: AbsFMF.n = abs( Fsq.(N.(n+1)) - Fsq.(N.n) ) by A65,A10;
A67: Fsq.(N.(n+1)) in Lp_Functions(M,k) & Fsq.(N.(n+1)) in Sq.(N.(n+1)) &
Fsq.(N.n) in Lp_Functions(M,k) & Fsq.(N.n) in Sq.m by A3; then
(-1)(#)(Fsq.m) in (-1)*(Sq.m) by Th54; then
Fsq.m1 - Fsq.m in Sq.m1 + (-1)*(Sq.m) by Th54,A67; then
Fsq.m1 - Fsq.m in Sq.m1 - Sq.m by RLVECT_1:16; then
A68: ex r be Real
st 0<=r & r = Integral(M,(abs (Fsq.m1 - Fsq.m)) to_power k) &
||. Sq.m1 - Sq.m .|| = r to_power (1/k) by Th53;
PAbsFMF.n = (KPAbsFMF.n) to_power (1/k) by A45,A64;
hence thesis by A68,A66,A43,A64;
end;
1/2 < 1; then
|.1/2.| < 1 by ABSVALUE:def 1; then
A69:(1/2) GeoSeq is summable & Sum((1/2) GeoSeq) = 1/(1-(1/2)) by SERIES_1:24;
for n be Nat holds 0<=PAbsFMF.n & PAbsFMF.n <= ((1/2) GeoSeq).n
proof
let n be Nat;
A70: PAbsFMF.n = ||. Sq.(N.(n+1)) - Sq.(N.n) .|| by A63;
hence 0 <= PAbsFMF.n;
((1/2) GeoSeq).n = (1/2) |^n by PREPOWER:def 1
.= (1/2) to_power n by POWER:41; then
A71: ((1/2) GeoSeq).n = 2 to_power (-n) by POWER:32;
N is Real_Sequence by FUNCT_2:7,NUMBERS:19; then
N.n < N.(n+1) by SEQM_3:def 6;
hence PAbsFMF.n <= ((1/2) GeoSeq).n by A5,A70,A71;
end; then
PAbsFMF is summable & Sum(PAbsFMF) <= Sum((1/2) GeoSeq)
by A69,SERIES_1:20; then
Partial_Sums(PAbsFMF) is convergent by SERIES_1:def 2; then
Partial_Sums(PAbsFMF) is bounded; then
consider Br be Real such that
A72: for n be Nat holds Partial_Sums(PAbsFMF).n < Br by SEQ_2:def 3;
for n being Nat holds
Ir.n < (RF0 to_power (1/k) + Br) to_power k
proof
let n being Nat;
A73: n in NAT by ORDINAL1:def 12;
(Ir.n) to_power (1/k) <= QAbsFMF.n by A48; then
A74: (Ir.n) to_power (1/k) <= RF0 to_power (1/k) + (Partial_Sums PAbsFMF).n
by A47,A73;
RF0 to_power (1/k) + (Partial_Sums PAbsFMF).n < RF0 to_power (1/k) + Br
by A72,XREAL_1:8; then
A75: (Ir.n) to_power (1/k) < RF0 to_power (1/k) + Br by A74,XXREAL_0:2;
Ir.n = Integral(M,Gp.n) by A38; then
Ir.n = Integral(M,(G.n) to_power k) by A23; then
A76:Ir.n = Integral(M,abs(G.n) to_power k) by A17;
A77: G.n in Lp_Functions(M,k) by A17; then
0 <= (Ir.n) to_power (1/k) by Th49,A76,Th4; then
((Ir.n) to_power (1/k)) to_power k
< (RF0 to_power (1/k) + Br) to_power k by A75,Th3; then
(Ir.n) to_power ((1/k)*k) < (RF0 to_power (1/k) + Br) to_power k
by A77,Th49,A76,HOLDER_1:2; then
(Ir.n) to_power 1 < (RF0 to_power (1/k) + Br) to_power k by XCMPLX_1:106;
hence thesis by POWER:25;
end; then
A78:Ir is bounded_above by SEQ_2:def 3;
for n,m be Nat st n <=m holds Ir.n <= Ir.m
proof
let n,m be Nat;
assume n <=m; then
A79: for x be Element of X st x in E holds (ExtGp.n).x <= (ExtGp.m).x by A28;
A80: ExtGp.n is E-measurable & ExtGp.m is E-measurable &
ExtGp.n is nonnegative & ExtGp.m is nonnegative by A26;
A81: dom(ExtGp.n) = E & dom(ExtGp.m) = E by A26; then
A82: (ExtGp.n)|E = ExtGp.n & (ExtGp.m)|E = ExtGp.m by RELAT_1:68;
I.n = Integral(M,ExtGp.n) & I.m = Integral(M,ExtGp.m) by A38;
hence thesis by A79,A81,A80,A82,MESFUNC9:15;
end; then
Ir is non-decreasing by SEQM_3:6; then
A83:I is convergent_to_finite_number & lim I = lim Ir by A78,RINFSUP2:14;
reconsider LExtGp = lim ExtGp as PartFunc of X,ExtREAL;
A84:E = dom LExtGp & LExtGp is E-measurable
by A26,A27,A37,MESFUNC8:25,def 9;
A85:for x be object st x in dom LExtGp holds 0 <= LExtGp.x
proof
let x be object;
assume A86: x in dom LExtGp; then
reconsider x1 = x as Element of X;
A87: x1 in E by A27,A86,MESFUNC8:def 9;
now let k1 being Nat;
reconsider k=k1 as Nat;
ExtGp#x1 is non-decreasing by A35,A87; then
A88: (ExtGp#x1).0 <= (ExtGp#x1).k by RINFSUP2:7;
0 <= (ExtGp.0).x1 by A27,SUPINF_2:39;
hence 0 <= (ExtGp#x1).k1 by A88,MESFUNC5:def 13;
end; then
0 <= lim (ExtGp#x1) by A87,A37,MESFUNC9:10;
hence thesis by A86,MESFUNC8:def 9;
end;
A89:eq_dom(LExtGp,+infty) = E /\ eq_dom(LExtGp,+infty)
by A84,RELAT_1:132,XBOOLE_1:28; then
reconsider EE=eq_dom(LExtGp,+infty) as Element of S by A84,MESFUNC1:33;
reconsider E0= E \ EE as Element of S;
E0` = (X \ E) \/ (X /\ EE) by XBOOLE_1:52; then
A90:E0` = E` \/ EE by XBOOLE_1:28;
M.EE = 0 by A38,A83,A84,A85,A89,MESFUNC9:13,SUPINF_2:52; then
A91:EE is measure_zero of M by MEASURE1:def 7;
E` is Element of S by MEASURE1:34; then
E` is measure_zero of M by A4,MEASURE1:def 7; then
E0` is measure_zero of M by A90,A91,MEASURE1:37; then
A92:M.E0` = 0 by MEASURE1:def 7;
A93:for x be Element of X st x in E0 holds LExtGp.x in REAL
proof
let x be Element of X;
assume x in E0; then
x in E & not x in EE by XBOOLE_0:def 5; then
LExtGp.x <> +infty & 0<= LExtGp.x by A84,A85,MESFUNC1:def 15;
hence LExtGp.x in REAL by XXREAL_0:14;
end;
A94:for x be Element of X st x in E0 holds
Gp#x is convergent & lim (Gp#x)= lim (ExtGp#x)
proof
let x be Element of X;
assume A95: x in E0; then
A96: x in E by XBOOLE_0:def 5; then
LExtGp.x = lim((ExtGp)#x) by A84,MESFUNC8:def 9; then
A97: lim((ExtGp)#x) in REAL by A93,A95;
(ExtGp)#x is convergent by A37,A96; then
A98: ex g be Real st lim((ExtGp)#x) = g &
(for p be Real st 0<p ex n be Nat st
for m be Nat st n<=m holds |. ((ExtGp)#x).m - lim((ExtGp)#x) .| < p) &
(ExtGp)#x is convergent_to_finite_number
by A97,MESFUNC5:def 12;
ExtGp#x = Gp#x by MESFUN7C:1;
hence thesis by A98,RINFSUP2:15;
end;
A99:for x be Element of X st x in E0 holds
for n be Nat holds (Gp#x).n = ((G#x).n) to_power k
proof
let x be Element of X;
assume A100: x in E0;
hereby let n be Nat;
x in E by A100,XBOOLE_0:def 5; then
x in dom(G.n) by A17; then
A101: 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 A101,MESFUN6C:def 4;
hence (Gp#x).n = ((G#x).n) to_power k by SEQFUNC:def 10;
end;
end;
A102:for x be Element of X st x in E0 holds
(Partial_Sums AbsFMF)#x is convergent
proof
let x be Element of X;
assume A103: x in E0; then
A104: Gp#x is convergent by A94;
A105: now let n be Nat;
G.n is nonnegative by A17; then
0 <= (G.n).x by MESFUNC6:51; hence
0 <= (G#x).n by SEQFUNC:def 10;
end;
for n be Nat holds
(Gp#x).n = ((G#x).n) to_power k by A103,A99; then
A106: G#x is convergent by A104,A105,Th9;
now let s be Real;
assume 0<s; then
consider n be Nat such that
A107: for m be Nat st n<=m holds |.(G#x).m -(G#x).n qua Complex.|<s
by A106,SEQ_4:41;
now let m be Nat;
assume A108: n<=m;
x in E by A103,XBOOLE_0:def 5; then
A109: 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 A109,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
A110: (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 |.((Partial_Sums AbsFMF)#x).m -((Partial_Sums AbsFMF)#x).n
qua Complex .| < s
by A107,A108,A110;
end;
hence ex n be Nat st for m be Nat st n<=m holds
|.((Partial_Sums AbsFMF)#x).m - ((Partial_Sums AbsFMF)#x).n
qua Complex.| < s;
end;
hence thesis by SEQ_4:41;
end;
A111:for x be Element of X st x in E0 holds
Partial_Sums abs(FMF#x) = (Partial_Sums AbsFMF)#x
proof
let x be Element of X;
assume x in E0; then
A112: x in E by XBOOLE_0:def 5;
defpred PQ[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
.= |.(FMF#x).0 .| by VALUED_1:18
.= |.(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
A113: PQ[ 0];
A114: now let n be Nat;
assume A115: PQ[n];
A116: (Partial_Sums AbsFMF).(n+1) = (Partial_Sums AbsFMF).n + AbsFMF.(n+1)
by MESFUN9C:def 2;
dom(AbsFMF.0) = E by A13; then
A117: x in dom((Partial_Sums AbsFMF).(n+1)) by A112,MESFUN9C:11;
A118: abs(FMF#x).(n+1) = |.(FMF#x).(n+1).| by VALUED_1:18
.= |.(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 A115,A118,SEQFUNC:def 10
.= ((Partial_Sums AbsFMF).(n+1)).x by A116,A117,VALUED_1:def 1
.= ((Partial_Sums AbsFMF)#x).(n+1) by SEQFUNC:def 10;
hence PQ[n+1];
end;
for n be Nat holds PQ[n] from NAT_1:sch 2(A113,A114);
then for n be Element of NAT holds PQ[n];
hence thesis by FUNCT_2:63;
end;
A119:for x be Element of X st x in E0 for n be Nat holds
(F1#x).(n+1) = (F1#x).0 + (Partial_Sums (FMF#x)).n
proof
let x be Element of X;
assume x in E0; then
A120:x in E by XBOOLE_0:def 5;
defpred PQ[Nat] means
(F1#x).($1+1) = (F1#x).0 + (Partial_Sums(FMF#x)).$1;
dom (FMF.0) = E by A11; then
A121: x in dom (F1.(0+1) - F1.0) by A10,A120;
(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
A122: (Partial_Sums (FMF#x)).0 = (F1.(0+1)).x - (F1.0).x by A121,VALUED_1:13;
(F1#x).0 + (Partial_Sums(FMF#x)).0
= (F1.0).x + (Partial_Sums (FMF#x)).0 by SEQFUNC:def 10; then
A123: PQ[ 0] by A122,SEQFUNC:def 10;
A124: now let n be Nat;
assume A125:PQ[n];
dom (FMF.(n+1)) = E by A11; then
A126: x in dom (F1.((n+1)+1) - F1.(n+1)) by A10,A120;
(FMF#x).(n+1) = (FMF.(n+1)).x by SEQFUNC:def 10
.= ((F1.((n+1)+1) - F1.(n+1)).x) by A10; then
A127: (FMF#x).(n+1) = (F1.((n+1)+1)).x - (F1.(n+1)).x by A126,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 A125,SEQFUNC:def 10;
hence PQ[n+1] by A127,SEQFUNC:def 10;
end;
for n be Nat holds PQ[n] from NAT_1:sch 2(A123,A124);
hence thesis;
end;
A128:for x be Element of X st x in E0 holds F1#x is convergent
proof
let x be Element of X;
assume A129: x in E0; then
Partial_Sums abs(FMF#x) = (Partial_Sums AbsFMF)#x by A111; then
Partial_Sums abs(FMF#x) is convergent by A129,A102; 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; then
A130:(Partial_Sums (FMF#x)) is convergent by SERIES_1:def 2;
now let s be Real;
assume 0<s; then
consider n be Nat such that
A131: for m be Nat st n<=m holds
|.(Partial_Sums (FMF#x)).m -(Partial_Sums (FMF#x)).n qua Complex.|<s
by A130,SEQ_4:41;
set n1=n+1;
now let m1 be Nat;
assume A132: n1<=m1;
1 <=n1 by NAT_1:11; then
reconsider m=m1-1 as Nat by A132,NAT_1:21,XXREAL_0:2;
n1-1<=m1-1 by A132,XREAL_1:9; then
A133: |.(Partial_Sums (FMF#x)).m -(Partial_Sums (FMF#x)).n.|<s by A131;
m1=m+1; then
(F1#x).(n1) = (F1#x).0 + (Partial_Sums (FMF#x)).n &
(F1#x).(m1) = (F1#x).0 + (Partial_Sums (FMF#x)).m by A119,A129;
hence |.(F1#x).m1-(F1#x).n1 qua Complex.|<s by A133;
end;
hence ex n be Nat st
for m be Nat st n<=m holds |.(F1#x).m-(F1#x).n qua Complex.|<s;
end;
hence thesis by SEQ_4:41;
end;
set F2 = F1||E0;
A134:for x be Element of X st x in E0 holds F2#x is convergent
proof
let x be Element of X;
assume A135: x in E0; then
F1#x is convergent by A128;
hence thesis by A135,MESFUN9C:1;
end;
A136:for x be Element of X st x in E0 holds F2#x = F1#x
proof
let x be Element of X;
assume A137:x in E0;
now let n be Element of NAT;
(F2#x).n = (F2.n).x by SEQFUNC:def 10
.= ((F1.n)|E0).x by MESFUN9C:def 1
.= (F1.n).x by A137,FUNCT_1:49;
hence (F2#x).n = (F1#x).n by SEQFUNC:def 10;
end;
hence thesis by FUNCT_2:63;
end;
A138:for n be Nat holds dom(F2.n) = E0 & F2.n is E0-measurable
proof
let n be Nat;
A139: dom(F1.0) = E by A7;
dom (F2.n) = dom((F1.n)|E0) by MESFUN9C:def 1; then
dom (F2.n) =dom(F1.n) /\ E0 by RELAT_1:61; then
dom (F2.n) = E /\ E0 by A7;
hence dom(F2.n) = E0 by XBOOLE_1:28,36;
for m be Nat holds F1.m is E0-measurable
proof
let m be Nat;
F1.m is E-measurable by A7;
hence F1.m is E0-measurable by MESFUNC6:16,XBOOLE_1:36;
end;
hence F2.n is E0-measurable by A139,MESFUN9C:4,XBOOLE_1:36;
end;
reconsider F2 as with_the_same_dom Functional_Sequence of X,REAL
by MESFUN9C:2;
A140:for n be Nat holds F2.n in Lp_Functions(M,k) & F2.n in Sq.(N.n)
proof
let n1 be Nat;
F2.n1 = (F1.n1)|E0 by MESFUN9C:def 1; then
abs(F2.n1) = (abs(F1.n1))|E0 by Th13; then
A141: ((abs (F1.n1)) to_power k)|E0 = (abs (F2.n1)) to_power k by Th20;
A142: F2.n1 is E0-measurable & dom(F2.n1) = E0 by A138;
F1.n1 in Lp_Functions(M,k) by A7; then
ex FMF be PartFunc of X,REAL st
F1.n1= FMF & ex ND be Element of S st M.ND` =0 & dom FMF = ND &
FMF is ND-measurable & (abs FMF) to_power k is_integrable_on M; then
((abs (F2.n1)) to_power k) is_integrable_on M by A141,MESFUNC6:91;
hence A143: F2.n1 in Lp_Functions(M,k) by A142,A92;
reconsider n=n1 as Nat;
set m = N.n;
F1.n = Fsq.m by A6; then
A144: 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 A142,RELAT_1:68; then
(F2.n)|EB` =(F1.n)|EB` by MESFUN9C:def 1; then
(F2.n) a.e.= (F1.n),M by A92;
hence thesis by A143,A144,Th36;
end;
A145:dom (lim F2) = dom (F2.0) by MESFUNC8:def 9; then
A146:dom (lim F2) = E0 by A138;
A147:for x be Element of X st x in E0 holds (lim F2).x = lim (F2#x)
proof
let x be Element of X;
assume x in E0; then
(lim F2).x =lim R_EAL(F2#x) & F2#x is convergent by A146,A134,MESFUN7C:14;
hence (lim F2).x = lim (F2#x) by RINFSUP2:14;
end;
now let y be object;
assume y in rng (lim F2); then
consider x be Element of X such that
A148: x in dom (lim F2) & y= (lim F2).x by PARTFUN1:3;
y = lim (F2#x) by A148,A146,A147;
hence y in REAL by XREAL_0:def 1;
end; then
rng (lim F2) c= REAL; then
reconsider F = lim F2 as PartFunc of X,REAL by A145,RELSET_1:4;
A149:dom(LExtGp|E0) = E /\ E0 by A84,RELAT_1:61; then
A150:dom(LExtGp|E0) = E0 by XBOOLE_1:28,36;
now let y be object;
assume y in rng (LExtGp|E0); then
consider x be Element of X such that
A151: x in dom (LExtGp|E0) & y=(LExtGp|E0).x by PARTFUN1:3;
y =(LExtGp).x by A150,A151,FUNCT_1:49;
hence y in REAL by A150,A151,A93;
end; then
rng (LExtGp|E0) c= REAL; then
reconsider gp = LExtGp|E0 as PartFunc of X,REAL by A149,RELSET_1:4;
A152:for x be Element of X st x in E0 holds gp.x = lim (Gp#x)
proof
let x be Element of X;
assume A153: x in E0; then
x in dom LExtGp by A84,XBOOLE_0:def 5; then
LExtGp.x = lim((ExtGp)#x) by MESFUNC8:def 9; then
gp.x = lim((ExtGp)#x) by A153,FUNCT_1:49;
hence gp.x = lim (Gp#x) by A94,A153;
end;
A154: LExtGp is nonnegative by A85,SUPINF_2:52;
Integral(M,LExtGp) in REAL by A83,A38,XREAL_0:def 1;
then LExtGp is_integrable_on M by A154,A84,Th2; then
R_EAL gp is_integrable_on M by MESFUNC5:97; then
A155:gp is_integrable_on M;
A156:dom(F2.0) = E0 by A138; then
A157:dom F = E0 by MESFUNC8:def 9; then
A158:E0 =dom abs F by VALUED_1:def 11; then
A159:E0 = dom((abs F) to_power k) by MESFUN6C:def 4;
A160:for x be Element of X, n be Nat st x in E0 holds
|.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.|
<= (G#x).n
proof
let x be Element of X,n be Nat;
assume A161: x in E0; then
x in E by XBOOLE_0:def 5; then
A162: 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 A162,VALUED_1:def 1; then
A163: (G.n).x = |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF).n).x
by VALUED_1:18;
(G#x).n = (G.n).x by SEQFUNC:def 10
.=|.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF)#x).n
by A163,SEQFUNC:def 10
.=|.(F1#x).0 qua Complex .| + ((Partial_Sums AbsFMF)#x).n
by SEQFUNC:def 10; then
A164: (G#x).n =|.(F1#x).0 qua Complex .| + (Partial_Sums abs(FMF#x)).n
by A111,A161;
|.(Partial_Sums (FMF#x)).n qua Complex.| <= Partial_Sums abs(FMF#x).n
by Lm1;
hence thesis by A164,XREAL_1:6;
end;
A165:for x be Element of X, n be Nat st x in E0 holds
|.(F1#x).0 + (Partial_Sums (FMF#x)).n qua Complex.| to_power k <= (Gp#x).n
proof
let x be Element of X ,n be Nat;
assume A166: x in E0; then
A167: (Gp#x).n = (((G#x)).n) to_power k by A99;
A168: |.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.|
<= (G#x).n
by A160,A166;
|.(F1#x).0 + (Partial_Sums (FMF#x)).n qua Complex.|
<= |.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.|
by COMPLEX1:56;
then
A169: |.(F1#x).0 + (Partial_Sums (FMF#x)).n.| <= (G#x).n by A168,XXREAL_0:2;
0 <= |.(F1#x).0 + (Partial_Sums (FMF#x)).n.| by COMPLEX1:46;
hence thesis by A167,A169,HOLDER_1:3;
end;
A170:for x be Element of X, n be Nat st x in E0 holds
|.(F2#x).n qua Complex.| to_power k <= (Gp#x).n
proof
let x be Element of X, n be Nat;
assume A171: x in E0; then
A172: F1#x = F2#x by A136;
per cases;
suppose A173:n = 0;
A174: (Gp#x).n = (((G#x)).n) to_power k by A171,A99;
A175: |.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.|
<= (G#x).n by A160,A171;
0 <= |.(Partial_Sums(FMF#x)).n.| by COMPLEX1:46; then
0 + |.(F1#x).0 qua Complex .|
<= |.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.|
by XREAL_1:6; then
A176: |.(F1#x).0 qua Complex .| <= (G#x).n by A175,XXREAL_0:2;
0 <= |.(F1#x).0 .| by COMPLEX1:46;
hence |.((F2#x).n) qua Complex.| to_power k
<= (Gp#x).n by A172,A173,A174,A176,
HOLDER_1:3;
end;
suppose n <> 0; then
consider m be Nat such that
A177: n=m+1 by NAT_1:6;
reconsider m as Nat;
(F1#x).(m+1) = (F1#x).0 + (Partial_Sums(FMF#x)).m by A119,A171; then
A178: |.(F1#x).(m+1) qua Complex.| to_power k <= (Gp#x).m by A165,A171;
x in E by A171,XBOOLE_0:def 5; then
A179: ExtGp#x is non-decreasing by A35;
A180: ((ExtGp)#x).m <= ((ExtGp)#x).(m+1) by A179;
ExtGp#x = Gp#x by MESFUN7C:1;
hence |.((F2#x).n) qua Complex.| to_power k <= (Gp#x).n
by A172,A177,A178,A180,
XXREAL_0:2;
end;
end;
A181:for x be Element of X st x in E0
holds |.((abs F) to_power k).x qua Complex .| <= gp.x
proof
let x be Element of X;
assume A182: x in E0; then
A183: Gp#x is convergent by A94;
deffunc ABSF2(set) = (abs(F2#x).$1 ) to_power k;
consider s be Real_Sequence such that
A184: for n be Nat holds s.n=ABSF2(n) from SEQ_1:sch 1;
A185: gp.x = lim (Gp#x) by A152,A182;
A186: ((abs F) to_power k).x = ((abs F).x) to_power k by A159,A182,
MESFUN6C:def 4
.= (|.F.x qua Complex.|) to_power k by A158,A182,VALUED_1:def 11
.= |.lim (F2#x) qua Complex.| to_power k by A182,A147
.= (lim (abs (F2#x))) to_power k by A134,A182,SEQ_4:14;
A187: now let n be Nat;
0 <= |.(F2#x).n.| by COMPLEX1:46;
hence 0 <=(abs(F2#x)).n by VALUED_1:18;
end;
abs (F2#x) is convergent by A182,A134,SEQ_4:13; then
A188: s is convergent & (lim (abs (F2#x))) to_power k = lim s
by A187,A184,HOLDER_1:10;
now let n be Nat;
|.(F2#x).n qua Complex.| to_power k <= (Gp#x).n by A170,A182; then
(abs(F2#x).n) to_power k <= (Gp#x).n by VALUED_1:18;
hence s.n <=(Gp#x).n by A184;
end; then
A189: ((abs F) to_power k).x <= gp.x by A188,A185,A186,A183,SEQ_2:18;
0 <= ((abs F) to_power k).x by MESFUNC6:51;
hence |.((abs F) to_power k).x qua Complex.| <= gp.x
by A189,ABSVALUE:def 1;
end;
R_EAL F is E0-measurable by A138,A156,A134,MESFUN7C:21; then
A190:F is E0-measurable; then
A191:(abs F) is E0-measurable by A157,MESFUNC6:48;
dom abs F = E0 by A157,VALUED_1:def 11; then
(abs F) to_power k is E0-measurable by A191,MESFUN6C:29; then
(abs F) to_power k is_integrable_on M by A150,A155,A159,A181,MESFUNC6:96;
then
A192:F in Lp_Functions(M,k) by A92,A157,A190;
A193:for x be Element of X, n,m be Nat st x in E0 & m <= n holds
|. (F1#x).n -(F1#x).m qua Complex.| to_power k <= (Gp#x).n
proof
let x be Element of X, n1,m1 be Nat;
assume A194: x in E0 & m1 <= n1;
now per cases;
suppose A195: m1= 0;
now per cases;
suppose A196: n1=0;
((G.n1) to_power k) is nonnegative by A24; then
Gp.n1 is nonnegative by A23; then
0 <= (Gp.n1).x by MESFUNC6:51; then
0 <= (Gp#x).n1 by SEQFUNC:def 10;
hence |. (F1#x).n1-(F1#x).m1 qua Complex .| to_power k <= (Gp#x).n1
by A195,A196,COMPLEX1:44,POWER:def 2;
end;
suppose n1<> 0; then
consider n be Nat such that
A197: n1=n+1 by NAT_1:6;
reconsider n as Nat;
A198: (F1#x).(n+1) = (F1#x).0 + (Partial_Sums (FMF#x)).n by A194,A119;
A199: |.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.|
<= (G#x).n by A160
,A194;
0 <= |.(F1#x).0 .| by COMPLEX1:46; then
|.(Partial_Sums (FMF#x)).n qua Complex.| + 0
<= |.(F1#x).0 qua Complex .| +
|.(Partial_Sums (FMF#x)).n qua Complex.|
by XREAL_1:6;
then
A200: |.(Partial_Sums (FMF#x)).n qua Complex.| <= (G#x).n by A199,XXREAL_0:2;
0 <= |.(Partial_Sums (FMF#x)).n.| by COMPLEX1:46; then
A201: |. (Partial_Sums(FMF#x)).n qua Complex .| to_power k
<= ((G#x).n) to_power k by A200,HOLDER_1:3;
A202: (Gp#x).n = (((G#x)).n) to_power k by A194,A99;
x in E by A194,XBOOLE_0:def 5; then
A203: ExtGp#x is non-decreasing by A35;
A204: ((ExtGp)#x).n <= ((ExtGp)#x).(n+1) by A203;
ExtGp#x = Gp#x by MESFUN7C:1;
hence |. (F1#x).n1 -(F1#x).m1 qua Complex .| to_power k <= (Gp#x).n1
by A195,A197,A204,A201,A202,A198,XXREAL_0:2;
end;
end;
hence |. (F1#x).n1-(F1#x).m1 qua Complex .| to_power k <= (Gp#x).n1;
end;
suppose A205: m1<> 0; then
consider m be Nat such that
A206: m1=m+1 by NAT_1:6;
reconsider m as Nat;
0 < n1 by A194,A205; then
consider n be Nat such that
A207: n1=n+1 by NAT_1:6;
reconsider n as Element of NAT by ORDINAL1:def 12;
A208: m1-1 <= n1-1 by A194,XREAL_1:9;
x in E by A194,XBOOLE_0:def 5; then
A209: x in dom(G.n) by A17; then
A210: x in dom ((G.n) to_power k) by MESFUN6C:def 4;
(Gp#x).n = (Gp.n).x by SEQFUNC:def 10; then
(Gp#x).n = ((G.n) to_power k).x by A23; then
A211: (Gp#x).n = ((G.n).x) to_power k by A210,MESFUN6C:def 4;
G.n = abs(F1.0) + (Partial_Sums AbsFMF).n by A16; then
(G.n).x = abs(F1.0).x + ((Partial_Sums AbsFMF).n).x
by A209,VALUED_1:def 1
.= |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF).n).x
by VALUED_1:18; then
A212
: (G.n).x = |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF)#x).n
by SEQFUNC:def 10;
A213: (F1#x).(n+1) = (F1#x).0 + (Partial_Sums (FMF#x)).n &
(F1#x).(m+1) = (F1#x).0 + (Partial_Sums (FMF#x)).m by A194,A119;
A214: |. (Partial_Sums (FMF#x)).n - (Partial_Sums (FMF#x)).m .|
<= (Partial_Sums abs(FMF#x)).n by Th10,A206,A207,A208;
A215: (Partial_Sums abs(FMF#x)).n = ((Partial_Sums AbsFMF)#x).n by A111,A194
;
0 <= |.(F1.0).x.| by COMPLEX1:46; then
0 + (Partial_Sums abs(FMF#x)).n
<= |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF)#x).n
by A215,XREAL_1:6; then
A216: |. (F1#x).(n+1)-(F1#x).(m+1) .| <= (G.n).x by A212,A213,A214,XXREAL_0:2
;
0 <= |. (F1#x).(n+1)-(F1#x).(m+1) .| by COMPLEX1:46; then
A217: (|. (F1#x).(n+1)-(F1#x).(m+1) qua Complex .|) to_power k <= (Gp#x).n
by A211,A216,HOLDER_1:3;
x in E by A194,XBOOLE_0:def 5; then
A218: ExtGp#x is non-decreasing by A35;
A219: ((ExtGp)#x).n <= ((ExtGp)#x).(n+1) by A218;
ExtGp#x = Gp#x by MESFUN7C:1;
hence (|. (F1#x).(n1)-(F1#x).(m1) qua Complex .|) to_power k
<= (Gp#x).n1
by A206,A207,A219,A217,XXREAL_0:2;
end;
end;
hence thesis;
end;
A220:for x be Element of X, n be Nat st x in E0 holds
|. F.x -(F2#x).n qua Complex .| to_power k <= gp.x
proof
let x be Element of X, n1 be Nat;
assume A221: x in E0; then
A222: Gp#x is convergent by A94;
A223: F1#x = F2#x by A136,A221;
A224: F2#x is convergent by A221,A134;
reconsider n=n1 as Nat;
deffunc AF2F20(Nat) = (F2#x).$1 -(F2#x).n;
consider s0 be Real_Sequence such that
A225: for j be Nat holds s0.j=AF2F20(j) from SEQ_1:sch 1;
A226: now let p be Real;
assume 0<p; then
consider n1 be Nat such that
A227: for m be Nat st n1<=m holds
|.(F2#x).m-lim (F2#x) qua Complex.|<p by A224,SEQ_2:def 7;
take n1;
thus for m be Nat st n1<=m holds
|.s0.m-(lim (F2#x)- (F2#x).n) qua Complex.| < p
proof
let m be Nat;
assume A228: n1<=m;
s0.m-(lim (F2#x)- (F2#x).n)
= (F2#x).m -(F2#x).n-(lim (F2#x)- (F2#x).n) by A225; then
s0.m-(lim (F2#x)- (F2#x).n) = (F2#x).m - lim (F2#x);
hence |.s0.m-(lim (F2#x)- (F2#x).n) qua Complex.|<p by A228,A227;
end;
end; then
A229: s0 is convergent by SEQ_2:def 6; then
lim s0 = lim (F2#x) - (F2#x).n by A226,SEQ_2:def 7; then
A230: lim abs s0 = |.lim (F2#x) - (F2#x).n.| by A229,SEQ_4:14;
A231: abs s0 is convergent by A229;
deffunc AF2F2(Nat)= |. (F2#x).$1-(F2#x).n qua Complex .| to_power k;
consider s be Real_Sequence such that
A232: for j be Nat holds s.j=AF2F2(j) from SEQ_1:sch 1;
A233: for j be Nat st n <= j holds s.j <= (Gp#x).j
proof
let j be Nat;
assume n <= j; then
|. (F2#x).j -(F2#x).n qua Complex .| to_power k <= (Gp#x).j
by A223,A221,A193;
hence thesis by A232;
end;
A234: now let n be Nat;
0 <= |.s0.n.| by COMPLEX1:46;
hence 0 <=(abs(s0)).n by VALUED_1:18;
end;
now let j be Nat;
thus s.j = |. (F2#x).j-(F2#x).n qua Complex .| to_power k by A232
.= |.s0.j qua Complex.| to_power k by A225
.= (abs(s0).j) to_power k by VALUED_1:18;
end; then
A235: s is convergent & lim s = (lim (abs s0)) to_power k
by A234,A231,HOLDER_1:10; then
A236: s^\n is convergent & lim (s^\n)=lim s by SEQ_4:20;
gp.x = lim (Gp#x) by A152,A221; then
A237: (Gp#x)^\n is convergent & lim ((Gp#x)^\n) = gp.x by A222,SEQ_4:20;
for j be Nat holds (s^\n).j <= ((Gp#x)^\n).j
proof
let j be Nat;
(s^\n).j = s.(n+j) & ((Gp#x)^\n).j = (Gp#x).(n+j) by NAT_1:def 3;
hence thesis by A233,NAT_1:11;
end; then
lim s <= gp.x by A236,A237,SEQ_2:18;
hence thesis by A230,A235,A147,A221;
end;
deffunc FX3(Nat) = (|. F -F2.$1 .|) to_power k;
consider FP be Functional_Sequence of X,REAL such that
A238: for n be Nat holds FP.n = FX3(n) from SEQFUNC:sch 1;
A239:for n be Nat holds dom (FP.n) = E0
proof
let n1 be Nat;
reconsider n=n1 as Nat;
A240: dom(F2.n) = E0 by A138;
dom(FP.n1) = dom(abs( F - F2.n ) to_power k) by A238; 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 A240,A146,VALUED_1:12;
hence dom(FP.n1) = E0;
end; then
A241:E0 = dom(FP.0); then
A242:dom (lim FP) = E0 by MESFUNC8:def 9;
for n,m be Nat holds dom(FP.n) = dom(FP.m)
proof
let n,m be Nat;
thus dom (FP.n) =E0 by A239 .=dom (FP.m) by A239;
end; then
reconsider FP as with_the_same_dom Functional_Sequence of X,REAL
by MESFUNC8:def 2;
A243:for n be Nat holds FP.n is E0-measurable
proof
let n1 be Nat;
reconsider n=n1 as Nat;
dom (F2.n) = E0 by A138; then
A244: dom (F - F2.n) = E0 /\ E0 by A146,VALUED_1:12;
F2.n is E0-measurable & dom (F2.n) = E0 by A138; then
F - F2.n is E0-measurable by A190,MESFUNC6:29; then
A245:abs (F - F2.n) is E0-measurable by A244,MESFUNC6:48;
dom (abs (F - F2.n) ) =E0 by A244,VALUED_1:def 11; then
(abs (F - F2.n) to_power k) is E0-measurable by A245,MESFUN6C:29;
hence thesis by A238;
end;
for x be Element of X, n be Nat st x in E0 holds (|. FP.n .|).x <= gp.x
proof
let x be Element of X, n1 be Nat;
reconsider n=n1 as Element of NAT by ORDINAL1:def 12;
assume A246: x in E0; then
A247: x in dom (FP.n) by A239; then
x in dom (( |.F -F2.n .| ) to_power k) by A238; then
x in dom (( |.F -F2.n .| ) ) by MESFUN6C:def 4; then
A248: x in dom (F -F2.n) by VALUED_1:def 11;
A249: FP.n1 = (|. F -F2.n1 .|) to_power k by A238;
A250:0 <= (|.F.x -(F2.n1).x qua Complex .|) 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 A247,A249,MESFUN6C:def 4
.= |. (|. (F -F2.n1).x qua Complex .|) to_power k .| by VALUED_1:18
.= |. (|. F.x -(F2.n1).x qua Complex .|) to_power k .| by A248,VALUED_1:13
.= (|. F.x -(F2.n1).x qua Complex .|) to_power k by A250,ABSVALUE:def 1
.= |. F.x - (F2#x).n qua Complex .| to_power k by SEQFUNC:def 10;
hence thesis by A220,A246;
end; then
consider Ip be Real_Sequence such that
A251: (for n be Nat holds Ip.n = Integral(M,FP.n)) &
( (for x be Element of X st x in E0 holds FP#x is convergent)
implies Ip is convergent & lim Ip = Integral(M,lim FP) )
by A150,A155,A241,A243,MESFUN9C:48;
A252:for x be Element of X st x in E0 holds FP#x is convergent & lim (FP#x) = 0
proof
let x be Element of X;
assume A253: x in E0;
A254: for n be Nat holds
(FP#x).n = ( |.lim (F2#x) - (F2#x).n qua Complex .|) to_power k
proof
let n be Nat;
x in dom (FP.n) by A253,A239; then
A255: x in dom (( |.F -F2.n .| ) to_power k) by A238; then
x in dom ( |.F -F2.n .| ) by MESFUN6C:def 4; then
A256: 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 A238
.= ( (|.F -F2.n .|).x ) to_power k by A255,MESFUN6C:def 4
.= ( |.(F -F2.n).x qua Complex .|) to_power k by VALUED_1:18
.= ( |.(F.x -(F2.n).x) qua Complex .|) to_power k by A256,VALUED_1:13
.= ( |.(lim (F2#x) -(F2.n).x) qua Complex .|) to_power k by A147,A253
.= ( |.(lim (F2#x) -(F2#x).n) qua Complex .|) to_power k
by SEQFUNC:def 10;
end;
F2#x is convergent by A253,A134;
hence thesis by A254,Th11;
end;
A257:for x be Element of X st x in dom (lim FP) holds 0= (lim FP).x
proof
let x be Element of X;
assume A258: x in dom (lim FP); then
A259: lim (FP#x) = 0 & (FP#x) is convergent by A252,A242;
(lim FP).x =lim R_EAL(FP#x) by A258,MESFUN7C:14;
hence thesis by A259,RINFSUP2:14;
end;
a.e-eq-class_Lp(F,M,k) in CosetSet(M,k) by A192; then
reconsider Sq0= a.e-eq-class_Lp(F,M,k) as Point of Lp-Space(M,k)
by Def11;
A260:for n be Nat holds Ip.n = (||.Sq0-Sq.(N.n).||) to_power k
proof
let n be Nat;
set m = N.n;
reconsider n1=n as Nat;
A261: FP.n = abs( F - F2.n1 ) to_power k by A238;
A262: F in Lp_Functions(M,k) & F in Sq0 by A192,Th38;
F2.n1 in Lp_Functions(M,k) & F2.n1 in (Sq.m) by A140; then
(-1)(#)(F2.n1) in (-1)*(Sq.m) by Th54; then
F -(F2.n1) in (Sq0) + (-1)*(Sq.m) by Th54,A262; then
F -(F2.n1) in (Sq0) - (Sq.m) by RLVECT_1:16; then
consider r be Real such that
A263: 0<= r & r = Integral(M,(abs (F -(F2.n1)) ) to_power k) &
||. Sq0 - (Sq.m) .|| =r to_power (1/k) by Th53;
||. Sq0 - (Sq.m) .|| to_power k = r to_power ((1/k)*k) by A263,HOLDER_1:2
.= r to_power 1 by XCMPLX_1:106
.= r by POWER:25;
hence thesis by A263,A261,A251;
end;
deffunc UZ(Nat) = ||.Sq0-Sq.(N.$1).||;
consider Iq be Real_Sequence such that
A264:for n be Nat holds Iq.n = UZ(n) from SEQ_1:sch 1;
A265: for n being Nat holds Iq.n = ||.Sq0-Sq.(N.n).|| by A264;
Iq is convergent & lim Iq = 0
proof
A266: for n holds Ip.n >= 0
proof
let n;
||. Sq0-Sq.(N.n) .|| to_power k >= 0 by Th4;
hence Ip.n >= 0 by A260;
end;
A267: for n be Nat holds Iq.n = (Ip.n) to_power (1/k)
proof
let n be Nat;
thus (Ip.n) to_power (1/k)
= ( ||.Sq0-Sq.(N.n).|| to_power k) to_power (1/k) by A260
.= ||.Sq0-Sq.(N.n).|| to_power (k*(1/k)) by HOLDER_1:2
.= (||.Sq0-Sq.(N.n).||) to_power 1 by XCMPLX_1:106
.= ||.Sq0-Sq.(N.n).|| by POWER:25
.= Iq.n by A265;
end;
hence Iq is convergent by A266,A252,A251,HOLDER_1:10;
lim Iq = (lim Ip) to_power (1/k) by A252,A251,A266,A267,HOLDER_1:10; then
lim Iq = 0 to_power (1/k) by A252,A251,A257,A242,LPSPACE1:22;
hence lim Iq = 0 by POWER:def 2;
end;
hence thesis by A2,A265,Lm7;
end;
registration let X,S,M;
let k be geq_than_1 Real;
cluster Lp-Space (M,k) -> complete;
coherence
proof
for Sq be sequence of Lp-Space(M,k) st Sq is Cauchy_sequence_by_Norm holds
Sq is convergent by Th70;
hence thesis by LOPBAN_1:def 15;
end;
end;
begin :: Relations between L1 Space and Lp Space
Lm8:
f in L1_Functions M implies f is_integrable_on M &
(ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable)
proof
assume f in L1_Functions M; then
ex f2 be PartFunc of X,REAL st f = f2 &
ex E be Element of S st M.E=0 & dom f2 = E` & f2 is_integrable_on M; then
consider D be Element of S such that
A1: M.D = 0 & dom f = D` & f is_integrable_on M;
thus f is_integrable_on M by A1;
reconsider E=D` as Element of S by MEASURE1:34;
take E;
thus M.E` = 0 & dom f = E by A1;
R_EAL f is_integrable_on M by A1; then
ex B be Element of S st
B = dom (R_EAL f) & (R_EAL f) is B-measurable;
hence f is E-measurable by A1;
end;
Lm9:
f in Lp_Functions(M,k) implies (abs f) to_power k is_integrable_on M
proof
assume f in Lp_Functions(M,k); then
ex f2 be PartFunc of X,REAL st f = f2 &
ex E be Element of S st M.E` = 0 & dom f2 = E &
f2 is E-measurable & (abs f2) to_power k is_integrable_on M;
hence thesis;
end;
Lm10:
(ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable) implies
a.e-eq-class_Lp(f,M,1) c= a.e-eq-class(f,M)
proof
assume A1: ex E be Element of S st
M.E`=0 & E = dom f & f is E-measurable;
let x be object;
assume x in a.e-eq-class_Lp(f,M,1); then
consider h be PartFunc of X,REAL such that
A2: x = h & h in Lp_Functions(M,1) & f a.e.= h,M;
A3: ex g be PartFunc of X,REAL st h = g &
(ex E be Element of S st M.E`=0 & dom g = E &
g is E-measurable & (abs g) to_power 1 is_integrable_on M)
by A2; then
consider Eh be Element of S such that
A4: M.(Eh`) = 0 & dom h = Eh &
h is Eh-measurable & (abs h) to_power 1 is_integrable_on M;
A5: dom((abs h) to_power 1) = dom(abs h) by MESFUN6C:def 4;
for x be Element of X st x in dom((abs h) to_power 1) holds
((abs h) to_power 1).x = (abs h).x
proof
let x be Element of X;
assume x in dom((abs h) to_power 1); then
((abs h) to_power 1).x = ((abs h).x) to_power 1 by MESFUN6C:def 4;
hence thesis by POWER:25;
end; then
(abs h) to_power 1 = abs h by A5,PARTFUN1:5; then
A6: h is_integrable_on M by A3,MESFUNC6:94;
reconsider ND = Eh` as Element of S by MEASURE1:34;
M.ND = 0 & dom h = ND` by A4; then
A7: h in L1_Functions M by A6;
ex E be Element of S st M.E = 0 & dom f = E` & f is_integrable_on M
proof
consider Ef be Element of S such that
A8: M.(Ef`)=0 & Ef = dom f & f is Ef-measurable by A1;
reconsider E = Ef` as Element of S by MEASURE1:34;
take E;
consider EE be Element of S such that
A9: M.EE = 0 & f|EE` = h|EE` by A2;
reconsider E1 = ND \/ EE as Element of S;
ND is measure_zero of M & EE is measure_zero of M
by A4,A9,MEASURE1:def 7; then
E1 is measure_zero of M by MEASURE1:37; then
A10: M.E1 = 0 by MEASURE1:def 7;
EE c= E1 by XBOOLE_1:7; then
E1` c= EE` by SUBSET_1:12; then
A11: f|E1` = (f|EE`)|E1` & h|E1` = (h|EE`)|E1` by FUNCT_1:51;
A12: dom max+(R_EAL f) = Ef & dom max-(R_EAL f) = Ef
by A8,MESFUNC2:def 2,def 3;
A13: Ef = dom(R_EAL f) & (R_EAL f) is Ef-measurable
by A8; then
A14: max+(R_EAL f) is Ef-measurable &
max-(R_EAL f) is Ef-measurable by MESFUNC2:25,26;
(for x being Element of X holds 0. <= (max+(R_EAL f)).x) &
(for x being Element of X holds 0. <= (max-(R_EAL f)).x)
by MESFUNC2:12,13; then
A15: max+(R_EAL f) is nonnegative & max-(R_EAL f) is nonnegative
by SUPINF_2:39;
A16: Ef = (Ef /\ E1) \/ (Ef \ E1) by XBOOLE_1:51;
reconsider E0 = Ef /\ E1 as Element of S;
A17: Ef \ E1 = Ef /\ E1` by SUBSET_1:13;
reconsider E2 = Ef \ E1 as Element of S;
max+(R_EAL f) = (max+(R_EAL f))|(dom(max+(R_EAL f))) &
max-(R_EAL f) = (max-(R_EAL f))|(dom(max-(R_EAL f))) by RELAT_1:69; then
A18: integral+(M,max+(R_EAL f))
= integral+(M,(max+(R_EAL f))|E0) + integral+(M,(max+(R_EAL f))|E2) &
integral+(M,max-(R_EAL f))
= integral+(M,(max-(R_EAL f))|E0) + integral+(M,(max-(R_EAL f))|E2)
by A12,A15,A16,A14,MESFUNC5:81,XBOOLE_1:89;
A19: integral+(M,(max+(R_EAL f))|E0) >= 0 &
integral+(M,(max-(R_EAL f))|E0) >= 0 by A15,A14,A12,MESFUNC5:80;
integral+(M,(max+(R_EAL f))|E1) = 0 &
integral+(M,(max-(R_EAL f))|E1) = 0 by A10,A12,A15,A14,MESFUNC5:82; then
integral+(M,(max+(R_EAL f))|E0) = 0 & integral+(M,(max-(R_EAL f))|E0) = 0
by A19,A12,A15,A14,MESFUNC5:83,XBOOLE_1:17; then
A20: integral+(M,max+(R_EAL f)) = integral+(M,(max+(R_EAL f))|E2) &
integral+(M,max-(R_EAL f)) = integral+(M,(max-(R_EAL f))|E2)
by A18,XXREAL_3:4;
A21: E2 c= E1` by A17,XBOOLE_1:17; then
f|E2 = (h|E1`)|E2 by A9,A11,FUNCT_1:51; then
A22: (R_EAL f)|E2 = (R_EAL h)|E2 by A21,FUNCT_1:51;
A23: max+(R_EAL f)|E2 = max+((R_EAL f)|E2) &
max+(R_EAL h)|E2 = max+((R_EAL h)|E2) &
max-(R_EAL f)|E2 = max-((R_EAL f)|E2) &
max-(R_EAL h)|E2 = max-((R_EAL h)|E2) by MESFUNC5:28;
A24: R_EAL h is_integrable_on M by A6; then
A25: integral+(M,max+(R_EAL h)) < +infty &
integral+(M,max-(R_EAL h)) < +infty;
integral+(M,max+((R_EAL h)|E2)) <= integral+(M,max+(R_EAL h)) &
integral+(M,max-((R_EAL h)|E2)) <= integral+(M,max-(R_EAL h))
by A24,MESFUNC5:97; then
integral+(M,max+(R_EAL f)) < +infty &
integral+(M,max-(R_EAL f)) < +infty by A20,A25,A23,A22,XXREAL_0:2; then
(R_EAL f) is_integrable_on M by A13;
hence thesis by A8;
end; then
f in L1_Functions M;
hence x in a.e-eq-class(f,M) by A2,A7;
end;
Lm11:
a.e-eq-class(f,M) c= a.e-eq-class_Lp(f,M,1)
proof
let x be object;
assume x in a.e-eq-class(f,M); then
consider g be PartFunc of X,REAL such that
A1: x = g & g in L1_Functions M & f in L1_Functions M & f a.e.= g,M;
A2: ex h be PartFunc of X,REAL st g = h &
ex D be Element of S st M.D=0 & dom h = D` & h is_integrable_on M
by A1; then
R_EAL g is_integrable_on M; then
consider A be Element of S such that
A3: A = dom(R_EAL g) & R_EAL g is A-measurable;
A4: A = dom g & g is A-measurable by A3;
A5: M.A` = 0 by A2,A3;
(abs g) to_power 1 = abs g by Th8; then
(abs g) to_power 1 is_integrable_on M by A2,A4,MESFUNC6:94; then
g in {p where p is PartFunc of X,REAL :
ex Ep be Element of S st M.(Ep`)=0 & dom p = Ep &
p is Ep-measurable & (abs p) to_power 1 is_integrable_on M}
by A4,A5;
hence x in a.e-eq-class_Lp(f,M,1) by A1;
end;
Lm12:
(ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable) implies
a.e-eq-class_Lp(f,M,1) = a.e-eq-class(f,M)
by Lm10,Lm11;
theorem Th71:
for X be non empty set, S be SigmaField of X,
M be sigma_Measure of S holds CosetSet M = CosetSet(M,1)
proof
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
now let x be object;
assume x in CosetSet M; then
consider g be PartFunc of X,REAL such that
A1: x = a.e-eq-class(g,M) & g in L1_Functions M;
A2: g is_integrable_on M &
ex E be Element of S st M.E`=0 & E = dom g & g is E-measurable
by A1,Lm8; then
A3: x = a.e-eq-class_Lp(g,M,1) by A1,Lm12;
(abs g) to_power 1 = abs g by Th8; then
(abs g) to_power 1 is_integrable_on M by A2,MESFUNC6:94; then
g in Lp_Functions(M,1) by A2;
hence x in CosetSet(M,1) by A3;
end; then
A4:CosetSet M c= CosetSet(M,1);
now let x be object;
assume x in CosetSet(M,1); then
consider g be PartFunc of X,REAL such that
A5: x = a.e-eq-class_Lp(g,M,1) & g in Lp_Functions(M,1);
consider E be Element of S such that
A6: M.E` = 0 & dom g = E & g is E-measurable by A5,Th35;
A7: x = a.e-eq-class(g,M) by A5,A6,Lm12;
reconsider D = E` as Element of S by MEASURE1:34;
A8: M.D = 0 & dom g = D` by A6;
(abs g) to_power 1 is_integrable_on M by A5,Lm9; then
abs g is_integrable_on M by Th8; then
g is_integrable_on M by A6,MESFUNC6:94; then
g in L1_Functions M by A8;
hence x in CosetSet M by A7;
end; then
CosetSet(M,1) c= CosetSet M;
hence thesis by A4;
end;
theorem Th72:
for X be non empty set, S be SigmaField of X,
M be sigma_Measure of S holds addCoset M = addCoset(M,1)
proof
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
A1:CosetSet M = CosetSet(M,1) by Th71;
now let A,B be Element of CosetSet M;
A in {a.e-eq-class(f,M) where f is PartFunc of X,REAL
: f in L1_Functions M}; then
consider a be PartFunc of X,REAL such that
A2: A = a.e-eq-class(a,M) & a in L1_Functions M;
B in {a.e-eq-class(f,M) where f is PartFunc of X,REAL
: f in L1_Functions M}; then
consider b be PartFunc of X,REAL such that
A3: B = a.e-eq-class(b,M) & b in L1_Functions M;
A4: A is Element of CosetSet(M,1) & B is Element of CosetSet(M,1) by Th71;
A5: a in a.e-eq-class(a,M) & b in a.e-eq-class(b,M) by A2,A3,LPSPACE1:38; then
A6: (addCoset M).(A,B) = a.e-eq-class(a+b,M) by A2,A3,LPSPACE1:def 15;
a+b in L1_Functions M by A2,A3,LPSPACE1:23; then
ex E be Element of S st M.E`=0 & E = dom(a+b) & (a+b) is E-measurable
by Lm8; then
(addCoset M).(A,B) = a.e-eq-class_Lp(a+b,M,1) by A6,Lm12;
hence (addCoset M).(A,B) = (addCoset(M,1)).(A,B) by A4,A5,A2,A3,Def8;
end;
hence addCoset M = addCoset(M,1) by A1,BINOP_1:2;
end;
theorem Th73:
for X be non empty set, S be SigmaField of X,
M be sigma_Measure of S holds zeroCoset M = zeroCoset(M,1)
proof
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
reconsider z = zeroCoset(M,1) as Element of CosetSet M by Th71;
X-->0 in Lp_Functions(M,1) by Th23; then
ex E be Element of S st
M.E`=0 & dom (X-->0) = E & (X-->0) is E-measurable by Th35; then
A1:z = a.e-eq-class(X-->0,M) by Lm12;
X-->0 in L1_Functions M by Th56;
hence thesis by A1,LPSPACE1:def 16;
end;
theorem Th74:
for X be non empty set, S be SigmaField of X,
M be sigma_Measure of S holds lmultCoset M = lmultCoset(M,1)
proof
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
A1:CosetSet M = CosetSet(M,1) by Th71;
now let z be Element of REAL, A be Element of CosetSet M;
A in {a.e-eq-class(f,M) where f is PartFunc of X,REAL
: f in L1_Functions M}; then
consider a be PartFunc of X,REAL such that
A2: A = a.e-eq-class(a,M) & a in L1_Functions M;
A3: A is Element of CosetSet(M,1) by Th71;
A4: a in A by A2,LPSPACE1:38; then
A5: (lmultCoset M).(z,A) = a.e-eq-class(z(#)a,M) by LPSPACE1:def 17;
z(#)a in L1_Functions M by A2,LPSPACE1:24; then
ex E be Element of S st M.E`=0 & E = dom(z(#)a)
& (z(#)a) is E-measurable by Lm8; then
(lmultCoset M).(z,A) = a.e-eq-class_Lp(z(#)a,M,1) by A5,Lm12;
hence (lmultCoset M).(z,A) = (lmultCoset(M,1)).(z,A) by A3,A4,Def10;
end;
hence lmultCoset M = lmultCoset(M,1) by A1,BINOP_1:2;
end;
theorem Th75:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds
Pre-L-Space M = Pre-Lp-Space(M,1)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
A1:the carrier of Pre-L-Space M = CosetSet M &
the addF of Pre-L-Space M = addCoset M &
0.(Pre-L-Space M) = zeroCoset M &
the Mult of Pre-L-Space M = lmultCoset M by LPSPACE1:def 18;
CosetSet M = CosetSet(M,1) & addCoset M = addCoset(M,1) &
zeroCoset M = zeroCoset(M,1) & lmultCoset M = lmultCoset(M,1)
by Th71,Th72,Th73,Th74;
hence thesis by A1,Def11;
end;
theorem Th76:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds
L-1-Norm M = Lp-Norm(M,1)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
A1:the carrier of Pre-L-Space M = the carrier of Pre-Lp-Space(M,1) by Th75;
now let x be Element of the carrier of Pre-L-Space M;
x in the carrier of Pre-L-Space M; then
x in CosetSet M by LPSPACE1:def 18;
then consider g be PartFunc of X,REAL such that
A2: x = a.e-eq-class(g,M) & g in L1_Functions M;
consider a be PartFunc of X,REAL such that
A3: a in x & (L-1-Norm M).x = Integral(M,|.a.|) by LPSPACE1:def 19;
A4: ex p be PartFunc of X,REAL st
a = p & p in L1_Functions M & g in L1_Functions M & g a.e.= p,M
by A2,A3;
consider b be PartFunc of X,REAL such that
A5: b in x & ex r be Real st r = Integral(M,(|.b.|) to_power 1) &
(Lp-Norm(M,1)).x = r to_power (1/1) by A1,Def12;
A6: ex q be PartFunc of X,REAL st b = q & q in L1_Functions M
& g in L1_Functions M & g a.e.= q,M by A2,A5;
a a.e.= g,M by A4; then
a a.e.= b,M by A6,LPSPACE1:30; then
A7: Integral(M,|.a.|) = Integral(M,|.b.|) by A2,A3,A5,LPSPACE1:45;
(|.b.|) to_power 1 = |.b.| by Th8;
hence (L-1-Norm M).x = (Lp-Norm(M,1)).x by A3,A5,A7,POWER:25;
end;
hence thesis by A1,FUNCT_2:63;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds
L-1-Space M = Lp-Space(M,1)
proof
let X be non empty set,
S be SigmaField of X,
M be sigma_Measure of S;
Pre-L-Space M = Pre-Lp-Space(M,1) by Th75;
hence thesis by Th76;
end;