let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
( abs f is integrable & abs (integral f) <= integral (abs f) )
let f be Function of A,REAL ; :: thesis: ( f | A is bounded & f is integrable implies ( abs f is integrable & abs (integral f) <= integral (abs f) ) )
assume that
A1: f | A is bounded and
A2: f is integrable ; :: thesis: ( abs f is integrable & abs (integral f) <= integral (abs f) )
( max+ f is total & max- f is total ) by Th13;
then A3: ( max+ f is Function of A,REAL & max- f is Function of A,REAL ) ;
( f | A is bounded_above & f | A is bounded_below ) by A1;
then ( (max+ f) | A is bounded_above & (max+ f) | A is bounded_below & (max- f) | A is bounded_above & (max- f) | A is bounded_below ) by Th14, Th15, Th16, Th17;
then A4: ( (max+ f) | A is bounded & (max- f) | A is bounded ) ;
A5: ( max+ f is integrable & max- f is integrable ) by A1, A2, Th20, Th22;
then (max+ f) + (max- f) is integrable by A3, A4, INTEGRA1:59;
hence abs f is integrable by RFUNCT_3:37; :: thesis: abs (integral f) <= integral (abs f)
A6: (integral (max+ f)) + (integral (max- f)) = integral ((max+ f) + (max- f)) by A3, A4, A5, INTEGRA1:59
.= integral (abs f) by RFUNCT_3:37 ;
A7: (integral (max+ f)) - (integral (max- f)) = integral ((max+ f) - (max- f)) by A3, A4, A5, INTEGRA2:33
.= integral f by RFUNCT_3:37 ;
A8: for x being Real st x in A holds
(max+ f) . x >= 0 by RFUNCT_3:40;
for x being Real st x in A holds
(max- f) . x >= 0 by RFUNCT_3:43;
then A9: ( integral (max+ f) >= 0 & integral (max- f) >= 0 ) by A3, A4, A5, A8, INTEGRA2:32;
(integral (abs f)) - (integral f) = 2 * (integral (max- f)) by A6, A7;
then (integral (abs f)) - (integral f) >= 0 by A9;
then A10: integral (abs f) >= integral f by XREAL_1:51;
(integral (abs f)) + (integral f) = 2 * (integral (max+ f)) by A6, A7;
then (integral (abs f)) + (integral f) >= 0 by A9;
then - (integral (abs f)) <= integral f by XREAL_1:63;
hence abs (integral f) <= integral (abs f) by A10, ABSVALUE:12; :: thesis: verum