:: Integrability and the Integral of Partial Functions from $\Bbb R$ into $\Bbb R$ :: by Noboru Endou , Yasunari Shidama and Masahiko Yamazaki :: :: Received November 17, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin theorem Th1: :: INTEGRA6:1 for a, b, c, d being real number st a <= b & c <= d & a + c = b + d holds ( a = b & c = d ) proofend; theorem Th2: :: INTEGRA6:2 for a, b, x being real number st a <= b holds ].(x - a),(x + a).[ c= ].(x - b),(x + b).[ proofend; theorem Th3: :: INTEGRA6:3 for R being Relation for A, B, C being set st A c= B & A c= C holds (R | B) | A = (R | C) | A proofend; theorem Th4: :: INTEGRA6:4 for A, B, C being set st A c= B & A c= C holds (chi (B,B)) | A = (chi (C,C)) | A proofend; theorem Th5: :: INTEGRA6:5 for a, b being real number st a <= b holds vol ['a,b'] = b - a proofend; theorem Th6: :: INTEGRA6:6 for a, b being real number holds vol ['(min (a,b)),(max (a,b))'] = abs (b - a) proofend; begin Lm1: 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 proofend; theorem Th7: :: INTEGRA6:7 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL st A c= dom f & f is_integrable_on A & f | A is bounded holds ( abs f is_integrable_on A & abs (integral (f,A)) <= integral ((abs f),A) ) proofend; theorem Th8: :: INTEGRA6:8 for a, b being real number for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds abs (integral (f,a,b)) <= integral ((abs f),a,b) proofend; theorem Th9: :: INTEGRA6:9 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for r being Real st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) proofend; theorem Th10: :: INTEGRA6:10 for a, b, c being real number for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds integral ((c (#) f),a,b) = c * (integral (f,a,b)) proofend; theorem Th11: :: INTEGRA6:11 for A being non empty closed_interval Subset of REAL for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds ( f + g is_integrable_on A & f - g is_integrable_on A & integral ((f + g),A) = (integral (f,A)) + (integral (g,A)) & integral ((f - g),A) = (integral (f,A)) - (integral (g,A)) ) proofend; theorem Th12: :: INTEGRA6:12 for a, b being real number for f, g being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded 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)) ) proofend; theorem :: INTEGRA6:13 for A being non empty closed_interval Subset of REAL for f, g being PartFunc of REAL,REAL st f | A is bounded & g | A is bounded holds (f (#) g) | A is bounded proofend; theorem :: INTEGRA6:14 for A being non empty closed_interval Subset of REAL for f, g being PartFunc of REAL,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds f (#) g is_integrable_on A proofend; theorem Th15: :: INTEGRA6:15 for A being non empty closed_interval Subset of REAL for n being Element of NAT st n > 0 & vol A > 0 holds ex D being Division of A st ( len D = n & ( for i being Element of NAT st i in dom D holds D . i = (lower_bound A) + (((vol A) / n) * i) ) ) proofend; begin theorem Th16: :: INTEGRA6:16 for A being non empty closed_interval Subset of REAL st vol A > 0 holds ex T being DivSequence of A st ( delta T is convergent & lim (delta T) = 0 & ( for n being Element of NAT ex Tn being Division of A st ( Tn divide_into_equal n + 1 & T . n = Tn ) ) ) proofend; Lm2: for a, b, c being real number for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & c in ['a,b'] & b <> c holds ( integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) & f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] ) proofend; theorem Th17: :: INTEGRA6:17 for a, b, c 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'] 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)) ) proofend; Lm3: for a, b, c being real number st a <= c & c <= b holds ( c in ['a,b'] & ['a,c'] c= ['a,b'] & ['c,b'] c= ['a,b'] ) proofend; theorem Th18: :: INTEGRA6:18 for a, c, d, b 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 ( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded & ['c,d'] c= dom f ) proofend; theorem :: INTEGRA6:19 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 ) proofend; Lm4: for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & 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)) proofend; theorem Th20: :: INTEGRA6:20 for a, b, c, d 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'] holds integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) proofend; Lm5: for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & 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 ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) proofend; theorem Th21: :: INTEGRA6:21 for a, b, c, d 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'] holds ( ['(min (c,d)),(max (c,d))'] c= dom (abs f) & abs f is_integrable_on ['(min (c,d)),(max (c,d))'] & (abs f) | ['(min (c,d)),(max (c,d))'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),(min (c,d)),(max (c,d))) ) proofend; Lm6: for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & 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 ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) ) proofend; Lm7: for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & 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 abs (integral (f,d,c)) <= integral ((abs f),c,d) proofend; theorem :: INTEGRA6:22 for a, b, c, d being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & 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 ( ['c,d'] c= dom (abs f) & abs f is_integrable_on ['c,d'] & (abs f) | ['c,d'] is bounded & abs (integral (f,c,d)) <= integral ((abs f),c,d) & abs (integral (f,d,c)) <= integral ((abs f),c,d) ) by Lm6, Lm7; Lm8: 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)) proofend; Lm9: for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & 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 abs (f . x) <= e ) holds abs (integral (f,c,d)) <= e * (d - c) proofend; Lm10: for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & 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 abs (f . x) <= e ) holds abs (integral (f,d,c)) <= e * (d - c) proofend; theorem :: INTEGRA6:23 for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & 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 abs (f . x) <= e ) holds ( abs (integral (f,c,d)) <= e * (d - c) & abs (integral (f,d,c)) <= e * (d - c) ) by Lm9, Lm10; Lm11: for a, b, c, d being real number for f, g being PartFunc of REAL,REAL st a <= b & c <= d & 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 ( f + g is_integrable_on ['c,d'] & (f + g) | ['c,d'] is bounded & integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) & f - g is_integrable_on ['c,d'] & (f - g) | ['c,d'] is bounded & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) proofend; theorem Th24: :: INTEGRA6:24 for a, b, c, d being real number for f, g being PartFunc of REAL,REAL 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)) & integral ((f - g),c,d) = (integral (f,c,d)) - (integral (g,c,d)) ) proofend; Lm12: for a, b, c, d, e being real number for f being PartFunc of REAL,REAL st a <= b & c <= d & 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 ((e (#) f),c,d) = e * (integral (f,c,d)) proofend; theorem :: INTEGRA6:25 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'] holds integral ((e (#) f),c,d) = e * (integral (f,c,d)) proofend; theorem Th26: :: INTEGRA6:26 for a, b, e being real number for f being PartFunc of REAL,REAL 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) = e * (b - a) ) proofend; theorem Th27: :: INTEGRA6:27 for a, b, e, c, d being real number for f being PartFunc of REAL,REAL 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) = e * (d - c) proofend; begin theorem Th28: :: INTEGRA6:28 for a, b being real number for f being PartFunc of REAL,REAL for x0 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 & ].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 ) proofend; Lm13: for a, b being real number for f being PartFunc of REAL,REAL ex F being PartFunc of REAL,REAL st ( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds F . x = integral (f,a,x) ) ) proofend; theorem :: INTEGRA6:29 for a, b being real number for f being PartFunc of REAL,REAL for x0 being real number 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 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 ) proofend;