begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
Lm1:
for A being closed-interval Subset of
for f being PartFunc of , st A c= dom f holds
f || A is Function of A, REAL
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
for
a,
b,
c being
real number for
f being
PartFunc of , 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)
theorem Th11:
theorem Th12:
for
a,
b being
real number for
f,
g being
PartFunc of , 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) )
theorem
theorem
theorem Th15:
begin
theorem Th16:
Lm2:
for a, b, c being real number
for f being PartFunc of , 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'] )
theorem Th17:
for
a,
b,
c being
real number for
f being
PartFunc of , 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) )
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'] )
theorem Th18:
for
a,
c,
d,
b being
real number for
f being
PartFunc of , 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 )
theorem
for
a,
c,
d,
b being
real number for
f,
g being
PartFunc of , 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 )
Lm4:
for a, b, c, d being real number
for f being PartFunc of , 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)
theorem Th20:
for
a,
b,
c,
d being
real number for
f being
PartFunc of , 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)
Lm5:
for a, b, c, d being real number
for f being PartFunc of , 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 )
theorem Th21:
for
a,
b,
c,
d being
real number for
f being
PartFunc of , 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) )
Lm6:
for a, b, c, d being real number
for f being PartFunc of , 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 )
Lm7:
for a, b, c, d being real number
for f being PartFunc of , 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
theorem
for
a,
b,
c,
d being
real number for
f being
PartFunc of , 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 , 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))
Lm9:
for a, b, c, d, e being real number
for f being PartFunc of , 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)
Lm10:
for a, b, c, d, e being real number
for f being PartFunc of , 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)
theorem
for
a,
b,
c,
d,
e being
real number for
f being
PartFunc of , 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 , 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) )
theorem Th24:
for
a,
b,
c,
d being
real number for
f,
g being
PartFunc of , 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) )
Lm12:
for a, b, c, d, e being real number
for f being PartFunc of , 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)
theorem
for
a,
b,
c,
d,
e being
real number for
f being
PartFunc of , 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)
theorem Th26:
theorem Th27:
for
a,
b,
e,
c,
d being
real number for
f being
PartFunc of , 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)
begin
theorem Th28:
for
a,
b being
real number for
f being
PartFunc of ,
for
x0 being
real number for
F being
PartFunc of , 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 )
Lm13:
for a, b being real number
for f being PartFunc of , ex F being PartFunc of , st
( ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = integral f,a,x ) )
theorem
for
a,
b being
real number for
f being
PartFunc of ,
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 , 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 )