:: 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 Association of Mizar Users

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 )

proof end;

theorem Th2: :: INTEGRA6:2

for a, b, x being real number st a <= b holds
].(x - a),(x + a).[ c= ].(x - b),(x + b).[

proof end;

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

proof end;

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

proof end;

theorem Th5: :: INTEGRA6:5

for a, b being real number st a <= b holds
vol ['a,b'] = b - a

proof end;

theorem Th6: :: INTEGRA6:6

for a, b being real number holds vol ['(min a,b),(max a,b)'] = abs (b - a)

proof end;

Lm1: for A being 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

proof end;

theorem Th7: :: INTEGRA6:7

for A being 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 )

proof end;

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

proof end;

theorem Th9: :: INTEGRA6:9

for A being 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) )

proof end;

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)

proof end;

theorem Th11: :: INTEGRA6:11

for A being 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) )

proof end;

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) )

proof end;

theorem :: INTEGRA6:13

for A being 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

proof end;

theorem :: INTEGRA6:14

for A being 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

proof end;

theorem Th15: :: INTEGRA6:15

for A being closed-interval Subset of REAL
for n being Element of NAT st n > 0 & vol A > 0 holds
ex D being Element of divs A st
( len D = n & ( for i being Element of NAT st i in dom D holds
D . i = (inf A) + (((vol A) / n) * i) ) )

proof end;

theorem Th16: :: INTEGRA6:16

for A being 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 Element of divs A st
( Tn divide_into_equal n + 1 & T . n = Tn ) ) )

proof end;

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'] )

proof end;

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) )

proof end;

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'] )

proof end;

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 )

proof end;

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 )

proof end;

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)

proof end;

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)

proof end;

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 )

proof end;

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) )

proof end;

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 )

proof end;

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

proof end;

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))

proof end;

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)

proof end;

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)

proof end;

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) )

proof end;

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) )

proof end;

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)

proof end;

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)

proof end;

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) )

proof end;

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)

proof end;

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 )

proof end;

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 ) )

proof end;

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 )

proof end;