let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S holds L-1-Norm M = Lp-Norm (M,1)
let S be SigmaField of X; for M being sigma_Measure of S holds L-1-Norm M = Lp-Norm (M,1)
let M be sigma_Measure of S; L-1-Norm M = Lp-Norm (M,1)
A1:
the carrier of (Pre-L-Space M) = the carrier of (Pre-Lp-Space (M,1))
by Th75;
now for x being Element of the carrier of (Pre-L-Space M) holds (L-1-Norm M) . x = (Lp-Norm (M,1)) . xlet x be
Element of the
carrier of
(Pre-L-Space M);
(L-1-Norm M) . x = (Lp-Norm (M,1)) . x
x in the
carrier of
(Pre-L-Space M)
;
then
x in CosetSet M
by LPSPACE1:def 18;
then consider g being
PartFunc of
X,
REAL such that A2:
(
x = a.e-eq-class (
g,
M) &
g in L1_Functions M )
;
consider a being
PartFunc of
X,
REAL such that A3:
(
a in x &
(L-1-Norm M) . x = Integral (
M,
|.a.|) )
by LPSPACE1:def 19;
A4:
ex
p being
PartFunc of
X,
REAL st
(
a = p &
p in L1_Functions M &
g in L1_Functions M &
g a.e.= p,
M )
by A2, A3;
consider b being
PartFunc of
X,
REAL such that A5:
(
b in x & ex
r being
Real st
(
r = Integral (
M,
(|.b.| to_power 1)) &
(Lp-Norm (M,1)) . x = r to_power (1 / 1) ) )
by A1, Def12;
A6:
ex
q being
PartFunc of
X,
REAL st
(
b = q &
q in L1_Functions M &
g in L1_Functions M &
g a.e.= q,
M )
by A2, A5;
a a.e.= g,
M
by A4;
then
a a.e.= b,
M
by A6, LPSPACE1:30;
then A7:
Integral (
M,
|.a.|)
= Integral (
M,
|.b.|)
by A2, A3, A5, LPSPACE1:45;
|.b.| to_power 1
= |.b.|
by Th8;
hence
(L-1-Norm M) . x = (Lp-Norm (M,1)) . x
by A3, A5, A7, POWER:25;
verum end;
hence
L-1-Norm M = Lp-Norm (M,1)
by A1, FUNCT_2:63; verum