:: by Noboru Endou , Yasunari Shidama and Masahiko Yamazaki

::

:: Received November 17, 2006

:: Copyright (c) 2006-2021 Association of Mizar Users

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

proof end;

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 & |.(integral (f,A)).| <= integral ((abs f),A) )

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 & |.(integral (f,A)).| <= integral ((abs f),A) )

proof end;

theorem Th8: :: INTEGRA6:8

for a, b being Real

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 (f,a,b)).| <= integral ((abs f),a,b)

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 (f,a,b)).| <= integral ((abs f),a,b)

proof end;

theorem Th9: :: INTEGRA6:9

for r being Real

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

( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

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

( 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

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

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

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

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

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

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

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 non empty closed_interval Subset of REAL

for n being Nat st n > 0 & vol A > 0 holds

ex D being Division of A st

( len D = n & ( for i being Nat st i in dom D holds

D . i = (lower_bound A) + (((vol A) / n) * i) ) )

for n being Nat st n > 0 & vol A > 0 holds

ex D being Division of A st

( len D = n & ( for i being Nat st i in dom D holds

D . i = (lower_bound A) + (((vol A) / n) * i) ) )

proof end;

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

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

proof end;

Lm2: for a, b, c being Real

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

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

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 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, b, c, d being Real

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 )

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, b, c, d being Real

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 )

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

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

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

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

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 & |.(integral (f,c,d)).| <= integral ((abs f),c,d) )

proof end;

theorem Th21: :: INTEGRA6:21

for a, b, c, d being Real

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 & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) )

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 & |.(integral (f,c,d)).| <= integral ((abs f),(min (c,d)),(max (c,d))) )

proof end;

Lm6: for a, b, c, d being Real

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 & |.(integral (f,c,d)).| <= integral ((abs f),c,d) )

proof end;

Lm7: for a, b, c, d being Real

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,d,c)).| <= integral ((abs f),c,d)

proof end;

theorem :: INTEGRA6:22

for a, b, c, d being Real

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 & |.(integral (f,c,d)).| <= integral ((abs f),c,d) & |.(integral (f,d,c)).| <= integral ((abs f),c,d) ) by Lm6, Lm7;

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 & |.(integral (f,c,d)).| <= integral ((abs f),c,d) & |.(integral (f,d,c)).| <= integral ((abs f),c,d) ) by Lm6, Lm7;

Lm8: for a, b, c, d, e being Real

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 st x in ['(min (c,d)),(max (c,d))'] holds

|.(f . x).| <= e ) holds

|.(integral (f,c,d)).| <= e * |.(d - c).|

proof end;

Lm9: for a, b, c, d, e being Real

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 st x in ['c,d'] holds

|.(f . x).| <= e ) holds

|.(integral (f,c,d)).| <= e * (d - c)

proof end;

Lm10: for a, b, c, d, e being Real

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 st x in ['c,d'] holds

|.(f . x).| <= e ) holds

|.(integral (f,d,c)).| <= e * (d - c)

proof end;

theorem :: INTEGRA6:23

for a, b, c, d, e being Real

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 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 Lm9, Lm10;

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 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 Lm9, Lm10;

Lm11: for a, b, c, d being Real

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

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

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

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

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

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

for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ( for x being Real 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) )

for f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & ( for x being Real 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, c, d, e being Real

for f being PartFunc of REAL,REAL st a <= b & ( for x being Real 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)

for f being PartFunc of REAL,REAL st a <= b & ( for x being Real 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

for f being PartFunc of REAL,REAL

for x0 being Real

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

for f being PartFunc of REAL,REAL

for x0 being Real

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

for f being PartFunc of REAL,REAL ex F being PartFunc of REAL,REAL st

( ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds

F . x = integral (f,a,x) ) )

proof end;

theorem :: INTEGRA6:29

for a, b being Real

for f being PartFunc of REAL,REAL

for x0 being Real 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 st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 )

for f being PartFunc of REAL,REAL

for x0 being Real 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 st x in ].a,b.[ holds

F . x = integral (f,a,x) ) & F is_differentiable_in x0 & diff (F,x0) = f . x0 )

proof end;