let a, b, c, d, e be Real; for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(f . x).| <= e ) holds
|.(integral (f,c,d)).| <= e * |.(d - c).|
let f be PartFunc of REAL,REAL; ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & ( for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(f . x).| <= e ) implies |.(integral (f,c,d)).| <= e * |.(d - c).| )
set A = ['(min (c,d)),(max (c,d))'];
assume that
A1:
( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] )
and
A2:
for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(f . x).| <= e
; |.(integral (f,c,d)).| <= e * |.(d - c).|
rng (abs f) c= REAL
;
then A3:
abs f is Function of (dom (abs f)),REAL
by FUNCT_2:2;
['(min (c,d)),(max (c,d))'] c= dom (abs f)
by A1, INTEGRA6:21;
then reconsider g = (abs f) | ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by A3, FUNCT_2:32;
A4:
vol ['(min (c,d)),(max (c,d))'] = |.(d - c).|
by INTEGRA6:6;
abs f is_integrable_on ['(min (c,d)),(max (c,d))']
by A1, INTEGRA6:21;
then A5:
g is integrable
;
consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that
A6:
rng h = {e}
and
A7:
h | ['(min (c,d)),(max (c,d))'] is bounded
by INTEGRA4:5;
A8:
now for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
g . x <= h . xlet x be
Real;
( x in ['(min (c,d)),(max (c,d))'] implies g . x <= h . x )assume A9:
x in ['(min (c,d)),(max (c,d))']
;
g . x <= h . xthen
g . x = (abs f) . x
by FUNCT_1:49;
then A10:
g . x = |.(f . x).|
by VALUED_1:18;
h . x in {e}
by A6, A9, FUNCT_2:4;
then
h . x = e
by TARSKI:def 1;
hence
g . x <= h . x
by A2, A9, A10;
verum end;
A11:
|.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d)))
by A1, INTEGRA6:21;
( min (c,d) <= c & c <= max (c,d) )
by XXREAL_0:17, XXREAL_0:25;
then
min (c,d) <= max (c,d)
by XXREAL_0:2;
then A12:
integral ((abs f),(min (c,d)),(max (c,d))) = integral ((abs f),['(min (c,d)),(max (c,d))'])
by INTEGRA5:def 4;
(abs f) | ['(min (c,d)),(max (c,d))'] is bounded
by A1, INTEGRA6:21;
then A13:
g | ['(min (c,d)),(max (c,d))'] is bounded
;
( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) )
by A6, INTEGRA4:4;
then
integral ((abs f),(min (c,d)),(max (c,d))) <= e * |.(d - c).|
by A12, A7, A8, A5, A13, A4, INTEGRA2:34;
hence
|.(integral (f,c,d)).| <= e * |.(d - c).|
by A11, XXREAL_0:2; verum