:: On $L^1$ Space Formed by Real-valued Partial Functions
:: by Yasushige Watase , Noboru Endou and Yasunari Shidama
::
:: Received August 26, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users

begin

definition

let V be non empty RLSStruct ;
let V1 be Subset of V;
attr V1 is multi-closed means :Def1: :: LPSPACE1:def 1
for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1;

end;

:: deftheorem Def1 defines multi-closed LPSPACE1:def 1 :
for V being non empty RLSStruct
for V1 being Subset of V holds
( V1 is multi-closed iff for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1 );

theorem :: LPSPACE1:1

for V being RealLinearSpace
for V1 being Subset of V holds
( V1 is linearly-closed iff ( V1 is add-closed & V1 is multi-closed ) )

proof end;

registration

let V be non empty RLSStruct ;
cluster non empty add-closed multi-closed Element of bool the carrier of V;
existence
ex b₁ being Subset of V st
( b₁ is add-closed & b₁ is multi-closed & not b₁ is empty )

proof end;

end;

definition

let X be non empty RLSStruct ;
let X1 be non empty multi-closed Subset of X;
func Mult_ X1 -> Function of [:REAL,X1:],X1 equals :: LPSPACE1:def 2
the Mult of X | [:REAL,X1:];
correctness
coherence
the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1;

proof end;

end;

:: deftheorem defines Mult_ LPSPACE1:def 2 :
for X being non empty RLSStruct
for X1 being non empty multi-closed Subset of X holds Mult_ X1 = the Mult of X | [:REAL,X1:];

theorem Th2: :: LPSPACE1:2

for V being non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for V1 being non empty Subset of V
for d1 being Element of V1
for A being BinOp of V1
for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )

proof end;

theorem Th3: :: LPSPACE1:3

for V being non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for V1 being non empty add-closed multi-closed Subset of V st 0. V in V1 holds
( RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is Abelian & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is add-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is right_zeroed & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is vector-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-unital )

proof end;

theorem Th4: :: LPSPACE1:4

for V being non empty RLSStruct
for V1 being non empty add-closed multi-closed Subset of V
for v, u being VECTOR of V
for w1, w2 being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w1 = v & w2 = u holds
w1 + w2 = v + u

proof end;

theorem Th5: :: LPSPACE1:5

for V being non empty RLSStruct
for V1 being non empty add-closed multi-closed Subset of V
for a being Real
for v being VECTOR of V
for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v

proof end;

begin

definition

let A, B be non empty set ;
let F be BinOp of (PFuncs (A,B));
let f, g be Element of PFuncs (A,B);
:: original: .
redefine func F . (f,g) -> Element of PFuncs (A,B);
coherence
F . (f,g) is Element of PFuncs (A,B)

proof end;

end;

definition

