let Y be RealBanachSpace; for a, b, c, d, e being Real
for f being continuous PartFunc of REAL, the carrier of Y st [.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 a, b, c, d, e be Real; for f being continuous PartFunc of REAL, the carrier of Y st [.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 continuous PartFunc of REAL, the carrier of Y; ( [.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.] 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).|
X0:
( a <= c & c <= b )
by A1, XXREAL_1:1;
then X3:
a <= b
by XXREAL_0:2;
X1:
[.a,b.] = ['a,b']
by X0, XXREAL_0:2, INTEGRA5:def 3;
rng ||.f.|| c= REAL
;
then A3:
||.f.|| is Function of (dom ||.f.||),REAL
by FUNCT_2:2;
( min (c,d) <= c & c <= max (c,d) )
by XXREAL_0:17, XXREAL_0:25;
then X2:
['(min (c,d)),(max (c,d))'] = [.(min (c,d)),(max (c,d)).]
by XXREAL_0:2, INTEGRA5:def 3;
dom ||.f.|| = dom f
by NORMSP_0:def 2;
then A4:
['(min (c,d)),(max (c,d))'] c= dom ||.f.||
by A1, X0, XXREAL_0:2, X1, INTEGR19:3;
then reconsider g = ||.f.|| | ['(min (c,d)),(max (c,d))'] as Function of ['(min (c,d)),(max (c,d))'],REAL by A3, FUNCT_2:32;
A5:
vol ['(min (c,d)),(max (c,d))'] = |.(d - c).|
by INTEGRA6:6;
A6:
||.f.|| is_integrable_on ['(min (c,d)),(max (c,d))']
by A1, X3, X1, INTEGR21:22;
consider h being Function of ['(min (c,d)),(max (c,d))'],REAL such that
A7:
rng h = {e}
and
A8:
h | ['(min (c,d)),(max (c,d))'] is bounded
by INTEGRA4:5;
A9:
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 A10:
x in ['(min (c,d)),(max (c,d))']
;
g . x <= h . xthen
g . x = ||.f.|| . x
by FUNCT_1:49;
then A11:
g . x = ||.(f /. x).||
by A10, A4, NORMSP_0:def 3;
h . x in {e}
by A7, A10, FUNCT_2:4;
then
h . x = e
by TARSKI:def 1;
hence
g . x <= h . x
by A11, A2, A10, X2;
verum end;
A12:
||.(integral (f,c,d)).|| <= integral (||.f.||,(min (c,d)),(max (c,d)))
by A1, X1, X3, INTEGR21:22;
( min (c,d) <= c & c <= max (c,d) )
by XXREAL_0:17, XXREAL_0:25;
then A13:
integral (||.f.||,(min (c,d)),(max (c,d))) = integral (||.f.||,['(min (c,d)),(max (c,d))'])
by INTEGRA5:def 4, XXREAL_0:2;
A14:
g | ['(min (c,d)),(max (c,d))'] is bounded
by A1, X1, X3, INTEGR21:22;
( h is integrable & integral h = e * (vol ['(min (c,d)),(max (c,d))']) )
by A7, INTEGRA4:4;
then
integral (||.f.||,(min (c,d)),(max (c,d))) <= e * |.(d - c).|
by A13, A8, A9, A6, A14, A5, INTEGRA2:34;
hence
||.(integral (f,c,d)).|| <= e * |.(d - c).|
by A12, XXREAL_0:2; verum