:: by Yasushige Watase , Noboru Endou and Yasunari Shidama

::

:: Received August 26, 2008

:: Copyright (c) 2008-2018 Association of Mizar Users

definition

let V be non empty RLSStruct ;

let V1 be Subset of V;

end;
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;

for a being Real

for v being VECTOR of V st v in V1 holds

a * v in V1;

:: 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 );

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 ) ) by RLSUB_1:def 1;

for V1 being Subset of V holds

( V1 is linearly-closed iff ( V1 is add-closed & V1 is multi-closed ) ) by RLSUB_1:def 1;

registration

let V be non empty RLSStruct ;

existence

ex b_{1} being Subset of V st

( b_{1} is add-closed & b_{1} is multi-closed & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

definition

let X be non empty RLSStruct ;

let X1 be non empty multi-closed Subset of X;

correctness

coherence

the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1;

end;
let X1 be non empty multi-closed Subset of X;

correctness

coherence

the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1;

proof 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:];

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 )

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 )

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 by ZFMISC_1:87, FUNCT_1:49;

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 by ZFMISC_1:87, FUNCT_1:49;

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

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;

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)

end;
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;

definition

let A be non empty set ;

ex b_{1} being BinOp of (PFuncs (A,REAL)) st

for f, g being Element of PFuncs (A,REAL) holds b_{1} . (f,g) = f (#) g

for b_{1}, b_{2} being BinOp of (PFuncs (A,REAL)) st ( for f, g being Element of PFuncs (A,REAL) holds b_{1} . (f,g) = f (#) g ) & ( for f, g being Element of PFuncs (A,REAL) holds b_{2} . (f,g) = f (#) g ) holds

b_{1} = b_{2}

end;
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 for f, g being Element of PFuncs (A,REAL) holds it . (f,g) = f (#) g;

ex b

for f, g being Element of PFuncs (A,REAL) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines multpfunc LPSPACE1:def 3 :

for A being non empty set

for b_{2} being BinOp of (PFuncs (A,REAL)) holds

( b_{2} = multpfunc A iff for f, g being Element of PFuncs (A,REAL) holds b_{2} . (f,g) = f (#) g );

for A being non empty set

for b

( b

definition

let A be non empty set ;

ex b_{1} 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_{1} . (a,f) = a (#) f

for b_{1}, b_{2} 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_{1} . (a,f) = a (#) f ) & ( for a being Real

for f being Element of PFuncs (A,REAL) holds b_{2} . (a,f) = a (#) f ) holds

b_{1} = b_{2}

end;
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 for a being Real

for f being Element of PFuncs (A,REAL) holds it . (a,f) = a (#) f;

ex b

for a being Real

for f being Element of PFuncs (A,REAL) holds b

proof end;

uniqueness for b

for f being Element of PFuncs (A,REAL) holds b

for f being Element of PFuncs (A,REAL) holds b

b

proof end;

:: deftheorem Def4 defines multrealpfunc LPSPACE1:def 4 :

for A being non empty set

for b_{2} being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) holds

( b_{2} = multrealpfunc A iff for a being Real

for f being Element of PFuncs (A,REAL) holds b_{2} . (a,f) = a (#) f );

for A being non empty set

for b

( b

for f being Element of PFuncs (A,REAL) holds b

:: deftheorem defines RealPFuncZero LPSPACE1:def 5 :

for A being non empty set holds RealPFuncZero A = A --> 0;

for A being non empty set holds RealPFuncZero A = A --> 0;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

:: deftheorem defines RealPFuncUnit LPSPACE1:def 6 :

for A being non empty set holds RealPFuncUnit A = A --> 1;

for A being non empty set holds RealPFuncUnit A = A --> 1;

theorem Th6: :: LPSPACE1:6

for A being non empty set

for f, g, h 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) ) ) )

for f, g, h 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 f, g, h 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) ) ) )

for f, g, h 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 Th9: :: LPSPACE1:9

for a being Real

for A being non empty set

for f, h 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) ) ) )

for A being non empty set

for f, h 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 :: 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)

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)

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

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

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)

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

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)

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)

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)))

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)))

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 ;

RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #) is non empty RLSStruct ;

end;
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) #);

RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #) is non empty RLSStruct ;

:: 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) #);

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 ;

( 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 )

end;
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;

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 )

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

end;
let r be Real;

:: original: -->

redefine func X --> r -> PartFunc of X,REAL;

coherence

X --> r is PartFunc of X,REAL

proof 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;

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);

end;
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 { 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 ) } ;

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;

:: 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 ) } ;

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

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

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;

coherence

( L1_Functions M is multi-closed & L1_Functions M is add-closed ) by Lm5;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

coherence

( L1_Functions M is multi-closed & L1_Functions M is add-closed ) by Lm5;

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

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;
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)) #);

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 ;

:: 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)) #);

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;

( 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;
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;

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

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

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;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f, g be PartFunc of X,REAL;

:: deftheorem 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 `) ) );

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 ) )

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

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 :: 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 ;

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 ;

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

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, g, f1, 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

for S being SigmaField of X

for M being sigma_Measure of S

for f, g, f1, 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

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;

{ 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)

end;
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 ) } ;

{ 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;

:: 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 ) } ;

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 )

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;

coherence

( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed ) by Lm6;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

coherence

( AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is multi-closed ) by Lm6;

theorem :: 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 )

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;

RLSStruct(# (AlmostZeroFunctions M),(In ((0. (RLSp_L1Funct M)),(AlmostZeroFunctions M))),(add| ((AlmostZeroFunctions M),(RLSp_L1Funct M))),(Mult_ (AlmostZeroFunctions M)) #) is non empty RLSStruct ;

end;
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)) #);

RLSStruct(# (AlmostZeroFunctions M),(In ((0. (RLSp_L1Funct M)),(AlmostZeroFunctions M))),(add| ((AlmostZeroFunctions M),(RLSp_L1Funct M))),(Mult_ (AlmostZeroFunctions M)) #) is non empty RLSStruct ;

:: 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)) #);

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;

( 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;
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 ) ;

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

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

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;

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);

end;
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 { g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) } ;

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;

:: 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 ) } ;

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) )

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)

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 )

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) )

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, g, f1, 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)

for S being SigmaField of X

for M being sigma_Measure of S

for f, g, f1, 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)

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;

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);

end;
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 { (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M } ;

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;

:: 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 } ;

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;

ex b_{1} 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_{1} . (A,B) = a.e-eq-class ((a + b),M)

for b_{1}, b_{2} 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_{1} . (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_{2} . (A,B) = a.e-eq-class ((a + b),M) ) holds

b_{1} = b_{2}

end;
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 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);

ex b

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

proof end;

uniqueness for b

for a, b being PartFunc of X,REAL st a in A & b in B holds

b

for a, b being PartFunc of X,REAL st a in A & b in B holds

b

b

proof 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_{4} being BinOp of (CosetSet M) holds

( b_{4} = 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_{4} . (A,B) = a.e-eq-class ((a + b),M) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

for a, b being PartFunc of X,REAL st a in A & b in B holds

b

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

existence

ex b_{1} being Element of CosetSet M ex f being PartFunc of X,REAL st

( f = X --> 0 & f in L1_Functions M & b_{1} = a.e-eq-class (f,M) );

uniqueness

for b_{1}, b_{2} being Element of CosetSet M st ex f being PartFunc of X,REAL st

( f = X --> 0 & f in L1_Functions M & b_{1} = a.e-eq-class (f,M) ) & ex f being PartFunc of X,REAL st

( f = X --> 0 & f in L1_Functions M & b_{2} = a.e-eq-class (f,M) ) holds

b_{1} = b_{2};

end;
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 ex f being PartFunc of X,REAL st

( f = X --> 0 & f in L1_Functions M & it = a.e-eq-class (f,M) );

existence

ex b

( f = X --> 0 & f in L1_Functions M & b

uniqueness

for b

( f = X --> 0 & f in L1_Functions M & b

( f = X --> 0 & f in L1_Functions M & b

b

proof 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_{4} being Element of CosetSet M holds

( b_{4} = zeroCoset M iff ex f being PartFunc of X,REAL st

( f = X --> 0 & f in L1_Functions M & b_{4} = a.e-eq-class (f,M) ) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

( f = X --> 0 & f in L1_Functions M & b

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

ex b_{1} being Function of [:REAL,(CosetSet M):],(CosetSet M) st

for z being Real

for A being Element of CosetSet M

for f being PartFunc of X,REAL st f in A holds

b_{1} . (z,A) = a.e-eq-class ((z (#) f),M)

for b_{1}, b_{2} being Function of [:REAL,(CosetSet M):],(CosetSet M) st ( for z being Real

for A being Element of CosetSet M

for f being PartFunc of X,REAL st f in A holds

b_{1} . (z,A) = a.e-eq-class ((z (#) f),M) ) & ( for z being Real

for A being Element of CosetSet M

for f being PartFunc of X,REAL st f in A holds

b_{2} . (z,A) = a.e-eq-class ((z (#) f),M) ) holds

b_{1} = b_{2}

end;
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 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 for z being 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);

ex b

for z being Real

for A being Element of CosetSet M

for f being PartFunc of X,REAL st f in A holds

b

proof end;

uniqueness for b

for A being Element of CosetSet M

for f being PartFunc of X,REAL st f in A holds

b

for A being Element of CosetSet M

for f being PartFunc of X,REAL st f in A holds

b

b

proof 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_{4} being Function of [:REAL,(CosetSet M):],(CosetSet M) holds

( b_{4} = lmultCoset M iff for z being Real

for A being Element of CosetSet M

for f being PartFunc of X,REAL st f in A holds

b_{4} . (z,A) = a.e-eq-class ((z (#) f),M) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

for A being Element of CosetSet M

for f being PartFunc of X,REAL st f in A holds

b

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

ex b_{1} 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_{1} = CosetSet M & the addF of b_{1} = addCoset M & 0. b_{1} = zeroCoset M & the Mult of b_{1} = lmultCoset M )

for b_{1}, b_{2} 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_{1} = CosetSet M & the addF of b_{1} = addCoset M & 0. b_{1} = zeroCoset M & the Mult of b_{1} = lmultCoset M & the carrier of b_{2} = CosetSet M & the addF of b_{2} = addCoset M & 0. b_{2} = zeroCoset M & the Mult of b_{2} = lmultCoset M holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = CosetSet M & the addF of it = addCoset M & 0. it = zeroCoset M & the Mult of it = lmultCoset M );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: 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_{4} being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds

( b_{4} = Pre-L-Space M iff ( the carrier of b_{4} = CosetSet M & the addF of b_{4} = addCoset M & 0. b_{4} = zeroCoset M & the Mult of b_{4} = lmultCoset M ) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

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)

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 )

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)) )

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 )

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

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 )

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 Th48: :: LPSPACE1:48

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)) )

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;

ex b_{1} 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_{1} . x = Integral (M,(abs f)) )

for b_{1}, b_{2} 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_{1} . 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_{2} . x = Integral (M,(abs f)) ) ) holds

b_{1} = b_{2}

end;
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 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)) );

ex b

for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st

( f in x & b

proof end;

uniqueness for b

( f in x & b

( f in x & b

b

proof 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_{4} being Function of the carrier of (Pre-L-Space M),REAL holds

( b_{4} = 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_{4} . x = Integral (M,(abs f)) ) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

( f in x & b

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

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;
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) #);

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 ;

:: 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) #);

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 Th49: :: LPSPACE1:49

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.|| ) )

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 Th50: :: LPSPACE1:50

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)) )

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 Th51: :: LPSPACE1:51

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 ) )

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 Th52: :: LPSPACE1:52

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

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 Th53: :: LPSPACE1:53

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

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 Th54: :: LPSPACE1:54

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

for S being SigmaField of X

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

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

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)))

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;

( 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;
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;