let A be non empty set ;
func multpfunc A -> BinOp of (PFuncs (A,REAL)) means :Def3: :: LPSPACE1:def 3
for f, g being Element of PFuncs (A,REAL) holds it . (f,g) = f (#) g;
existence
ex b₁ being BinOp of (PFuncs (A,REAL)) st
for f, g being Element of PFuncs (A,REAL) holds b₁ . (f,g) = f (#) g

proof end;

uniqueness
for b₁, b₂ being BinOp of (PFuncs (A,REAL)) st ( for f, g being Element of PFuncs (A,REAL) holds b₁ . (f,g) = f (#) g ) & ( for f, g being Element of PFuncs (A,REAL) holds b₂ . (f,g) = f (#) g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines multpfunc LPSPACE1:def 3 :
for A being non empty set
for b₂ being BinOp of (PFuncs (A,REAL)) holds
( b₂ = multpfunc A iff for f, g being Element of PFuncs (A,REAL) holds b₂ . (f,g) = f (#) g );

definition

let A be non empty set ;
func multrealpfunc A -> Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) means :Def4: :: LPSPACE1:def 4
for a being Real
for f being Element of PFuncs (A,REAL) holds it . (a,f) = a (#) f;
existence
ex b₁ being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) st
for a being Real
for f being Element of PFuncs (A,REAL) holds b₁ . (a,f) = a (#) f

proof end;

uniqueness
for b₁, b₂ being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) st ( for a being Real
for f being Element of PFuncs (A,REAL) holds b₁ . (a,f) = a (#) f ) & ( for a being Real
for f being Element of PFuncs (A,REAL) holds b₂ . (a,f) = a (#) f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines multrealpfunc LPSPACE1:def 4 :
for A being non empty set
for b₂ being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) holds
( b₂ = multrealpfunc A iff for a being Real
for f being Element of PFuncs (A,REAL) holds b₂ . (a,f) = a (#) f );

definition

let A be non empty set ;
func RealPFuncZero A -> Element of PFuncs (A,REAL) equals :: LPSPACE1:def 5
A --> 0;
coherence
A --> 0 is Element of PFuncs (A,REAL)

proof end;

end;

:: deftheorem defines RealPFuncZero LPSPACE1:def 5 :
for A being non empty set holds RealPFuncZero A = A --> 0;

definition

let A be non empty set ;
func RealPFuncUnit A -> Element of PFuncs (A,REAL) equals :: LPSPACE1:def 6
A --> 1;
coherence
A --> 1 is Element of PFuncs (A,REAL)

proof end;

end;

:: deftheorem defines RealPFuncUnit LPSPACE1:def 6 :
for A being non empty set holds RealPFuncUnit A = A --> 1;

theorem Th6: :: LPSPACE1:6

for A being non empty set
for h, f, g being Element of PFuncs (A,REAL) holds
( h = (addpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) ) )

proof end;

theorem Th7: :: LPSPACE1:7

for A being non empty set
for h, f, g being Element of PFuncs (A,REAL) holds
( h = (multpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) ) )

proof end;

theorem :: LPSPACE1:8

for A being non empty set holds RealPFuncZero A <> RealPFuncUnit A

proof end;

theorem Th9: :: LPSPACE1:9

for a being Real
for A being non empty set
for h, f being Element of PFuncs (A,REAL) holds
( h = (multrealpfunc A) . (a,f) iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )

proof end;

theorem Th10: :: LPSPACE1:10

for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,g) = (addpfunc A) . (g,f)

proof end;

theorem Th11: :: LPSPACE1:11

for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((addpfunc A) . (f,g)),h)

proof end;

theorem :: LPSPACE1:12

for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,g) = (multpfunc A) . (g,f)

proof end;

theorem :: LPSPACE1:13

for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,((multpfunc A) . (g,h))) = (multpfunc A) . (((multpfunc A) . (f,g)),h)

proof end;

theorem :: LPSPACE1:14

for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multpfunc A) . ((RealPFuncUnit A),f) = f

proof end;

theorem Th15: :: LPSPACE1:15

for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . ((RealPFuncZero A),f) = f

proof end;

theorem Th16: :: LPSPACE1:16

for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f)

proof end;

theorem Th17: :: LPSPACE1:17

for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (1,f) = f

proof end;

theorem Th18: :: LPSPACE1:18

for a, b being Real
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)

proof end;

theorem Th19: :: LPSPACE1:19

for a, b being Real
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a + b),f)

proof end;

Lm1: for a being Real
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g)))

proof end;

theorem :: LPSPACE1:20

for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))

proof end;

theorem :: LPSPACE1:21

for a being Real
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (multpfunc A) . (((multrealpfunc A) . (a,f)),g) = (multrealpfunc A) . (a,((multpfunc A) . (f,g)))

proof end;

definition

let A be non empty set ;
func RLSp_PFunct A -> non empty RLSStruct equals :: LPSPACE1:def 7
RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #);
coherence
RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #) is non empty RLSStruct ;

end;

:: deftheorem defines RLSp_PFunct LPSPACE1:def 7 :
for A being non empty set holds RLSp_PFunct A = RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #);

registration

let A be non empty set ;
cluster RLSp_PFunct A -> non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSp_PFunct A is strict & RLSp_PFunct A is Abelian & RLSp_PFunct A is add-associative & RLSp_PFunct A is right_zeroed & RLSp_PFunct A is vector-distributive & RLSp_PFunct A is scalar-distributive & RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )

