let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for f being Real-Valued-Random-Variable of Sigma
for r being Real st 0 <= r holds
(abs f) to_power r is Real-Valued-Random-Variable of Sigma
let Sigma be SigmaField of Omega; :: thesis: for f being Real-Valued-Random-Variable of Sigma
for r being Real st 0 <= r holds
(abs f) to_power r is Real-Valued-Random-Variable of Sigma
let f be Real-Valued-Random-Variable of Sigma; :: thesis: for r being Real st 0 <= r holds
(abs f) to_power r is Real-Valued-Random-Variable of Sigma
let r be Real; :: thesis: ( 0 <= r implies (abs f) to_power r is Real-Valued-Random-Variable of Sigma )
assume A1: 0 <= r ; :: thesis: (abs f) to_power r is Real-Valued-Random-Variable of Sigma
abs f is nonnegative by Lm12;
hence (abs f) to_power r is Real-Valued-Random-Variable of Sigma by A1, Th23; :: thesis: verum