let X be non empty set ; :: thesis: 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 RealLinearSpace-like & 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 )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is RealLinearSpace-like & 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 )
let M be sigma_Measure of S; :: thesis: ( L-1-Space M is RealNormSpace-like & L-1-Space M is RealLinearSpace-like & 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 )
now let x,
y be
Point of
(L-1-Space M);
:: thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (L-1-Space M) ) & ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )let a be
Real;
:: thesis: ( ( ||.x.|| = 0 implies x = 0. (L-1-Space M) ) & ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )hereby :: thesis: ( ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
assume A2:
||.x.|| = 0
;
:: thesis: x = 0. (L-1-Space M)reconsider x1 =
x as
Point of
(Pre-L-Space M) ;
consider f being
PartFunc of
X,
REAL such that A3:
f in x1
and
(L-1-Norm M) . x1 = Integral M,
(abs f)
by Def20;
A4:
Integral M,
(abs f) = 0
by A2, A3, Lm17x;
set g =
X --> 0 ;
A6:
(
f in L1_Functions M &
f is_integrable_on M )
by Lm16, A3;
then A5:
f a.e.= X --> 0 ,
M
by A4, Lm261;
A8:
X --> 0 in L1_Functions M
by LmDef1;
A7:
a.e-eq-class (X --> 0 ),
M = a.e-eq-class f,
M
by A5, A6, A8, EQC02;
a.e-eq-class f,
M in CosetSet M
by A6;
then
zeroCoset M = a.e-eq-class f,
M
by VSPDef4X, A7, A8;
then
0. (Pre-L-Space M) = a.e-eq-class f,
M
by VSPDef6X;
hence
x = 0. (L-1-Space M)
by A3, Lm17z;
:: thesis: verum
end; consider f being
PartFunc of
X,
REAL such that A15:
(
f in x &
||.x.|| = Integral M,
(abs f) )
by Def20;
consider g being
PartFunc of
X,
REAL such that A16:
(
g in y &
||.y.|| = Integral M,
(abs g) )
by Def20;
A17:
(
f in L1_Functions M &
f is_integrable_on M )
by Lm16, A15;
then
|.(Integral M,f).| <= Integral M,
(abs f)
by MESFUNC6:95;
hence
0 <= ||.x.||
by A15, EXTREAL2:51;
:: thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
f + g in x + y
by Lm17Y, A15, A16;
then A20:
||.(x + y).|| = Integral M,
(abs (f + g))
by Lm17x;
A21:
(Integral M,(abs f)) + (Integral M,(abs g)) = ||.x.|| + ||.y.||
by A15, A16, SUPINF_2:1;
(
g in L1_Functions M &
g is_integrable_on M )
by Lm16, A16;
hence
||.(x + y).|| <= ||.x.|| + ||.y.||
by Lm263, A20, A21, A17;
:: thesis: ||.(a * x).|| = (abs a) * ||.x.||A25:
a (#) f in a * x
by Lm17Y, A15;
abs f is_integrable_on M
by Lm16, A15;
then
Integral M,
((abs a) (#) (abs f)) = (R_EAL (abs a)) * (Integral M,(abs f))
by MESFUNC6:102;
then
Integral M,
(abs (a (#) f)) = (R_EAL (abs a)) * (Integral M,(abs f))
by RFUNCT_1:37;
then
Integral M,
(abs (a (#) f)) = (abs a) * ||.x.||
by A15, EXTREAL1:13;
hence
||.(a * x).|| = (abs a) * ||.x.||
by A25, Lm17x;
:: thesis: verum end;
hence
( L-1-Space M is RealNormSpace-like & L-1-Space M is RealLinearSpace-like & 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 NORMSP_1:def 2, RSSPACE3:4; :: thesis: verum