proof end;

end;

begin

theorem Th22: :: LPSPACE1:22

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )

proof end;

definition

let X be non empty set ;
let r be Real;
:: original: -->
redefine func X --> r -> PartFunc of X,REAL;
coherence
X --> r is PartFunc of X,REAL

proof end;

end;

Lm2: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st X = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )

proof end;

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func L1_Functions M -> non empty Subset of (RLSp_PFunct X) equals :: LPSPACE1:def 8
{ f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } ;
correctness
coherence
{ f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } is non empty Subset of (RLSp_PFunct X);

proof end;

end;

:: deftheorem defines L1_Functions LPSPACE1:def 8 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L1_Functions M = { f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 & dom f = ND ` & f is_integrable_on M ) } ;

Lm3: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( X --> 0 is PartFunc of X,REAL & X --> 0 in L1_Functions M )

proof end;

Lm4: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S st M . E1 = 0 & M . E2 = 0 holds
M . (E1 \/ E2) = 0

proof end;

theorem Th23: :: LPSPACE1:23

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
f + g in L1_Functions M

proof end;

theorem Th24: :: LPSPACE1:24

for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
a (#) f in L1_Functions M

proof end;

Lm5: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( L1_Functions M is add-closed & L1_Functions M is multi-closed )

proof end;

registration

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster L1_Functions M -> non empty add-closed multi-closed ;
coherence
( L1_Functions M is multi-closed & L1_Functions M is add-closed ) by Lm5;

end;

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func RLSp_L1Funct M -> non empty RLSStruct equals :: LPSPACE1:def 9
RLSStruct(# (L1_Functions M),(In ((0. (RLSp_PFunct X)),(L1_Functions M))),(add| ((L1_Functions M),(RLSp_PFunct X))),(Mult_ (L1_Functions M)) #);
coherence
RLSStruct(# (L1_Functions M),(In ((0. (RLSp_PFunct X)),(L1_Functions M))),(add| ((L1_Functions M),(RLSp_PFunct X))),(Mult_ (L1_Functions M)) #) is non empty RLSStruct ;

end;

:: deftheorem defines RLSp_L1Funct LPSPACE1:def 9 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds RLSp_L1Funct M = RLSStruct(# (L1_Functions M),(In ((0. (RLSp_PFunct X)),(L1_Functions M))),(add| ((L1_Functions M),(RLSp_PFunct X))),(Mult_ (L1_Functions M)) #);

registration

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster RLSp_L1Funct M -> non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSp_L1Funct M is strict & RLSp_L1Funct M is Abelian & RLSp_L1Funct M is add-associative & RLSp_L1Funct M is right_zeroed & RLSp_L1Funct M is vector-distributive & RLSp_L1Funct M is scalar-distributive & RLSp_L1Funct M is scalar-associative & RLSp_L1Funct M is scalar-unital )

proof end;

end;

begin

theorem Th25: :: LPSPACE1:25

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_L1Funct M) st f = v & g = u holds
f + g = v + u

proof end;

theorem Th26: :: LPSPACE1:26

for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
a (#) f = a * u

proof end;

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f, g be PartFunc of X,REAL;
pred f a.e.= g,M means :Def10: :: LPSPACE1:def 10
ex E being Element of S st
( M . E = 0 & f | (E `) = g | (E `) );

end;

:: deftheorem Def10 defines a.e.= LPSPACE1:def 10 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL holds
( f a.e.= g,M iff ex E being Element of S st
( M . E = 0 & f | (E `) = g | (E `) ) );

theorem Th27: :: LPSPACE1:27

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_L1Funct M) st f = u holds
( u + ((- 1) * u) = (X --> 0) | (dom f) & ex v, g being PartFunc of X,REAL st
( v in L1_Functions M & g in L1_Functions M & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) )

proof end;

theorem Th28: :: LPSPACE1:28

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL holds f a.e.= f,M

proof end;

theorem Th29: :: LPSPACE1:29

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
g a.e.= f,M

proof end;

theorem Th30: :: LPSPACE1:30

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g, h being PartFunc of X,REAL st f a.e.= g,M & g a.e.= h,M holds
f a.e.= h,M

proof end;

theorem Th31: :: LPSPACE1:31

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f a.e.= f1,M & g a.e.= g1,M holds
f + g a.e.= f1 + g1,M

proof end;

theorem Th32: :: LPSPACE1:32

for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M

proof end;

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func AlmostZeroFunctions M -> non empty Subset of (RLSp_L1Funct M) equals :: LPSPACE1:def 11
{ f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M ) } ;
coherence
{ f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M ) } is non empty Subset of (RLSp_L1Funct M)

proof end;

end;

:: deftheorem defines AlmostZeroFunctions LPSPACE1:def 11 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds AlmostZeroFunctions M = { f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0,M ) } ;

theorem Th33: :: LPSPACE1:33

for a being Real
for X being non empty set holds
( (X --> 0) + (X --> 0) = X --> 0 & a (#) (X --> 0) = X --> 0 )

proof end;

Lm6: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed )

proof end;

registration

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster AlmostZeroFunctions M -> non empty add-closed multi-closed ;
coherence
( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed ) by Lm6;

end;

theorem Th34: :: LPSPACE1:34

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( 0. (RLSp_L1Funct M) = X --> 0 & 0. (RLSp_L1Funct M) in AlmostZeroFunctions M )

proof end;

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func RLSp_AlmostZeroFunct M -> non empty RLSStruct equals :: LPSPACE1:def 12
RLSStruct(# (AlmostZeroFunctions M),(In ((0. (RLSp_L1Funct M)),(AlmostZeroFunctions M))),(add| ((AlmostZeroFunctions M),(RLSp_L1Funct M))),(Mult_ (AlmostZeroFunctions M)) #);
coherence
RLSStruct(# (AlmostZeroFunctions M),(In ((0. (RLSp_L1Funct M)),(AlmostZeroFunctions M))),(add| ((AlmostZeroFunctions M),(RLSp_L1Funct M))),(Mult_ (AlmostZeroFunctions M)) #) is non empty RLSStruct ;

end;

:: deftheorem defines RLSp_AlmostZeroFunct LPSPACE1:def 12 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds RLSp_AlmostZeroFunct M = RLSStruct(# (AlmostZeroFunctions M),(In ((0. (RLSp_L1Funct M)),(AlmostZeroFunctions M))),(add| ((AlmostZeroFunctions M),(RLSp_L1Funct M))),(Mult_ (AlmostZeroFunctions M)) #);

registration

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster RLSp_L1Funct M -> non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSp_L1Funct M is strict & RLSp_L1Funct M is strict & RLSp_L1Funct M is Abelian & RLSp_L1Funct M is add-associative & RLSp_L1Funct M is right_zeroed & RLSp_L1Funct M is vector-distributive & RLSp_L1Funct M is scalar-distributive & RLSp_L1Funct M is scalar-associative & RLSp_L1Funct M is scalar-unital ) ;

end;

theorem :: LPSPACE1:35

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for v, u being VECTOR of (RLSp_AlmostZeroFunct M) st f = v & g = u holds
f + g = v + u

proof end;

theorem :: LPSPACE1:36

for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for u being VECTOR of (RLSp_AlmostZeroFunct M) st f = u holds
a (#) f = a * u

proof end;

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,REAL;
func a.e-eq-class (f,M) -> Subset of (L1_Functions M) equals :: LPSPACE1:def 13
{ g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) } ;
correctness
coherence
{ g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) } is Subset of (L1_Functions M);

proof end;

end;

:: deftheorem defines a.e-eq-class LPSPACE1:def 13 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL holds a.e-eq-class (f,M) = { g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) } ;

theorem Th37: :: LPSPACE1:37

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( g a.e.= f,M iff g in a.e-eq-class (f,M) )

proof end;

theorem Th38: :: LPSPACE1:38

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
f in a.e-eq-class (f,M)

proof end;

theorem Th39: :: LPSPACE1:39

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )

proof end;

theorem :: LPSPACE1:40

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff g in a.e-eq-class (f,M) )

proof end;

theorem Th41: :: LPSPACE1:41

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M & g1 in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (f1,M) & a.e-eq-class (g,M) = a.e-eq-class (g1,M) holds
a.e-eq-class ((f + g),M) = a.e-eq-class ((f1 + g1),M)

proof end;

theorem Th42: :: LPSPACE1:42

for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & a.e-eq-class (f,M) = a.e-eq-class (g,M) holds
a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M)

proof end;

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func CosetSet M -> non empty Subset-Family of (L1_Functions M) equals :: LPSPACE1:def 14
{ (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M } ;
correctness
coherence
{ (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M } is non empty Subset-Family of (L1_Functions M);

proof end;

end;

:: deftheorem defines CosetSet LPSPACE1:def 14 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CosetSet M = { (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M } ;

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func addCoset M -> BinOp of (CosetSet M) means :Def15: :: LPSPACE1:def 15
for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
it . (A,B) = a.e-eq-class ((a + b),M);
existence
ex b₁ being BinOp of (CosetSet M) st
for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b₁ . (A,B) = a.e-eq-class ((a + b),M)

proof end;

uniqueness
for b₁, b₂ being BinOp of (CosetSet M) st ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b₁ . (A,B) = a.e-eq-class ((a + b),M) ) & ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b₂ . (A,B) = a.e-eq-class ((a + b),M) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines addCoset LPSPACE1:def 15 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being BinOp of (CosetSet M) holds
( b₄ = addCoset M iff for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
b₄ . (A,B) = a.e-eq-class ((a + b),M) );

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func zeroCoset M -> Element of CosetSet M means :Def16: :: LPSPACE1:def 16
ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & it = a.e-eq-class (f,M) );
correctness
existence
ex b₁ being Element of CosetSet M ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b₁ = a.e-eq-class (f,M) );
uniqueness
for b₁, b₂ being Element of CosetSet M st ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b₁ = a.e-eq-class (f,M) ) & ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b₂ = a.e-eq-class (f,M) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def16 defines zeroCoset LPSPACE1:def 16 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Element of CosetSet M holds
( b₄ = zeroCoset M iff ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b₄ = a.e-eq-class (f,M) ) );

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func lmultCoset M -> Function of [:REAL,(CosetSet M):],(CosetSet M) means :Def17: :: LPSPACE1:def 17
for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
it . (z,A) = a.e-eq-class ((z (#) f),M);
existence
ex b₁ being Function of [:REAL,(CosetSet M):],(CosetSet M) st
for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b₁ . (z,A) = a.e-eq-class ((z (#) f),M)

proof end;

uniqueness
for b₁, b₂ being Function of [:REAL,(CosetSet M):],(CosetSet M) st ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b₁ . (z,A) = a.e-eq-class ((z (#) f),M) ) & ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b₂ . (z,A) = a.e-eq-class ((z (#) f),M) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines lmultCoset LPSPACE1:def 17 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Function of [:REAL,(CosetSet M):],(CosetSet M) holds
( b₄ = lmultCoset M iff for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b₄ . (z,A) = a.e-eq-class ((z (#) f),M) );

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func Pre-L-Space M -> non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct means :Def18: :: LPSPACE1:def 18
( the carrier of it = CosetSet M & the addF of it = addCoset M & 0. it = zeroCoset M & the Mult of it = lmultCoset M );
existence
ex b₁ being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct st
( the carrier of b₁ = CosetSet M & the addF of b₁ = addCoset M & 0. b₁ = zeroCoset M & the Mult of b₁ = lmultCoset M )

proof end;

uniqueness
for b₁, b₂ being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct st the carrier of b₁ = CosetSet M & the addF of b₁ = addCoset M & 0. b₁ = zeroCoset M & the Mult of b₁ = lmultCoset M & the carrier of b₂ = CosetSet M & the addF of b₂ = addCoset M & 0. b₂ = zeroCoset M & the Mult of b₂ = lmultCoset M holds
b₁ = b₂ ;

end;

:: deftheorem Def18 defines Pre-L-Space LPSPACE1:def 18 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds
( b₄ = Pre-L-Space M iff ( the carrier of b₄ = CosetSet M & the addF of b₄ = addCoset M & 0. b₄ = zeroCoset M & the Mult of b₄ = lmultCoset M ) );

begin

theorem Th43: :: LPSPACE1:43

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
Integral (M,f) = Integral (M,g)

proof end;

theorem Th44: :: LPSPACE1:44

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f is_integrable_on M holds
( Integral (M,f) in REAL & Integral (M,(abs f)) in REAL & abs f is_integrable_on M )

proof end;

theorem Th45: :: LPSPACE1:45

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M & f a.e.= g,M holds
( abs f a.e.= abs g,M & Integral (M,(abs f)) = Integral (M,(abs g)) )

proof end;

theorem Th46: :: LPSPACE1:46

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) holds
( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )

proof end;

theorem Th47: :: LPSPACE1:47

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S ex NORM being Function of the carrier of (Pre-L-Space M),REAL st
for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & NORM . x = Integral (M,(abs f)) )

proof end;

theorem Th48: :: LPSPACE1:48

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x holds
( f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M )

proof end;

theorem Th49: :: LPSPACE1:49

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x being Point of (Pre-L-Space M) st f in x & g in x holds
( f a.e.= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )

proof end;

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func L-1-Norm M -> Function of the carrier of (Pre-L-Space M),REAL means :Def19: :: LPSPACE1:def 19
for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & it . x = Integral (M,(abs f)) );
existence
ex b₁ being Function of the carrier of (Pre-L-Space M),REAL st
for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b₁ . x = Integral (M,(abs f)) ) by Th47;
uniqueness
for b₁, b₂ being Function of the carrier of (Pre-L-Space M),REAL st ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b₁ . x = Integral (M,(abs f)) ) ) & ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b₂ . x = Integral (M,(abs f)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines L-1-Norm LPSPACE1:def 19 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Function of the carrier of (Pre-L-Space M),REAL holds
( b₄ = L-1-Norm M iff for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x & b₄ . x = Integral (M,(abs f)) ) );

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func L-1-Space M -> non empty NORMSTR equals :: LPSPACE1:def 20
NORMSTR(# the carrier of (Pre-L-Space M), the ZeroF of (Pre-L-Space M), the addF of (Pre-L-Space M), the Mult of (Pre-L-Space M),(L-1-Norm M) #);
coherence
NORMSTR(# the carrier of (Pre-L-Space M), the ZeroF of (Pre-L-Space M), the addF of (Pre-L-Space M), the Mult of (Pre-L-Space M),(L-1-Norm M) #) is non empty NORMSTR ;

end;

:: deftheorem defines L-1-Space LPSPACE1:def 20 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L-1-Space M = NORMSTR(# the carrier of (Pre-L-Space M), the ZeroF of (Pre-L-Space M), the addF of (Pre-L-Space M), the Mult of (Pre-L-Space M),(L-1-Norm M) #);

theorem Th50: :: LPSPACE1:50

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )

proof end;

theorem Th51: :: LPSPACE1:51

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) )

proof end;

theorem Th52: :: LPSPACE1:52

for a being Real
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x, y being Point of (L-1-Space M) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )

proof end;

theorem Th53: :: LPSPACE1:53

for r being Real
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is_measurable_on E

proof end;

theorem Th54: :: LPSPACE1:54

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M & Integral (M,(abs f)) = 0 holds
f a.e.= X --> 0,M

proof end;

theorem Th55: :: LPSPACE1:55

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds Integral (M,(abs (X --> 0))) = 0

proof end;

theorem Th56: :: LPSPACE1:56

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))

proof end;

Lm7: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )

proof end;

registration

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster L-1-Space M -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealNormSpace-like ;
coherence
( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable ) by Lm7;

end;