:: 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-2021 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
= N.i holds ||. Sq.j - Sq.(N.i) .|| < 2 to_power (-i) proof let X be RealNormSpace, Sq be sequence of X; assume A1: Sq is Cauchy_sequence_by_Norm; 1 =2 to_power (-0) by POWER:24; then consider N0 be Nat such that A2: for j,i be Nat st j >= N0 & i >= N0 holds ||. Sq.j - Sq.i .|| < 2 to_power (-0) by A1,RSSPACE3:8; reconsider N0 as Element of NAT by ORDINAL1:def 12; defpred P[set,set,set] means ex n,x,y be Nat st n=$1 & x=$2 & y=$3 & ( ( for j be Nat st j >= x holds ||.Sq.j -Sq.x.|| < 2 to_power (-n) ) implies x < y & ( for j be Nat st j >= y holds ||.Sq.j -Sq.y.|| < 2 to_power (-(n+1)) ) ); A3:for n being Nat,x being Element of NAT ex y being Element of NAT st P[n,x,y] proof let n be Nat, x be Element of NAT; now assume for j be Nat st j >= x holds ||.Sq.j -Sq.x.|| < 2 to_power (-n); 0 < 2 to_power (-(n+1)) by POWER:34; then consider N2 be Nat such that A4: for j,i be Nat st j >= N2 & i >= N2 holds ||.Sq.j -Sq.i.|| < 2 to_power (-(n+1)) by A1,RSSPACE3:8; set y= max(x,N2)+1; take y; x <= max(x,N2) by XXREAL_0:25; hence x < y by NAT_1:13; N2 <= max(x,N2) by XXREAL_0:25; then A5: N2 < y by NAT_1:13; thus for j be Nat st j >= y holds ||.Sq.j -Sq.y.|| < 2 to_power (-(n+1)) proof let j be Nat; assume j >= y; then j >= N2 & y >=N2 by A5,XXREAL_0:2; hence thesis by A4; end; end; hence thesis; end; consider f being sequence of NAT such that A6: f.0 = N0 & for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A3); defpred Q[Nat] means for j be Nat st j >= f.$1 holds ||. Sq.j - Sq.(f.$1) .|| < 2 to_power (-$1); A7:Q[ 0] by A2,A6; A8:now let i be Nat; assume A9: Q[i]; ex n,x,y be Nat st n=i & x=f.i & y=f.(i+1) & ( (for j be Nat st j >= x holds ||.Sq.j -Sq.x.|| < 2 to_power (-n)) implies x < y & (for j be Nat st j >= y holds ||.Sq.j -Sq.y.|| < 2 to_power (-(n+1)) ) ) by A6; hence Q[i+1] by A9; end; A10:for i be Nat holds Q[i] from NAT_1:sch 2(A7,A8); now let i be Nat; ex n,x,y be Nat st n=i & x=f.i & y=f.(i+1) & ( (for j be Nat st j >= x holds ||.Sq.j -Sq.x.|| < 2 to_power (-n)) implies x < y & (for j be Nat st j >= y holds ||.Sq.j -Sq.y.|| < 2 to_power (-(n+1))) ) by A6; hence f.i < f.(i+1) by A10; end; then f is increasing; hence thesis by A10; end; theorem Th66: for F be Functional_Sequence of X,REAL st (for m be Nat holds F.m in Lp_Functions(M,k)) holds for m be Nat holds (Partial_Sums F).m in Lp_Functions(M,k) proof let F be Functional_Sequence of X,REAL; assume A1: for m be Nat holds F.m in Lp_Functions(M,k); defpred P[Nat] means (Partial_Sums F).$1 in Lp_Functions(M,k); (Partial_Sums F).0 = F.0 by MESFUN9C:def 2; then A2:P[ 0] by A1; A3:now let j be Nat; assume P[j]; then A4:(Partial_Sums F).j in Lp_Functions(M,k) & F.(j+1) in Lp_Functions(M,k) by A1; (Partial_Sums F).(j+1) = (Partial_Sums F).j + F.(j+1) by MESFUN9C:def 2; hence P[j+1] by A4,Th25; end; for j being Nat holds P[j] from NAT_1:sch 2(A2,A3); hence thesis; end; theorem Th67: for F be Functional_Sequence of X,REAL st (for m be Nat holds F.m is nonnegative) holds for m be Nat holds (Partial_Sums F).m is nonnegative proof let F be Functional_Sequence of X,REAL; assume A1: for m be Nat holds F.m is nonnegative; defpred P[Nat] means (Partial_Sums F).$1 is nonnegative; (Partial_Sums F).0 = F.0 by MESFUN9C:def 2; then A2:P[ 0] by A1; A3:now let k be Nat; assume P[k]; then A4:(Partial_Sums F).k is nonnegative & F.(k+1) is nonnegative by A1; (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by MESFUN9C:def 2; hence P[k+1] by A4,MESFUNC6:56; end; for k being Nat holds P[k] from NAT_1:sch 2(A2,A3); hence thesis; end; theorem Th68: for F be Functional_Sequence of X,REAL, x be Element of X, n,m be Nat st F is with_the_same_dom & x in dom(F.0) & (for k be Nat holds F.k is nonnegative) & n <= m holds ((Partial_Sums F).n).x <= ((Partial_Sums F).m).x proof let F be Functional_Sequence of X,REAL, x be Element of X, n,m be Nat; assume A1: F is with_the_same_dom; assume A2: x in dom(F.0); assume A3: for m be Nat holds F.m is nonnegative; assume A4: n <= m; set PF = Partial_Sums F; defpred P[Nat] means (PF.n).x <= (PF.$1).x; A5:for k be Nat holds (PF.k).x <= (PF.(k+1)).x proof let k be Nat; A6:PF.(k+1) = PF.k + F.(k+1) by MESFUN9C:def 2; A7:dom(PF.(k+1)) = dom(F.0) by A1,MESFUN9C:11; F.(k+1) is nonnegative & PF.k is nonnegative by A3,Th67; then 0 <= (F.(k+1)).x & 0 <= (PF.k).x by MESFUNC6:51; then (PF.k).x + 0 <= (PF.k).x + (F.(k+1)).x by XREAL_1:7; hence thesis by A7,A2,A6,VALUED_1:def 1; end; A8:for k be Nat st k >= n & (for l be Nat st l >= n & l < k holds P[l]) holds P[k] proof let k be Nat; assume A9: k >= n & for l be Nat st l >= n & l < k holds P[l]; now assume k > n; then k >= n + 1 by NAT_1:13; then A10: k = n+1 or k > n+1 by XXREAL_0:1; now assume A11: k > n+1; then reconsider l = k-1 as Nat by NAT_1:20; k < k+1 by NAT_1:13; then k > l & l >= n by A11,XREAL_1:19; then A12: (PF.n).x <= (PF.l).x by A9; k = l+1; then (PF.l).x <= (PF.k).x by A5; hence thesis by A12,XXREAL_0:2; end; hence thesis by A10,A5; end; hence thesis by A9,XXREAL_0:1; end; for k being Nat st k >= n holds P[k] from NAT_1:sch 9(A8); hence thesis by A4; end; theorem Th69: for F be Functional_Sequence of X,REAL st F is with_the_same_dom holds (abs F) is with_the_same_dom proof let F be Functional_Sequence of X,REAL; assume A1: F is with_the_same_dom; for n,m be Nat holds dom((abs F).n) = dom((abs F).m) proof let n,m be Nat; (abs F).n = abs(F.n) & (abs F).m = abs(F.m) by SEQFUNC:def 4; then dom((abs F).n) = dom(F.n) & dom((abs F).m) = dom(F.m) by VALUED_1:def 11; hence dom((abs F).n) = dom((abs F).m) by A1,MESFUNC8:def 2; end; hence abs F is with_the_same_dom by MESFUNC8:def 2; end; theorem Th70: for k be geq_than_1 Real, Sq be sequence of Lp-Space(M,k) st Sq is Cauchy_sequence_by_Norm holds Sq is convergent proof let k be geq_than_1 Real; let Sq be sequence of Lp-Space(M,k); A1:1 <= k by Def1; assume A2: Sq is Cauchy_sequence_by_Norm; consider Fsq be with_the_same_dom Functional_Sequence of X,REAL such that A3: for n be Nat holds Fsq.n in Lp_Functions(M,k) & Fsq.n in Sq.n & Sq.n= a.e-eq-class_Lp(Fsq.n,M,k) & ex r be Real st 0<=r & r = Integral(M,(abs (Fsq.n)) to_power k) & ||. Sq.n .|| =r to_power (1/k) by Th63; Fsq.0 in Lp_Functions(M,k) by A3; then A4: ex D be Element of S st M.D` =0 & dom(Fsq.0) = D & (Fsq.0) is D-measurable by Th35; then reconsider E = dom(Fsq.0) as Element of S; consider N be increasing sequence of NAT such that A5: for i,j be Nat st j >= N.i holds ||. Sq.j - Sq.(N.i) .|| < 2 to_power (-i) by Th65,A2; deffunc FsqN(Nat) = Fsq.(N.$1); consider F1 be Functional_Sequence of X,REAL such that A6: for n be Nat holds F1.n = FsqN(n) from SEQFUNC:sch 1; A7: for n be Nat holds dom(F1.n) = E & F1.n in Lp_Functions(M,k) & F1.n is E-measurable & abs(F1.n) in Lp_Functions(M,k) proof let n be Nat; A8: F1.n = Fsq.(N.n) by A6; hence A9: dom(F1.n) = E & F1.n in Lp_Functions(M,k) by A3,MESFUNC8:def 2; then consider F be PartFunc of X,REAL such that Z1: F1.n = F & ex ND be Element of S st M.ND` =0 & dom F = ND & F is ND-measurable & (abs F) to_power k is_integrable_on M; consider ND be Element of S such that Z2: M.ND` =0 & dom F = ND & F is ND-measurable & (abs F) to_power k is_integrable_on M by Z1; ND = E by Z1,Z2,A8,MESFUNC8:def 2; hence F1.n is E-measurable by Z1,Z2; thus abs(F1.n) in Lp_Functions(M,k) by A9,Th28; end; for n,m be Nat holds dom (F1.n) = dom (F1.m) proof let n,m be Nat; dom(F1.n) = E & dom(F1.m) = E by A7; hence thesis; end; then reconsider F1 as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2; deffunc FF(Nat) = F1.($1+1) - F1.$1; consider FMF be Functional_Sequence of X,REAL such that A10: for n be Nat holds FMF.n = FF(n) from SEQFUNC:sch 1; A11: for n be Nat holds dom(FMF.n) = E & FMF.n in Lp_Functions(M,k) proof let n be Nat; A12: dom(F1.n) = E & dom(F1.(n+1)) = E by A7; FMF.n = F1.(n+1) - F1.n by A10; then dom(FMF.n) = dom (F1.(n+1)) /\ dom (F1.n) by VALUED_1:12; hence dom(FMF.n) = E by A12; Fsq.(N.(n+1)) in Lp_Functions(M,k) & Fsq.(N.n) in Lp_Functions(M,k) by A3; then F1.(n+1) in Lp_Functions(M,k) & F1.n in Lp_Functions(M,k) by A6; then F1.(n+1) - F1.n in Lp_Functions(M,k) by Th27; hence FMF.n in Lp_Functions(M,k) by A10; end; for n,m be Nat holds dom(FMF.n) = dom(FMF.m) proof let n,m be Nat; dom(FMF.n) = E & dom(FMF.m) = E by A11; hence thesis; end; then reconsider FMF as with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2; set AbsFMF = abs FMF; A13: for n be Nat holds AbsFMF.n is nonnegative & dom(AbsFMF.n) = E & abs(AbsFMF.n) = AbsFMF.n & AbsFMF.n in Lp_Functions(M,k) & AbsFMF.n is E-measurable proof let n be Nat; A14: AbsFMF.n = abs (FMF.n) by SEQFUNC:def 4; hence AbsFMF.n is nonnegative; A15: dom(FMF.n) = E & FMF.n in Lp_Functions(M,k) by A11; hence dom(AbsFMF.n) = E & abs(AbsFMF.n) = AbsFMF.n by A14,VALUED_1:def 11; thus AbsFMF.n in Lp_Functions(M,k) by A11,A14,Th28; then consider D be Element of S such that Z1: M.D` = 0 & dom(AbsFMF.n) = D & AbsFMF.n is D-measurable by Th35; D = E by Z1,A15,A14,VALUED_1:def 11; hence AbsFMF.n is E-measurable by Z1; end; reconsider AbsFMF as with_the_same_dom Functional_Sequence of X,REAL by Th69; deffunc Gk(Nat) =abs(F1.0) + (Partial_Sums AbsFMF).$1; consider G be Functional_Sequence of X,REAL such that A16: for n be Nat holds G.n = Gk(n) from SEQFUNC:sch 1; A17:for n be Nat holds dom(G.n) = E & G.n in Lp_Functions(M,k) & G.n is nonnegative & G.n is E-measurable & abs(G.n) = G.n proof let n be Nat; A18: G.n = abs(F1.0) + (Partial_Sums AbsFMF).n by A16; then A19: dom(G.n) = dom(abs(F1.0)) /\ dom((Partial_Sums AbsFMF).n) by VALUED_1:def 1 .= dom(F1.0) /\ dom((Partial_Sums AbsFMF).n) by VALUED_1:def 11 .= dom(F1.0) /\ dom(AbsFMF.0) by MESFUN9C:11; A20: (Partial_Sums AbsFMF).n in Lp_Functions(M,k) & (Partial_Sums AbsFMF).n is nonnegative & (Partial_Sums AbsFMF).n is E-measurable by A13,Th66,Th67,MESFUN9C:16; A21: dom(AbsFMF.0) = E by A13; A22: F1.0 in Lp_Functions(M,k) & dom(F1.0) = E & F1.0 is E-measurable by A7; then abs(F1.0) in Lp_Functions(M,k) & abs(F1.0) is nonnegative & abs(F1.0) is E-measurable by Th28,MESFUNC6:48; hence thesis by A19,A22,A21,A18,A20,Th14,Th25,MESFUNC6:26,56; end; deffunc Gpk(Nat) =(G.$1) to_power k; consider Gp be Functional_Sequence of X,REAL such that A23: for n be Nat holds Gp.n = Gpk(n) from SEQFUNC:sch 1; A24:for n be Nat holds ((G.n) to_power k) is nonnegative & ((G.n) to_power k) is E-measurable proof let n be Nat; A25: G.n is nonnegative by A17; hence ((G.n) to_power k) is nonnegative; G.n is E-measurable & dom(G.n) = E by A17; hence ((G.n) to_power k) is E-measurable by A25,MESFUN6C:29; end; reconsider ExtGp = R_EAL Gp as Functional_Sequence of X,ExtREAL; A26:for n be Nat holds dom(ExtGp.n) = E & ExtGp.n is E-measurable & ExtGp.n is nonnegative proof let n be Nat; ExtGp.n = R_EAL((G.n) to_power k) by A23; then dom(ExtGp.n) = dom (G.n) by MESFUN6C:def 4; hence dom(ExtGp.n) = E by A17; ((G.n) to_power k) is E-measurable by A24; then R_EAL((G.n) to_power k) is E-measurable; hence ExtGp.n is E-measurable by A23; ((G.n) to_power k) is nonnegative by A24; hence ExtGp.n is nonnegative by A23; end; then A27:dom(ExtGp.0) = E & ExtGp.0 is nonnegative; for n,m be Nat holds dom (ExtGp.n) = dom (ExtGp.m) proof let n,m be Nat; dom (ExtGp.n) = E & dom(ExtGp.m) = E by A26; hence thesis; end; then reconsider ExtGp as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2; A28:for n,m be Nat st n <=m holds for x be Element of X st x in E holds (ExtGp.n).x <= (ExtGp.m).x proof let n,m be Nat; assume A29:n <=m; let x be Element of X; assume A30:x in E; then A31: x in dom (G.n) & x in dom (G.m) by A17; then x in dom((G.n) to_power k) & x in dom((G.m) to_power k) by MESFUN6C:def 4; then ((G.n).x) to_power k = ((G.n) to_power k).x & ((G.m).x) to_power k = ((G.m) to_power k).x by MESFUN6C:def 4; then A32: ((G.n).x) to_power k = (ExtGp.n).x & ((G.m).x) to_power k = (ExtGp.m).x by A23; dom(AbsFMF.0) = E by A13; then ((Partial_Sums AbsFMF).n).x <= ((Partial_Sums AbsFMF).m).x by Th68,A29,A30,A13; then A33: (abs(F1.0)).x + ((Partial_Sums AbsFMF).n).x <= (abs(F1.0)).x + ((Partial_Sums AbsFMF).m).x by XREAL_1:6; G.m= abs(F1.0) + (Partial_Sums AbsFMF).m & G.n= abs(F1.0) + (Partial_Sums AbsFMF).n by A16; then A34: (G.m).x= (abs(F1.0)).x + ((Partial_Sums AbsFMF).m).x & (G.n).x= (abs(F1.0)).x + ((Partial_Sums AbsFMF).n).x by A31,VALUED_1:def 1 ; G.n is nonnegative by A17; then 0 <= (G.n).x by MESFUNC6:51; hence thesis by A32,A33,A34,HOLDER_1:3; end; A35:for x be Element of X st x in E holds ExtGp#x is non-decreasing proof let x be Element of X; assume A36: x in E; for n,m be Nat st m<=n holds ((ExtGp)#x).m <= ((ExtGp)#x).n proof let n,m be Nat; assume m <= n; then ((ExtGp).m).x <= ((ExtGp).n).x by A28,A36; then ((ExtGp)#x).m <= ((ExtGp).n).x by MESFUNC5:def 13; hence thesis by MESFUNC5:def 13; end; hence ExtGp#x is non-decreasing by RINFSUP2:7; end; A37:for x be Element of X st x in E holds ExtGp#x is convergent proof let x be Element of X; assume x in E; then ExtGp#x is non-decreasing by A35; hence thesis by RINFSUP2:37; end; then consider I be ExtREAL_sequence such that A38: (for n be Nat holds I.n = Integral(M,ExtGp.n)) & I is convergent & Integral(M,lim ExtGp) = lim I by A27,A26,A28,MESFUNC9:52; now let y be object; assume y in rng I; then consider x be Element of NAT such that A39: y = I.x by FUNCT_2:113; A40: y = Integral(M,Gp.x) by A39,A38; G.x = abs(G.x) by A17; then A41: Gp.x = abs(G.x) to_power k by A23; G.x in Lp_Functions(M,k) by A17; hence y in REAL by A40,A41,Th49; end; then rng I c= REAL; then reconsider Ir = I as sequence of REAL by FUNCT_2:6; deffunc KAbsFMF(Nat) = Integral(M,(AbsFMF.$1) to_power k); A42:for x being Element of NAT holds KAbsFMF(x) is Element of REAL proof let x being Element of NAT; (AbsFMF.x) in Lp_Functions(M,k) by A13; then Integral(M,(abs(AbsFMF.x)) to_power k) in REAL by Th49; hence thesis by A13; end; consider KPAbsFMF being sequence of REAL such that A43: for x be Element of NAT holds KPAbsFMF.x = KAbsFMF(x) from FUNCT_2:sch 9(A42); deffunc KKAbsFMF(Nat) = (KPAbsFMF.$1) to_power (1/k); A44:for x being Element of NAT holds KKAbsFMF(x) is Element of REAL by XREAL_0:def 1; consider PAbsFMF being sequence of REAL such that A45: for x be Element of NAT holds PAbsFMF.x = KKAbsFMF(x) from FUNCT_2:sch 9(A44); F1.0 in Lp_Functions(M,k) by A7; then reconsider RF0=Integral(M,(abs(F1.0)) to_power k) as Element of REAL by Th49; deffunc LAbsFMF(Nat) = RF0 to_power (1/k) + (Partial_Sums PAbsFMF).$1; A46:for x being Element of NAT holds LAbsFMF(x) is Element of REAL by XREAL_0:def 1; consider QAbsFMF being sequence of REAL such that A47: for x being Element of NAT holds QAbsFMF.x = LAbsFMF(x) from FUNCT_2:sch 9(A46); A48:for n being Nat holds (Ir.n) to_power (1/k) <= QAbsFMF.n proof defpred PN[Nat] means (Ir.$1) to_power (1/k) <= QAbsFMF.$1; A49: abs(F1.0) in Lp_Functions(M,k) & AbsFMF.0 in Lp_Functions(M,k) by A13,A7; G.0 = abs(F1.0) + (Partial_Sums AbsFMF).0 by A16; then A50: G.0 =abs(F1.0) + AbsFMF.0 by MESFUN9C:def 2; Ir.0 = Integral(M,Gp.0) by A38; then Ir.0 = Integral(M,(G.0) to_power k) by A23; then A51: Ir.0 = Integral(M,abs( abs(F1.0) + AbsFMF.0 ) to_power k) by A17,A50; KPAbsFMF.0 = Integral(M,(AbsFMF.0) to_power k) by A43; then A52: KPAbsFMF.0 = Integral(M,abs(AbsFMF.0) to_power k) by A13; A53: RF0 = Integral(M,abs(abs(F1.0)) to_power k); QAbsFMF.0 = RF0 to_power (1/k) + (Partial_Sums PAbsFMF).0 by A47; then QAbsFMF.0 = RF0 to_power (1/k) + PAbsFMF.0 by SERIES_1:def 1; then QAbsFMF.0 = RF0 to_power (1/k) + (KPAbsFMF.0) to_power (1/k) by A45; then A54: PN[ 0] by A1,A49,A51,A52,A53,Th61; A55: now let n being Nat; A56: n in NAT by ORDINAL1:def 12; assume PN[n]; then A57: (Ir.n) to_power (1/k) + PAbsFMF.(n+1) <= QAbsFMF.n + PAbsFMF.(n+1) by XREAL_1:6; G.(n+1) = abs(F1.0) + (Partial_Sums AbsFMF).(n+1) by A16 .= abs(F1.0) + ((Partial_Sums AbsFMF).n + AbsFMF.(n+1)) by MESFUN9C:def 2 .= abs(F1.0) +(Partial_Sums AbsFMF).n + AbsFMF.(n+1) by RFUNCT_1:8; then A58: G.(n+1) = G.n + AbsFMF.(n+1) by A16; A59: AbsFMF.(n+1) in Lp_Functions(M,k) & G.n in Lp_Functions(M,k) by A13,A17; KPAbsFMF.(n+1) = Integral(M,(AbsFMF.(n+1)) to_power k) by A43; then A60: KPAbsFMF.(n+1) = Integral(M,abs (AbsFMF.(n+1)) to_power k) by A13; A61: PAbsFMF.(n+1) = (KPAbsFMF.(n+1)) to_power (1/k) by A45; Ir.n = Integral(M,Gp.n) & Ir.(n+1) = Integral(M,Gp.(n+1)) by A38; then Ir.n = Integral(M,(G.n) to_power k) & Ir.(n+1) = Integral(M,(G.(n+1)) to_power k) by A23; then Ir.n = Integral(M,abs (G.n) to_power k) & Ir.(n+1) =Integral(M,abs (G.n + AbsFMF.(n+1)) to_power k) by A58,A17; then (Ir.(n+1)) to_power (1/k) <= (Ir.n) to_power (1/k) + PAbsFMF.(n+1) by A1,A59,A60,A61,Th61; then A62: (Ir.(n+1)) to_power (1/k) <= QAbsFMF.n + PAbsFMF.(n+1) by A57,XXREAL_0:2 ; QAbsFMF.n + PAbsFMF.(n+1) = RF0 to_power (1/k) + (Partial_Sums PAbsFMF).n + PAbsFMF.(n+1) by A47,A56 .= RF0 to_power (1/k) + ((Partial_Sums PAbsFMF).n + PAbsFMF.(n+1)) .= RF0 to_power (1/k) + (Partial_Sums PAbsFMF).(n+1) by SERIES_1:def 1; hence PN[n+1] by A62,A47; end; for n be Nat holds PN[n] from NAT_1:sch 2(A54,A55); hence thesis; end; A63:for n be Nat holds PAbsFMF.n = ||. Sq.(N.(n+1))-Sq.(N.n) .|| proof let n be Nat; A64: n in NAT by ORDINAL1:def 12; set m = N.n; set m1 = N.(n+1); A65: F1.(n+1) = Fsq.(N.(n+1)) & F1.n = Fsq.(N.n) by A6; AbsFMF.n = abs (FMF.n) by SEQFUNC:def 4; then A66: AbsFMF.n = abs( Fsq.(N.(n+1)) - Fsq.(N.n) ) by A65,A10; A67: Fsq.(N.(n+1)) in Lp_Functions(M,k) & Fsq.(N.(n+1)) in Sq.(N.(n+1)) & Fsq.(N.n) in Lp_Functions(M,k) & Fsq.(N.n) in Sq.m by A3; then (-1)(#)(Fsq.m) in (-1)*(Sq.m) by Th54; then Fsq.m1 - Fsq.m in Sq.m1 + (-1)*(Sq.m) by Th54,A67; then Fsq.m1 - Fsq.m in Sq.m1 - Sq.m by RLVECT_1:16; then A68: ex r be Real st 0<=r & r = Integral(M,(abs (Fsq.m1 - Fsq.m)) to_power k) & ||. Sq.m1 - Sq.m .|| = r to_power (1/k) by Th53; PAbsFMF.n = (KPAbsFMF.n) to_power (1/k) by A45,A64; hence thesis by A68,A66,A43,A64; end; 1/2 < 1; then |.1/2.| < 1 by ABSVALUE:def 1; then A69:(1/2) GeoSeq is summable & Sum((1/2) GeoSeq) = 1/(1-(1/2)) by SERIES_1:24; for n be Nat holds 0<=PAbsFMF.n & PAbsFMF.n <= ((1/2) GeoSeq).n proof let n be Nat; A70: PAbsFMF.n = ||. Sq.(N.(n+1)) - Sq.(N.n) .|| by A63; hence 0 <= PAbsFMF.n; ((1/2) GeoSeq).n = (1/2) |^n by PREPOWER:def 1 .= (1/2) to_power n by POWER:41; then A71: ((1/2) GeoSeq).n = 2 to_power (-n) by POWER:32; N is Real_Sequence by FUNCT_2:7,NUMBERS:19; then N.n < N.(n+1) by SEQM_3:def 6; hence PAbsFMF.n <= ((1/2) GeoSeq).n by A5,A70,A71; end; then PAbsFMF is summable & Sum(PAbsFMF) <= Sum((1/2) GeoSeq) by A69,SERIES_1:20; then Partial_Sums(PAbsFMF) is convergent by SERIES_1:def 2; then Partial_Sums(PAbsFMF) is bounded; then consider Br be Real such that A72: for n be Nat holds Partial_Sums(PAbsFMF).n < Br by SEQ_2:def 3; for n being Nat holds Ir.n < (RF0 to_power (1/k) + Br) to_power k proof let n being Nat; A73: n in NAT by ORDINAL1:def 12; (Ir.n) to_power (1/k) <= QAbsFMF.n by A48; then A74: (Ir.n) to_power (1/k) <= RF0 to_power (1/k) + (Partial_Sums PAbsFMF).n by A47,A73; RF0 to_power (1/k) + (Partial_Sums PAbsFMF).n < RF0 to_power (1/k) + Br by A72,XREAL_1:8; then A75: (Ir.n) to_power (1/k) < RF0 to_power (1/k) + Br by A74,XXREAL_0:2; Ir.n = Integral(M,Gp.n) by A38; then Ir.n = Integral(M,(G.n) to_power k) by A23; then A76:Ir.n = Integral(M,abs(G.n) to_power k) by A17; A77: G.n in Lp_Functions(M,k) by A17; then 0 <= (Ir.n) to_power (1/k) by Th49,A76,Th4; then ((Ir.n) to_power (1/k)) to_power k < (RF0 to_power (1/k) + Br) to_power k by A75,Th3; then (Ir.n) to_power ((1/k)*k) < (RF0 to_power (1/k) + Br) to_power k by A77,Th49,A76,HOLDER_1:2; then (Ir.n) to_power 1 < (RF0 to_power (1/k) + Br) to_power k by XCMPLX_1:106; hence thesis by POWER:25; end; then A78:Ir is bounded_above by SEQ_2:def 3; for n,m be Nat st n <=m holds Ir.n <= Ir.m proof let n,m be Nat; assume n <=m; then A79: for x be Element of X st x in E holds (ExtGp.n).x <= (ExtGp.m).x by A28; A80: ExtGp.n is E-measurable & ExtGp.m is E-measurable & ExtGp.n is nonnegative & ExtGp.m is nonnegative by A26; A81: dom(ExtGp.n) = E & dom(ExtGp.m) = E by A26; then A82: (ExtGp.n)|E = ExtGp.n & (ExtGp.m)|E = ExtGp.m by RELAT_1:68; I.n = Integral(M,ExtGp.n) & I.m = Integral(M,ExtGp.m) by A38; hence thesis by A79,A81,A80,A82,MESFUNC9:15; end; then Ir is non-decreasing by SEQM_3:6; then A83:I is convergent_to_finite_number & lim I = lim Ir by A78,RINFSUP2:14; reconsider LExtGp = lim ExtGp as PartFunc of X,ExtREAL; A84:E = dom LExtGp & LExtGp is E-measurable by A26,A27,A37,MESFUNC8:25,def 9; A85:for x be object st x in dom LExtGp holds 0 <= LExtGp.x proof let x be object; assume A86: x in dom LExtGp; then reconsider x1 = x as Element of X; A87: x1 in E by A27,A86,MESFUNC8:def 9; now let k1 being Nat; reconsider k=k1 as Nat; ExtGp#x1 is non-decreasing by A35,A87; then A88: (ExtGp#x1).0 <= (ExtGp#x1).k by RINFSUP2:7; 0 <= (ExtGp.0).x1 by A27,SUPINF_2:39; hence 0 <= (ExtGp#x1).k1 by A88,MESFUNC5:def 13; end; then 0 <= lim (ExtGp#x1) by A87,A37,MESFUNC9:10; hence thesis by A86,MESFUNC8:def 9; end; A89:eq_dom(LExtGp,+infty) = E /\ eq_dom(LExtGp,+infty) by A84,RELAT_1:132,XBOOLE_1:28; then reconsider EE=eq_dom(LExtGp,+infty) as Element of S by A84,MESFUNC1:33; reconsider E0= E \ EE as Element of S; E0` = (X \ E) \/ (X /\ EE) by XBOOLE_1:52; then A90:E0` = E` \/ EE by XBOOLE_1:28; M.EE = 0 by A38,A83,A84,A85,A89,MESFUNC9:13,SUPINF_2:52; then A91:EE is measure_zero of M by MEASURE1:def 7; E` is Element of S by MEASURE1:34; then E` is measure_zero of M by A4,MEASURE1:def 7; then E0` is measure_zero of M by A90,A91,MEASURE1:37; then A92:M.E0` = 0 by MEASURE1:def 7; A93:for x be Element of X st x in E0 holds LExtGp.x in REAL proof let x be Element of X; assume x in E0; then x in E & not x in EE by XBOOLE_0:def 5; then LExtGp.x <> +infty & 0<= LExtGp.x by A84,A85,MESFUNC1:def 15; hence LExtGp.x in REAL by XXREAL_0:14; end; A94:for x be Element of X st x in E0 holds Gp#x is convergent & lim (Gp#x)= lim (ExtGp#x) proof let x be Element of X; assume A95: x in E0; then A96: x in E by XBOOLE_0:def 5; then LExtGp.x = lim((ExtGp)#x) by A84,MESFUNC8:def 9; then A97: lim((ExtGp)#x) in REAL by A93,A95; (ExtGp)#x is convergent by A37,A96; then A98: ex g be Real st lim((ExtGp)#x) = g & (for p be Real st 0
0; then consider m be Nat such that A177: n=m+1 by NAT_1:6; reconsider m as Nat; (F1#x).(m+1) = (F1#x).0 + (Partial_Sums(FMF#x)).m by A119,A171; then A178: |.(F1#x).(m+1) qua Complex.| to_power k <= (Gp#x).m by A165,A171; x in E by A171,XBOOLE_0:def 5; then A179: ExtGp#x is non-decreasing by A35; A180: ((ExtGp)#x).m <= ((ExtGp)#x).(m+1) by A179; ExtGp#x = Gp#x by MESFUN7C:1; hence |.((F2#x).n) qua Complex.| to_power k <= (Gp#x).n by A172,A177,A178,A180, XXREAL_0:2; end; end; A181:for x be Element of X st x in E0 holds |.((abs F) to_power k).x qua Complex .| <= gp.x proof let x be Element of X; assume A182: x in E0; then A183: Gp#x is convergent by A94; deffunc ABSF2(set) = (abs(F2#x).$1 ) to_power k; consider s be Real_Sequence such that A184: for n be Nat holds s.n=ABSF2(n) from SEQ_1:sch 1; A185: gp.x = lim (Gp#x) by A152,A182; A186: ((abs F) to_power k).x = ((abs F).x) to_power k by A159,A182, MESFUN6C:def 4 .= (|.F.x qua Complex.|) to_power k by A158,A182,VALUED_1:def 11 .= |.lim (F2#x) qua Complex.| to_power k by A182,A147 .= (lim (abs (F2#x))) to_power k by A134,A182,SEQ_4:14; A187: now let n be Nat; 0 <= |.(F2#x).n.| by COMPLEX1:46; hence 0 <=(abs(F2#x)).n by VALUED_1:18; end; abs (F2#x) is convergent by A182,A134,SEQ_4:13; then A188: s is convergent & (lim (abs (F2#x))) to_power k = lim s by A187,A184,HOLDER_1:10; now let n be Nat; |.(F2#x).n qua Complex.| to_power k <= (Gp#x).n by A170,A182; then (abs(F2#x).n) to_power k <= (Gp#x).n by VALUED_1:18; hence s.n <=(Gp#x).n by A184; end; then A189: ((abs F) to_power k).x <= gp.x by A188,A185,A186,A183,SEQ_2:18; 0 <= ((abs F) to_power k).x by MESFUNC6:51; hence |.((abs F) to_power k).x qua Complex.| <= gp.x by A189,ABSVALUE:def 1; end; R_EAL F is E0-measurable by A138,A156,A134,MESFUN7C:21; then A190:F is E0-measurable; then A191:(abs F) is E0-measurable by A157,MESFUNC6:48; dom abs F = E0 by A157,VALUED_1:def 11; then (abs F) to_power k is E0-measurable by A191,MESFUN6C:29; then (abs F) to_power k is_integrable_on M by A150,A155,A159,A181,MESFUNC6:96; then A192:F in Lp_Functions(M,k) by A92,A157,A190; A193:for x be Element of X, n,m be Nat st x in E0 & m <= n holds |. (F1#x).n -(F1#x).m qua Complex.| to_power k <= (Gp#x).n proof let x be Element of X, n1,m1 be Nat; assume A194: x in E0 & m1 <= n1; now per cases; suppose A195: m1= 0; now per cases; suppose A196: n1=0; ((G.n1) to_power k) is nonnegative by A24; then Gp.n1 is nonnegative by A23; then 0 <= (Gp.n1).x by MESFUNC6:51; then 0 <= (Gp#x).n1 by SEQFUNC:def 10; hence |. (F1#x).n1-(F1#x).m1 qua Complex .| to_power k <= (Gp#x).n1 by A195,A196,COMPLEX1:44,POWER:def 2; end; suppose n1<> 0; then consider n be Nat such that A197: n1=n+1 by NAT_1:6; reconsider n as Nat; A198: (F1#x).(n+1) = (F1#x).0 + (Partial_Sums (FMF#x)).n by A194,A119; A199: |.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.| <= (G#x).n by A160 ,A194; 0 <= |.(F1#x).0 .| by COMPLEX1:46; then |.(Partial_Sums (FMF#x)).n qua Complex.| + 0 <= |.(F1#x).0 qua Complex .| + |.(Partial_Sums (FMF#x)).n qua Complex.| by XREAL_1:6; then A200: |.(Partial_Sums (FMF#x)).n qua Complex.| <= (G#x).n by A199,XXREAL_0:2; 0 <= |.(Partial_Sums (FMF#x)).n.| by COMPLEX1:46; then A201: |. (Partial_Sums(FMF#x)).n qua Complex .| to_power k <= ((G#x).n) to_power k by A200,HOLDER_1:3; A202: (Gp#x).n = (((G#x)).n) to_power k by A194,A99; x in E by A194,XBOOLE_0:def 5; then A203: ExtGp#x is non-decreasing by A35; A204: ((ExtGp)#x).n <= ((ExtGp)#x).(n+1) by A203; ExtGp#x = Gp#x by MESFUN7C:1; hence |. (F1#x).n1 -(F1#x).m1 qua Complex .| to_power k <= (Gp#x).n1 by A195,A197,A204,A201,A202,A198,XXREAL_0:2; end; end; hence |. (F1#x).n1-(F1#x).m1 qua Complex .| to_power k <= (Gp#x).n1; end; suppose A205: m1<> 0; then consider m be Nat such that A206: m1=m+1 by NAT_1:6; reconsider m as Nat; 0 < n1 by A194,A205; then consider n be Nat such that A207: n1=n+1 by NAT_1:6; reconsider n as Element of NAT by ORDINAL1:def 12; A208: m1-1 <= n1-1 by A194,XREAL_1:9; x in E by A194,XBOOLE_0:def 5; then A209: x in dom(G.n) by A17; then A210: x in dom ((G.n) to_power k) by MESFUN6C:def 4; (Gp#x).n = (Gp.n).x by SEQFUNC:def 10; then (Gp#x).n = ((G.n) to_power k).x by A23; then A211: (Gp#x).n = ((G.n).x) to_power k by A210,MESFUN6C:def 4; G.n = abs(F1.0) + (Partial_Sums AbsFMF).n by A16; then (G.n).x = abs(F1.0).x + ((Partial_Sums AbsFMF).n).x by A209,VALUED_1:def 1 .= |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF).n).x by VALUED_1:18; then A212 : (G.n).x = |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF)#x).n by SEQFUNC:def 10; A213: (F1#x).(n+1) = (F1#x).0 + (Partial_Sums (FMF#x)).n & (F1#x).(m+1) = (F1#x).0 + (Partial_Sums (FMF#x)).m by A194,A119; A214: |. (Partial_Sums (FMF#x)).n - (Partial_Sums (FMF#x)).m .| <= (Partial_Sums abs(FMF#x)).n by Th10,A206,A207,A208; A215: (Partial_Sums abs(FMF#x)).n = ((Partial_Sums AbsFMF)#x).n by A111,A194 ; 0 <= |.(F1.0).x.| by COMPLEX1:46; then 0 + (Partial_Sums abs(FMF#x)).n <= |.(F1.0).x qua Complex.| + ((Partial_Sums AbsFMF)#x).n by A215,XREAL_1:6; then A216: |. (F1#x).(n+1)-(F1#x).(m+1) .| <= (G.n).x by A212,A213,A214,XXREAL_0:2 ; 0 <= |. (F1#x).(n+1)-(F1#x).(m+1) .| by COMPLEX1:46; then A217: (|. (F1#x).(n+1)-(F1#x).(m+1) qua Complex .|) to_power k <= (Gp#x).n by A211,A216,HOLDER_1:3; x in E by A194,XBOOLE_0:def 5; then A218: ExtGp#x is non-decreasing by A35; A219: ((ExtGp)#x).n <= ((ExtGp)#x).(n+1) by A218; ExtGp#x = Gp#x by MESFUN7C:1; hence (|. (F1#x).(n1)-(F1#x).(m1) qua Complex .|) to_power k <= (Gp#x).n1 by A206,A207,A219,A217,XXREAL_0:2; end; end; hence thesis; end; A220:for x be Element of X, n be Nat st x in E0 holds |. F.x -(F2#x).n qua Complex .| to_power k <= gp.x proof let x be Element of X, n1 be Nat; assume A221: x in E0; then A222: Gp#x is convergent by A94; A223: F1#x = F2#x by A136,A221; A224: F2#x is convergent by A221,A134; reconsider n=n1 as Nat; deffunc AF2F20(Nat) = (F2#x).$1 -(F2#x).n; consider s0 be Real_Sequence such that A225: for j be Nat holds s0.j=AF2F20(j) from SEQ_1:sch 1; A226: now let p be Real; assume 0
= 0 proof let n; ||. Sq0-Sq.(N.n) .|| to_power k >= 0 by Th4; hence Ip.n >= 0 by A260; end; A267: for n be Nat holds Iq.n = (Ip.n) to_power (1/k) proof let n be Nat; thus (Ip.n) to_power (1/k) = ( ||.Sq0-Sq.(N.n).|| to_power k) to_power (1/k) by A260 .= ||.Sq0-Sq.(N.n).|| to_power (k*(1/k)) by HOLDER_1:2 .= (||.Sq0-Sq.(N.n).||) to_power 1 by XCMPLX_1:106 .= ||.Sq0-Sq.(N.n).|| by POWER:25 .= Iq.n by A265; end; hence Iq is convergent by A266,A252,A251,HOLDER_1:10; lim Iq = (lim Ip) to_power (1/k) by A252,A251,A266,A267,HOLDER_1:10; then lim Iq = 0 to_power (1/k) by A252,A251,A257,A242,LPSPACE1:22; hence lim Iq = 0 by POWER:def 2; end; hence thesis by A2,A265,Lm7; end; registration let X,S,M; let k be geq_than_1 Real; cluster Lp-Space (M,k) -> complete; coherence proof for Sq be sequence of Lp-Space(M,k) st Sq is Cauchy_sequence_by_Norm holds Sq is convergent by Th70; hence thesis by LOPBAN_1:def 15; end; end; begin :: Relations between L1 Space and Lp Space Lm8: f in L1_Functions M implies f is_integrable_on M & (ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable) proof assume f in L1_Functions M; then ex f2 be PartFunc of X,REAL st f = f2 & ex E be Element of S st M.E=0 & dom f2 = E` & f2 is_integrable_on M; then consider D be Element of S such that A1: M.D = 0 & dom f = D` & f is_integrable_on M; thus f is_integrable_on M by A1; reconsider E=D` as Element of S by MEASURE1:34; take E; thus M.E` = 0 & dom f = E by A1; R_EAL f is_integrable_on M by A1; then ex B be Element of S st B = dom (R_EAL f) & (R_EAL f) is B-measurable; hence f is E-measurable by A1; end; Lm9: f in Lp_Functions(M,k) implies (abs f) to_power k is_integrable_on M proof assume f in Lp_Functions(M,k); then ex f2 be PartFunc of X,REAL st f = f2 & ex E be Element of S st M.E` = 0 & dom f2 = E & f2 is E-measurable & (abs f2) to_power k is_integrable_on M; hence thesis; end; Lm10: (ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable) implies a.e-eq-class_Lp(f,M,1) c= a.e-eq-class(f,M) proof assume A1: ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable; let x be object; assume x in a.e-eq-class_Lp(f,M,1); then consider h be PartFunc of X,REAL such that A2: x = h & h in Lp_Functions(M,1) & f a.e.= h,M; A3: ex g be PartFunc of X,REAL st h = g & (ex E be Element of S st M.E`=0 & dom g = E & g is E-measurable & (abs g) to_power 1 is_integrable_on M) by A2; then consider Eh be Element of S such that A4: M.(Eh`) = 0 & dom h = Eh & h is Eh-measurable & (abs h) to_power 1 is_integrable_on M; A5: dom((abs h) to_power 1) = dom(abs h) by MESFUN6C:def 4; for x be Element of X st x in dom((abs h) to_power 1) holds ((abs h) to_power 1).x = (abs h).x proof let x be Element of X; assume x in dom((abs h) to_power 1); then ((abs h) to_power 1).x = ((abs h).x) to_power 1 by MESFUN6C:def 4; hence thesis by POWER:25; end; then (abs h) to_power 1 = abs h by A5,PARTFUN1:5; then A6: h is_integrable_on M by A3,MESFUNC6:94; reconsider ND = Eh` as Element of S by MEASURE1:34; M.ND = 0 & dom h = ND` by A4; then A7: h in L1_Functions M by A6; ex E be Element of S st M.E = 0 & dom f = E` & f is_integrable_on M proof consider Ef be Element of S such that A8: M.(Ef`)=0 & Ef = dom f & f is Ef-measurable by A1; reconsider E = Ef` as Element of S by MEASURE1:34; take E; consider EE be Element of S such that A9: M.EE = 0 & f|EE` = h|EE` by A2; reconsider E1 = ND \/ EE as Element of S; ND is measure_zero of M & EE is measure_zero of M by A4,A9,MEASURE1:def 7; then E1 is measure_zero of M by MEASURE1:37; then A10: M.E1 = 0 by MEASURE1:def 7; EE c= E1 by XBOOLE_1:7; then E1` c= EE` by SUBSET_1:12; then A11: f|E1` = (f|EE`)|E1` & h|E1` = (h|EE`)|E1` by FUNCT_1:51; A12: dom max+(R_EAL f) = Ef & dom max-(R_EAL f) = Ef by A8,MESFUNC2:def 2,def 3; A13: Ef = dom(R_EAL f) & (R_EAL f) is Ef-measurable by A8; then A14: max+(R_EAL f) is Ef-measurable & max-(R_EAL f) is Ef-measurable by MESFUNC2:25,26; (for x being Element of X holds 0. <= (max+(R_EAL f)).x) & (for x being Element of X holds 0. <= (max-(R_EAL f)).x) by MESFUNC2:12,13; then A15: max+(R_EAL f) is nonnegative & max-(R_EAL f) is nonnegative by SUPINF_2:39; A16: Ef = (Ef /\ E1) \/ (Ef \ E1) by XBOOLE_1:51; reconsider E0 = Ef /\ E1 as Element of S; A17: Ef \ E1 = Ef /\ E1` by SUBSET_1:13; reconsider E2 = Ef \ E1 as Element of S; max+(R_EAL f) = (max+(R_EAL f))|(dom(max+(R_EAL f))) & max-(R_EAL f) = (max-(R_EAL f))|(dom(max-(R_EAL f))) by RELAT_1:69; then A18: integral+(M,max+(R_EAL f)) = integral+(M,(max+(R_EAL f))|E0) + integral+(M,(max+(R_EAL f))|E2) & integral+(M,max-(R_EAL f)) = integral+(M,(max-(R_EAL f))|E0) + integral+(M,(max-(R_EAL f))|E2) by A12,A15,A16,A14,MESFUNC5:81,XBOOLE_1:89; A19: integral+(M,(max+(R_EAL f))|E0) >= 0 & integral+(M,(max-(R_EAL f))|E0) >= 0 by A15,A14,A12,MESFUNC5:80; integral+(M,(max+(R_EAL f))|E1) = 0 & integral+(M,(max-(R_EAL f))|E1) = 0 by A10,A12,A15,A14,MESFUNC5:82; then integral+(M,(max+(R_EAL f))|E0) = 0 & integral+(M,(max-(R_EAL f))|E0) = 0 by A19,A12,A15,A14,MESFUNC5:83,XBOOLE_1:17; then A20: integral+(M,max+(R_EAL f)) = integral+(M,(max+(R_EAL f))|E2) & integral+(M,max-(R_EAL f)) = integral+(M,(max-(R_EAL f))|E2) by A18,XXREAL_3:4; A21: E2 c= E1` by A17,XBOOLE_1:17; then f|E2 = (h|E1`)|E2 by A9,A11,FUNCT_1:51; then A22: (R_EAL f)|E2 = (R_EAL h)|E2 by A21,FUNCT_1:51; A23: max+(R_EAL f)|E2 = max+((R_EAL f)|E2) & max+(R_EAL h)|E2 = max+((R_EAL h)|E2) & max-(R_EAL f)|E2 = max-((R_EAL f)|E2) & max-(R_EAL h)|E2 = max-((R_EAL h)|E2) by MESFUNC5:28; A24: R_EAL h is_integrable_on M by A6; then A25: integral+(M,max+(R_EAL h)) < +infty & integral+(M,max-(R_EAL h)) < +infty; integral+(M,max+((R_EAL h)|E2)) <= integral+(M,max+(R_EAL h)) & integral+(M,max-((R_EAL h)|E2)) <= integral+(M,max-(R_EAL h)) by A24,MESFUNC5:97; then integral+(M,max+(R_EAL f)) < +infty & integral+(M,max-(R_EAL f)) < +infty by A20,A25,A23,A22,XXREAL_0:2; then (R_EAL f) is_integrable_on M by A13; hence thesis by A8; end; then f in L1_Functions M; hence x in a.e-eq-class(f,M) by A2,A7; end; Lm11: a.e-eq-class(f,M) c= a.e-eq-class_Lp(f,M,1) proof let x be object; assume x in a.e-eq-class(f,M); then consider g be PartFunc of X,REAL such that A1: x = g & g in L1_Functions M & f in L1_Functions M & f a.e.= g,M; A2: ex h be PartFunc of X,REAL st g = h & ex D be Element of S st M.D=0 & dom h = D` & h is_integrable_on M by A1; then R_EAL g is_integrable_on M; then consider A be Element of S such that A3: A = dom(R_EAL g) & R_EAL g is A-measurable; A4: A = dom g & g is A-measurable by A3; A5: M.A` = 0 by A2,A3; (abs g) to_power 1 = abs g by Th8; then (abs g) to_power 1 is_integrable_on M by A2,A4,MESFUNC6:94; then g in {p where p is PartFunc of X,REAL : ex Ep be Element of S st M.(Ep`)=0 & dom p = Ep & p is Ep-measurable & (abs p) to_power 1 is_integrable_on M} by A4,A5; hence x in a.e-eq-class_Lp(f,M,1) by A1; end; Lm12: (ex E be Element of S st M.E`=0 & E = dom f & f is E-measurable) implies a.e-eq-class_Lp(f,M,1) = a.e-eq-class(f,M) by Lm10,Lm11; theorem Th71: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds CosetSet M = CosetSet(M,1) proof let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; now let x be object; assume x in CosetSet M; then consider g be PartFunc of X,REAL such that A1: x = a.e-eq-class(g,M) & g in L1_Functions M; A2: g is_integrable_on M & ex E be Element of S st M.E`=0 & E = dom g & g is E-measurable by A1,Lm8; then A3: x = a.e-eq-class_Lp(g,M,1) by A1,Lm12; (abs g) to_power 1 = abs g by Th8; then (abs g) to_power 1 is_integrable_on M by A2,MESFUNC6:94; then g in Lp_Functions(M,1) by A2; hence x in CosetSet(M,1) by A3; end; then A4:CosetSet M c= CosetSet(M,1); now let x be object; assume x in CosetSet(M,1); then consider g be PartFunc of X,REAL such that A5: x = a.e-eq-class_Lp(g,M,1) & g in Lp_Functions(M,1); consider E be Element of S such that A6: M.E` = 0 & dom g = E & g is E-measurable by A5,Th35; A7: x = a.e-eq-class(g,M) by A5,A6,Lm12; reconsider D = E` as Element of S by MEASURE1:34; A8: M.D = 0 & dom g = D` by A6; (abs g) to_power 1 is_integrable_on M by A5,Lm9; then abs g is_integrable_on M by Th8; then g is_integrable_on M by A6,MESFUNC6:94; then g in L1_Functions M by A8; hence x in CosetSet M by A7; end; then CosetSet(M,1) c= CosetSet M; hence thesis by A4; end; theorem Th72: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds addCoset M = addCoset(M,1) proof let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; A1:CosetSet M = CosetSet(M,1) by Th71; now let A,B be Element of CosetSet M; A in {a.e-eq-class(f,M) where f is PartFunc of X,REAL : f in L1_Functions M}; then consider a be PartFunc of X,REAL such that A2: A = a.e-eq-class(a,M) & a in L1_Functions M; B in {a.e-eq-class(f,M) where f is PartFunc of X,REAL : f in L1_Functions M}; then consider b be PartFunc of X,REAL such that A3: B = a.e-eq-class(b,M) & b in L1_Functions M; A4: A is Element of CosetSet(M,1) & B is Element of CosetSet(M,1) by Th71; A5: a in a.e-eq-class(a,M) & b in a.e-eq-class(b,M) by A2,A3,LPSPACE1:38; then A6: (addCoset M).(A,B) = a.e-eq-class(a+b,M) by A2,A3,LPSPACE1:def 15; a+b in L1_Functions M by A2,A3,LPSPACE1:23; then ex E be Element of S st M.E`=0 & E = dom(a+b) & (a+b) is E-measurable by Lm8; then (addCoset M).(A,B) = a.e-eq-class_Lp(a+b,M,1) by A6,Lm12; hence (addCoset M).(A,B) = (addCoset(M,1)).(A,B) by A4,A5,A2,A3,Def8; end; hence addCoset M = addCoset(M,1) by A1,BINOP_1:2; end; theorem Th73: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds zeroCoset M = zeroCoset(M,1) proof let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; reconsider z = zeroCoset(M,1) as Element of CosetSet M by Th71; X-->0 in Lp_Functions(M,1) by Th23; then ex E be Element of S st M.E`=0 & dom (X-->0) = E & (X-->0) is E-measurable by Th35; then A1:z = a.e-eq-class(X-->0,M) by Lm12; X-->0 in L1_Functions M by Th56; hence thesis by A1,LPSPACE1:def 16; end; theorem Th74: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds lmultCoset M = lmultCoset(M,1) proof let X be non empty set; let S be SigmaField of X; let M be sigma_Measure of S; A1:CosetSet M = CosetSet(M,1) by Th71; now let z be Element of REAL, A be Element of CosetSet M; A in {a.e-eq-class(f,M) where f is PartFunc of X,REAL : f in L1_Functions M}; then consider a be PartFunc of X,REAL such that A2: A = a.e-eq-class(a,M) & a in L1_Functions M; A3: A is Element of CosetSet(M,1) by Th71; A4: a in A by A2,LPSPACE1:38; then A5: (lmultCoset M).(z,A) = a.e-eq-class(z(#)a,M) by LPSPACE1:def 17; z(#)a in L1_Functions M by A2,LPSPACE1:24; then ex E be Element of S st M.E`=0 & E = dom(z(#)a) & (z(#)a) is E-measurable by Lm8; then (lmultCoset M).(z,A) = a.e-eq-class_Lp(z(#)a,M,1) by A5,Lm12; hence (lmultCoset M).(z,A) = (lmultCoset(M,1)).(z,A) by A3,A4,Def10; end; hence lmultCoset M = lmultCoset(M,1) by A1,BINOP_1:2; end; theorem Th75: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds Pre-L-Space M = Pre-Lp-Space(M,1) proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; A1:the carrier of Pre-L-Space M = CosetSet M & the addF of Pre-L-Space M = addCoset M & 0.(Pre-L-Space M) = zeroCoset M & the Mult of Pre-L-Space M = lmultCoset M by LPSPACE1:def 18; CosetSet M = CosetSet(M,1) & addCoset M = addCoset(M,1) & zeroCoset M = zeroCoset(M,1) & lmultCoset M = lmultCoset(M,1) by Th71,Th72,Th73,Th74; hence thesis by A1,Def11; end; theorem Th76: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds L-1-Norm M = Lp-Norm(M,1) proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; A1:the carrier of Pre-L-Space M = the carrier of Pre-Lp-Space(M,1) by Th75; now let x be Element of the carrier of Pre-L-Space M; x in the carrier of Pre-L-Space M; then x in CosetSet M by LPSPACE1:def 18; then consider g be PartFunc of X,REAL such that A2: x = a.e-eq-class(g,M) & g in L1_Functions M; consider a be PartFunc of X,REAL such that A3: a in x & (L-1-Norm M).x = Integral(M,|.a.|) by LPSPACE1:def 19; A4: ex p be PartFunc of X,REAL st a = p & p in L1_Functions M & g in L1_Functions M & g a.e.= p,M by A2,A3; consider b be PartFunc of X,REAL such that A5: b in x & ex r be Real st r = Integral(M,(|.b.|) to_power 1) & (Lp-Norm(M,1)).x = r to_power (1/1) by A1,Def12; A6: ex q be PartFunc of X,REAL st b = q & q in L1_Functions M & g in L1_Functions M & g a.e.= q,M by A2,A5; a a.e.= g,M by A4; then a a.e.= b,M by A6,LPSPACE1:30; then A7: Integral(M,|.a.|) = Integral(M,|.b.|) by A2,A3,A5,LPSPACE1:45; (|.b.|) to_power 1 = |.b.| by Th8; hence (L-1-Norm M).x = (Lp-Norm(M,1)).x by A3,A5,A7,POWER:25; end; hence thesis by A1,FUNCT_2:63; end; theorem for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds L-1-Space M = Lp-Space(M,1) proof let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; Pre-L-Space M = Pre-Lp-Space(M,1) by Th75; hence thesis by Th76; end;