let n be Element of NAT ; for a, b, c, d, e being Real
for f being PartFunc of REAL,(REAL n) 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)).| <= (n * e) * |.(d - c).|
let a, b, c, d, e be Real; for f being PartFunc of REAL,(REAL n) 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)).| <= (n * e) * |.(d - c).|
let f be PartFunc of REAL,(REAL n); ( 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)).| <= (n * e) * |.(d - c).| )
assume 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'] & ( for x being Real st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) )
; |.(integral (f,c,d)).| <= (n * e) * |.(d - c).|
A2:
now for i being Element of NAT st i in Seg n holds
|.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).|let i be
Element of
NAT ;
( i in Seg n implies |.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).| )set P =
proj (
i,
n);
assume A3:
i in Seg n
;
|.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).|
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then
rng f c= dom (proj (i,n))
;
then A4:
['a,b'] c= dom ((proj (i,n)) * f)
by A1, RELAT_1:27;
set f1 =
(proj (i,n)) * f;
A5:
for
x being
Real st
x in ['(min (c,d)),(max (c,d))'] holds
|.(((proj (i,n)) * f) . x).| <= e
proof
let x be
Real;
( x in ['(min (c,d)),(max (c,d))'] implies |.(((proj (i,n)) * f) . x).| <= e )
assume A6:
x in ['(min (c,d)),(max (c,d))']
;
|.(((proj (i,n)) * f) . x).| <= e
['(min (c,d)),(max (c,d))'] c= ['a,b']
by A1, Lm2;
then A7:
x in dom ((proj (i,n)) * f)
by A4, A6;
then A8:
x in dom f
by FUNCT_1:11;
A9:
|.(f /. x).| <= e
by A1, A6;
A10:
((proj (i,n)) * f) . x =
(proj (i,n)) . (f . x)
by A7, FUNCT_1:12
.=
(proj (i,n)) . (f /. x)
by A8, PARTFUN1:def 6
;
( 1
<= i &
i <= n )
by A3, FINSEQ_1:1;
then
|.((proj (i,n)) . (f /. x)).| <= |.(f /. x).|
by PDIFF_8:5;
hence
|.(((proj (i,n)) * f) . x).| <= e
by A10, A9, XXREAL_0:2;
verum
end; A11:
(proj (i,n)) * f is_integrable_on ['a,b']
by A1, A3;
A12:
(proj (i,n)) * (f | ['a,b']) is
bounded
by A1, A3;
((proj (i,n)) * f) | ['a,b'] = (proj (i,n)) * (f | ['a,b'])
by RELAT_1:83;
hence
|.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).|
by A12, A1, A4, A5, A11, Lm4;
verum end;
now for i being Element of NAT st 1 <= i & i <= n holds
|.((integral (f,c,d)) . i).| <= e * |.(d - c).|let i be
Element of
NAT ;
( 1 <= i & i <= n implies |.((integral (f,c,d)) . i).| <= e * |.(d - c).| )set P =
proj (
i,
n);
assume
( 1
<= i &
i <= n )
;
|.((integral (f,c,d)) . i).| <= e * |.(d - c).|then A13:
i in Seg n
;
then
|.(integral (((proj (i,n)) * f),c,d)).| <= e * |.(d - c).|
by A2;
hence
|.((integral (f,c,d)) . i).| <= e * |.(d - c).|
by A13, INTEGR15:def 18;
verum end;
then
|.(integral (f,c,d)).| <= n * (e * |.(d - c).|)
by PDIFF_8:15;
hence
|.(integral (f,c,d)).| <= (n * e) * |.(d - c).|
; verum