let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real
for Sq being sequence of (Lp-Space (M,k)) ex Fsq being Functional_Sequence of X,REAL st
for n being Nat holds
( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st
( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )
let S be SigmaField of X; for M being sigma_Measure of S
for k being positive Real
for Sq being sequence of (Lp-Space (M,k)) ex Fsq being Functional_Sequence of X,REAL st
for n being Nat holds
( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st
( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )
let M be sigma_Measure of S; for k being positive Real
for Sq being sequence of (Lp-Space (M,k)) ex Fsq being Functional_Sequence of X,REAL st
for n being Nat holds
( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st
( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )
let k be positive Real; for Sq being sequence of (Lp-Space (M,k)) ex Fsq being Functional_Sequence of X,REAL st
for n being Nat holds
( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st
( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )
let Sq be sequence of (Lp-Space (M,k)); ex Fsq being Functional_Sequence of X,REAL st
for n being Nat holds
( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st
( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )
defpred S1[ Nat, set ] means ex f being PartFunc of X,REAL st
( $2 = f & f in Lp_Functions (M,k) & f in Sq . $1 & Sq . $1 = a.e-eq-class_Lp (f,M,k) & ex r being Real st
( r = Integral (M,((abs f) to_power k)) & ||.(Sq . $1).|| = r to_power (1 / k) ) );
A1:
for x being Element of NAT ex y being Element of PFuncs (X,REAL) st S1[x,y]
proof
let x be
Element of
NAT ;
ex y being Element of PFuncs (X,REAL) st S1[x,y]
consider y being
PartFunc of
X,
REAL such that A2:
(
y in Lp_Functions (
M,
k) &
Sq . x = a.e-eq-class_Lp (
y,
M,
k) )
by Th53;
ex
r being
Real st
(
0 <= r &
r = Integral (
M,
((abs y) to_power k)) &
||.(Sq . x).|| = r to_power (1 / k) )
by Th53, A2, Th38;
hence
ex
y being
Element of
PFuncs (
X,
REAL) st
S1[
x,
y]
by A2, Th38;
verum
end;
consider G being sequence of (PFuncs (X,REAL)) such that
A3:
for n being Element of NAT holds S1[n,G . n]
from FUNCT_2:sch 3(A1);
reconsider G = G as Functional_Sequence of X,REAL ;
now for n being Nat holds
( G . n in Lp_Functions (M,k) & G . n in Sq . n & Sq . n = a.e-eq-class_Lp ((G . n),M,k) & ex r being Real st
( r = Integral (M,((abs (G . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )let n be
Nat;
( G . n in Lp_Functions (M,k) & G . n in Sq . n & Sq . n = a.e-eq-class_Lp ((G . n),M,k) & ex r being Real st
( r = Integral (M,((abs (G . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )
n in NAT
by ORDINAL1:def 12;
then
ex
f being
PartFunc of
X,
REAL st
(
G . n = f &
f in Lp_Functions (
M,
k) &
f in Sq . n &
Sq . n = a.e-eq-class_Lp (
f,
M,
k) & ex
r being
Real st
(
r = Integral (
M,
((abs f) to_power k)) &
||.(Sq . n).|| = r to_power (1 / k) ) )
by A3;
hence
(
G . n in Lp_Functions (
M,
k) &
G . n in Sq . n &
Sq . n = a.e-eq-class_Lp (
(G . n),
M,
k) & ex
r being
Real st
(
r = Integral (
M,
((abs (G . n)) to_power k)) &
||.(Sq . n).|| = r to_power (1 / k) ) )
;
verum end;
hence
ex Fsq being Functional_Sequence of X,REAL st
for n being Nat holds
( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st
( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )
; verum