let X be 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 m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) holds
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) holds
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
let M be sigma_Measure of S; for f, g being PartFunc of X,REAL
for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) holds
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
let f, g be PartFunc of X,REAL; for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) holds
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
let m, n be positive Real; ( (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) implies ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) )
assume A1:
( (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) )
; ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
then A2:
( m > 1 & n > 1 )
by Th1;
consider f1 being PartFunc of X,REAL such that
A3:
( f = f1 & ex NDf being Element of S st
( M . (NDf `) = 0 & dom f1 = NDf & f1 is NDf -measurable & (abs f1) to_power m is_integrable_on M ) )
by A1;
consider EDf being Element of S such that
A4:
( M . (EDf `) = 0 & dom f1 = EDf & f1 is EDf -measurable )
by A3;
consider g1 being PartFunc of X,REAL such that
A5:
( g = g1 & ex NDg being Element of S st
( M . (NDg `) = 0 & dom g1 = NDg & g1 is NDg -measurable & (abs g1) to_power n is_integrable_on M ) )
by A1;
consider EDg being Element of S such that
A6:
( M . (EDg `) = 0 & dom g1 = EDg & g1 is EDg -measurable )
by A5;
set u = (abs f1) to_power m;
set v = (abs g1) to_power n;
A7:
( 0 <= Integral (M,((abs f1) to_power m)) & 0 <= Integral (M,((abs g1) to_power n)) )
by A3, A5, A1, Th49;
reconsider s1 = Integral (M,((abs f1) to_power m)), s2 = Integral (M,((abs g1) to_power n)) as Element of REAL by A3, A5, A1, Th49;
A8:
( dom f1 = dom (abs f1) & dom g1 = dom (abs g1) )
by VALUED_1:def 11;
reconsider Nf = EDf ` , Ng = EDg ` as Element of S by MEASURE1:34;
set t1 = s1 to_power (1 / m);
set t2 = s2 to_power (1 / n);
set E = EDf /\ EDg;
A9:
(EDf /\ EDg) ` = (EDf `) \/ (EDg `)
by XBOOLE_1:54;
( Nf is measure_zero of M & Ng is measure_zero of M )
by A4, A6, MEASURE1:def 7;
then A10:
(EDf /\ EDg) ` is measure_zero of M
by A9, MEASURE1:37;
A11:
dom (f1 (#) g1) = EDf /\ EDg
by A4, A6, VALUED_1:def 4;
( f1 is EDf /\ EDg -measurable & g1 is EDf /\ EDg -measurable )
by A4, A6, MESFUNC6:16, XBOOLE_1:17;
then A12:
f1 (#) g1 is EDf /\ EDg -measurable
by A4, A6, MESFUN7C:31;
A13:
f1 (#) g1 in L1_Functions M
by A1, A3, A5, Th59;
then A14:
ex fg1 being PartFunc of X,REAL st
( fg1 = f1 (#) g1 & ex ND being Element of S st
( M . ND = 0 & dom fg1 = ND ` & fg1 is_integrable_on M ) )
;
then A15:
( Integral (M,(abs (f1 (#) g1))) in REAL & abs (f1 (#) g1) is_integrable_on M )
by LPSPACE1:44;
per cases
( ( s1 = 0 & s2 >= 0 ) or ( s1 > 0 & s2 = 0 ) or ( s1 <> 0 & s2 <> 0 ) )
by A3, A5, A1, Th49;
suppose A16:
(
s1 = 0 &
s2 >= 0 )
;
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
f1 in Lp_Functions (
M,
m)
by A3;
then
f1 a.e.= X --> 0,
M
by A16, Th57;
then consider Nf1 being
Element of
S such that A17:
(
M . Nf1 = 0 &
f1 | (Nf1 `) = (X --> 0) | (Nf1 `) )
;
reconsider Z =
((EDf /\ EDg) \ Nf1) ` as
Element of
S by MEASURE1:34;
A18:
((EDf /\ EDg) \ Nf1) ` = ((EDf /\ EDg) `) \/ Nf1
by SUBSET_1:14;
Nf1 is
measure_zero of
M
by A17, MEASURE1:def 7;
then
Z is
measure_zero of
M
by A10, A18, MEASURE1:37;
then A19:
M . Z = 0
by MEASURE1:def 7;
dom (X --> 0) = X
by FUNCOP_1:13;
then A20:
dom ((X --> 0) | (Z `)) = Z `
by RELAT_1:62;
A21:
dom ((f1 (#) g1) | (Z `)) = Z `
by A11, RELAT_1:62, XBOOLE_1:36;
for
x being
object st
x in dom ((f1 (#) g1) | (Z `)) holds
((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x
then
(f1 (#) g1) | (Z `) = (X --> 0) | (Z `)
by A20, A21, FUNCT_1:def 11;
then A25:
f1 (#) g1 a.e.= X --> 0,
M
by A19;
X --> 0 in L1_Functions M
by Th56;
then
Integral (
M,
(abs (f1 (#) g1)))
= Integral (
M,
(abs (X --> 0)))
by A13, A25, LPSPACE1:45;
then A26:
Integral (
M,
(abs (f1 (#) g1)))
= 0
by LPSPACE1:54;
(s1 to_power (1 / m)) * (s2 to_power (1 / n)) = 0 * (s2 to_power (1 / n))
by A16, POWER:def 2;
hence
ex
r1 being
Real st
(
r1 = Integral (
M,
((abs f) to_power m)) & ex
r2 being
Real st
(
r2 = Integral (
M,
((abs g) to_power n)) &
Integral (
M,
(abs (f (#) g)))
<= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
by A3, A5, A26;
verum end; suppose A27:
(
s1 > 0 &
s2 = 0 )
;
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
g1 in Lp_Functions (
M,
n)
by A5;
then
g1 a.e.= X --> 0,
M
by A27, Th57;
then consider Ng1 being
Element of
S such that A28:
(
M . Ng1 = 0 &
g1 | (Ng1 `) = (X --> 0) | (Ng1 `) )
;
reconsider Z =
((EDf /\ EDg) \ Ng1) ` as
Element of
S by MEASURE1:34;
A29:
((EDf /\ EDg) \ Ng1) ` = ((EDf /\ EDg) `) \/ Ng1
by SUBSET_1:14;
Ng1 is
measure_zero of
M
by A28, MEASURE1:def 7;
then
Z is
measure_zero of
M
by A10, A29, MEASURE1:37;
then A30:
M . Z = 0
by MEASURE1:def 7;
dom (X --> 0) = X
by FUNCOP_1:13;
then A31:
dom ((X --> 0) | (Z `)) = Z `
by RELAT_1:62;
A32:
dom ((f1 (#) g1) | (Z `)) = Z `
by A11, RELAT_1:62, XBOOLE_1:36;
for
x being
object st
x in dom ((f1 (#) g1) | (Z `)) holds
((f1 (#) g1) | (Z `)) . x = ((X --> 0) | (Z `)) . x
then
(f1 (#) g1) | (Z `) = (X --> 0) | (Z `)
by A31, A32, FUNCT_1:def 11;
then A36:
f1 (#) g1 a.e.= X --> 0,
M
by A30;
X --> 0 in L1_Functions M
by Th56;
then
Integral (
M,
(abs (f1 (#) g1)))
= Integral (
M,
(abs (X --> 0)))
by A13, A36, LPSPACE1:45;
then A37:
Integral (
M,
(abs (f1 (#) g1)))
= 0
by LPSPACE1:54;
(s1 to_power (1 / m)) * (s2 to_power (1 / n)) = (s1 to_power (1 / m)) * 0
by A27, POWER:def 2;
hence
ex
r1 being
Real st
(
r1 = Integral (
M,
((abs f) to_power m)) & ex
r2 being
Real st
(
r2 = Integral (
M,
((abs g) to_power n)) &
Integral (
M,
(abs (f (#) g)))
<= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
by A3, A5, A37;
verum end; suppose A38:
(
s1 <> 0 &
s2 <> 0 )
;
ex r1 being Real st
( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )then A39:
(
s1 to_power (1 / m) > 0 &
s2 to_power (1 / n) > 0 )
by A7, POWER:34;
then A40:
|.(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))).| = 1
/ ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))
by ABSVALUE:def 1;
set w =
(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1);
set F =
(1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m);
set G =
(1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n);
set z =
((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n));
A41:
(
dom ((1 / (s1 to_power (1 / m))) (#) (abs f1)) = dom (abs f1) &
dom ((1 / (s2 to_power (1 / n))) (#) (abs g1)) = dom (abs g1) )
by VALUED_1:def 5;
(
dom ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) = dom (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) &
dom ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) = dom (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) )
by VALUED_1:def 5;
then A42:
(
dom ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) = dom (abs f1) &
dom ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) = dom (abs g1) )
by A41, MESFUN6C:def 4;
then A43:
dom (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) = (dom (abs f1)) /\ (dom (abs g1))
by VALUED_1:def 1;
(
((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m = ((1 / (s1 to_power (1 / m))) to_power m) (#) ((abs f1) to_power m) &
((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n = ((1 / (s2 to_power (1 / n))) to_power n) (#) ((abs g1) to_power n) )
by A39, Th19;
then A44:
(
((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m is_integrable_on M &
((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n is_integrable_on M )
by A3, A5, MESFUNC6:102;
then A45:
(
(1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) is_integrable_on M &
(1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) is_integrable_on M )
by MESFUNC6:102;
then A46:
((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) is_integrable_on M
by MESFUNC6:100;
A47:
dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = dom (f1 (#) g1)
by VALUED_1:def 5;
then A48:
dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = (dom f1) /\ (dom g1)
by VALUED_1:def 4;
dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))) = dom (abs (f1 (#) g1))
by VALUED_1:def 5;
then A49:
dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))) = dom (f1 (#) g1)
by VALUED_1:def 11;
A50:
(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1) is
EDf /\ EDg -measurable
by A11, A12, MESFUNC6:21;
for
x being
Element of
X st
x in dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) holds
|.(((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x).| <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x
proof
let x be
Element of
X;
( x in dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) implies |.(((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x).| <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x )
assume A51:
x in dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1))
;
|.(((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x).| <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x
(
(abs f1) . x >= 0 &
(abs g1) . x >= 0 )
by MESFUNC6:51;
then A52:
((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) * ((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) <= ((((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) to_power m) / m) + ((((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) to_power n) / n)
by A1, A2, A39, HOLDER_1:5;
dom ((abs f1) (#) (abs g1)) = (dom (abs f1)) /\ (dom (abs g1))
by VALUED_1:def 4;
then A53:
((abs f1) (#) (abs g1)) . x = ((abs f1) . x) * ((abs g1) . x)
by A8, A48, A51, VALUED_1:def 4;
A54:
((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) * ((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) =
(((1 / (s1 to_power (1 / m))) * (1 / (s2 to_power (1 / n)))) * ((abs f1) . x)) * ((abs g1) . x)
.=
((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * ((abs f1) . x)) * ((abs g1) . x)
by XCMPLX_1:102
.=
(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * (((abs f1) (#) (abs g1)) . x)
by A53
.=
(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * ((abs (f1 (#) g1)) . x)
by RFUNCT_1:24
.=
((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))) . x
by A47, A51, A49, VALUED_1:def 5
.=
(abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1))) . x
by A40, RFUNCT_1:25
;
A55:
(
(1 / (s1 to_power (1 / m))) * ((abs f1) . x) = ((1 / (s1 to_power (1 / m))) (#) (abs f1)) . x &
(1 / (s2 to_power (1 / n))) * ((abs g1) . x) = ((1 / (s2 to_power (1 / n))) (#) (abs g1)) . x )
by VALUED_1:6;
(
dom (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) = dom f1 &
dom (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) = dom g1 )
by A8, A41, MESFUN6C:def 4;
then
(
x in dom (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) &
x in dom (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) )
by A48, A51, XBOOLE_0:def 4;
then
(
(((1 / (s1 to_power (1 / m))) (#) (abs f1)) . x) to_power m = (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) . x &
(((1 / (s2 to_power (1 / n))) (#) (abs g1)) . x) to_power n = (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) . x )
by MESFUN6C:def 4;
then
(
((((1 / (s1 to_power (1 / m))) (#) (abs f1)) . x) to_power m) / m = ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) . x &
((((1 / (s2 to_power (1 / n))) (#) (abs g1)) . x) to_power n) / n = ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) . x )
by VALUED_1:6;
then
((((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) to_power m) / m) + ((((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) to_power n) / n) = (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x
by A8, A48, A51, A43, A55, VALUED_1:def 1;
hence
|.(((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x).| <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x
by A52, A54, VALUED_1:18;
verum
end; then A56:
Integral (
M,
(abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1))))
<= Integral (
M,
(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))))
by A4, A6, A46, A8, A48, A43, A50, MESFUNC6:96;
consider E1 being
Element of
S such that A57:
(
E1 = (dom ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m))) /\ (dom ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) &
Integral (
M,
(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))))
= (Integral (M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) | E1))) + (Integral (M,(((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) | E1))) )
by A45, MESFUNC6:101;
(
EDf = X /\ EDf &
EDg = X /\ EDg )
by XBOOLE_1:28;
then A58:
(
EDf = X \ Nf &
EDg = X \ Ng )
by XBOOLE_1:48;
A59:
EDf \ (EDf /\ EDg) =
EDf \ EDg
by XBOOLE_1:47
.=
((X \ Nf) \ X) \/ ((X \ Nf) /\ Ng)
by A58, XBOOLE_1:52
.=
(X \ (Nf \/ X)) \/ ((X \ Nf) /\ Ng)
by XBOOLE_1:41
.=
(X \ X) \/ ((X \ Nf) /\ Ng)
by XBOOLE_1:12
.=
{} \/ ((X \ Nf) /\ Ng)
by XBOOLE_1:37
;
A60:
EDg \ (EDf /\ EDg) =
EDg \ EDf
by XBOOLE_1:47
.=
((X \ Ng) \ X) \/ ((X \ Ng) /\ Nf)
by A58, XBOOLE_1:52
.=
(X \ (Ng \/ X)) \/ ((X \ Ng) /\ Nf)
by XBOOLE_1:41
.=
(X \ X) \/ ((X \ Ng) /\ Nf)
by XBOOLE_1:12
.=
{} \/ ((X \ Ng) /\ Nf)
by XBOOLE_1:37
;
set NF =
EDf /\ Ng;
set NG =
EDg /\ Nf;
(
Nf is
measure_zero of
M &
Ng is
measure_zero of
M )
by A4, A6, MEASURE1:def 7;
then
(
EDf /\ Ng is
measure_zero of
M &
EDg /\ Nf is
measure_zero of
M )
by MEASURE1:36, XBOOLE_1:17;
then A61:
(
M . (EDf /\ Ng) = 0 &
M . (EDg /\ Nf) = 0 )
by MEASURE1:def 7;
(
EDf /\ EDg = EDf /\ (EDf /\ EDg) &
EDf /\ EDg = EDg /\ (EDf /\ EDg) )
by XBOOLE_1:17, XBOOLE_1:28;
then A62:
(
EDf /\ EDg = EDf \ (EDf /\ Ng) &
EDf /\ EDg = EDg \ (EDg /\ Nf) )
by A58, A59, A60, XBOOLE_1:48;
R_EAL ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) is_integrable_on M
by A45;
then
ex
E being
Element of
S st
(
E = dom (R_EAL ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m))) &
R_EAL ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) is
E -measurable )
;
then A63:
(1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) is
EDf -measurable
by A42, A8, A4;
R_EAL ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) is_integrable_on M
by A45;
then
ex
E being
Element of
S st
(
E = dom (R_EAL ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) &
R_EAL ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) is
E -measurable )
;
then A64:
(1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) is
EDg -measurable
by A42, A8, A6;
(1 / (s1 to_power (1 / m))) to_power m = (s1 to_power (1 / m)) to_power (- m)
by A38, A7, POWER:32, POWER:34;
then
(1 / (s1 to_power (1 / m))) to_power m = s1 to_power ((1 / m) * (- m))
by A7, A38, POWER:33;
then
(1 / (s1 to_power (1 / m))) to_power m = s1 to_power (- ((1 * (1 / m)) * m))
;
then
(1 / (s1 to_power (1 / m))) to_power m = s1 to_power (- 1)
by XCMPLX_1:106;
then
(1 / (s1 to_power (1 / m))) to_power m = (1 / s1) to_power 1
by A7, A38, POWER:32;
then A65:
(1 / (s1 to_power (1 / m))) to_power m = 1
/ s1
by POWER:25;
A66:
(
(1 / s1) * s1 = 1 &
(1 / s2) * s2 = 1 )
by A38, XCMPLX_1:106;
A67:
(1 / (s2 to_power (1 / n))) to_power n =
(s2 to_power (1 / n)) to_power (- n)
by A38, A7, POWER:32, POWER:34
.=
s2 to_power ((1 / n) * (- n))
by A7, A38, POWER:33
.=
s2 to_power (- ((1 * (1 / n)) * n))
.=
s2 to_power (- 1)
by XCMPLX_1:106
.=
(1 / s2) to_power 1
by A7, A38, POWER:32
.=
1
/ s2
by POWER:25
;
A68:
Integral (
M,
(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) | (EDf /\ EDg))) =
Integral (
M,
((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)))
by A4, A8, A42, A62, A61, A63, MESFUNC6:89
.=
(1 / m) * (Integral (M,(((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)))
by A44, MESFUNC6:102
.=
(1 / m) * (Integral (M,(((1 / (s1 to_power (1 / m))) to_power m) (#) ((abs f1) to_power m))))
by A39, Th19
.=
(1 / m) * (((1 / (s1 to_power (1 / m))) to_power m) * (Integral (M,((abs f1) to_power m))))
by A3, MESFUNC6:102
.=
1
/ m
by A65, A66, XXREAL_3:81
;
A69:
Integral (
M,
(((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) | (EDf /\ EDg))) =
Integral (
M,
((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)))
by A6, A8, A42, A62, A61, A64, MESFUNC6:89
.=
(1 / n) * (Integral (M,(((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)))
by A44, MESFUNC6:102
.=
(1 / n) * (Integral (M,(((1 / (s2 to_power (1 / n))) to_power n) (#) ((abs g1) to_power n))))
by A39, Th19
.=
(1 / n) * (((1 / (s2 to_power (1 / n))) to_power n) * (Integral (M,((abs g1) to_power n))))
by A5, MESFUNC6:102
.=
1
/ n
by A66, A67, XXREAL_3:81
;
reconsider n1 = 1
/ n,
m1 = 1
/ m as
Real ;
A70:
Integral (
M,
(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)))) =
(Integral (M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) | (EDf /\ EDg)))) + (Integral (M,(((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) | (EDf /\ EDg))))
by A42, A4, A6, A8, A57
.=
m1 + n1
by A69, A68, SUPINF_2:1
.=
jj
by A1
;
abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = |.(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))).| (#) (abs (f1 (#) g1))
by RFUNCT_1:25;
then
abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))
by A39, ABSVALUE:def 1;
then A71:
Integral (
M,
(abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1))))
= (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * (Integral (M,(abs (f1 (#) g1))))
by A15, MESFUNC6:102;
reconsider c1 =
Integral (
M,
(abs (f1 (#) g1))) as
Element of
REAL by A14, LPSPACE1:44;
(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * (Integral (M,(abs (f1 (#) g1)))) = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * c1
;
then
(1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * (Integral (M,(abs (f1 (#) g1)))) = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * c1
;
then
((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * c1) <= ((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * 1
by A39, A56, A71, A70, XREAL_1:64;
then A72:
(((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))))) * c1 <= (s1 to_power (1 / m)) * (s2 to_power (1 / n))
;
((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) = 1
by A39, XCMPLX_1:106;
hence
ex
r1 being
Real st
(
r1 = Integral (
M,
((abs f) to_power m)) & ex
r2 being
Real st
(
r2 = Integral (
M,
((abs g) to_power n)) &
Integral (
M,
(abs (f (#) g)))
<= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
by A3, A5, A72;
verum end;