theorem Th60: :: LPSPACE2:60

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