:: deftheorem defines Lp_Functions LPSPACE2:def 2 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real holds Lp_Functions (M,k) = { f where f is PartFunc of X,REAL : ex Ef being Element of S st
( M . (Ef `) = 0 & dom f = Ef & f is Ef -measurable & (abs f) to_power k is_integrable_on M ) } ;