:: INTEGR19 semantic presentation
begin
Lm1: for n being Element of NAT
for f, g being PartFunc of REAL,(REAL n) holds f - g = f + (- g)
by NDIFF_4:1;
theorem Th1: :: INTEGR19:1
for a, c, b being real number st a <= c & c <= b holds
( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
proof
let a, c, b be real number ; ::_thesis: ( a <= c & c <= b implies ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) )
assume that
A1: a <= c and
A2: c <= b ; ::_thesis: ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
A3: c in [.a,b.] by A1, A2, XXREAL_1:1;
hence c in ['a,b'] by A1, A2, INTEGRA5:def_3, XXREAL_0:2; ::_thesis: ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] )
A4: ['c,b'] = [.c,b.] by A2, INTEGRA5:def_3;
a <= b by A1, A2, XXREAL_0:2;
then A5: ( a in [.a,b.] & b in [.a,b.] ) by XXREAL_1:1;
( ['a,b'] = [.a,b.] & ['a,c'] = [.a,c.] ) by A1, A2, INTEGRA5:def_3, XXREAL_0:2;
hence ( ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) by A4, A3, A5, XXREAL_2:def_12; ::_thesis: verum
end;
theorem Th2: :: INTEGR19:2
for X being set
for a, c, d, b being real number st a <= c & c <= d & d <= b & ['a,b'] c= X holds
['c,d'] c= X
proof
let X be set ; ::_thesis: for a, c, d, b being real number st a <= c & c <= d & d <= b & ['a,b'] c= X holds
['c,d'] c= X
let a, c, d, b be real number ; ::_thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= X implies ['c,d'] c= X )
assume that
A1: ( a <= c & c <= d & d <= b ) and
A2: ['a,b'] c= X ; ::_thesis: ['c,d'] c= X
A3: ['c,d'] c= ['c,b'] by Th1, A1;
c <= b by A1, XXREAL_0:2;
then ['c,b'] c= ['a,b'] by Th1, A1;
then ['c,d'] c= ['a,b'] by A3, XBOOLE_1:1;
hence ['c,d'] c= X by A2, XBOOLE_1:1; ::_thesis: verum
end;
Lm2: for a, b, c, d being real number st a <= b & c in ['a,b'] & d in ['a,b'] holds
['(min (c,d)),(max (c,d))'] c= ['a,b']
proof
let a, b, c, d be real number ; ::_thesis: ( a <= b & c in ['a,b'] & d in ['a,b'] implies ['(min (c,d)),(max (c,d))'] c= ['a,b'] )
assume A1: ( a <= b & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ['(min (c,d)),(max (c,d))'] c= ['a,b']
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A2: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1;
percases ( c <= d or not c <= d ) ;
supposeA3: c <= d ; ::_thesis: ['(min (c,d)),(max (c,d))'] c= ['a,b']
then A4: ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def_9, XXREAL_0:def_10;
A5: ['c,b'] c= ['a,b'] by A2, Th1;
['c,d'] c= ['c,b'] by A2, A3, Th1;
hence ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A4, A5, XBOOLE_1:1; ::_thesis: verum
end;
supposeA6: not c <= d ; ::_thesis: ['(min (c,d)),(max (c,d))'] c= ['a,b']
then A7: ( d = min (c,d) & c = max (c,d) ) by XXREAL_0:def_9, XXREAL_0:def_10;
A8: ['d,b'] c= ['a,b'] by A2, Th1;
['d,c'] c= ['d,b'] by A2, A6, Th1;
hence ['(min (c,d)),(max (c,d))'] c= ['a,b'] by A7, A8, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
theorem Th3: :: INTEGR19:3
for X being set
for a, b, c, d being real number st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= X holds
['(min (c,d)),(max (c,d))'] c= X
proof
let X be set ; ::_thesis: for a, b, c, d being real number st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= X holds
['(min (c,d)),(max (c,d))'] c= X
let a, b, c, d be real number ; ::_thesis: ( a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= X implies ['(min (c,d)),(max (c,d))'] c= X )
assume ( a <= b & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( not ['a,b'] c= X or ['(min (c,d)),(max (c,d))'] c= X )
then ['(min (c,d)),(max (c,d))'] c= ['a,b'] by Lm2;
hence ( not ['a,b'] c= X or ['(min (c,d)),(max (c,d))'] c= X ) by XBOOLE_1:1; ::_thesis: verum
end;
theorem Th4: :: INTEGR19:4
for n being Element of NAT
for a, c, d, b being real number
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
['c,d'] c= dom (f + g)
proof
let n be Element of NAT ; ::_thesis: for a, c, d, b being real number
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
['c,d'] c= dom (f + g)
let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
['c,d'] c= dom (f + g)
let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g implies ['c,d'] c= dom (f + g) )
assume that
A1: ( a <= c & c <= d & d <= b ) and
A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) ; ::_thesis: ['c,d'] c= dom (f + g)
dom (f + g) = (dom f) /\ (dom g) by VALUED_2:def_45;
then ['a,b'] /\ ['a,b'] c= dom (f + g) by A2, XBOOLE_1:27;
hence ['c,d'] c= dom (f + g) by A1, Th2; ::_thesis: verum
end;
theorem Th5: :: INTEGR19:5
for n being Element of NAT
for a, c, d, b being real number
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
['c,d'] c= dom (f - g)
proof
let n be Element of NAT ; ::_thesis: for a, c, d, b being real number
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
['c,d'] c= dom (f - g)
let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds
['c,d'] c= dom (f - g)
let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g implies ['c,d'] c= dom (f - g) )
assume that
A1: ( a <= c & c <= d & d <= b ) and
A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) ; ::_thesis: ['c,d'] c= dom (f - g)
dom (f - g) = (dom f) /\ (dom g) by VALUED_2:def_46;
then ['a,b'] /\ ['a,b'] c= dom (f - g) by A2, XBOOLE_1:27;
hence ['c,d'] c= dom (f - g) by A1, Th2; ::_thesis: verum
end;
Lm3: for X, Y, Z being non empty set
for f being PartFunc of X,Y st Z c= dom f holds
f | Z is Function of Z,Y
proof
let X, Y, Z be non empty set ; ::_thesis: for f being PartFunc of X,Y st Z c= dom f holds
f | Z is Function of Z,Y
let f be PartFunc of X,Y; ::_thesis: ( Z c= dom f implies f | Z is Function of Z,Y )
rng f c= Y ;
then f is Function of (dom f),Y by FUNCT_2:2;
hence ( Z c= dom f implies f | Z is Function of Z,Y ) by FUNCT_2:32; ::_thesis: verum
end;
theorem Th6: :: INTEGR19:6
for a, c, d, b, r being real number
for f being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
proof
let a, c, d, b, r be real number ; ::_thesis: for f being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
let f be PartFunc of REAL,REAL; ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded ) )
assume that
A1: a <= c and
A2: ( c <= d & d <= b ) and
A3: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) and
A4: ['a,b'] c= dom f ; ::_thesis: ( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
A5: r is Real by XREAL_0:def_1;
A6: f | ['c,d'] is bounded by A1, A2, A3, A4, INTEGRA6:18;
A7: ['c,d'] c= dom f by A2, A1, Th2, A4;
f is_integrable_on ['c,d'] by A1, A2, A3, A4, INTEGRA6:18;
hence r (#) f is_integrable_on ['c,d'] by A6, A7, A5, INTEGRA6:9; ::_thesis: (r (#) f) | ['c,d'] is bounded
thus (r (#) f) | ['c,d'] is bounded by A6, RFUNCT_1:80; ::_thesis: verum
end;
theorem :: INTEGR19:7
for a, c, d, b being real number
for f, g being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded )
proof
let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,REAL st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded )
let f, g be PartFunc of REAL,REAL; ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g implies ( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded ) )
assume A1: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g ) ; ::_thesis: ( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded )
A2: ((- 1) (#) g) | ['a,b'] is bounded by A1, RFUNCT_1:80;
A3: ['a,b'] c= dom ((- 1) (#) g) by A1, VALUED_1:def_5;
- 1 is Real by XREAL_0:def_1;
then (- 1) (#) g is_integrable_on ['a,b'] by A1, INTEGRA6:9;
hence ( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded ) by A1, A2, A3, INTEGRA6:19; ::_thesis: verum
end;
Lm4: for a, b, c, d, e being real number
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 number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ) holds
abs (integral (f,c,d)) <= e * (abs (d - c))
proof
let a, b, c, d, e be real number ; ::_thesis: 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 number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ) holds
abs (integral (f,c,d)) <= e * (abs (d - c))
let f be PartFunc of REAL,REAL; ::_thesis: ( 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 number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ) implies abs (integral (f,c,d)) <= e * (abs (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 number st x in ['(min (c,d)),(max (c,d))'] holds
abs (f . x) <= e ; ::_thesis: abs (integral (f,c,d)) <= e * (abs (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))'] = abs (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 by INTEGRA5:def_1;
e is Real by XREAL_0:def_1;
then 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__::_thesis:_for_x_being_Real_st_x_in_['(min_(c,d)),(max_(c,d))']_holds_
g_._x_<=_h_._x
let x be Real; ::_thesis: ( x in ['(min (c,d)),(max (c,d))'] implies g . x <= h . x )
assume A9: x in ['(min (c,d)),(max (c,d))'] ; ::_thesis: g . x <= h . x
then g . x = (abs f) . x by FUNCT_1:49;
then A10: g . x = abs (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; ::_thesis: verum
end;
A11: abs (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 ;
e is Real by XREAL_0:def_1;
then ( 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 * (abs (d - c)) by A12, A7, A8, A5, A13, A4, INTEGRA2:34;
hence abs (integral (f,c,d)) <= e * (abs (d - c)) by A11, XXREAL_0:2; ::_thesis: verum
end;
Lm5: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f holds
f | A is Function of A,REAL
by Lm3;
theorem :: INTEGR19:8
for n being Element of NAT
for a, b, c being real number
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'] holds
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
proof
let n be Element of NAT ; ::_thesis: for a, b, c being real number
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'] holds
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
let a, b, c be real number ; ::_thesis: 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'] holds
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] implies ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) ; ::_thesis: ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(_(proj_(i,n))_*_f_is_integrable_on_['a,c']_&_(proj_(i,n))_*_f_is_integrable_on_['c,b']_&_integral_(((proj_(i,n))_*_f),a,b)_=_(integral_(((proj_(i,n))_*_f),a,c))_+_(integral_(((proj_(i,n))_*_f),c,b))_)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) ) )
set P = proj (i,n);
assume A3: i in Seg n ; ::_thesis: ( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) )
then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, INTEGR15:def_16;
(proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15;
then A5: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
hence ( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) ) by A4, A5, A1, INTEGRA6:17; ::_thesis: verum
end;
then for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on ['a,c'] ;
hence f is_integrable_on ['a,c'] by INTEGR15:def_16; ::_thesis: ( f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on ['c,b'] by A2;
hence f is_integrable_on ['c,b'] by INTEGR15:def_16; ::_thesis: integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))
A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_(f,a,b))_holds_
(integral_(f,a,b))_._i_=_((integral_(f,a,c))_+_(integral_(f,c,b)))_._i
let i be Nat; ::_thesis: ( i in dom (integral (f,a,b)) implies (integral (f,a,b)) . i = ((integral (f,a,c)) + (integral (f,c,b))) . i )
assume i in dom (integral (f,a,b)) ; ::_thesis: (integral (f,a,b)) . i = ((integral (f,a,c)) + (integral (f,c,b))) . i
then A7: i in Seg n by INTEGR15:def_18;
set P = proj (i,n);
thus (integral (f,a,b)) . i = integral (((proj (i,n)) * f),a,b) by A7, INTEGR15:def_18
.= (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) by A7, A2
.= ((integral (f,a,c)) . i) + (integral (((proj (i,n)) * f),c,b)) by A7, INTEGR15:def_18
.= ((integral (f,a,c)) . i) + ((integral (f,c,b)) . i) by A7, INTEGR15:def_18
.= ((integral (f,a,c)) + (integral (f,c,b))) . i by RVSUM_1:11 ; ::_thesis: verum
end;
A8: Seg n = dom (integral (f,a,b)) by INTEGR15:def_18;
len ((integral (f,a,c)) + (integral (f,c,b))) = n by CARD_1:def_7;
then Seg n = dom ((integral (f,a,c)) + (integral (f,c,b))) by FINSEQ_1:def_3;
hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A8, A6, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th9: :: INTEGR19:9
for n being Element of NAT
for a, c, d, b being real number
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
proof
let n be Element of NAT ; ::_thesis: for a, c, d, b being real number
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
let a, c, d, b be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded ) )
assume A1: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f ) ; ::_thesis: ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(_(proj_(i,n))_*_f_is_integrable_on_['c,d']_&_(proj_(i,n))_*_(f_|_['c,d'])_is_bounded_)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (proj (i,n)) * f is_integrable_on ['c,d'] & (proj (i,n)) * (f | ['c,d']) is bounded ) )
set P = proj (i,n);
assume A3: i in Seg n ; ::_thesis: ( (proj (i,n)) * f is_integrable_on ['c,d'] & (proj (i,n)) * (f | ['c,d']) is bounded )
then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, INTEGR15:def_16;
(proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15;
then A5: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
then ( (proj (i,n)) * f is_integrable_on ['c,d'] & ((proj (i,n)) * f) | ['c,d'] is bounded & ['c,d'] c= dom ((proj (i,n)) * f) ) by A4, A5, A1, INTEGRA6:18;
hence ( (proj (i,n)) * f is_integrable_on ['c,d'] & (proj (i,n)) * (f | ['c,d']) is bounded ) by RELAT_1:83; ::_thesis: verum
end;
then for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on ['c,d'] ;
hence f is_integrable_on ['c,d'] by INTEGR15:def_16; ::_thesis: f | ['c,d'] is bounded
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * (f | ['c,d']) is bounded by A2;
hence f | ['c,d'] is bounded by INTEGR15:def_15; ::_thesis: verum
end;
theorem Th10: :: INTEGR19:10
for n being Element of NAT
for a, c, d, b being real number
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
proof
let n be Element of NAT ; ::_thesis: for a, c, d, b being real number
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g implies ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded ) )
assume that
A1: ( a <= c & c <= d & d <= b ) and
A2: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded ) and
A3: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) ; ::_thesis: ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded )
A4: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(_(proj_(i,n))_*_(f_+_g)_is_integrable_on_['c,d']_&_(proj_(i,n))_*_((f_+_g)_|_['c,d'])_is_bounded_)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (proj (i,n)) * (f + g) is_integrable_on ['c,d'] & (proj (i,n)) * ((f + g) | ['c,d']) is bounded ) )
set P = proj (i,n);
assume A5: i in Seg n ; ::_thesis: ( (proj (i,n)) * (f + g) is_integrable_on ['c,d'] & (proj (i,n)) * ((f + g) | ['c,d']) is bounded )
then A6: (proj (i,n)) * f is_integrable_on ['a,b'] by A2, INTEGR15:def_16;
(proj (i,n)) * (f | ['a,b']) is bounded by A5, A2, INTEGR15:def_15;
then A7: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
A8: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then A9: dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
A10: (proj (i,n)) * g is_integrable_on ['a,b'] by A5, A2, INTEGR15:def_16;
(proj (i,n)) * (g | ['a,b']) is bounded by A5, A2, INTEGR15:def_15;
then A11: ((proj (i,n)) * g) | ['a,b'] is bounded by RELAT_1:83;
rng g c= dom (proj (i,n)) by A8;
then dom ((proj (i,n)) * g) = dom g by RELAT_1:27;
then A12: ( ((proj (i,n)) * f) + ((proj (i,n)) * g) is_integrable_on ['c,d'] & (((proj (i,n)) * f) + ((proj (i,n)) * g)) | ['c,d'] is bounded ) by A1, A3, A6, A7, A9, A10, A11, INTEGRA6:19;
(((proj (i,n)) * f) + ((proj (i,n)) * g)) | ['c,d'] = ((proj (i,n)) * (f + g)) | ['c,d'] by INTEGR15:15
.= (proj (i,n)) * ((f + g) | ['c,d']) by RELAT_1:83 ;
hence ( (proj (i,n)) * (f + g) is_integrable_on ['c,d'] & (proj (i,n)) * ((f + g) | ['c,d']) is bounded ) by A12, INTEGR15:15; ::_thesis: verum
end;
then for i being Element of NAT st i in Seg n holds
(proj (i,n)) * (f + g) is_integrable_on ['c,d'] ;
hence f + g is_integrable_on ['c,d'] by INTEGR15:def_16; ::_thesis: (f + g) | ['c,d'] is bounded
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * ((f + g) | ['c,d']) is bounded by A4;
hence (f + g) | ['c,d'] is bounded by INTEGR15:def_15; ::_thesis: verum
end;
theorem Th11: :: INTEGR19:11
for n being Element of NAT
for a, c, d, b, r being real number
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
proof
let n be Element of NAT ; ::_thesis: for a, c, d, b, r being real number
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
let a, c, d, b, r be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded ) )
assume that
A1: ( a <= c & c <= d & d <= b ) and
A2: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) and
A3: ['a,b'] c= dom f ; ::_thesis: ( r (#) f is_integrable_on ['c,d'] & (r (#) f) | ['c,d'] is bounded )
A4: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(_(proj_(i,n))_*_(r_(#)_f)_is_integrable_on_['c,d']_&_(proj_(i,n))_*_((r_(#)_f)_|_['c,d'])_is_bounded_)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (proj (i,n)) * (r (#) f) is_integrable_on ['c,d'] & (proj (i,n)) * ((r (#) f) | ['c,d']) is bounded ) )
set P = proj (i,n);
assume A5: i in Seg n ; ::_thesis: ( (proj (i,n)) * (r (#) f) is_integrable_on ['c,d'] & (proj (i,n)) * ((r (#) f) | ['c,d']) is bounded )
then A6: (proj (i,n)) * f is_integrable_on ['a,b'] by A2, INTEGR15:def_16;
(proj (i,n)) * (f | ['a,b']) is bounded by A5, A2, INTEGR15:def_15;
then A7: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then A8: dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
A9: ( r (#) ((proj (i,n)) * f) is_integrable_on ['c,d'] & (r (#) ((proj (i,n)) * f)) | ['c,d'] is bounded ) by A1, A3, Th6, A6, A7, A8;
A10: r is Real by XREAL_0:def_1;
then (r (#) ((proj (i,n)) * f)) | ['c,d'] = ((proj (i,n)) * (r (#) f)) | ['c,d'] by INTEGR15:16
.= (proj (i,n)) * ((r (#) f) | ['c,d']) by RELAT_1:83 ;
hence ( (proj (i,n)) * (r (#) f) is_integrable_on ['c,d'] & (proj (i,n)) * ((r (#) f) | ['c,d']) is bounded ) by A10, A9, INTEGR15:16; ::_thesis: verum
end;
then for i being Element of NAT st i in Seg n holds
(proj (i,n)) * (r (#) f) is_integrable_on ['c,d'] ;
hence r (#) f is_integrable_on ['c,d'] by INTEGR15:def_16; ::_thesis: (r (#) f) | ['c,d'] is bounded
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * ((r (#) f) | ['c,d']) is bounded by A4;
hence (r (#) f) | ['c,d'] is bounded by INTEGR15:def_15; ::_thesis: verum
end;
theorem Th12: :: INTEGR19:12
for n being Element of NAT
for a, c, d, b being real number
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( - f is_integrable_on ['c,d'] & (- f) | ['c,d'] is bounded )
proof
let n be Element of NAT ; ::_thesis: for a, c, d, b being real number
for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( - f is_integrable_on ['c,d'] & (- f) | ['c,d'] is bounded )
let a, c, d, b be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
( - f is_integrable_on ['c,d'] & (- f) | ['c,d'] is bounded )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( - f is_integrable_on ['c,d'] & (- f) | ['c,d'] is bounded ) )
- f = (- 1) (#) f by NFCONT_4:7;
hence ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f implies ( - f is_integrable_on ['c,d'] & (- f) | ['c,d'] is bounded ) ) by Th11; ::_thesis: verum
end;
theorem Th13: :: INTEGR19:13
for n being Element of NAT
for a, c, d, b being real number
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded )
proof
let n be Element of NAT ; ::_thesis: for a, c, d, b being real number
for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded )
let a, c, d, b be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded )
let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g implies ( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded ) )
assume that
A1: ( a <= c & c <= d & d <= b ) and
A2: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded ) and
A3: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) ; ::_thesis: ( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded )
A4: dom g = dom (- g) by NFCONT_4:def_3;
A5: f - g = f + (- g) by Lm1;
a <= d by A1, XXREAL_0:2;
then a <= b by A1, XXREAL_0:2;
then ( - g is_integrable_on ['a,b'] & (- g) | ['a,b'] is bounded ) by A2, A3, Th12;
hence ( f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded ) by A5, A1, A2, A3, A4, Th10; ::_thesis: verum
end;
theorem Th14: :: INTEGR19:14
for A being non empty closed_interval Subset of REAL
for n being non empty Element of NAT
for f being Function of A,(REAL n) holds
( f is bounded iff |.f.| is bounded )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for n being non empty Element of NAT
for f being Function of A,(REAL n) holds
( f is bounded iff |.f.| is bounded )
let n be non empty Element of NAT ; ::_thesis: for f being Function of A,(REAL n) holds
( f is bounded iff |.f.| is bounded )
let f be Function of A,(REAL n); ::_thesis: ( f is bounded iff |.f.| is bounded )
hereby ::_thesis: ( |.f.| is bounded implies f is bounded )
assume A1: f is bounded ; ::_thesis: |.f.| is bounded
defpred S1[ Nat, set ] means ex K being Element of REAL st
( 0 <= K & K = $2 & ( for y being set st y in dom ((proj ($1,n)) * f) holds
abs (((proj ($1,n)) * f) . y) < K ) );
A2: for i being Nat st i in Seg n holds
ex r being Element of REAL st S1[i,r]
proof
let i be Nat; ::_thesis: ( i in Seg n implies ex r being Element of REAL st S1[i,r] )
assume A3: i in Seg n ; ::_thesis: ex r being Element of REAL st S1[i,r]
set P = proj (i,n);
(proj (i,n)) * f is bounded by A1, A3, INTEGR15:def_12;
then consider L being real number such that
A4: for y being set st y in dom ((proj (i,n)) * f) holds
abs (((proj (i,n)) * f) . y) < L by COMSEQ_2:def_3;
now__::_thesis:_for_y_being_set_st_y_in_dom_((proj_(i,n))_*_f)_holds_
abs_(((proj_(i,n))_*_f)_._y)_<_abs_L
let y be set ; ::_thesis: ( y in dom ((proj (i,n)) * f) implies abs (((proj (i,n)) * f) . y) < abs L )
assume A5: y in dom ((proj (i,n)) * f) ; ::_thesis: abs (((proj (i,n)) * f) . y) < abs L
L <= abs L by ABSVALUE:4;
hence abs (((proj (i,n)) * f) . y) < abs L by A4, A5, XXREAL_0:2; ::_thesis: verum
end;
hence ex r being Element of REAL st S1[i,r] by COMPLEX1:46; ::_thesis: verum
end;
consider w being FinSequence of REAL such that
A6: ( dom w = Seg n & ( for i being Nat st i in Seg n holds
S1[i,w . i] ) ) from FINSEQ_1:sch_5(A2);
A7: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(_0_<=_w_._i_&_(_for_y_being_set_st_y_in_dom_((proj_(i,n))_*_f)_holds_
abs_(((proj_(i,n))_*_f)_._y)_<_w_._i_)_)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds
abs (((proj (i,n)) * f) . y) < w . i ) ) )
set P = proj (i,n);
assume i in Seg n ; ::_thesis: ( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds
abs (((proj (i,n)) * f) . y) < w . i ) )
then S1[i,w . i] by A6;
hence ( 0 <= w . i & ( for y being set st y in dom ((proj (i,n)) * f) holds
abs (((proj (i,n)) * f) . y) < w . i ) ) ; ::_thesis: verum
end;
len w = n by A6, FINSEQ_1:def_3;
then reconsider w = w as Element of REAL n by FINSEQ_2:92;
A8: for i being Element of NAT st i in Seg n holds
0 <= w . i by A7;
set KK = Sum w;
for y being set st y in dom |.f.| holds
abs (|.f.| . y) < (n * (Sum w)) + 1
proof
let y be set ; ::_thesis: ( y in dom |.f.| implies abs (|.f.| . y) < (n * (Sum w)) + 1 )
assume A9: y in dom |.f.| ; ::_thesis: abs (|.f.| . y) < (n * (Sum w)) + 1
then A10: |.f.| . y = |.f.| /. y by PARTFUN1:def_6
.= |.(f /. y).| by A9, NFCONT_4:def_2 ;
then A11: abs (|.f.| . y) = |.f.| . y by ABSVALUE:def_1;
now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_
|.((proj_(i,n))_._(f_/._y)).|_<=_Sum_w
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies |.((proj (i,n)) . (f /. y)).| <= Sum w )
set P = proj (i,n);
assume A12: ( 1 <= i & i <= n ) ; ::_thesis: |.((proj (i,n)) . (f /. y)).| <= Sum w
A13: y in dom f by A9, NFCONT_4:def_2;
then f . y in rng f by FUNCT_1:3;
then f . y in REAL n ;
then f . y in dom (proj (i,n)) by FUNCT_2:def_1;
then A14: y in dom ((proj (i,n)) * f) by A13, FUNCT_1:11;
A15: i in Seg n by A12;
then abs (((proj (i,n)) * f) . y) < w . i by A7, A14;
then abs ((proj (i,n)) . (f . y)) < w . i by A14, FUNCT_1:12;
then A16: |.((proj (i,n)) . (f /. y)).| < w . i by A13, PARTFUN1:def_6;
w . i <= Sum w by A8, A15, REAL_NS1:7;
hence |.((proj (i,n)) . (f /. y)).| <= Sum w by A16, XXREAL_0:2; ::_thesis: verum
end;
then |.(f /. y).| <= n * (Sum w) by PDIFF_8:17;
then 0 + (abs (|.f.| . y)) < (n * (Sum w)) + 1 by A10, A11, XREAL_1:8;
hence abs (|.f.| . y) < (n * (Sum w)) + 1 ; ::_thesis: verum
end;
hence |.f.| is bounded by COMSEQ_2:def_3; ::_thesis: verum
end;
assume |.f.| is bounded ; ::_thesis: f is bounded
then consider K being real number such that
A17: for y being set st y in dom |.f.| holds
abs (|.f.| . y) < K by COMSEQ_2:def_3;
let i be Element of NAT ; :: according to INTEGR15:def_12 ::_thesis: ( not i in Seg n or (proj (i,n)) * f is bounded )
set P = proj (i,n);
assume A18: i in Seg n ; ::_thesis: (proj (i,n)) * f is bounded
for y being set st y in dom ((proj (i,n)) * f) holds
abs (((proj (i,n)) * f) . y) < K
proof
let y be set ; ::_thesis: ( y in dom ((proj (i,n)) * f) implies abs (((proj (i,n)) * f) . y) < K )
assume A19: y in dom ((proj (i,n)) * f) ; ::_thesis: abs (((proj (i,n)) * f) . y) < K
then A20: y in dom f by FUNCT_1:11;
A21: ((proj (i,n)) * f) . y = (proj (i,n)) . (f . y) by A19, FUNCT_1:12
.= (proj (i,n)) . (f /. y) by A20, PARTFUN1:def_6 ;
( 1 <= i & i <= n ) by A18, FINSEQ_1:1;
then A22: |.((proj (i,n)) . (f /. y)).| <= |.(f /. y).| by PDIFF_8:5;
A23: y in dom |.f.| by A20, NFCONT_4:def_2;
then abs (|.f.| . y) < K by A17;
then abs (|.f.| /. y) < K by A23, PARTFUN1:def_6;
then abs |.(f /. y).| < K by A23, NFCONT_4:def_2;
then |.(f /. y).| < K by ABSVALUE:def_1;
hence abs (((proj (i,n)) * f) . y) < K by A21, A22, XXREAL_0:2; ::_thesis: verum
end;
hence (proj (i,n)) * f is bounded by COMSEQ_2:def_3; ::_thesis: verum
end;
Lm6: for n being Element of NAT
for E being Element of REAL n
for p being FinSequence of REAL n st ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds
E = Sum p
proof
let n be Element of NAT ; ::_thesis: for E being Element of REAL n
for p being FinSequence of REAL n st ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds
E = Sum p
let E be Element of REAL n; ::_thesis: for p being FinSequence of REAL n st ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds
E = Sum p
defpred S1[ Element of NAT ] means for p being FinSequence of REAL n
for r being Element of REAL n st len p = $1 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum p;
A1: S1[ 0 ]
proof
let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n st len p = 0 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum p
let r be Element of REAL n; ::_thesis: ( len p = 0 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum p )
assume A2: ( len p = 0 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum p
A3: p = {} by A2;
len r = n by CARD_1:def_7;
then A4: dom r = Seg n by FINSEQ_1:def_3;
A5: dom ((Seg n) --> 0) = Seg n by FUNCOP_1:13;
A6: now__::_thesis:_for_x_being_set_st_x_in_dom_r_holds_
r_._x_=_((Seg_n)_-->_0)_._x
let x be set ; ::_thesis: ( x in dom r implies r . x = ((Seg n) --> 0) . x )
assume A7: x in dom r ; ::_thesis: r . x = ((Seg n) --> 0) . x
then reconsider i = x as Element of NAT ;
set P = proj (i,n);
consider Pi being FinSequence of REAL such that
A8: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A2, A4, A7;
r . x = 0 by A3, A8, RVSUM_1:72;
hence r . x = ((Seg n) --> 0) . x by A4, A7, FUNCOP_1:7; ::_thesis: verum
end;
Sum p = 0* n by A2, EUCLID_7:def_11;
hence r = Sum p by A6, A4, A5, FUNCT_1:2; ::_thesis: verum
end;
A9: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A10: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_p_being_FinSequence_of_REAL_n
for_r_being_Element_of_REAL_n_st_len_p_=_k_+_1_&_(_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
ex_Pi_being_FinSequence_of_REAL_st_
(_Pi_=_(proj_(i,n))_*_p_&_r_._i_=_Sum_Pi_)_)_holds_
r_=_Sum_p
let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n st len p = k + 1 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum p
let r be Element of REAL n; ::_thesis: ( len p = k + 1 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum p )
assume A11: ( len p = k + 1 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum p
set p1 = p | k;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom p by A11, FINSEQ_1:def_3;
then p . (k + 1) in rng p by FUNCT_1:3;
then reconsider pk1 = p . (k + 1) as Element of REAL n ;
defpred S2[ Nat, set ] means ex P1i being FinSequence of REAL st
( P1i = (proj ($1,n)) * (p | k) & $2 = Sum P1i );
A12: for i being Nat st i in Seg n holds
ex r being Element of REAL st S2[i,r]
proof
let i be Nat; ::_thesis: ( i in Seg n implies ex r being Element of REAL st S2[i,r] )
assume i in Seg n ; ::_thesis: ex r being Element of REAL st S2[i,r]
take Sum ((proj (i,n)) * (p | k)) ; ::_thesis: S2[i, Sum ((proj (i,n)) * (p | k))]
thus S2[i, Sum ((proj (i,n)) * (p | k))] ; ::_thesis: verum
end;
consider r1 being FinSequence of REAL such that
A13: ( dom r1 = Seg n & ( for i being Nat st i in Seg n holds
S2[i,r1 . i] ) ) from FINSEQ_1:sch_5(A12);
len r1 = n by A13, FINSEQ_1:def_3;
then reconsider r1 = r1 as Element of REAL n by FINSEQ_2:92;
A14: for i being Element of NAT st i in Seg n holds
ex P1i being FinSequence of REAL st
( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A13;
A15: k <= len p by A11, NAT_1:16;
then A16: len (p | k) = k by FINSEQ_1:59;
A17: len r = n by CARD_1:def_7;
A18: len (r1 + pk1) = n by CARD_1:def_7;
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_n_holds_
r_._i_=_(r1_+_pk1)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= n implies r . i = (r1 + pk1) . i )
set P = proj (i,n);
assume ( 1 <= i & i <= n ) ; ::_thesis: r . i = (r1 + pk1) . i
then A19: i in Seg n by FINSEQ_1:1;
consider Pi being FinSequence of REAL such that
A20: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A19, A11;
consider P1i being FinSequence of REAL such that
A21: ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A19, A13;
A22: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then A23: rng p c= dom (proj (i,n)) ;
A24: dom Pi = dom p by A23, A20, RELAT_1:27
.= Seg (len p) by FINSEQ_1:def_3 ;
A25: len p = (len (p | k)) + (len <*(pk1 . i)*>) by A11, A16, FINSEQ_1:40;
A26: rng (p | k) c= dom (proj (i,n)) by A22;
A27: dom P1i = dom (p | k) by A26, A21, RELAT_1:27
.= Seg (len (p | k)) by FINSEQ_1:def_3 ;
then A28: len P1i = len (p | k) by FINSEQ_1:def_3;
A29: dom Pi = Seg ((len P1i) + (len <*(pk1 . i)*>)) by A24, A25, A27, FINSEQ_1:def_3;
len (p | k) <= len p by A15, FINSEQ_1:59;
then A30: Seg (len (p | k)) c= Seg (len p) by FINSEQ_1:5;
A31: for k being Nat st k in dom P1i holds
Pi . k = P1i . k
proof
let k be Nat; ::_thesis: ( k in dom P1i implies Pi . k = P1i . k )
assume A32: k in dom P1i ; ::_thesis: Pi . k = P1i . k
then A33: k in dom (p | k) by A27, FINSEQ_1:def_3;
thus P1i . k = (proj (i,n)) . ((p | k) . k) by A21, A32, FUNCT_1:12
.= (proj (i,n)) . (p . k) by A33, FUNCT_1:47
.= Pi . k by A20, A32, A24, A27, A30, FUNCT_1:12 ; ::_thesis: verum
end;
for k being Nat st k in dom <*(pk1 . i)*> holds
Pi . ((len P1i) + k) = <*(pk1 . i)*> . k
proof
let j be Nat; ::_thesis: ( j in dom <*(pk1 . i)*> implies Pi . ((len P1i) + j) = <*(pk1 . i)*> . j )
assume j in dom <*(pk1 . i)*> ; ::_thesis: Pi . ((len P1i) + j) = <*(pk1 . i)*> . j
then j in Seg (len <*(pk1 . i)*>) by FINSEQ_1:def_3;
then j in Seg 1 by FINSEQ_1:40;
then A34: j = 1 by FINSEQ_1:2, TARSKI:def_1;
hence Pi . ((len P1i) + j) = (proj (i,n)) . (p . (k + 1)) by A20, A24, A11, A28, A16, FINSEQ_1:4, FUNCT_1:12
.= pk1 . i by PDIFF_1:def_1
.= <*(pk1 . i)*> . j by A34, FINSEQ_1:40 ;
::_thesis: verum
end;
then Pi = P1i ^ <*(pk1 . i)*> by A31, A29, FINSEQ_1:def_7;
hence r . i = (r1 . i) + (pk1 . i) by A20, A21, RVSUM_1:74
.= (r1 + pk1) . i by RVSUM_1:11 ;
::_thesis: verum
end;
then A35: r = r1 + pk1 by A17, A18, FINSEQ_1:14;
ex v being Element of REAL n st
( v = p . (len p) & Sum p = (Sum (p | k)) + v ) by A16, A11, PDIFF_6:15;
hence r = Sum p by A11, A35, A10, A14, A16; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A36: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A9);
let p be FinSequence of REAL n; ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) implies E = Sum p )
assume A37: for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ; ::_thesis: E = Sum p
len p = len p ;
hence E = Sum p by A37, A36; ::_thesis: verum
end;
Lm7: for n being Element of NAT
for E being Element of REAL n
for p being FinSequence of REAL n
for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds
|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds
|.E.| <= Sum q
proof
let n be Element of NAT ; ::_thesis: for E being Element of REAL n
for p being FinSequence of REAL n
for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds
|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds
|.E.| <= Sum q
let E be Element of REAL n; ::_thesis: for p being FinSequence of REAL n
for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds
|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds
|.E.| <= Sum q
let p be FinSequence of REAL n; ::_thesis: for q being FinSequence of REAL st len p = len q & ( for j being Nat st j in dom p holds
|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds
|.E.| <= Sum q
let q be FinSequence of REAL ; ::_thesis: ( len p = len q & ( for j being Nat st j in dom p holds
|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) implies |.E.| <= Sum q )
assume A1: ( len p = len q & ( for j being Nat st j in dom p holds
|.(p /. j).| <= q /. j ) & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) ) ; ::_thesis: |.E.| <= Sum q
then A2: E = Sum p by Lm6;
defpred S1[ Nat, set ] means ex v being Element of REAL n st
( v = p . $1 & $2 = |.v.| );
A3: for i being Nat st i in Seg (len p) holds
ex x being Element of REAL st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len p) implies ex x being Element of REAL st S1[i,x] )
assume i in Seg (len p) ; ::_thesis: ex x being Element of REAL st S1[i,x]
then A4: i in dom p by FINSEQ_1:def_3;
take |.(p /. i).| ; ::_thesis: S1[i,|.(p /. i).|]
thus S1[i,|.(p /. i).|] by A4, PARTFUN1:def_6; ::_thesis: verum
end;
consider u being FinSequence of REAL such that
A5: ( dom u = Seg (len p) & ( for i being Nat st i in Seg (len p) holds
S1[i,u . i] ) ) from FINSEQ_1:sch_5(A3);
A6: for i being Element of NAT st i in dom p holds
ex v being Element of REAL n st
( v = p . i & u . i = |.v.| )
proof
let i be Element of NAT ; ::_thesis: ( i in dom p implies ex v being Element of REAL n st
( v = p . i & u . i = |.v.| ) )
assume i in dom p ; ::_thesis: ex v being Element of REAL n st
( v = p . i & u . i = |.v.| )
then i in Seg (len p) by FINSEQ_1:def_3;
hence ex v being Element of REAL n st
( v = p . i & u . i = |.v.| ) by A5; ::_thesis: verum
end;
A7: len u = len p by A5, FINSEQ_1:def_3;
then A8: |.(Sum p).| <= Sum u by A6, PDIFF_6:17;
set i = len p;
reconsider uu = u as Element of (len p) -tuples_on REAL by A7, FINSEQ_2:92;
reconsider qq = q as Element of (len p) -tuples_on REAL by A1, FINSEQ_2:92;
now__::_thesis:_for_j_being_Nat_st_j_in_Seg_(len_p)_holds_
uu_._j_<=_qq_._j
let j be Nat; ::_thesis: ( j in Seg (len p) implies uu . j <= qq . j )
assume A9: j in Seg (len p) ; ::_thesis: uu . j <= qq . j
then A10: j in dom p by FINSEQ_1:def_3;
then A11: |.(p /. j).| <= q /. j by A1;
j in dom q by A9, A1, FINSEQ_1:def_3;
then A12: q /. j = q . j by PARTFUN1:def_6;
ex v being Element of REAL n st
( v = p . j & u . j = |.v.| ) by A6, A10;
hence uu . j <= qq . j by A11, A12, A10, PARTFUN1:def_6; ::_thesis: verum
end;
then Sum uu <= Sum qq by RVSUM_1:82;
hence |.E.| <= Sum q by A2, A8, XXREAL_0:2; ::_thesis: verum
end;
Lm8: for A being non empty closed_interval Subset of REAL
for n being non empty Element of NAT
for h being Function of A,(REAL n)
for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds
|.(integral h).| <= integral f
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for n being non empty Element of NAT
for h being Function of A,(REAL n)
for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds
|.(integral h).| <= integral f
let n be non empty Element of NAT ; ::_thesis: for h being Function of A,(REAL n)
for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds
|.(integral h).| <= integral f
let h be Function of A,(REAL n); ::_thesis: for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds
|.(integral h).| <= integral f
let f be Function of A,REAL; ::_thesis: ( h is bounded & h is integrable & f = |.h.| & f is integrable implies |.(integral h).| <= integral f )
assume A1: ( h is bounded & h is integrable & f = |.h.| & f is integrable ) ; ::_thesis: |.(integral h).| <= integral f
then A2: f is bounded by Th14;
consider T being DivSequence of A such that
A3: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11;
set S = the middle_volume_Sequence of h,T;
A4: dom f = dom h by A1, NFCONT_4:def_2;
defpred S1[ Element of NAT , set ] means ex p being FinSequence of REAL st
( p = $2 & len p = len (T . $1) & ( for i being Nat st i in dom (T . $1) holds
( p . i in dom (h | (divset ((T . $1),i))) & ex z being Element of REAL n st
( z = (h | (divset ((T . $1),i))) . (p . i) & ( the middle_volume_Sequence of h,T . $1) . i = (vol (divset ((T . $1),i))) * z ) ) ) );
A5: for k being Element of NAT ex p being Element of REAL * st S1[k,p]
proof
let k be Element of NAT ; ::_thesis: ex p being Element of REAL * st S1[k,p]
defpred S2[ Nat, set ] means ( $2 in dom (h | (divset ((T . k),$1))) & ex c being Element of REAL n st
( c = (h | (divset ((T . k),$1))) . $2 & ( the middle_volume_Sequence of h,T . k) . $1 = (vol (divset ((T . k),$1))) * c ) );
A6: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3;
A7: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of REAL st S2[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] )
assume i in Seg (len (T . k)) ; ::_thesis: ex x being Element of REAL st S2[i,x]
then i in dom (T . k) by FINSEQ_1:def_3;
then consider c being Element of REAL n such that
A8: ( c in rng (h | (divset ((T . k),i))) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * c ) by INTEGR15:def_5;
consider x being set such that
A9: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def_3;
( x in dom h & x in divset ((T . k),i) ) by A9, RELAT_1:57;
then reconsider x = x as Element of REAL ;
take x ; ::_thesis: S2[i,x]
thus S2[i,x] by A8, A9; ::_thesis: verum
end;
consider p being FinSequence of REAL such that
A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S2[i,p . i] ) ) from FINSEQ_1:sch_5(A7);
take p ; ::_thesis: ( p is Element of REAL * & S1[k,p] )
len p = len (T . k) by A10, FINSEQ_1:def_3;
hence ( p is Element of REAL * & S1[k,p] ) by A10, A6, FINSEQ_1:def_11; ::_thesis: verum
end;
consider F being Function of NAT,(REAL *) such that
A11: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A5);
defpred S2[ Element of NAT , set ] means ex q being middle_volume of f,T . $1 st
( q = $2 & ( for i being Nat st i in dom (T . $1) holds
ex z being Element of REAL st
( (F . $1) . i in dom (f | (divset ((T . $1),i))) & z = (f | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = (vol (divset ((T . $1),i))) * z ) ) );
A12: for k being Element of NAT ex y being Element of REAL * st S2[k,y]
proof
let k be Element of NAT ; ::_thesis: ex y being Element of REAL * st S2[k,y]
defpred S3[ Nat, set ] means ex c being Element of REAL st
( (F . k) . $1 in dom (f | (divset ((T . k),$1))) & c = (f | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = (vol (divset ((T . k),$1))) * c );
A13: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def_3;
A14: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of REAL st S3[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S3[i,x] )
assume i in Seg (len (T . k)) ; ::_thesis: ex x being Element of REAL st S3[i,x]
then A15: i in dom (T . k) by FINSEQ_1:def_3;
consider p being FinSequence of REAL such that
A16: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds
( p . i in dom (h | (divset ((T . k),i))) & ex z being Element of REAL n st
( z = (h | (divset ((T . k),i))) . (p . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11;
p . i in dom (h | (divset ((T . k),i))) by A15, A16;
then ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57;
then A17: (F . k) . i in dom (f | (divset ((T . k),i))) by A16, A4, RELAT_1:57;
(vol (divset ((T . k),i))) * ((f | (divset ((T . k),i))) . (p . i)) is Element of REAL ;
hence ex x being Element of REAL st S3[i,x] by A16, A17; ::_thesis: verum
end;
consider q being FinSequence of REAL such that
A18: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S3[i,q . i] ) ) from FINSEQ_1:sch_5(A14);
A19: len q = len (T . k) by A18, FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(T_._k)_holds_
ex_c_being_Element_of_REAL_st_
(_c_in_rng_(f_|_(divset_((T_._k),i)))_&_q_._i_=_c_*_(vol_(divset_((T_._k),i)))_)
let i be Nat; ::_thesis: ( i in dom (T . k) implies ex c being Element of REAL st
( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) ) )
assume i in dom (T . k) ; ::_thesis: ex c being Element of REAL st
( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) )
then i in Seg (len (T . k)) by FINSEQ_1:def_3;
then consider c being Element of REAL such that
A20: ( (F . k) . i in dom (f | (divset ((T . k),i))) & c = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A18;
thus ex c being Element of REAL st
( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) ) by A20, FUNCT_1:3; ::_thesis: verum
end;
then reconsider q = q as middle_volume of f,T . k by A19, INTEGR15:def_1;
q is Element of REAL * by FINSEQ_1:def_11;
hence ex y being Element of REAL * st S2[k,y] by A13, A18; ::_thesis: verum
end;
consider Sf being Function of NAT,(REAL *) such that
A21: for x being Element of NAT holds S2[x,Sf . x] from FUNCT_2:sch_3(A12);
now__::_thesis:_for_k_being_Element_of_NAT_holds_Sf_._k_is_middle_volume_of_f,T_._k
let k be Element of NAT ; ::_thesis: Sf . k is middle_volume of f,T . k
ex q being middle_volume of f,T . k st
( q = Sf . k & ( for i being Nat st i in dom (T . k) holds
ex z being Element of REAL st
( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A21;
hence Sf . k is middle_volume of f,T . k ; ::_thesis: verum
end;
then reconsider Sf = Sf as middle_volume_Sequence of f,T by INTEGR15:def_3;
A22: ( middle_sum (f,Sf) is convergent & lim (middle_sum (f,Sf)) = integral f ) by A1, A2, A3, INTEGR15:9;
A23: ( middle_sum (h, the middle_volume_Sequence of h,T) is convergent & lim (middle_sum (h, the middle_volume_Sequence of h,T)) = integral h ) by A1, A3, INTEGR15:11;
A24: for k being Element of NAT holds ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k
proof
let k be Element of NAT ; ::_thesis: ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k
A25: (middle_sum (f,Sf)) . k = middle_sum (f,(Sf . k)) by INTEGR15:def_4
.= Sum (Sf . k) ;
A26: (middle_sum (h, the middle_volume_Sequence of h,T)) . k = middle_sum (h,( the middle_volume_Sequence of h,T . k)) by INTEGR15:def_8;
A27: for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * ( the middle_volume_Sequence of h,T . k) & (middle_sum (h,( the middle_volume_Sequence of h,T . k))) . i = Sum Pi ) by INTEGR15:def_6;
A28: ex p being FinSequence of REAL st
( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds
( p . i in dom (h | (divset ((T . k),i))) & ex z being Element of REAL n st
( z = (h | (divset ((T . k),i))) . (p . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11;
A29: ex q being middle_volume of f,T . k st
( q = Sf . k & ( for i being Nat st i in dom (T . k) holds
ex z being Element of REAL st
( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A21;
A30: len (Sf . k) = len (T . k) by INTEGR15:def_1;
A31: len ( the middle_volume_Sequence of h,T . k) = len (T . k) by INTEGR15:def_5;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(_the_middle_volume_Sequence_of_h,T_._k)_holds_
|.((_the_middle_volume_Sequence_of_h,T_._k)_/._i).|_<=_(Sf_._k)_/._i
let i be Nat; ::_thesis: ( i in dom ( the middle_volume_Sequence of h,T . k) implies |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i )
assume A32: i in dom ( the middle_volume_Sequence of h,T . k) ; ::_thesis: |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i
then A33: i in Seg (len (T . k)) by A31, FINSEQ_1:def_3;
then A34: i in dom (T . k) by FINSEQ_1:def_3;
A35: i in dom (Sf . k) by A30, A33, FINSEQ_1:def_3;
A36: (F . k) . i in dom (h | (divset ((T . k),i))) by A34, A28;
consider z being Element of REAL n such that
A37: ( z = (h | (divset ((T . k),i))) . ((F . k) . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) by A28, A34;
consider w being Element of REAL such that
A38: ( (F . k) . i in dom (f | (divset ((T . k),i))) & w = (f | (divset ((T . k),i))) . ((F . k) . i) & (Sf . k) . i = (vol (divset ((T . k),i))) * w ) by A29, A34;
A39: ( the middle_volume_Sequence of h,T . k) /. i = ( the middle_volume_Sequence of h,T . k) . i by A32, PARTFUN1:def_6;
A40: 0 <= vol (divset ((T . k),i)) by INTEGRA1:9;
A41: |.(( the middle_volume_Sequence of h,T . k) /. i).| = (abs (vol (divset ((T . k),i)))) * |.z.| by A37, A39, EUCLID:11
.= (vol (divset ((T . k),i))) * |.z.| by A40, ABSVALUE:def_1 ;
A42: dom (h | (divset ((T . k),i))) c= dom h by RELAT_1:60;
A43: (h | (divset ((T . k),i))) . ((F . k) . i) = h . ((F . k) . i) by A36, FUNCT_1:47
.= h /. ((F . k) . i) by A42, A36, PARTFUN1:def_6 ;
A44: dom (f | (divset ((T . k),i))) c= dom f by RELAT_1:60;
(f | (divset ((T . k),i))) . ((F . k) . i) = f . ((F . k) . i) by A38, FUNCT_1:47
.= |.h.| /. ((F . k) . i) by A44, A1, A38, PARTFUN1:def_6
.= |.(h /. ((F . k) . i)).| by A44, A1, A38, NFCONT_4:def_2 ;
hence |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i by A41, A43, A38, A37, A35, PARTFUN1:def_6; ::_thesis: verum
end;
then |.(middle_sum (h,( the middle_volume_Sequence of h,T . k))).| <= Sum (Sf . k) by Lm7, A27, A30, A31;
hence ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k by A25, A26, REAL_NS1:1; ::_thesis: verum
end;
A45: now__::_thesis:_for_i_being_Element_of_NAT_holds_||.(middle_sum_(h,_the_middle_volume_Sequence_of_h,T)).||_._i_<=_(middle_sum_(f,Sf))_._i
let i be Element of NAT ; ::_thesis: ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . i
||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i = ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . i).|| by NORMSP_0:def_4;
hence ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . i by A24; ::_thesis: verum
end;
||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| is convergent by A1, A3, INTEGR15:11, NORMSP_1:23;
then lim ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| <= lim (middle_sum (f,Sf)) by A45, A22, SEQ_2:18;
then ||.(lim (middle_sum (h, the middle_volume_Sequence of h,T))).|| <= lim (middle_sum (f,Sf)) by A23, LOPBAN_1:41;
hence |.(integral h).| <= integral f by A22, A1, A3, INTEGR15:11, REAL_NS1:1; ::_thesis: verum
end;
Lm9: for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for h being PartFunc of REAL,(REAL n) st A c= dom h holds
h | A is Function of A,(REAL n)
by Lm3;
theorem :: INTEGR19:15
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds
f | A is bounded
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds
f | A is bounded
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds
f | A is bounded
let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is bounded & A c= dom f implies f | A is bounded )
assume A1: ( f is bounded & A c= dom f ) ; ::_thesis: f | A is bounded
let i be Element of NAT ; :: according to INTEGR15:def_15 ::_thesis: ( not i in Seg n or (proj (i,n)) * (f | A) is bounded )
set P = proj (i,n);
assume i in Seg n ; ::_thesis: (proj (i,n)) * (f | A) is bounded
then (proj (i,n)) * f is bounded by A1, INTEGR15:def_15;
then consider r being real number such that
A2: for c being set st c in dom ((proj (i,n)) * f) holds
abs (((proj (i,n)) * f) . c) <= r by RFUNCT_1:72;
now__::_thesis:_for_c_being_set_st_c_in_A_/\_(dom_((proj_(i,n))_*_f))_holds_
abs_(((proj_(i,n))_*_f)_._c)_<=_r
let c be set ; ::_thesis: ( c in A /\ (dom ((proj (i,n)) * f)) implies abs (((proj (i,n)) * f) . c) <= r )
assume c in A /\ (dom ((proj (i,n)) * f)) ; ::_thesis: abs (((proj (i,n)) * f) . c) <= r
then c in dom ((proj (i,n)) * f) by XBOOLE_0:def_4;
hence abs (((proj (i,n)) * f) . c) <= r by A2; ::_thesis: verum
end;
then ((proj (i,n)) * f) | A is bounded by RFUNCT_1:73;
hence (proj (i,n)) * (f | A) is bounded by RELAT_1:83; ::_thesis: verum
end;
theorem Th16: :: INTEGR19:16
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f is bounded & f = g holds
g is bounded
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f is bounded & f = g holds
g is bounded
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f is bounded & f = g holds
g is bounded
let f be PartFunc of REAL,(REAL n); ::_thesis: for g being Function of A,(REAL n) st f is bounded & f = g holds
g is bounded
let g be Function of A,(REAL n); ::_thesis: ( f is bounded & f = g implies g is bounded )
assume A1: ( f is bounded & f = g ) ; ::_thesis: g is bounded
let i be Element of NAT ; :: according to INTEGR15:def_12 ::_thesis: ( not i in Seg n or (proj (i,n)) * g is bounded )
thus ( not i in Seg n or (proj (i,n)) * g is bounded ) by A1, INTEGR15:def_15; ::_thesis: verum
end;
theorem Th17: :: INTEGR19:17
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f = g holds
|.f.| = |.g.|
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f = g holds
|.f.| = |.g.|
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f = g holds
|.f.| = |.g.|
let f be PartFunc of REAL,(REAL n); ::_thesis: for g being Function of A,(REAL n) st f = g holds
|.f.| = |.g.|
let g be Function of A,(REAL n); ::_thesis: ( f = g implies |.f.| = |.g.| )
assume A1: f = g ; ::_thesis: |.f.| = |.g.|
A2: dom |.f.| = dom f by NFCONT_4:def_2
.= dom |.g.| by A1, NFCONT_4:def_2 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_|.f.|_holds_
|.f.|_._x_=_|.g.|_._x
let x be set ; ::_thesis: ( x in dom |.f.| implies |.f.| . x = |.g.| . x )
assume A3: x in dom |.f.| ; ::_thesis: |.f.| . x = |.g.| . x
thus |.f.| . x = |.f.| /. x by A3, PARTFUN1:def_6
.= |.(f /. x).| by A3, NFCONT_4:def_2
.= |.g.| /. x by A1, A2, A3, NFCONT_4:def_2
.= |.g.| . x by A2, A3, PARTFUN1:def_6 ; ::_thesis: verum
end;
hence |.f.| = |.g.| by A2, FUNCT_1:2; ::_thesis: verum
end;
theorem Th18: :: INTEGR19:18
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for h being PartFunc of REAL,(REAL n) st A c= dom h holds
|.(h | A).| = |.h.| | A
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for h being PartFunc of REAL,(REAL n) st A c= dom h holds
|.(h | A).| = |.h.| | A
let A be non empty closed_interval Subset of REAL; ::_thesis: for h being PartFunc of REAL,(REAL n) st A c= dom h holds
|.(h | A).| = |.h.| | A
let h be PartFunc of REAL,(REAL n); ::_thesis: ( A c= dom h implies |.(h | A).| = |.h.| | A )
assume A1: A c= dom h ; ::_thesis: |.(h | A).| = |.h.| | A
A2: dom (h | A) = A by A1, RELAT_1:62;
A3: dom (|.h.| | A) = (dom |.h.|) /\ A by RELAT_1:61
.= (dom h) /\ A by NFCONT_4:def_2
.= A by A1, XBOOLE_1:28 ;
A4: dom |.(h | A).| = dom (|.h.| | A) by A3, A2, NFCONT_4:def_2;
now__::_thesis:_for_x_being_set_st_x_in_dom_(|.h.|_|_A)_holds_
(|.h.|_|_A)_._x_=_|.(h_|_A).|_._x
let x be set ; ::_thesis: ( x in dom (|.h.| | A) implies (|.h.| | A) . x = |.(h | A).| . x )
assume A5: x in dom (|.h.| | A) ; ::_thesis: (|.h.| | A) . x = |.(h | A).| . x
then A6: x in (dom |.h.|) /\ A by RELAT_1:61;
then A7: x in (dom h) /\ A by NFCONT_4:def_2;
then A8: x in dom (h | A) by RELAT_1:61;
A9: x in dom |.h.| by A6, XBOOLE_0:def_4;
A10: x in dom h by A7, XBOOLE_0:def_4;
A11: h /. x = h . x by A10, PARTFUN1:def_6
.= (h | A) . x by A8, FUNCT_1:47
.= (h | A) /. x by A8, PARTFUN1:def_6 ;
thus (|.h.| | A) . x = |.h.| . x by A6, FUNCT_1:48
.= |.h.| /. x by A9, PARTFUN1:def_6
.= |.(h /. x).| by A9, NFCONT_4:def_2
.= |.(h | A).| /. x by A11, A4, A5, NFCONT_4:def_2
.= |.(h | A).| . x by A4, A5, PARTFUN1:def_6 ; ::_thesis: verum
end;
hence |.(h | A).| = |.h.| | A by A4, FUNCT_1:2; ::_thesis: verum
end;
theorem Th19: :: INTEGR19:19
for A being non empty closed_interval Subset of REAL
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded holds
|.h.| | A is bounded
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded holds
|.h.| | A is bounded
let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded holds
|.h.| | A is bounded
let h be PartFunc of REAL,(REAL n); ::_thesis: ( A c= dom h & h | A is bounded implies |.h.| | A is bounded )
assume A1: ( A c= dom h & h | A is bounded ) ; ::_thesis: |.h.| | A is bounded
A2: |.(h | A).| = |.h.| | A by Th18, A1;
reconsider g = h | A as Function of A,(REAL n) by A1, Lm9;
g is bounded by Th16, A1;
then |.g.| is bounded by Th14;
hence |.h.| | A is bounded by A2, Th17; ::_thesis: verum
end;
theorem Th20: :: INTEGR19:20
for A being non empty closed_interval Subset of REAL
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds
|.(integral (h,A)).| <= integral (|.h.|,A)
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds
|.(integral (h,A)).| <= integral (|.h.|,A)
let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A holds
|.(integral (h,A)).| <= integral (|.h.|,A)
let h be PartFunc of REAL,(REAL n); ::_thesis: ( A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A implies |.(integral (h,A)).| <= integral (|.h.|,A) )
assume A1: ( A c= dom h & h | A is bounded & h is_integrable_on A & |.h.| is_integrable_on A ) ; ::_thesis: |.(integral (h,A)).| <= integral (|.h.|,A)
set f = |.h.|;
reconsider hA = h | A as Function of A,(REAL n) by A1, Lm9;
A2: integral (h,A) = integral hA by INTEGR15:14;
A c= dom |.h.| by A1, NFCONT_4:def_2;
then reconsider fA = |.h.| | A as Function of A,REAL by Lm5;
A3: fA is integrable by A1, INTEGRA5:def_1;
A4: hA is integrable by A1, INTEGR15:13;
|.hA.| = |.(h | A).| by Th17
.= |.h.| | A by Th18, A1 ;
hence |.(integral (h,A)).| <= integral (|.h.|,A) by A2, A3, A4, A1, Th16, Lm8; ::_thesis: verum
end;
theorem Th21: :: INTEGR19:21
for a, b being real number
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) st a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded holds
|.(integral (h,a,b)).| <= integral (|.h.|,a,b)
proof
let a, b be real number ; ::_thesis: for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) st a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded holds
|.(integral (h,a,b)).| <= integral (|.h.|,a,b)
let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) st a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded holds
|.(integral (h,a,b)).| <= integral (|.h.|,a,b)
let h be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded implies |.(integral (h,a,b)).| <= integral (|.h.|,a,b) )
assume A1: ( a <= b & ['a,b'] c= dom h & h is_integrable_on ['a,b'] & |.h.| is_integrable_on ['a,b'] & h | ['a,b'] is bounded ) ; ::_thesis: |.(integral (h,a,b)).| <= integral (|.h.|,a,b)
A2: ( a is Real & b is Real ) by XREAL_0:def_1;
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A3: integral (h,a,b) = integral (h,['a,b']) by A2, INTEGR15:19;
integral (|.h.|,a,b) = integral (|.h.|,['a,b']) by A1, INTEGRA5:def_4;
hence |.(integral (h,a,b)).| <= integral (|.h.|,a,b) by Th20, A1, A3; ::_thesis: verum
end;
Lm10: for a, b, c, d being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) )
proof
let a, b, c, d be real number ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) )
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['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'] implies ( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f ) and
A4: ( c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: ( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) )
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A5: ( a <= c & d <= b ) by A4, XXREAL_1:1;
then A6: f | ['c,d'] is bounded by A2, A3, Th9;
A7: ( ['c,d'] c= dom f & f is_integrable_on ['c,d'] ) by A2, A3, A5, Th9, Th2;
A8: ['a,b'] c= dom |.f.| by A3, NFCONT_4:def_2;
|.f.| | ['a,b'] is bounded by A3, Th19;
then ( ['c,d'] c= dom |.f.| & |.f.| is_integrable_on ['c,d'] ) by A2, A3, A5, A8, INTEGRA6:18;
hence ( f is_integrable_on ['c,d'] & |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) by A2, A6, A7, Th21, Th19; ::_thesis: verum
end;
theorem Th22: :: INTEGR19:22
for a, b, c, d being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['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'] holds
( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )
proof
let a, b, c, d be real number ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['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'] holds
( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['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'] holds
( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['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'] implies ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) )
assume A1: ( a <= b & f is_integrable_on ['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'] ) ; ::_thesis: ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )
A2: ( c is Real & d is Real ) by XREAL_0:def_1;
percases ( not c <= d or c <= d ) ;
supposeA3: not c <= d ; ::_thesis: ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )
then A4: ['d,c'] = [.d,c.] by INTEGRA5:def_3;
then integral (f,c,d) = - (integral (f,['d,c'])) by A2, INTEGR15:20;
then integral (f,c,d) = - (integral (f,d,c)) by A2, A4, INTEGR15:19;
then A5: |.(integral (f,c,d)).| = |.(integral (f,d,c)).| by EUCLID:10;
( d = min (c,d) & c = max (c,d) ) by A3, XXREAL_0:def_9, XXREAL_0:def_10;
hence ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) by A1, A3, A5, Lm10; ::_thesis: verum
end;
supposeA6: c <= d ; ::_thesis: ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) )
then ( c = min (c,d) & d = max (c,d) ) by XXREAL_0:def_9, XXREAL_0:def_10;
hence ( |.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] & |.f.| | ['(min (c,d)),(max (c,d))'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) ) by A1, A6, Lm10; ::_thesis: verum
end;
end;
end;
Lm11: for a, b, c, d being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) )
proof
let a, b, c, d be real number ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) )
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['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'] implies ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['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'] ) ; ::_thesis: ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) )
( min (c,d) = c & max (c,d) = d ) by A2, XXREAL_0:def_9, XXREAL_0:def_10;
hence ( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) ) by A1, A3, Th22; ::_thesis: verum
end;
Lm12: for a, b, c, d being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
|.(integral (f,d,c)).| <= integral (|.f.|,c,d)
proof
let a, b, c, d be real number ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
|.(integral (f,d,c)).| <= integral (|.f.|,c,d)
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
|.(integral (f,d,c)).| <= integral (|.f.|,c,d)
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['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'] implies |.(integral (f,d,c)).| <= integral (|.f.|,c,d) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) and
A4: d in ['a,b'] ; ::_thesis: |.(integral (f,d,c)).| <= integral (|.f.|,c,d)
A5: ( c is Real & d is Real ) by XREAL_0:def_1;
['c,d'] = [.c,d.] by A2, INTEGRA5:def_3;
then A6: ( |.(integral (f,c,d)).| <= integral (|.f.|,c,d) & integral (f,c,d) = integral (f,['c,d']) ) by A1, A2, A3, A4, Lm11, INTEGR15:19;
['c,d'] = [.c,d.] by A2, INTEGRA5:def_3;
then integral (f,d,c) = - (integral (f,['c,d'])) by A5, INTEGR15:20;
hence |.(integral (f,d,c)).| <= integral (|.f.|,c,d) by A6, EUCLID:10; ::_thesis: verum
end;
theorem :: INTEGR19:23
for a, b, c, d being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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'] holds
( |.f.| is_integrable_on ['c,d'] & |.f.| | ['c,d'] is bounded & |.(integral (f,c,d)).| <= integral (|.f.|,c,d) & |.(integral (f,d,c)).| <= integral (|.f.|,c,d) ) by Lm11, Lm12;
Lm13: for a, b, c, d, e being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * (abs (d - c))
proof
let a, b, c, d, e be real number ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * (abs (d - c))
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * (abs (d - c))
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) implies |.(integral (f,c,d)).| <= e * (abs (d - c)) )
set A = ['(min (c,d)),(max (c,d))'];
assume that
A1: ( a <= b & f is_integrable_on ['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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ; ::_thesis: |.(integral (f,c,d)).| <= e * (abs (d - c))
rng |.f.| c= REAL ;
then A3: |.f.| is Function of (dom |.f.|),REAL by FUNCT_2:2;
dom |.f.| = dom f by NFCONT_4:def_2;
then A4: ['(min (c,d)),(max (c,d))'] c= dom |.f.| by A1, Th3;
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))'] = abs (d - c) by INTEGRA6:6;
|.f.| is_integrable_on ['(min (c,d)),(max (c,d))'] by A1, Th22;
then A6: g is integrable by INTEGRA5:def_1;
e is Real by XREAL_0:def_1;
then 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__::_thesis:_for_x_being_Real_st_x_in_['(min_(c,d)),(max_(c,d))']_holds_
g_._x_<=_h_._x
let x be Real; ::_thesis: ( x in ['(min (c,d)),(max (c,d))'] implies g . x <= h . x )
assume A10: x in ['(min (c,d)),(max (c,d))'] ; ::_thesis: g . x <= h . x
then g . x = |.f.| . x by FUNCT_1:49;
then g . x = |.f.| /. x by A10, A4, PARTFUN1:def_6;
then A11: g . x = |.(f /. x).| by A10, A4, NFCONT_4:def_2;
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; ::_thesis: verum
end;
A12: |.(integral (f,c,d)).| <= integral (|.f.|,(min (c,d)),(max (c,d))) by A1, Th22;
( 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 A13: integral (|.f.|,(min (c,d)),(max (c,d))) = integral (|.f.|,['(min (c,d)),(max (c,d))']) by INTEGRA5:def_4;
|.f.| | ['(min (c,d)),(max (c,d))'] is bounded by A1, Th22;
then A14: g | ['(min (c,d)),(max (c,d))'] is bounded ;
e is Real by XREAL_0:def_1;
then ( 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 * (abs (d - c)) by A13, A8, A9, A6, A14, A5, INTEGRA2:34;
hence |.(integral (f,c,d)).| <= e * (abs (d - c)) by A12, XXREAL_0:2; ::_thesis: verum
end;
Lm14: for a, b, c, d, e being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * (d - c)
proof
let a, b, c, d, e be real number ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * (d - c)
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= e * (d - c)
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) implies |.(integral (f,c,d)).| <= e * (d - c) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) ) ; ::_thesis: |.(integral (f,c,d)).| <= e * (d - c)
0 <= d - c by A2, XREAL_1:48;
then A4: abs (d - c) = d - c by ABSVALUE:def_1;
( min (c,d) = c & max (c,d) = d ) by A2, XXREAL_0:def_9, XXREAL_0:def_10;
hence |.(integral (f,c,d)).| <= e * (d - c) by A1, A3, A4, Lm13; ::_thesis: verum
end;
Lm15: for a, b, c, d, e being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,d,c)).| <= e * (d - c)
proof
let a, b, c, d, e be real number ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,d,c)).| <= e * (d - c)
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,d,c)).| <= e * (d - c)
let f be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & c <= d & f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) implies |.(integral (f,d,c)).| <= e * (d - c) )
assume that
A1: a <= b and
A2: c <= d and
A3: ( f is_integrable_on ['a,b'] & |.f.| is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] ) and
A4: d in ['a,b'] and
A5: for x being real number st x in ['c,d'] holds
|.(f /. x).| <= e ; ::_thesis: |.(integral (f,d,c)).| <= e * (d - c)
['c,d'] = [.c,d.] by A2, INTEGRA5:def_3;
then A6: ( |.(integral (f,c,d)).| <= e * (d - c) & integral (f,c,d) = integral (f,['c,d']) ) by A1, A2, A3, A4, A5, Lm14, INTEGR15:19;
A7: ( c is Real & d is Real ) by XREAL_0:def_1;
['c,d'] = [.c,d.] by A2, INTEGRA5:def_3;
then integral (f,d,c) = - (integral (f,['c,d'])) by A7, INTEGR15:20;
hence |.(integral (f,d,c)).| <= e * (d - c) by A6, EUCLID:10; ::_thesis: verum
end;
theorem :: INTEGR19:24
for a, b, c, d, e being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL n) st a <= b & c <= d & f is_integrable_on ['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 number st x in ['c,d'] holds
|.(f /. x).| <= e ) holds
( |.(integral (f,c,d)).| <= e * (d - c) & |.(integral (f,d,c)).| <= e * (d - c) ) by Lm14, Lm15;
theorem Th25: :: INTEGR19:25
for n being Element of NAT
for a, b, c, d, r being real number
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'] holds
integral ((r (#) f),c,d) = r * (integral (f,c,d))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d, r being real number
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'] holds
integral ((r (#) f),c,d) = r * (integral (f,c,d))
let a, b, c, d, r be real number ; ::_thesis: 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'] holds
integral ((r (#) f),c,d) = r * (integral (f,c,d))
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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'] implies integral ((r (#) f),c,d) = r * (integral (f,c,d)) )
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'] ) ; ::_thesis: integral ((r (#) f),c,d) = r * (integral (f,c,d))
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
integral_(((proj_(i,n))_*_(r_(#)_f)),c,d)_=_r_*_(integral_(((proj_(i,n))_*_f),c,d))
let i be Element of NAT ; ::_thesis: ( i in Seg n implies integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d)) )
set P = proj (i,n);
assume A3: i in Seg n ; ::_thesis: integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d))
then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, INTEGR15:def_16;
(proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15;
then A5: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then A6: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27;
r is Real by XREAL_0:def_1;
then (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) by INTEGR15:16;
hence integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d)) by A4, A5, A6, A1, INTEGRA6:25; ::_thesis: verum
end;
A7: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_((r_(#)_f),c,d))_holds_
(integral_((r_(#)_f),c,d))_._i_=_(r_*_(integral_(f,c,d)))_._i
let i be Nat; ::_thesis: ( i in dom (integral ((r (#) f),c,d)) implies (integral ((r (#) f),c,d)) . i = (r * (integral (f,c,d))) . i )
assume i in dom (integral ((r (#) f),c,d)) ; ::_thesis: (integral ((r (#) f),c,d)) . i = (r * (integral (f,c,d))) . i
then A8: i in Seg n by INTEGR15:def_18;
set P = proj (i,n);
thus (integral ((r (#) f),c,d)) . i = integral (((proj (i,n)) * (r (#) f)),c,d) by A8, INTEGR15:def_18
.= r * (integral (((proj (i,n)) * f),c,d)) by A8, A2
.= r * ((integral (f,c,d)) . i) by A8, INTEGR15:def_18
.= (r * (integral (f,c,d))) . i by RVSUM_1:44 ; ::_thesis: verum
end;
A9: Seg n = dom (integral ((r (#) f),c,d)) by INTEGR15:def_18;
len (r * (integral (f,c,d))) = n by CARD_1:def_7;
then Seg n = dom (r * (integral (f,c,d))) by FINSEQ_1:def_3;
hence integral ((r (#) f),c,d) = r * (integral (f,c,d)) by A9, A7, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th26: :: INTEGR19:26
for n being Element of NAT
for a, b, c, d being real number
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'] holds
integral ((- f),c,d) = - (integral (f,c,d))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
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'] holds
integral ((- f),c,d) = - (integral (f,c,d))
let a, b, c, d be real number ; ::_thesis: 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'] holds
integral ((- f),c,d) = - (integral (f,c,d))
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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'] implies integral ((- f),c,d) = - (integral (f,c,d)) )
- f = (- 1) (#) f by NFCONT_4:7;
hence ( 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'] implies integral ((- f),c,d) = - (integral (f,c,d)) ) by Th25; ::_thesis: verum
end;
theorem Th27: :: INTEGR19:27
for n being Element of NAT
for a, b, c, d being real number
for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
integral_(((proj_(i,n))_*_(f_+_g)),c,d)_=_(integral_(((proj_(i,n))_*_f),c,d))_+_(integral_(((proj_(i,n))_*_g),c,d))
let i be Element of NAT ; ::_thesis: ( i in Seg n implies integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) )
set P = proj (i,n);
assume A3: i in Seg n ; ::_thesis: integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d))
then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, INTEGR15:def_16;
(proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15;
then A5: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
A6: (proj (i,n)) * g is_integrable_on ['a,b'] by A3, A1, INTEGR15:def_16;
(proj (i,n)) * (g | ['a,b']) is bounded by A3, A1, INTEGR15:def_15;
then A7: ((proj (i,n)) * g) | ['a,b'] is bounded by RELAT_1:83;
A8: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then A9: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27;
rng g c= dom (proj (i,n)) by A8;
then A10: ['a,b'] c= dom ((proj (i,n)) * g) by A1, RELAT_1:27;
A11: (proj (i,n)) * (f + g) = ((proj (i,n)) * f) + ((proj (i,n)) * g) by INTEGR15:15;
thus integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) by A4, A5, A9, A6, A7, A10, A1, A11, INTEGRA6:24; ::_thesis: verum
end;
A12: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_((f_+_g),c,d))_holds_
(integral_((f_+_g),c,d))_._i_=_((integral_(f,c,d))_+_(integral_(g,c,d)))_._i
let i be Nat; ::_thesis: ( i in dom (integral ((f + g),c,d)) implies (integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . i )
assume i in dom (integral ((f + g),c,d)) ; ::_thesis: (integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . i
then A13: i in Seg n by INTEGR15:def_18;
set P = proj (i,n);
thus (integral ((f + g),c,d)) . i = integral (((proj (i,n)) * (f + g)),c,d) by A13, INTEGR15:def_18
.= (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) by A13, A2
.= ((integral (f,c,d)) . i) + (integral (((proj (i,n)) * g),c,d)) by A13, INTEGR15:def_18
.= ((integral (f,c,d)) . i) + ((integral (g,c,d)) . i) by A13, INTEGR15:def_18
.= ((integral (f,c,d)) + (integral (g,c,d))) . i by RVSUM_1:11 ; ::_thesis: verum
end;
A14: Seg n = dom (integral ((f + g),c,d)) by INTEGR15:def_18;
len ((integral (f,c,d)) + (integral (g,c,d))) = n by CARD_1:def_7;
then Seg n = dom ((integral (f,c,d)) + (integral (g,c,d))) by FINSEQ_1:def_3;
hence integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) by A14, A12, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th28: :: INTEGR19:28
for n being Element of NAT
for a, b, c, d being real number
for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
let f, g be PartFunc of REAL,(REAL n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
A2: ( - g is_integrable_on ['a,b'] & (- g) | ['a,b'] is bounded ) by A1, Th12;
A3: dom g = dom (- g) by NFCONT_4:def_3;
f - g = f + (- g) by Lm1;
hence integral ((f - g),c,d) = (integral (f,c,d)) + (integral ((- g),c,d)) by A1, A2, A3, Th27
.= (integral (f,c,d)) - (integral (g,c,d)) by A1, Th26 ;
::_thesis: verum
end;
theorem Th29: :: INTEGR19:29
for n being Element of NAT
for a, b being real number
for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
proof
let n be Element of NAT ; ::_thesis: for a, b being real number
for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
let a, b be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
let f be PartFunc of REAL,(REAL n); ::_thesis: for E being Element of REAL n st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
let E be Element of REAL n; ::_thesis: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) implies ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E ) )
assume A1: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) ) ; ::_thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(_(proj_(i,n))_*_f_is_integrable_on_['a,b']_&_((proj_(i,n))_*_f)_|_['a,b']_is_bounded_&_integral_(((proj_(i,n))_*_f),a,b)_=_((proj_(i,n))_._E)_*_(b_-_a)_)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (proj (i,n)) * f is_integrable_on ['a,b'] & ((proj (i,n)) * f) | ['a,b'] is bounded & integral (((proj (i,n)) * f),a,b) = ((proj (i,n)) . E) * (b - a) ) )
set P = proj (i,n);
assume i in Seg n ; ::_thesis: ( (proj (i,n)) * f is_integrable_on ['a,b'] & ((proj (i,n)) * f) | ['a,b'] is bounded & integral (((proj (i,n)) * f),a,b) = ((proj (i,n)) . E) * (b - a) )
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then A3: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27;
for x being real number st x in ['a,b'] holds
((proj (i,n)) * f) . x = (proj (i,n)) . E
proof
let x be real number ; ::_thesis: ( x in ['a,b'] implies ((proj (i,n)) * f) . x = (proj (i,n)) . E )
assume A4: x in ['a,b'] ; ::_thesis: ((proj (i,n)) * f) . x = (proj (i,n)) . E
A5: f . x = f /. x by A4, A1, PARTFUN1:def_6;
hence ((proj (i,n)) * f) . x = (proj (i,n)) . (f /. x) by A4, A3, FUNCT_1:12
.= (proj (i,n)) . E by A4, A1, A5 ;
::_thesis: verum
end;
hence ( (proj (i,n)) * f is_integrable_on ['a,b'] & ((proj (i,n)) * f) | ['a,b'] is bounded & integral (((proj (i,n)) * f),a,b) = ((proj (i,n)) . E) * (b - a) ) by A3, A1, INTEGRA6:26; ::_thesis: verum
end;
then A6: for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on ['a,b'] ;
A7: Seg n = dom (integral (f,a,b)) by INTEGR15:def_18;
A8: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(proj_(i,n))_*_(f_|_['a,b'])_is_bounded
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * (f | ['a,b']) is bounded )
set P = proj (i,n);
assume i in Seg n ; ::_thesis: (proj (i,n)) * (f | ['a,b']) is bounded
then ((proj (i,n)) * f) | ['a,b'] is bounded by A2;
hence (proj (i,n)) * (f | ['a,b']) is bounded by RELAT_1:83; ::_thesis: verum
end;
A9: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_(f,a,b))_holds_
(integral_(f,a,b))_._i_=_((b_-_a)_*_E)_._i
let i be Nat; ::_thesis: ( i in dom (integral (f,a,b)) implies (integral (f,a,b)) . i = ((b - a) * E) . i )
assume A10: i in dom (integral (f,a,b)) ; ::_thesis: (integral (f,a,b)) . i = ((b - a) * E) . i
hence (integral (f,a,b)) . i = integral (((proj (i,n)) * f),a,b) by A7, INTEGR15:def_18
.= ((proj (i,n)) . E) * (b - a) by A10, A2, A7
.= (b - a) * (E . i) by PDIFF_1:def_1
.= ((b - a) * E) . i by RVSUM_1:44 ;
::_thesis: verum
end;
len ((b - a) * E) = n by CARD_1:def_7;
then Seg n = dom ((b - a) * E) by FINSEQ_1:def_3;
hence ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E ) by A6, A8, A7, A9, FINSEQ_1:13, INTEGR15:def_15, INTEGR15:def_16; ::_thesis: verum
end;
theorem Th30: :: INTEGR19:30
for n being Element of NAT
for a, b, c, d being real number
for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ( for x being real number st x in ['a,b'] holds
f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = (d - c) * E
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ( for x being real number st x in ['a,b'] holds
f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = (d - c) * E
let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n st a <= b & ( for x being real number st x in ['a,b'] holds
f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = (d - c) * E
let f be PartFunc of REAL,(REAL n); ::_thesis: for E being Element of REAL n st a <= b & ( for x being real number st x in ['a,b'] holds
f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = (d - c) * E
let E be Element of REAL n; ::_thesis: ( a <= b & ( for x being real number st x in ['a,b'] holds
f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = (d - c) * E )
assume A1: ( a <= b & ( for x being real number st x in ['a,b'] holds
f . x = E ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,c,d) = (d - c) * E
A2: Seg n = dom (integral (f,c,d)) by INTEGR15:def_18;
A3: now__::_thesis:_for_i_being_Element_of_NAT_holds_integral_(((proj_(i,n))_*_f),c,d)_=_((proj_(i,n))_._E)_*_(d_-_c)
let i be Element of NAT ; ::_thesis: integral (((proj (i,n)) * f),c,d) = ((proj (i,n)) . E) * (d - c)
set P = proj (i,n);
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;
for x being real number st x in ['a,b'] holds
((proj (i,n)) * f) . x = (proj (i,n)) . E
proof
let x be real number ; ::_thesis: ( x in ['a,b'] implies ((proj (i,n)) * f) . x = (proj (i,n)) . E )
assume A5: x in ['a,b'] ; ::_thesis: ((proj (i,n)) * f) . x = (proj (i,n)) . E
then A6: f . x = f /. x by A1, PARTFUN1:def_6;
((proj (i,n)) * f) . x = (proj (i,n)) . (f /. x) by A4, A5, A6, FUNCT_1:12
.= (proj (i,n)) . E by A6, A5, A1 ;
hence ((proj (i,n)) * f) . x = (proj (i,n)) . E ; ::_thesis: verum
end;
hence integral (((proj (i,n)) * f),c,d) = ((proj (i,n)) . E) * (d - c) by A4, A1, INTEGRA6:27; ::_thesis: verum
end;
A7: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_(f,c,d))_holds_
(integral_(f,c,d))_._i_=_((d_-_c)_*_E)_._i
let i be Nat; ::_thesis: ( i in dom (integral (f,c,d)) implies (integral (f,c,d)) . i = ((d - c) * E) . i )
set P = proj (i,n);
assume A8: i in dom (integral (f,c,d)) ; ::_thesis: (integral (f,c,d)) . i = ((d - c) * E) . i
hence (integral (f,c,d)) . i = integral (((proj (i,n)) * f),c,d) by A2, INTEGR15:def_18
.= ((proj (i,n)) . E) * (d - c) by A3, A8
.= (d - c) * (E . i) by PDIFF_1:def_1
.= ((d - c) * E) . i by RVSUM_1:44 ;
::_thesis: verum
end;
len ((d - c) * E) = n by CARD_1:def_7;
then Seg n = dom ((d - c) * E) by FINSEQ_1:def_3;
hence integral (f,c,d) = (d - c) * E by A2, A7, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th31: :: INTEGR19:31
for n being Element of NAT
for a, b, c, d being real number
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'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
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'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let a, b, c, d be real number ; ::_thesis: 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'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) )
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'] ) ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
integral_(((proj_(i,n))_*_f),a,d)_=_(integral_(((proj_(i,n))_*_f),a,c))_+_(integral_(((proj_(i,n))_*_f),c,d))
let i be Element of NAT ; ::_thesis: ( i in Seg n implies integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d)) )
set P = proj (i,n);
assume A3: i in Seg n ; ::_thesis: integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d))
then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, INTEGR15:def_16;
(proj (i,n)) * (f | ['a,b']) is bounded by A3, A1, INTEGR15:def_15;
then A5: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
hence integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d)) by A4, A5, A1, INTEGRA6:20; ::_thesis: verum
end;
A6: Seg n = dom (integral (f,a,d)) by INTEGR15:def_18;
A7: now__::_thesis:_for_i0_being_Nat_st_i0_in_dom_(integral_(f,a,d))_holds_
(integral_(f,a,d))_._i0_=_((integral_(f,a,c))_+_(integral_(f,c,d)))_._i0
let i0 be Nat; ::_thesis: ( i0 in dom (integral (f,a,d)) implies (integral (f,a,d)) . i0 = ((integral (f,a,c)) + (integral (f,c,d))) . i0 )
assume A8: i0 in dom (integral (f,a,d)) ; ::_thesis: (integral (f,a,d)) . i0 = ((integral (f,a,c)) + (integral (f,c,d))) . i0
set P = proj (i0,n);
thus (integral (f,a,d)) . i0 = integral (((proj (i0,n)) * f),a,d) by A8, A6, INTEGR15:def_18
.= (integral (((proj (i0,n)) * f),a,c)) + (integral (((proj (i0,n)) * f),c,d)) by A8, A2, A6
.= ((integral (f,a,c)) . i0) + (integral (((proj (i0,n)) * f),c,d)) by A8, A6, INTEGR15:def_18
.= ((integral (f,a,c)) . i0) + ((integral (f,c,d)) . i0) by A8, A6, INTEGR15:def_18
.= ((integral (f,a,c)) + (integral (f,c,d))) . i0 by RVSUM_1:11 ; ::_thesis: verum
end;
len ((integral (f,a,c)) + (integral (f,c,d))) = n by CARD_1:def_7;
then Seg n = dom ((integral (f,a,c)) + (integral (f,c,d))) by FINSEQ_1:def_3;
hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A6, A7, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th32: :: INTEGR19:32
for n being Element of NAT
for a, b, c, d, e being real number
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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= (n * e) * (abs (d - c))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d, e being real number
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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= (n * e) * (abs (d - c))
let a, b, c, d, e be real number ; ::_thesis: 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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) holds
|.(integral (f,c,d)).| <= (n * e) * (abs (d - c))
let f be PartFunc of REAL,(REAL n); ::_thesis: ( 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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) implies |.(integral (f,c,d)).| <= (n * e) * (abs (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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f /. x).| <= e ) ) ; ::_thesis: |.(integral (f,c,d)).| <= (n * e) * (abs (d - c))
A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
|.(integral_(((proj_(i,n))_*_f),c,d)).|_<=_e_*_(abs_(d_-_c))
let i be Element of NAT ; ::_thesis: ( i in Seg n implies |.(integral (((proj (i,n)) * f),c,d)).| <= e * (abs (d - c)) )
set P = proj (i,n);
assume A3: i in Seg n ; ::_thesis: |.(integral (((proj (i,n)) * f),c,d)).| <= e * (abs (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 number st x in ['(min (c,d)),(max (c,d))'] holds
|.(((proj (i,n)) * f) . x).| <= e
proof
let x be real number ; ::_thesis: ( 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))'] ; ::_thesis: |.(((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, TARSKI:def_3;
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; ::_thesis: verum
end;
A11: (proj (i,n)) * f is_integrable_on ['a,b'] by A1, A3, INTEGR15:def_16;
A12: (proj (i,n)) * (f | ['a,b']) is bounded by A1, A3, INTEGR15:def_15;
((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 * (abs (d - c)) by A12, A1, A4, A5, A11, Lm4; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_
|.((integral_(f,c,d))_._i).|_<=_e_*_(abs_(d_-_c))
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies |.((integral (f,c,d)) . i).| <= e * (abs (d - c)) )
set P = proj (i,n);
assume ( 1 <= i & i <= n ) ; ::_thesis: |.((integral (f,c,d)) . i).| <= e * (abs (d - c))
then A13: i in Seg n ;
then |.(integral (((proj (i,n)) * f),c,d)).| <= e * (abs (d - c)) by A2;
hence |.((integral (f,c,d)) . i).| <= e * (abs (d - c)) by A13, INTEGR15:def_18; ::_thesis: verum
end;
then |.(integral (f,c,d)).| <= n * (e * (abs (d - c))) by PDIFF_8:15;
hence |.(integral (f,c,d)).| <= (n * e) * (abs (d - c)) ; ::_thesis: verum
end;
theorem Th33: :: INTEGR19:33
for n being Element of NAT
for b, a being real number
for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))
proof
let n be Element of NAT ; ::_thesis: for b, a being real number
for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))
let b, a be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))
let f be PartFunc of REAL,(REAL n); ::_thesis: integral (f,b,a) = - (integral (f,a,b))
A1: ( a is Real & b is Real ) by XREAL_0:def_1;
percases ( a <= b or not a <= b ) ;
suppose a <= b ; ::_thesis: integral (f,b,a) = - (integral (f,a,b))
then A2: ['a,b'] = [.a,b.] by INTEGRA5:def_3;
integral (f,['a,b']) = integral (f,a,b) by A1, A2, INTEGR15:19;
hence integral (f,b,a) = - (integral (f,a,b)) by A1, A2, INTEGR15:20; ::_thesis: verum
end;
suppose not a <= b ; ::_thesis: integral (f,b,a) = - (integral (f,a,b))
then A3: ['b,a'] = [.b,a.] by INTEGRA5:def_3;
then - (integral (f,['b,a'])) = integral (f,a,b) by A1, INTEGR15:20;
hence integral (f,b,a) = - (integral (f,a,b)) by A1, A3, INTEGR15:19; ::_thesis: verum
end;
end;
end;
begin
Lm16: for n being Element of NAT
for p being FinSequence of REAL n
for r being Element of REAL n
for q being FinSequence of (REAL-NS n) st p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum q
proof
let n be Element of NAT ; ::_thesis: for p being FinSequence of REAL n
for r being Element of REAL n
for q being FinSequence of (REAL-NS n) st p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum q
defpred S1[ Element of NAT ] means for p being FinSequence of REAL n
for r being Element of REAL n
for q being FinSequence of (REAL-NS n) st len p = $1 & p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum q;
A1: S1[ 0 ]
proof
let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n
for q being FinSequence of (REAL-NS n) st len p = 0 & p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum q
let r be Element of REAL n; ::_thesis: for q being FinSequence of (REAL-NS n) st len p = 0 & p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum q
let q be FinSequence of (REAL-NS n); ::_thesis: ( len p = 0 & p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum q )
assume A2: ( len p = 0 & p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum q
then A3: p = {} ;
A4: q = <*> the carrier of (REAL-NS n) by A2;
len r = n by CARD_1:def_7;
then A5: dom r = Seg n by FINSEQ_1:def_3;
A6: dom ((Seg n) --> 0) = Seg n by FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_dom_r_holds_
r_._x_=_((Seg_n)_-->_0)_._x
let x be set ; ::_thesis: ( x in dom r implies r . x = ((Seg n) --> 0) . x )
assume A7: x in dom r ; ::_thesis: r . x = ((Seg n) --> 0) . x
then reconsider i = x as Element of NAT ;
set P = proj (i,n);
consider Pi being FinSequence of REAL such that
A8: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A2, A5, A7;
r . x = 0 by A3, A8, RVSUM_1:72;
hence r . x = ((Seg n) --> 0) . x by A5, A7, FUNCOP_1:7; ::_thesis: verum
end;
then r = 0* n by A5, A6, FUNCT_1:2;
then r = 0. (REAL-NS n) by REAL_NS1:def_4;
hence r = Sum q by A4, RLVECT_1:43; ::_thesis: verum
end;
A9: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A10: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_p_being_FinSequence_of_REAL_n
for_r_being_Element_of_REAL_n
for_q_being_FinSequence_of_(REAL-NS_n)_st_len_p_=_k_+_1_&_p_=_q_&_(_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
ex_Pi_being_FinSequence_of_REAL_st_
(_Pi_=_(proj_(i,n))_*_p_&_r_._i_=_Sum_Pi_)_)_holds_
r_=_Sum_q
let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n
for q being FinSequence of (REAL-NS n) st len p = k + 1 & p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum q
let r be Element of REAL n; ::_thesis: for q being FinSequence of (REAL-NS n) st len p = k + 1 & p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum q
let q be FinSequence of (REAL-NS n); ::_thesis: ( len p = k + 1 & p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum q )
assume A11: ( len p = k + 1 & p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum q
set p1 = p | k;
A12: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom p by A11, FINSEQ_1:def_3;
then p . (k + 1) in rng p by FUNCT_1:3;
then reconsider pk1 = p . (k + 1) as Element of REAL n ;
set q1 = q | k;
k + 1 in dom q by A11, A12, FINSEQ_1:def_3;
then q . (k + 1) in rng q by FUNCT_1:3;
then reconsider qk1 = q . (k + 1) as Point of (REAL-NS n) ;
defpred S2[ Nat, set ] means ex P1i being FinSequence of REAL st
( P1i = (proj ($1,n)) * (p | k) & $2 = Sum P1i );
A13: for i being Nat st i in Seg n holds
ex r being Element of REAL st S2[i,r]
proof
let i be Nat; ::_thesis: ( i in Seg n implies ex r being Element of REAL st S2[i,r] )
assume i in Seg n ; ::_thesis: ex r being Element of REAL st S2[i,r]
take Sum ((proj (i,n)) * (p | k)) ; ::_thesis: S2[i, Sum ((proj (i,n)) * (p | k))]
thus S2[i, Sum ((proj (i,n)) * (p | k))] ; ::_thesis: verum
end;
consider r1 being FinSequence of REAL such that
A14: ( dom r1 = Seg n & ( for i being Nat st i in Seg n holds
S2[i,r1 . i] ) ) from FINSEQ_1:sch_5(A13);
len r1 = n by A14, FINSEQ_1:def_3;
then reconsider r1 = r1 as Element of REAL n by FINSEQ_2:92;
A15: for i being Element of NAT st i in Seg n holds
ex P1i being FinSequence of REAL st
( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A14;
A16: k <= len p by A11, NAT_1:16;
then A17: len (p | k) = k by FINSEQ_1:59;
A18: r1 = Sum (q | k) by A10, A11, A15, A17;
A19: len r = n by CARD_1:def_7;
A20: len (r1 + pk1) = n by CARD_1:def_7;
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_n_holds_
r_._i_=_(r1_+_pk1)_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= n implies r . i = (r1 + pk1) . i )
set P = proj (i,n);
assume ( 1 <= i & i <= n ) ; ::_thesis: r . i = (r1 + pk1) . i
then A21: i in Seg n by FINSEQ_1:1;
consider Pi being FinSequence of REAL such that
A22: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A21, A11;
consider P1i being FinSequence of REAL such that
A23: ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A21, A14;
A24: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then A25: rng p c= dom (proj (i,n)) ;
A26: dom Pi = dom p by A25, A22, RELAT_1:27
.= Seg (len p) by FINSEQ_1:def_3 ;
A27: len p = (len (p | k)) + 1 by A11, A16, FINSEQ_1:59
.= (len (p | k)) + (len <*(pk1 . i)*>) by FINSEQ_1:40 ;
A28: rng (p | k) c= dom (proj (i,n)) by A24;
A29: dom P1i = dom (p | k) by A28, A23, RELAT_1:27
.= Seg (len (p | k)) by FINSEQ_1:def_3 ;
then A30: dom Pi = Seg ((len P1i) + (len <*(pk1 . i)*>)) by A26, A27, FINSEQ_1:def_3;
len (p | k) <= len p by A16, FINSEQ_1:59;
then A31: Seg (len (p | k)) c= Seg (len p) by FINSEQ_1:5;
A32: for k being Nat st k in dom P1i holds
Pi . k = P1i . k
proof
let k be Nat; ::_thesis: ( k in dom P1i implies Pi . k = P1i . k )
assume A33: k in dom P1i ; ::_thesis: Pi . k = P1i . k
then A34: k in dom (p | k) by A29, FINSEQ_1:def_3;
thus P1i . k = (proj (i,n)) . ((p | k) . k) by A23, A33, FUNCT_1:12
.= (proj (i,n)) . (p . k) by A34, FUNCT_1:47
.= Pi . k by A22, A33, A29, A26, A31, FUNCT_1:12 ; ::_thesis: verum
end;
for k being Nat st k in dom <*(pk1 . i)*> holds
Pi . ((len P1i) + k) = <*(pk1 . i)*> . k
proof
let j be Nat; ::_thesis: ( j in dom <*(pk1 . i)*> implies Pi . ((len P1i) + j) = <*(pk1 . i)*> . j )
assume j in dom <*(pk1 . i)*> ; ::_thesis: Pi . ((len P1i) + j) = <*(pk1 . i)*> . j
then j in Seg (len <*(pk1 . i)*>) by FINSEQ_1:def_3;
then j in {1} by FINSEQ_1:2, FINSEQ_1:40;
then A35: j = 1 by TARSKI:def_1;
thus Pi . ((len P1i) + j) = Pi . (k + 1) by A29, A17, A35, FINSEQ_1:def_3
.= (proj (i,n)) . (p . (k + 1)) by A22, A26, A11, FINSEQ_1:4, FUNCT_1:12
.= pk1 . i by PDIFF_1:def_1
.= <*(pk1 . i)*> . j by A35, FINSEQ_1:40 ; ::_thesis: verum
end;
then Pi = P1i ^ <*(pk1 . i)*> by A32, A30, FINSEQ_1:def_7;
hence r . i = (r1 . i) + (pk1 . i) by A22, A23, RVSUM_1:74
.= (r1 + pk1) . i by RVSUM_1:11 ;
::_thesis: verum
end;
then A36: r = r1 + pk1 by A19, A20, FINSEQ_1:14;
A37: len q = (len (q | k)) + 1 by A16, A11, FINSEQ_1:59;
A38: q | k = q | (dom (q | k)) by A17, A11, FINSEQ_1:def_3;
thus r = (Sum (q | k)) + qk1 by A36, A18, A11, REAL_NS1:2
.= Sum q by A11, A37, A38, RLVECT_1:38 ; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
A39: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A9);
let p be FinSequence of REAL n; ::_thesis: for r being Element of REAL n
for q being FinSequence of (REAL-NS n) st p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum q
let r be Element of REAL n; ::_thesis: for q being FinSequence of (REAL-NS n) st p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum q
let q be FinSequence of (REAL-NS n); ::_thesis: ( p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum q )
assume A40: ( p = q & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; ::_thesis: r = Sum q
len p = len p ;
hence r = Sum q by A40, A39; ::_thesis: verum
end;
definition
let R be RealNormSpace;
let X be non empty set ;
let g be PartFunc of X,R;
attrg is bounded means :Def1: :: INTEGR19:def 1
ex r being real number st
for y being set st y in dom g holds
||.(g /. y).|| < r;
end;
:: deftheorem Def1 defines bounded INTEGR19:def_1_:_
for R being RealNormSpace
for X being non empty set
for g being PartFunc of X,R holds
( g is bounded iff ex r being real number st
for y being set st y in dom g holds
||.(g /. y).|| < r );
theorem Th34: :: INTEGR19:34
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g holds
( f is bounded iff g is bounded )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g holds
( f is bounded iff g is bounded )
let f be PartFunc of REAL,(REAL n); ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g holds
( f is bounded iff g is bounded )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = g implies ( f is bounded iff g is bounded ) )
assume A1: f = g ; ::_thesis: ( f is bounded iff g is bounded )
thus ( f is bounded implies g is bounded ) ::_thesis: ( g is bounded implies f is bounded )
proof
assume A2: f is bounded ; ::_thesis: g is bounded
defpred S1[ Element of NAT , Element of REAL ] means for y being set st y in dom ((proj ($1,n)) * f) holds
abs (((proj ($1,n)) * f) . y) < $2;
A3: for i being Element of NAT st i in Seg n holds
ex di being Element of REAL st S1[i,di]
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex di being Element of REAL st S1[i,di] )
set P = proj (i,n);
assume i in Seg n ; ::_thesis: ex di being Element of REAL st S1[i,di]
then (proj (i,n)) * f is bounded by A2, INTEGR15:def_15;
then consider r being real number such that
A4: for y being set st y in dom ((proj (i,n)) * f) holds
abs (((proj (i,n)) * f) . y) < r by COMSEQ_2:def_3;
reconsider r = r as Element of REAL by XREAL_0:def_1;
take r ; ::_thesis: S1[i,r]
thus S1[i,r] by A4; ::_thesis: verum
end;
consider d being FinSequence of REAL such that
A5: ( dom d = Seg n & ( for k being Element of NAT st k in Seg n holds
S1[k,d /. k] ) ) from RECDEF_1:sch_17(A3);
set K = max d;
for y being set st y in dom g holds
||.(g /. y).|| < (n * (max d)) + 1
proof
let y be set ; ::_thesis: ( y in dom g implies ||.(g /. y).|| < (n * (max d)) + 1 )
assume A6: y in dom g ; ::_thesis: ||.(g /. y).|| < (n * (max d)) + 1
set s = f /. y;
now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<=_n_holds_
abs_((f_/._y)_._i)_<=_max_d
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n implies abs ((f /. y) . i) <= max d )
set P = proj (i,n);
assume A7: ( 1 <= i & i <= n ) ; ::_thesis: abs ((f /. y) . i) <= max d
then A8: i in Seg n ;
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then A9: y in dom ((proj (i,n)) * f) by A6, A1, RELAT_1:27;
then A10: abs (((proj (i,n)) * f) . y) < d /. i by A8, A5;
f . y = f /. y by A6, A1, PARTFUN1:def_6;
then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by A9, FUNCT_1:12;
then A11: abs ((f /. y) . i) < d /. i by A10, PDIFF_1:def_1;
len d = n by A5, FINSEQ_1:def_3;
then d . i <= max d by A7, RFINSEQ2:1;
then d /. i <= max d by A8, A5, PARTFUN1:def_6;
hence abs ((f /. y) . i) <= max d by A11, XXREAL_0:2; ::_thesis: verum
end;
then A12: |.(f /. y).| < (n * (max d)) + 1 by PDIFF_8:15, XREAL_1:145;
g /. y = g . y by A6, PARTFUN1:def_6
.= f /. y by A1, A6, PARTFUN1:def_6 ;
hence ||.(g /. y).|| < (n * (max d)) + 1 by A12, REAL_NS1:1; ::_thesis: verum
end;
hence g is bounded by Def1; ::_thesis: verum
end;
assume A13: g is bounded ; ::_thesis: f is bounded
consider r being real number such that
A14: for y being set st y in dom g holds
||.(g /. y).|| < r by A13, Def1;
let i be Element of NAT ; :: according to INTEGR15:def_15 ::_thesis: ( not i in Seg n or (proj (i,n)) * f is bounded )
set P = proj (i,n);
assume A15: i in Seg n ; ::_thesis: (proj (i,n)) * f is bounded
for y being set st y in dom ((proj (i,n)) * f) holds
abs (((proj (i,n)) * f) . y) < r
proof
let y be set ; ::_thesis: ( y in dom ((proj (i,n)) * f) implies abs (((proj (i,n)) * f) . y) < r )
assume A16: y in dom ((proj (i,n)) * f) ; ::_thesis: abs (((proj (i,n)) * f) . y) < r
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then A17: y in dom f by A16, RELAT_1:27;
then A18: ||.(g /. y).|| < r by A14, A1;
set s = f /. y;
g /. y = g . y by A17, A1, PARTFUN1:def_6
.= f /. y by A1, A17, PARTFUN1:def_6 ;
then A19: |.(f /. y).| < r by A18, REAL_NS1:1;
abs ((f /. y) . i) <= |.(f /. y).| by A15, REAL_NS1:8;
then A20: abs ((f /. y) . i) < r by A19, XXREAL_0:2;
f . y = f /. y by A17, PARTFUN1:def_6;
then ((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y) by A16, FUNCT_1:12;
hence abs (((proj (i,n)) * f) . y) < r by A20, PDIFF_1:def_1; ::_thesis: verum
end;
hence (proj (i,n)) * f is bounded by COMSEQ_2:def_3; ::_thesis: verum
end;
theorem Th35: :: INTEGR19:35
for n being Element of NAT
for X, Y being set
for f1, f2 being PartFunc of REAL,(REAL-NS n) st f1 | X is bounded & f2 | Y is bounded holds
( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
proof
let n be Element of NAT ; ::_thesis: for X, Y being set
for f1, f2 being PartFunc of REAL,(REAL-NS n) st f1 | X is bounded & f2 | Y is bounded holds
( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
let X, Y be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL-NS n) st f1 | X is bounded & f2 | Y is bounded holds
( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
let f1, f2 be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f1 | X is bounded & f2 | Y is bounded implies ( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) )
assume A1: ( f1 | X is bounded & f2 | Y is bounded ) ; ::_thesis: ( (f1 + f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded )
consider r1 being real number such that
A2: for x being set st x in dom (f1 | X) holds
||.((f1 | X) /. x).|| < r1 by A1, Def1;
consider r2 being real number such that
A3: for x being set st x in dom (f2 | Y) holds
||.((f2 | Y) /. x).|| < r2 by A1, Def1;
now__::_thesis:_for_x_being_set_st_x_in_dom_((f1_+_f2)_|_(X_/\_Y))_holds_
||.(((f1_+_f2)_|_(X_/\_Y))_/._x).||_<_r1_+_r2
let x be set ; ::_thesis: ( x in dom ((f1 + f2) | (X /\ Y)) implies ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2 )
assume x in dom ((f1 + f2) | (X /\ Y)) ; ::_thesis: ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2
then A4: ( x in dom (f1 + f2) & x in X /\ Y ) by RELAT_1:57;
then x in (dom f1) /\ (dom f2) by VFUNCT_1:def_1;
then A5: ( x in dom f1 & x in dom f2 ) by XBOOLE_0:def_4;
A6: ( x in X & x in Y ) by A4, XBOOLE_0:def_4;
((f1 + f2) | (X /\ Y)) /. x = (f1 + f2) /. x by A4, PARTFUN2:17
.= (f1 /. x) + (f2 /. x) by A4, VFUNCT_1:def_1
.= ((f1 | X) /. x) + (f2 /. x) by A5, A6, PARTFUN2:17
.= ((f1 | X) /. x) + ((f2 | Y) /. x) by A5, A6, PARTFUN2:17 ;
then A7: ||.(((f1 + f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:def_1;
x in dom (f1 | X) by A5, A6, RELAT_1:57;
then A8: ||.((f1 | X) /. x).|| < r1 by A2;
x in dom (f2 | Y) by A5, A6, RELAT_1:57;
then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A3, A8, XREAL_1:8;
hence ||.(((f1 + f2) | (X /\ Y)) /. x).|| < r1 + r2 by A7, XXREAL_0:2; ::_thesis: verum
end;
hence (f1 + f2) | (X /\ Y) is bounded by Def1; ::_thesis: (f1 - f2) | (X /\ Y) is bounded
take r1 + r2 ; :: according to INTEGR19:def_1 ::_thesis: for y being set st y in dom ((f1 - f2) | (X /\ Y)) holds
||.(((f1 - f2) | (X /\ Y)) /. y).|| < r1 + r2
let x be set ; ::_thesis: ( x in dom ((f1 - f2) | (X /\ Y)) implies ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2 )
assume x in dom ((f1 - f2) | (X /\ Y)) ; ::_thesis: ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2
then A9: ( x in dom (f1 - f2) & x in X /\ Y ) by RELAT_1:57;
then x in (dom f1) /\ (dom f2) by VFUNCT_1:def_2;
then A10: ( x in dom f1 & x in dom f2 ) by XBOOLE_0:def_4;
A11: ( x in X & x in Y ) by A9, XBOOLE_0:def_4;
((f1 - f2) | (X /\ Y)) /. x = (f1 - f2) /. x by A9, PARTFUN2:17
.= (f1 /. x) - (f2 /. x) by A9, VFUNCT_1:def_2
.= ((f1 | X) /. x) - (f2 /. x) by A10, A11, PARTFUN2:17
.= ((f1 | X) /. x) - ((f2 | Y) /. x) by A10, A11, PARTFUN2:17 ;
then A12: ||.(((f1 - f2) | (X /\ Y)) /. x).|| <= ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| by NORMSP_1:3;
x in dom (f1 | X) by A10, A11, RELAT_1:57;
then A13: ||.((f1 | X) /. x).|| < r1 by A2;
x in dom (f2 | Y) by A10, A11, RELAT_1:57;
then ||.((f1 | X) /. x).|| + ||.((f2 | Y) /. x).|| < r1 + r2 by A13, A3, XREAL_1:8;
hence ||.(((f1 - f2) | (X /\ Y)) /. x).|| < r1 + r2 by A12, XXREAL_0:2; ::_thesis: verum
end;
theorem Th36: :: INTEGR19:36
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of (REAL-NS n) st f = g & p = q holds
( p is middle_volume of f,D iff q is middle_volume of g,D )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of (REAL-NS n) st f = g & p = q holds
( p is middle_volume of f,D iff q is middle_volume of g,D )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of (REAL-NS n) st f = g & p = q holds
( p is middle_volume of f,D iff q is middle_volume of g,D )
let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n)
for D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of (REAL-NS n) st f = g & p = q holds
( p is middle_volume of f,D iff q is middle_volume of g,D )
let g be Function of A,(REAL-NS n); ::_thesis: for D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of (REAL-NS n) st f = g & p = q holds
( p is middle_volume of f,D iff q is middle_volume of g,D )
let D be Division of A; ::_thesis: for p being FinSequence of REAL n
for q being FinSequence of (REAL-NS n) st f = g & p = q holds
( p is middle_volume of f,D iff q is middle_volume of g,D )
let p be FinSequence of REAL n; ::_thesis: for q being FinSequence of (REAL-NS n) st f = g & p = q holds
( p is middle_volume of f,D iff q is middle_volume of g,D )
let q be FinSequence of (REAL-NS n); ::_thesis: ( f = g & p = q implies ( p is middle_volume of f,D iff q is middle_volume of g,D ) )
assume A1: ( f = g & p = q ) ; ::_thesis: ( p is middle_volume of f,D iff q is middle_volume of g,D )
thus ( p is middle_volume of f,D implies q is middle_volume of g,D ) ::_thesis: ( q is middle_volume of g,D implies p is middle_volume of f,D )
proof
assume A2: p is middle_volume of f,D ; ::_thesis: q is middle_volume of g,D
then A3: len q = len D by A1, INTEGR15:def_5;
for i being Nat st i in dom D holds
ex c being Point of (REAL-NS n) st
( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c )
proof
let i be Nat; ::_thesis: ( i in dom D implies ex c being Point of (REAL-NS n) st
( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) )
assume i in dom D ; ::_thesis: ex c being Point of (REAL-NS n) st
( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c )
then consider r being Element of REAL n such that
A4: ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) by A2, INTEGR15:def_5;
reconsider c = r as Point of (REAL-NS n) by REAL_NS1:def_4;
take c ; ::_thesis: ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c )
thus ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) by A4, A1, REAL_NS1:3; ::_thesis: verum
end;
hence q is middle_volume of g,D by A3, INTEGR18:def_1; ::_thesis: verum
end;
thus ( q is middle_volume of g,D implies p is middle_volume of f,D ) ::_thesis: verum
proof
assume A5: q is middle_volume of g,D ; ::_thesis: p is middle_volume of f,D
then A6: len p = len D by A1, INTEGR18:def_1;
for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r )
proof
let i be Nat; ::_thesis: ( i in dom D implies ex r being Element of REAL n st
( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) )
assume A7: i in dom D ; ::_thesis: ex r being Element of REAL n st
( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r )
consider c being Point of (REAL-NS n) such that
A8: ( c in rng (g | (divset (D,i))) & q . i = (vol (divset (D,i))) * c ) by A5, A7, INTEGR18:def_1;
reconsider r = c as Element of REAL n by REAL_NS1:def_4;
take r ; ::_thesis: ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r )
thus ( r in rng (f | (divset (D,i))) & p . i = (vol (divset (D,i))) * r ) by A8, A1, REAL_NS1:3; ::_thesis: verum
end;
hence p is middle_volume of f,D by A6, INTEGR15:def_5; ::_thesis: verum
end;
end;
theorem Th37: :: INTEGR19:37
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for D being Division of A
for p being middle_volume of f,D
for q being middle_volume of g,D st f = g & p = q holds
middle_sum (f,p) = middle_sum (g,q)
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for D being Division of A
for p being middle_volume of f,D
for q being middle_volume of g,D st f = g & p = q holds
middle_sum (f,p) = middle_sum (g,q)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for D being Division of A
for p being middle_volume of f,D
for q being middle_volume of g,D st f = g & p = q holds
middle_sum (f,p) = middle_sum (g,q)
let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n)
for D being Division of A
for p being middle_volume of f,D
for q being middle_volume of g,D st f = g & p = q holds
middle_sum (f,p) = middle_sum (g,q)
let g be Function of A,(REAL-NS n); ::_thesis: for D being Division of A
for p being middle_volume of f,D
for q being middle_volume of g,D st f = g & p = q holds
middle_sum (f,p) = middle_sum (g,q)
let D be Division of A; ::_thesis: for p being middle_volume of f,D
for q being middle_volume of g,D st f = g & p = q holds
middle_sum (f,p) = middle_sum (g,q)
let p be middle_volume of f,D; ::_thesis: for q being middle_volume of g,D st f = g & p = q holds
middle_sum (f,p) = middle_sum (g,q)
let q be middle_volume of g,D; ::_thesis: ( f = g & p = q implies middle_sum (f,p) = middle_sum (g,q) )
assume A1: ( f = g & p = q ) ; ::_thesis: middle_sum (f,p) = middle_sum (g,q)
for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & (middle_sum (f,p)) . i = Sum Pi ) by INTEGR15:def_6;
hence middle_sum (f,p) = middle_sum (g,q) by Lm16, A1; ::_thesis: verum
end;
theorem Th38: :: INTEGR19:38
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for T being DivSequence of A
for p being Function of NAT,((REAL n) *)
for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for T being DivSequence of A
for p being Function of NAT,((REAL n) *)
for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for T being DivSequence of A
for p being Function of NAT,((REAL n) *)
for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )
let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n)
for T being DivSequence of A
for p being Function of NAT,((REAL n) *)
for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )
let g be Function of A,(REAL-NS n); ::_thesis: for T being DivSequence of A
for p being Function of NAT,((REAL n) *)
for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )
let T be DivSequence of A; ::_thesis: for p being Function of NAT,((REAL n) *)
for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )
let p be Function of NAT,((REAL n) *); ::_thesis: for q being Function of NAT,( the carrier of (REAL-NS n) *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )
let q be Function of NAT,( the carrier of (REAL-NS n) *); ::_thesis: ( f = g & p = q implies ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T ) )
assume A1: ( f = g & p = q ) ; ::_thesis: ( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )
hereby ::_thesis: ( q is middle_volume_Sequence of g,T implies p is middle_volume_Sequence of f,T )
assume A2: p is middle_volume_Sequence of f,T ; ::_thesis: q is middle_volume_Sequence of g,T
for k being Element of NAT holds q . k is middle_volume of g,T . k
proof
let k be Element of NAT ; ::_thesis: q . k is middle_volume of g,T . k
A3: p . k is middle_volume of f,T . k by A2, INTEGR15:def_7;
q . k is FinSequence of (REAL-NS n) by FINSEQ_2:def_3;
hence q . k is middle_volume of g,T . k by A1, A3, Th36; ::_thesis: verum
end;
hence q is middle_volume_Sequence of g,T by INTEGR18:def_3; ::_thesis: verum
end;
assume A4: q is middle_volume_Sequence of g,T ; ::_thesis: p is middle_volume_Sequence of f,T
for k being Element of NAT holds p . k is middle_volume of f,T . k
proof
let k be Element of NAT ; ::_thesis: p . k is middle_volume of f,T . k
A5: q . k is middle_volume of g,T . k by A4, INTEGR18:def_3;
p . k is FinSequence of REAL n by FINSEQ_2:def_3;
hence p . k is middle_volume of f,T . k by A1, A5, Th36; ::_thesis: verum
end;
hence p is middle_volume_Sequence of f,T by INTEGR15:def_7; ::_thesis: verum
end;
theorem Th39: :: INTEGR19:39
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let g be Function of A,(REAL-NS n); ::_thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T
for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let S be middle_volume_Sequence of f,T; ::_thesis: for U being middle_volume_Sequence of g,T st f = g & S = U holds
middle_sum (f,S) = middle_sum (g,U)
let U be middle_volume_Sequence of g,T; ::_thesis: ( f = g & S = U implies middle_sum (f,S) = middle_sum (g,U) )
assume A1: ( f = g & S = U ) ; ::_thesis: middle_sum (f,S) = middle_sum (g,U)
A2: dom (middle_sum (f,S)) = NAT by FUNCT_2:def_1
.= dom (middle_sum (g,U)) by FUNCT_2:def_1 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_(middle_sum_(f,S))_holds_
(middle_sum_(f,S))_._x_=_(middle_sum_(g,U))_._x
let x be set ; ::_thesis: ( x in dom (middle_sum (f,S)) implies (middle_sum (f,S)) . x = (middle_sum (g,U)) . x )
assume x in dom (middle_sum (f,S)) ; ::_thesis: (middle_sum (f,S)) . x = (middle_sum (g,U)) . x
then reconsider n = x as Element of NAT ;
A3: middle_sum (f,(S . n)) = middle_sum (g,(U . n)) by A1, Th37;
thus (middle_sum (f,S)) . x = middle_sum (f,(S . n)) by INTEGR15:def_8
.= (middle_sum (g,U)) . x by A3, INTEGR18:def_4 ; ::_thesis: verum
end;
hence middle_sum (f,S) = middle_sum (g,U) by A2, FUNCT_1:2; ::_thesis: verum
end;
theorem Th40: :: INTEGR19:40
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for I being Element of REAL n
for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for I being Element of REAL n
for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n)
for I being Element of REAL n
for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n)
for I being Element of REAL n
for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let g be Function of A,(REAL-NS n); ::_thesis: for I being Element of REAL n
for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let I be Element of REAL n; ::_thesis: for J being Point of (REAL-NS n) st f = g & I = J holds
( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
let J be Point of (REAL-NS n); ::_thesis: ( f = g & I = J implies ( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) )
assume A1: ( f = g & I = J ) ; ::_thesis: ( ( for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) iff for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) )
hereby ::_thesis: ( ( for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ) implies for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
assume A2: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; ::_thesis: for T being DivSequence of A
for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )
A3: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
thus for T being DivSequence of A
for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) ::_thesis: verum
proof
let T be DivSequence of A; ::_thesis: for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )
let S0 be middle_volume_Sequence of g,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) )
assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J )
reconsider S = S0 as middle_volume_Sequence of f,T by A3, A1, Th38;
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A2, A4;
hence ( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = J ) by A1, Th39; ::_thesis: verum
end;
end;
assume A5: for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = J ) ; ::_thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )
A6: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def_4;
thus for T being DivSequence of A
for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) ::_thesis: verum
proof
let T be DivSequence of A; ::_thesis: for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I )
let S0 be middle_volume_Sequence of f,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) )
assume A7: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I )
reconsider S = S0 as middle_volume_Sequence of g,T by A6, A1, Th38;
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = I ) by A1, A5, A7;
hence ( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I ) by A1, Th39; ::_thesis: verum
end;
end;
theorem Th41: :: INTEGR19:41
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n) st f = g & f is bounded holds
( f is integrable iff g is integrable )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n) st f = g & f is bounded holds
( f is integrable iff g is integrable )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n) st f = g & f is bounded holds
( f is integrable iff g is integrable )
let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n) st f = g & f is bounded holds
( f is integrable iff g is integrable )
let g be Function of A,(REAL-NS n); ::_thesis: ( f = g & f is bounded implies ( f is integrable iff g is integrable ) )
assume A1: ( f = g & f is bounded ) ; ::_thesis: ( f is integrable iff g is integrable )
hereby ::_thesis: ( g is integrable implies f is integrable )
assume f is integrable ; ::_thesis: g is integrable
then consider I being Element of REAL n such that
A2: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, INTEGR15:12;
reconsider I0 = I as Point of (REAL-NS n) by REAL_NS1:def_4;
I = I0 ;
then for T being DivSequence of A
for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = I0 ) by A2, A1, Th40;
hence g is integrable by INTEGR18:def_5; ::_thesis: verum
end;
assume g is integrable ; ::_thesis: f is integrable
then consider I being Point of (REAL-NS n) such that
A3: for T being DivSequence of A
for S being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S) is convergent & lim (middle_sum (g,S)) = I ) by INTEGR18:def_5;
reconsider I0 = I as Element of REAL n by REAL_NS1:def_4;
I0 = I ;
then for T being DivSequence of A
for S0 being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S0) is convergent & lim (middle_sum (f,S0)) = I0 ) by A3, A1, Th40;
hence f is integrable by A1, INTEGR15:12; ::_thesis: verum
end;
theorem Th42: :: INTEGR19:42
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds
( g is integrable & integral f = integral g )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds
( g is integrable & integral f = integral g )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n)
for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds
( g is integrable & integral f = integral g )
let f be Function of A,(REAL n); ::_thesis: for g being Function of A,(REAL-NS n) st f = g & f is bounded & f is integrable holds
( g is integrable & integral f = integral g )
let g be Function of A,(REAL-NS n); ::_thesis: ( f = g & f is bounded & f is integrable implies ( g is integrable & integral f = integral g ) )
assume A1: ( f = g & f is bounded & f is integrable ) ; ::_thesis: ( g is integrable & integral f = integral g )
then A2: g is integrable by Th41;
A3: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) by A1, INTEGR15:11;
reconsider I0 = integral f as Point of (REAL-NS n) by REAL_NS1:def_4;
integral f = I0 ;
then for T being DivSequence of A
for S0 being middle_volume_Sequence of g,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (g,S0) is convergent & lim (middle_sum (g,S0)) = I0 ) by A3, A1, Th40;
hence ( g is integrable & integral f = integral g ) by A2, INTEGR18:def_6; ::_thesis: verum
end;
theorem Th43: :: INTEGR19:43
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f holds
( f is_integrable_on A iff g is_integrable_on A )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f holds
( f is_integrable_on A iff g is_integrable_on A )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f holds
( f is_integrable_on A iff g is_integrable_on A )
let f be PartFunc of REAL,(REAL n); ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f holds
( f is_integrable_on A iff g is_integrable_on A )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = g & f | A is bounded & A c= dom f implies ( f is_integrable_on A iff g is_integrable_on A ) )
assume A1: ( f = g & f | A is bounded & A c= dom f ) ; ::_thesis: ( f is_integrable_on A iff g is_integrable_on A )
reconsider h = f | A as Function of A,(REAL n) by Lm3, A1;
reconsider k = h as Function of A,(REAL-NS n) by REAL_NS1:def_4;
A2: h is bounded by A1, Th16;
hereby ::_thesis: ( g is_integrable_on A implies f is_integrable_on A )
assume f is_integrable_on A ; ::_thesis: g is_integrable_on A
then h is integrable by INTEGR15:13;
then k is integrable by A2, Th41;
hence g is_integrable_on A by A1, INTEGR18:def_7; ::_thesis: verum
end;
assume g is_integrable_on A ; ::_thesis: f is_integrable_on A
then k is integrable by A1, INTEGR18:8;
then h is integrable by A2, Th41;
hence f is_integrable_on A by INTEGR15:13; ::_thesis: verum
end;
theorem Th44: :: INTEGR19:44
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds
( g is_integrable_on A & integral (f,A) = integral (g,A) )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds
( g is_integrable_on A & integral (f,A) = integral (g,A) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds
( g is_integrable_on A & integral (f,A) = integral (g,A) )
let f be PartFunc of REAL,(REAL n); ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g & f | A is bounded & A c= dom f & f is_integrable_on A holds
( g is_integrable_on A & integral (f,A) = integral (g,A) )
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = g & f | A is bounded & A c= dom f & f is_integrable_on A implies ( g is_integrable_on A & integral (f,A) = integral (g,A) ) )
assume A1: ( f = g & f | A is bounded & A c= dom f & f is_integrable_on A ) ; ::_thesis: ( g is_integrable_on A & integral (f,A) = integral (g,A) )
hence g is_integrable_on A by Th43; ::_thesis: integral (f,A) = integral (g,A)
reconsider h = f | A as Function of A,(REAL n) by Lm3, A1;
reconsider k = h as Function of A,(REAL-NS n) by REAL_NS1:def_4;
A2: integral (f,A) = integral h by INTEGR15:14;
A3: h is bounded by A1, Th16;
h is integrable by A1, INTEGR15:13;
then integral h = integral k by A3, Th42;
hence integral (f,A) = integral (g,A) by A2, A1, INTEGR18:9; ::_thesis: verum
end;
theorem Th45: :: INTEGR19:45
for n being Element of NAT
for a, b being real number
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds
integral (f,a,b) = integral (g,a,b)
proof
let n be Element of NAT ; ::_thesis: for a, b being real number
for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds
integral (f,a,b) = integral (g,a,b)
let a, b be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds
integral (f,a,b) = integral (g,a,b)
let f be PartFunc of REAL,(REAL n); ::_thesis: for g being PartFunc of REAL,(REAL-NS n) st f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] holds
integral (f,a,b) = integral (g,a,b)
let g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] implies integral (f,a,b) = integral (g,a,b) )
assume A1: ( f = g & a <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f & f is_integrable_on ['a,b'] ) ; ::_thesis: integral (f,a,b) = integral (g,a,b)
A2: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
A3: integral (g,['a,b']) = integral (f,['a,b']) by A1, Th44;
A4: ( a is Real & b is Real ) by XREAL_0:def_1;
then integral (g,['a,b']) = integral (g,a,b) by A2, INTEGR18:16;
hence integral (f,a,b) = integral (g,a,b) by A3, A2, A4, INTEGR15:19; ::_thesis: verum
end;
theorem :: INTEGR19:46
for n being Element of NAT
for a, b being real number
for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) )
proof
let n be Element of NAT ; ::_thesis: for a, b being real number
for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) )
let a, b be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g holds
( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) )
let f, g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g implies ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) ) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & ['a,b'] c= dom f & ['a,b'] c= dom g ) ; ::_thesis: ( integral ((f + g),a,b) = (integral (f,a,b)) + (integral (g,a,b)) & integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b)) )
A2: ( f + g is_integrable_on ['a,b'] & integral ((f + g),['a,b']) = (integral (f,['a,b'])) + (integral (g,['a,b'])) ) by A1, INTEGR18:14;
A3: ( f - g is_integrable_on ['a,b'] & integral ((f - g),['a,b']) = (integral (f,['a,b'])) - (integral (g,['a,b'])) ) by A1, INTEGR18:15;
A4: ( a is Real & b is Real ) by XREAL_0:def_1;
A5: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
thus integral ((f + g),a,b) = integral ((f + g),['a,b']) by A5, A4, INTEGR18:16
.= (integral (f,a,b)) + (integral (g,['a,b'])) by A5, A4, A2, INTEGR18:16
.= (integral (f,a,b)) + (integral (g,a,b)) by A5, A4, INTEGR18:16 ; ::_thesis: integral ((f - g),a,b) = (integral (f,a,b)) - (integral (g,a,b))
thus integral ((f - g),a,b) = integral ((f - g),['a,b']) by A5, A4, INTEGR18:16
.= (integral (f,a,b)) - (integral (g,['a,b'])) by A5, A4, A3, INTEGR18:16
.= (integral (f,a,b)) - (integral (g,a,b)) by A5, A4, INTEGR18:16 ; ::_thesis: verum
end;
theorem Th47: :: INTEGR19:47
for n being Element of NAT
for a, b being real number
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f holds
integral (f,b,a) = - (integral (f,a,b))
proof
let n be Element of NAT ; ::_thesis: for a, b being real number
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f holds
integral (f,b,a) = - (integral (f,a,b))
let a, b be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f holds
integral (f,b,a) = - (integral (f,a,b))
let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & ['a,b'] c= dom f implies integral (f,b,a) = - (integral (f,a,b)) )
assume A1: ( a <= b & ['a,b'] c= dom f ) ; ::_thesis: integral (f,b,a) = - (integral (f,a,b))
then A2: ['a,b'] = [.a,b.] by INTEGRA5:def_3;
A3: ( a is Real & b is Real ) by XREAL_0:def_1;
then integral (f,['a,b']) = integral (f,a,b) by A2, INTEGR18:16;
hence integral (f,b,a) = - (integral (f,a,b)) by A3, A2, A1, INTEGR18:18; ::_thesis: verum
end;
theorem Th48: :: INTEGR19:48
for n being Element of NAT
for a, b, c, d being real number
for f being PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = integral (g,c,d)
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
for f being PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = integral (g,c,d)
let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = integral (g,c,d)
let f be PartFunc of REAL,(REAL-NS n); ::_thesis: for g being PartFunc of REAL,(REAL n) st f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = integral (g,c,d)
let g be PartFunc of REAL,(REAL n); ::_thesis: ( f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = integral (g,c,d) )
assume A1: ( f = g & a <= b & ['a,b'] c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,c,d) = integral (g,c,d)
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A2: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1;
A3: g | ['a,b'] is bounded by A1, Th34;
A4: g is_integrable_on ['a,b'] by Th43, A3, A1;
percases ( c <= d or not c <= d ) ;
supposeA5: c <= d ; ::_thesis: integral (f,c,d) = integral (g,c,d)
( ['c,d'] c= dom g & g | ['c,d'] is bounded & g is_integrable_on ['c,d'] ) by A3, A4, A1, Th9, A2, A5, Th2;
hence integral (f,c,d) = integral (g,c,d) by A1, A5, Th45; ::_thesis: verum
end;
supposeA6: not c <= d ; ::_thesis: integral (f,c,d) = integral (g,c,d)
A7: ( ['d,c'] c= dom g & g | ['d,c'] is bounded & g is_integrable_on ['d,c'] ) by A3, A4, A1, Th9, A2, A6, Th2;
then A8: integral (f,d,c) = integral (g,d,c) by A1, A6, Th45;
thus integral (g,c,d) = - (integral (g,d,c)) by Th33
.= - (integral (f,d,c)) by A8, REAL_NS1:4
.= integral (f,c,d) by A6, A7, A1, Th47 ; ::_thesis: verum
end;
end;
end;
theorem :: INTEGR19:49
for n being Element of NAT
for a, b, c, d being real number
for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
let f, g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
reconsider f1 = f, g1 = g as PartFunc of REAL,(REAL n) by REAL_NS1:def_4;
A2: f1 | ['a,b'] is bounded by Th34, A1;
A3: g1 | ['a,b'] is bounded by Th34, A1;
A4: f1 is_integrable_on ['a,b'] by Th43, A2, A1;
A5: g1 is_integrable_on ['a,b'] by Th43, A3, A1;
A6: f1 + g1 = f + g by NFCONT_4:5;
A7: ( integral (f1,c,d) = integral (f,c,d) & integral (g1,c,d) = integral (g,c,d) ) by A1, Th48;
A8: ['a,b'] c= dom (f + g) by A1, A6, Th4;
( f1 + g1 is_integrable_on ['a,b'] & (f1 + g1) | ['a,b'] is bounded ) by A1, A2, A3, A4, A5, Th10;
then ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) by Th43, A6, A8, Th34;
hence integral ((f + g),c,d) = integral ((f1 + g1),c,d) by A1, A8, Th48, NFCONT_4:5
.= (integral (f1,c,d)) + (integral (g1,c,d)) by A1, A2, A3, A4, A5, Th27
.= (integral (f,c,d)) + (integral (g,c,d)) by A7, REAL_NS1:2 ;
::_thesis: verum
end;
theorem Th50: :: INTEGR19:50
for n being Element of NAT
for a, b, c, d being real number
for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
let a, b, c, d be real number ; ::_thesis: for f, g being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
let f, g be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d))
reconsider f1 = f, g1 = g as PartFunc of REAL,(REAL n) by REAL_NS1:def_4;
A2: f1 | ['a,b'] is bounded by Th34, A1;
A3: g1 | ['a,b'] is bounded by Th34, A1;
A4: f1 is_integrable_on ['a,b'] by Th43, A2, A1;
A5: g1 is_integrable_on ['a,b'] by Th43, A3, A1;
A6: f1 - g1 = f - g by NFCONT_4:10;
A7: ( integral (f1,c,d) = integral (f,c,d) & integral (g1,c,d) = integral (g,c,d) ) by A1, Th48;
A8: ['a,b'] c= dom (f - g) by A1, A6, Th5;
( f1 - g1 is_integrable_on ['a,b'] & (f1 - g1) | ['a,b'] is bounded ) by A1, A2, A3, A4, A5, Th13;
then ( f - g is_integrable_on ['a,b'] & (f - g) | ['a,b'] is bounded ) by Th43, A6, A8, Th34;
hence integral ((f - g),c,d) = integral ((f1 - g1),c,d) by A1, A8, Th48, NFCONT_4:10
.= (integral (f1,c,d)) - (integral (g1,c,d)) by A1, A2, A3, A4, A5, Th28
.= (integral (f,c,d)) - (integral (g,c,d)) by A7, REAL_NS1:5 ;
::_thesis: verum
end;
theorem Th51: :: INTEGR19:51
for n being Element of NAT
for a, b being real number
for E being Point of (REAL-NS n)
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
proof
let n be Element of NAT ; ::_thesis: for a, b being real number
for E being Point of (REAL-NS n)
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
let a, b be real number ; ::_thesis: for E being Point of (REAL-NS n)
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )
let e be Point of (REAL-NS n); ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e )
let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) implies ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e ) )
assume A1: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) ) ; ::_thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e )
reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def_4;
reconsider e1 = e as Element of REAL n by REAL_NS1:def_4;
A2: for x being real number st x in ['a,b'] holds
f1 . x = e1 by A1;
A3: ( f1 is_integrable_on ['a,b'] & f1 | ['a,b'] is bounded & integral (f1,a,b) = (b - a) * e1 ) by Th29, A1, A2;
integral (f1,a,b) = integral (f,a,b) by A3, A1, Th45;
hence ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e ) by A3, Th43, A1, Th34, REAL_NS1:3; ::_thesis: verum
end;
theorem Th52: :: INTEGR19:52
for n being Element of NAT
for a, b, c, d being real number
for E being Point of (REAL-NS n)
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = (d - c) * E
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
for E being Point of (REAL-NS n)
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = (d - c) * E
let a, b, c, d be real number ; ::_thesis: for E being Point of (REAL-NS n)
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = E ) & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = (d - c) * E
let e be Point of (REAL-NS n); ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) & c in ['a,b'] & d in ['a,b'] holds
integral (f,c,d) = (d - c) * e
let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = (d - c) * e )
assume A1: ( a <= b & ['a,b'] c= dom f & ( for x being real number st x in ['a,b'] holds
f . x = e ) & c in ['a,b'] & d in ['a,b'] ) ; ::_thesis: integral (f,c,d) = (d - c) * e
reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def_4;
reconsider e1 = e as Element of REAL n by REAL_NS1:def_4;
A2: for x being real number st x in ['a,b'] holds
f1 . x = e1 by A1;
A3: ( f1 is_integrable_on ['a,b'] & f1 | ['a,b'] is bounded & integral (f1,a,b) = (b - a) * e1 ) by Th29, A1, A2;
A4: integral (f1,c,d) = (d - c) * e1 by Th30, A1;
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A5: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1;
percases ( c <= d or not c <= d ) ;
supposeA6: c <= d ; ::_thesis: integral (f,c,d) = (d - c) * e
A7: ( ['c,d'] c= dom f1 & f1 | ['c,d'] is bounded & f1 is_integrable_on ['c,d'] ) by A3, A1, Th9, A5, A6, Th2;
integral (f1,c,d) = integral (f,c,d) by A7, A6, Th45;
hence integral (f,c,d) = (d - c) * e by A4, REAL_NS1:3; ::_thesis: verum
end;
supposeA8: not c <= d ; ::_thesis: integral (f,c,d) = (d - c) * e
A9: ( ['d,c'] c= dom f1 & f1 | ['d,c'] is bounded & f1 is_integrable_on ['d,c'] ) by A3, A1, Th9, A5, A8, Th2;
A10: integral (f1,d,c) = integral (f,d,c) by A9, A8, Th45;
integral (f1,c,d) = - (integral (f1,d,c)) by Th33
.= - (integral (f,d,c)) by A10, REAL_NS1:4
.= integral (f,c,d) by A8, A9, Th47 ;
hence integral (f,c,d) = (d - c) * e by A4, REAL_NS1:3; ::_thesis: verum
end;
end;
end;
theorem Th53: :: INTEGR19:53
for n being Element of NAT
for a, b, c, d being real number
for f being PartFunc of REAL,(REAL-NS 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'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d being real number
for f being PartFunc of REAL,(REAL-NS 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'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let a, b, c, d be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS 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'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( 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'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) )
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'] ) ; ::_thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A2: ( a in ['a,b'] & b in ['a,b'] ) by A1, XXREAL_1:1;
reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def_4;
A3: f1 | ['a,b'] is bounded by A1, Th34;
A4: f1 is_integrable_on ['a,b'] by Th43, A3, A1;
A5: integral (f1,a,d) = (integral (f1,a,c)) + (integral (f1,c,d)) by A3, A4, A1, Th31;
A6: integral (f,a,d) = integral (f1,a,d) by A2, Th48, A1;
A7: integral (f,a,c) = integral (f1,a,c) by A2, Th48, A1;
integral (f,c,d) = integral (f1,c,d) by Th48, A1;
hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A7, A5, A6, REAL_NS1:2; ::_thesis: verum
end;
theorem Th54: :: INTEGR19:54
for n being Element of NAT
for a, b, c, d, e being real number
for f being PartFunc of REAL,(REAL-NS 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 number st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c))
proof
let n be Element of NAT ; ::_thesis: for a, b, c, d, e being real number
for f being PartFunc of REAL,(REAL-NS 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 number st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c))
let a, b, c, d, e be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS 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 number st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c))
let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( 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 number st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) implies ||.(integral (f,c,d)).|| <= (n * e) * (abs (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 number st x in ['(min (c,d)),(max (c,d))'] holds
||.(f /. x).|| <= e ) ) ; ::_thesis: ||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c))
reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def_4;
A2: f1 | ['a,b'] is bounded by A1, Th34;
A3: f1 is_integrable_on ['a,b'] by Th43, A2, A1;
for x being real number st x in ['(min (c,d)),(max (c,d))'] holds
|.(f1 /. x).| <= e
proof
let x be real number ; ::_thesis: ( x in ['(min (c,d)),(max (c,d))'] implies |.(f1 /. x).| <= e )
assume A4: x in ['(min (c,d)),(max (c,d))'] ; ::_thesis: |.(f1 /. x).| <= e
then A5: ||.(f /. x).|| <= e by A1;
['(min (c,d)),(max (c,d))'] c= ['a,b'] by A1, Lm2;
then A6: x in ['a,b'] by A4;
then f /. x = f . x by A1, PARTFUN1:def_6
.= f1 /. x by A6, A1, PARTFUN1:def_6 ;
hence |.(f1 /. x).| <= e by A5, REAL_NS1:1; ::_thesis: verum
end;
then |.(integral (f1,c,d)).| <= (n * e) * (abs (d - c)) by A1, A2, A3, Th32;
hence ||.(integral (f,c,d)).|| <= (n * e) * (abs (d - c)) by Th48, A1, REAL_NS1:1; ::_thesis: verum
end;
begin
Lm17: for a being real number
for X being RealNormSpace
for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / (abs a)
proof
let a be real number ; ::_thesis: for X being RealNormSpace
for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / (abs a)
let X be RealNormSpace; ::_thesis: for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / (abs a)
let x be Point of X; ::_thesis: ||.((a ") * x).|| = ||.x.|| / (abs a)
thus ||.((a ") * x).|| = (abs (a ")) * ||.x.|| by NORMSP_1:def_1
.= ((abs a) ") * ||.x.|| by COMPLEX1:66
.= (1 / (abs a)) * ||.x.|| by XCMPLX_1:215
.= ||.x.|| / (abs a) by XCMPLX_1:99 ; ::_thesis: verum
end;
theorem Th55: :: INTEGR19:55
for a, b, x0 being real number
for n being non empty Element of NAT
for F, f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff (F,x0) = f /. x0 )
proof
let a, b, x0 be real number ; ::_thesis: for n being non empty Element of NAT
for F, f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff (F,x0) = f /. x0 )
let n be non empty Element of NAT ; ::_thesis: for F, f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff (F,x0) = f /. x0 )
let F, f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 implies ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) )
deffunc H1( set ) -> Element of the carrier of (REAL-NS n) = 0. (REAL-NS n);
assume that
A1: a <= b and
A2: f is_integrable_on ['a,b'] and
A3: f | ['a,b'] is bounded and
A4: ['a,b'] c= dom f and
A5: ].a,b.[ c= dom F and
A6: for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) and
A7: x0 in ].a,b.[ and
A8: f is_continuous_in x0 ; ::_thesis: ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 )
defpred S1[ set ] means x0 + (R_id $1) in ].a,b.[;
deffunc H2( Element of REAL ) -> Element of the carrier of (REAL-NS n) = $1 * (f /. x0);
consider L being Function of REAL,(REAL-NS n) such that
A9: for h being Real holds L . h = H2(h) from FUNCT_2:sch_4();
reconsider L = L as LinearFunc of (REAL-NS n) by A9, NDIFF_3:def_2;
deffunc H3( set ) -> Element of the carrier of (REAL-NS n) = ((F /. (x0 + (R_id $1))) - (F /. x0)) - (L . (R_id $1));
consider R being Function such that
A10: ( dom R = REAL & ( for x being set st x in REAL holds
( ( S1[x] implies R . x = H3(x) ) & ( not S1[x] implies R . x = H1(x) ) ) ) ) from PARTFUN1:sch_1();
rng R c= the carrier of (REAL-NS n)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng R or y in the carrier of (REAL-NS n) )
assume y in rng R ; ::_thesis: y in the carrier of (REAL-NS n)
then consider x being set such that
A11: x in dom R and
A12: y = R . x by FUNCT_1:def_3;
A13: ( not S1[x] implies R . x = H1(x) ) by A10, A11;
( S1[x] implies R . x = H3(x) ) by A10, A11;
hence y in the carrier of (REAL-NS n) by A12, A13; ::_thesis: verum
end;
then reconsider R = R as PartFunc of REAL,(REAL-NS n) by A10, RELSET_1:4;
A14: R is total by A10, PARTFUN1:def_2;
A15: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
A16: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) )
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) )
set Z0 = 0. (REAL-NS n);
A17: for e being Real st 0 < e holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e
proof
set g = REAL --> (f /. x0);
let e0 be Real; ::_thesis: ( 0 < e0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 )
set e = (e0 / 2) / n;
A18: ( h is convergent & lim h = 0 ) ;
assume A19: 0 < e0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0
then 0 < e0 / 2 by XREAL_1:215;
then 0 < (e0 / 2) / n by XREAL_1:139;
then consider p being real number such that
A20: 0 < p and
A21: for t being real number st t in dom f & abs (t - x0) < p holds
||.((f /. t) - (f /. x0)).|| < (e0 / 2) / n by A8, NFCONT_3:8;
A22: 0 < p / 2 by A20, XREAL_1:215;
A23: p / 2 < p by A20, XREAL_1:216;
consider N being Neighbourhood of x0 such that
A24: N c= ].a,b.[ by A7, RCOMP_1:18;
consider q being real number such that
A25: 0 < q and
A26: N = ].(x0 - q),(x0 + q).[ by RCOMP_1:def_6;
A27: q / 2 < q by A25, XREAL_1:216;
set r = min ((p / 2),(q / 2));
0 < q / 2 by A25, XREAL_1:215;
then 0 < min ((p / 2),(q / 2)) by A22, XXREAL_0:15;
then consider n0 being Element of NAT such that
A28: for m being Element of NAT st n0 <= m holds
abs ((h . m) - 0) < min ((p / 2),(q / 2)) by A18, SEQ_2:def_7;
take n0 ; ::_thesis: for m being Element of NAT st n0 <= m holds
||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0
let m be Element of NAT ; ::_thesis: ( n0 <= m implies ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 )
min ((p / 2),(q / 2)) <= q / 2 by XXREAL_0:17;
then A29: ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ c= ].(x0 - q),(x0 + q).[ by A27, INTEGRA6:2, XXREAL_0:2;
assume n0 <= m ; ::_thesis: ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0
then A30: abs ((h . m) - 0) < min ((p / 2),(q / 2)) by A28;
then abs ((x0 + (h . m)) - x0) < min ((p / 2),(q / 2)) ;
then x0 + (h . m) in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1;
then A31: x0 + (h . m) in ].(x0 - q),(x0 + q).[ by A29;
then A32: x0 + (h . m) in ].a,b.[ by A24, A26;
then x0 + (R_id (h . m)) in ].a,b.[ by RSSPACE:def_3;
then R . (h . m) = ((F /. (x0 + (R_id (h . m)))) - (F /. x0)) - (L . (R_id (h . m))) by A10;
then R . (h . m) = ((F /. (x0 + (h . m))) - (F /. x0)) - (L . (R_id (h . m))) by RSSPACE:def_3;
then A33: R . (h . m) = ((F /. (x0 + (h . m))) - (F /. x0)) - (L . (h . m)) by RSSPACE:def_3;
A34: F /. x0 = F . x0 by A7, A5, PARTFUN1:def_6
.= integral (f,a,x0) by A6, A7 ;
F /. (x0 + (h . m)) = F . (x0 + (h . m)) by A32, A5, PARTFUN1:def_6
.= integral (f,a,(x0 + (h . m))) by A6, A24, A26, A31 ;
then A35: R . (h . m) = ((integral (f,a,(x0 + (h . m)))) - (integral (f,a,x0))) - ((h . m) * (f /. x0)) by A34, A9, A33;
A36: dom (REAL --> (f /. x0)) = REAL by FUNCT_2:def_1;
then ['a,b'] /\ ['a,b'] c= (dom f) /\ (dom (REAL --> (f /. x0))) by A4, XBOOLE_1:27;
then A37: ['a,b'] c= dom (f - (REAL --> (f /. x0))) by VFUNCT_1:def_2;
A38: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A39: integral (f,a,(x0 + (h . m))) = (integral (f,a,x0)) + (integral (f,x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A15, A32, Th53;
A40: min ((p / 2),(q / 2)) <= p / 2 by XXREAL_0:17;
A41: for x being real number st x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] holds
||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n
proof
let x be real number ; ::_thesis: ( x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] implies ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n )
A42: ( min (x0,(x0 + (h . m))) <= x0 & x0 <= max (x0,(x0 + (h . m))) ) by XXREAL_0:17, XXREAL_0:25;
assume x in ['(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m))))'] ; ::_thesis: ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n
then A43: x in [.(min (x0,(x0 + (h . m)))),(max (x0,(x0 + (h . m)))).] by A42, INTEGRA5:def_3, XXREAL_0:2;
abs (x - x0) <= abs (h . m)
proof
percases ( x0 <= x0 + (h . m) or not x0 <= x0 + (h . m) ) ;
suppose x0 <= x0 + (h . m) ; ::_thesis: abs (x - x0) <= abs (h . m)
then ( x0 = min (x0,(x0 + (h . m))) & x0 + (h . m) = max (x0,(x0 + (h . m))) ) by XXREAL_0:def_9, XXREAL_0:def_10;
then A44: ex z being Real st
( x = z & x0 <= z & z <= x0 + (h . m) ) by A43;
then 0 <= x - x0 by XREAL_1:48;
then A45: abs (x - x0) = x - x0 by ABSVALUE:def_1;
A46: x - x0 <= (x0 + (h . m)) - x0 by A44, XREAL_1:9;
then 0 <= h . m by A44, XREAL_1:48;
hence abs (x - x0) <= abs (h . m) by A46, A45, ABSVALUE:def_1; ::_thesis: verum
end;
supposeA47: not x0 <= x0 + (h . m) ; ::_thesis: abs (x - x0) <= abs (h . m)
then ( x0 = max (x0,(x0 + (h . m))) & x0 + (h . m) = min (x0,(x0 + (h . m))) ) by XXREAL_0:def_9, XXREAL_0:def_10;
then A48: ex z being Real st
( x = z & x0 + (h . m) <= z & z <= x0 ) by A43;
then A49: (x0 + (h . m)) - x0 <= x - x0 by XREAL_1:9;
percases ( x - x0 <> 0 or x - x0 = 0 ) ;
supposeA50: x - x0 <> 0 ; ::_thesis: abs (x - x0) <= abs (h . m)
(x0 + (h . m)) - x0 < x0 - x0 by A47, XREAL_1:14;
then A51: abs (h . m) = - (h . m) by ABSVALUE:def_1;
x - x0 < 0 by A48, A50, XREAL_1:47;
then abs (x - x0) = - (x - x0) by ABSVALUE:def_1;
hence abs (x - x0) <= abs (h . m) by A49, A51, XREAL_1:24; ::_thesis: verum
end;
suppose x - x0 = 0 ; ::_thesis: abs (x - x0) <= abs (h . m)
then abs (x - x0) = 0 by ABSVALUE:def_1;
hence abs (x - x0) <= abs (h . m) by COMPLEX1:46; ::_thesis: verum
end;
end;
end;
end;
end;
then A52: abs (x - x0) < min ((p / 2),(q / 2)) by A30, XXREAL_0:2;
then x in ].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ by RCOMP_1:1;
then x in ].(x0 - q),(x0 + q).[ by A29;
then x in ].a,b.[ by A24, A26;
then A53: x in [.a,b.] by A38;
reconsider xx = x as Real by XREAL_0:def_1;
abs (x - x0) < p / 2 by A40, A52, XXREAL_0:2;
then abs (x - x0) < p by A23, XXREAL_0:2;
then ||.((f /. x) - (f /. x0)).|| <= (e0 / 2) / n by A4, A15, A21, A53;
then ||.((f /. x) - ((REAL --> (f /. x0)) /. xx)).|| <= (e0 / 2) / n by FUNCOP_1:7;
hence ||.((f - (REAL --> (f /. x0))) /. x).|| <= (e0 / 2) / n by A15, A37, A53, VFUNCT_1:def_2; ::_thesis: verum
end;
A54: for x being real number st x in ['a,b'] holds
(REAL --> (f /. x0)) . x = f /. x0 by FUNCOP_1:7;
then A55: (REAL --> (f /. x0)) | ['a,b'] is bounded by A1, A36, Th51;
then A56: (f - (REAL --> (f /. x0))) | (['a,b'] /\ ['a,b']) is bounded by A3, Th35;
rng h c= dom R by A10;
then ((h . m) ") * (R /. (h . m)) = ((h . m) ") * ((R /* h) . m) by FUNCT_2:109;
then ((h . m) ") * (R /. (h . m)) = ((h ") . m) * ((R /* h) . m) by VALUED_1:10;
then A57: ((h . m) ") * (R /. (h . m)) = ((h ") (#) (R /* h)) . m by NDIFF_1:def_2;
dom h = NAT by FUNCT_2:def_1;
then h . m <> 0 ;
then A58: 0 < abs (h . m) by COMPLEX1:47;
A59: REAL --> (f /. x0) is_integrable_on ['a,b'] by A1, A36, A54, Th51;
then A60: ||.(integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m)))).|| <= (n * ((e0 / 2) / n)) * (abs ((x0 + (h . m)) - x0)) by A1, A7, A15, A38, A32, A56, A37, A41, Th54, A2, A4, A36, INTEGR18:15;
A61: integral ((REAL --> (f /. x0)),x0,(x0 + (h . m))) = ((x0 + (h . m)) - x0) * (f /. x0) by A1, A7, A15, A38, A32, A36, A54, Th52
.= (h . m) * (f /. x0) ;
A62: integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m))) = (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A1, A2, A3, A4, A7, A15, A38, A32, A36, A59, A55, Th50;
R . (h . m) = ((integral (f,x0,(x0 + (h . m)))) + ((integral (f,a,x0)) - (integral (f,a,x0)))) - ((h . m) * (f /. x0)) by A35, A39, RLVECT_1:28
.= ((integral (f,x0,(x0 + (h . m)))) + (0. (REAL-NS n))) - ((h . m) * (f /. x0)) by RLVECT_1:15
.= (integral (f,x0,(x0 + (h . m)))) - (integral ((REAL --> (f /. x0)),x0,(x0 + (h . m)))) by A61, RLVECT_1:def_4 ;
then R /. (h . m) = integral ((f - (REAL --> (f /. x0))),x0,(x0 + (h . m))) by A62, A10, PARTFUN1:def_6;
then ( ||.(((h . m) ") * (R /. (h . m))).|| = ||.(R /. (h . m)).|| / (abs (h . m)) & ||.(R /. (h . m)).|| / (abs (h . m)) <= ((n * ((e0 / 2) / n)) * (abs (h . m))) / (abs (h . m)) ) by A60, A58, Lm17, XREAL_1:72;
then ||.(((h . m) ") * (R /. (h . m))).|| <= n * ((e0 / 2) / n) by A58, XCMPLX_1:89;
then A63: ||.(((h . m) ") * (R /. (h . m))).|| <= e0 / 2 by XCMPLX_1:87;
e0 / 2 < e0 by A19, XREAL_1:216;
then ||.(((h ") (#) (R /* h)) . m).|| < e0 by A63, A57, XXREAL_0:2;
hence ||.((((h ") (#) (R /* h)) . m) - (0. (REAL-NS n))).|| < e0 by RLVECT_1:13; ::_thesis: verum
end;
hence (h ") (#) (R /* h) is convergent by NORMSP_1:def_6; ::_thesis: lim ((h ") (#) (R /* h)) = 0. (REAL-NS n)
hence lim ((h ") (#) (R /* h)) = 0. (REAL-NS n) by A17, NORMSP_1:def_7; ::_thesis: verum
end;
consider N being Neighbourhood of x0 such that
A64: N c= ].a,b.[ by A7, RCOMP_1:18;
reconsider R = R as RestFunc of (REAL-NS n) by A14, A16, NDIFF_3:def_1;
A65: for x being Real st x in N holds
(F /. x) - (F /. x0) = (L . (x - x0)) + (R /. (x - x0))
proof
let x be Real; ::_thesis: ( x in N implies (F /. x) - (F /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
assume x in N ; ::_thesis: (F /. x) - (F /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x0 + (x - x0) in N ;
then x0 + (R_id (x - x0)) in N by RSSPACE:def_3;
then ( x0 + (R_id (x - x0)) = x0 + (x - x0) & R . (x - x0) = H3(x - x0) ) by A10, A64, RSSPACE:def_3;
then R /. (x - x0) = ((F /. x) - (F /. x0)) - (L . (x - x0)) by A10, PARTFUN1:def_6;
then (R /. (x - x0)) + (L . (x - x0)) = ((F /. x) - (F /. x0)) - ((L . (x - x0)) - (L . (x - x0))) by RLVECT_1:29
.= ((F /. x) - (F /. x0)) - (0. (REAL-NS n)) by RLVECT_1:15
.= (F /. x) - (F /. x0) by RLVECT_1:13 ;
hence (F /. x) - (F /. x0) = (L . (x - x0)) + (R /. (x - x0)) ; ::_thesis: verum
end;
A66: N c= dom F by A5, A64, XBOOLE_1:1;
hence A67: F is_differentiable_in x0 by A65, NDIFF_3:def_3; ::_thesis: diff (F,x0) = f /. x0
reconsider N1 = 1 as Real ;
L . 1 = N1 * (f /. x0) by A9
.= f /. x0 by RLVECT_1:def_8 ;
hence diff (F,x0) = f /. x0 by A66, A65, A67, NDIFF_3:def_4; ::_thesis: verum
end;
Lm18: for n being Element of NAT
for a, b being real number
for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )
proof
let n be Element of NAT ; ::_thesis: for a, b being real number
for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )
let a, b be real number ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n) ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )
deffunc H1( real number ) -> Element of the carrier of (REAL-NS n) = 0. (REAL-NS n);
let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )
defpred S1[ set ] means $1 in ].a,b.[;
deffunc H2( real number ) -> Element of the carrier of (REAL-NS n) = integral (f,a,$1);
consider F being Function such that
A1: ( dom F = REAL & ( for x being Element of REAL holds
( ( S1[x] implies F . x = H2(x) ) & ( not S1[x] implies F . x = H1(x) ) ) ) ) from PARTFUN1:sch_4();
now__::_thesis:_for_y_being_set_st_y_in_rng_F_holds_
y_in_the_carrier_of_(REAL-NS_n)
let y be set ; ::_thesis: ( y in rng F implies y in the carrier of (REAL-NS n) )
assume y in rng F ; ::_thesis: y in the carrier of (REAL-NS n)
then consider x being set such that
A2: x in dom F and
A3: y = F . x by FUNCT_1:def_3;
reconsider x = x as Element of REAL by A1, A2;
A4: now__::_thesis:_(_not_x_in_].a,b.[_implies_y_in_the_carrier_of_(REAL-NS_n)_)
assume not x in ].a,b.[ ; ::_thesis: y in the carrier of (REAL-NS n)
then F . x = 0. (REAL-NS n) by A1;
hence y in the carrier of (REAL-NS n) by A3; ::_thesis: verum
end;
now__::_thesis:_(_x_in_].a,b.[_implies_y_in_the_carrier_of_(REAL-NS_n)_)
assume x in ].a,b.[ ; ::_thesis: y in the carrier of (REAL-NS n)
then F . x = integral (f,a,x) by A1;
hence y in the carrier of (REAL-NS n) by A3; ::_thesis: verum
end;
hence y in the carrier of (REAL-NS n) by A4; ::_thesis: verum
end;
then rng F c= the carrier of (REAL-NS n) by TARSKI:def_3;
then reconsider F = F as PartFunc of REAL,(REAL-NS n) by A1, RELSET_1:4;
take F ; ::_thesis: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) )
thus ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) ) by A1; ::_thesis: verum
end;
theorem :: INTEGR19:56
for a, b, x0 being real number
for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds
ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )
proof
let a, b, x0 be real number ; ::_thesis: for n being non empty Element of NAT
for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds
ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )
let n be non empty Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds
ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )
let f be PartFunc of REAL,(REAL-NS n); ::_thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 implies ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) )
consider F being PartFunc of REAL,(REAL-NS n) such that
A1: ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) ) by Lm18;
assume ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 ) ; ::_thesis: ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 )
then ( F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) by A1, Th55;
hence ex F being PartFunc of REAL,(REAL-NS n) st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f /. x0 ) by A1; ::_thesis: verum
end;