INTEGRA7: Riemann Indefinite Integral of Functions of Real Variable

:: Riemann Indefinite Integral of Functions of Real Variable
:: by Yasunari Shidama , Noboru Endou , Katsumi Wasaki and Katuhiko Kanazashi
::
:: Received June 6, 2007
:: Copyright (c) 2007-2011 Association of Mizar Users

begin

theorem Th1: :: INTEGRA7:1

for a being real number
for A being non empty set
for f, g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ) holds
( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a )

proof end;

theorem Th2: :: INTEGRA7:2

for a being real number
for A being non empty set
for f, g being Function of A,REAL st rng f is bounded_below & rng g is bounded_below & ( for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ) holds
( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a )

proof end;

theorem :: INTEGRA7:3

for X being set
for f being PartFunc of REAL,REAL st (f | X) | X is bounded holds
f | X is bounded by RELAT_1:101;

theorem Th4: :: INTEGRA7:4

for X being set
for f being PartFunc of REAL,REAL
for x being Real st x in X & f | X is_differentiable_in x holds
f is_differentiable_in x

proof end;

theorem :: INTEGRA7:5

for X being set
for f being PartFunc of REAL,REAL st f | X is_differentiable_on X holds
f is_differentiable_on X

proof end;

theorem Th6: :: INTEGRA7:6

for X being set
for f, g being PartFunc of REAL,REAL st f is_differentiable_on X & g is_differentiable_on X holds
( f + g is_differentiable_on X & f - g is_differentiable_on X & f (#) g is_differentiable_on X )

proof end;

theorem Th7: :: INTEGRA7:7

for r being real number
for X being set
for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
r (#) f is_differentiable_on X

proof end;

theorem Th8: :: INTEGRA7:8

for X being set
for g, f being PartFunc of REAL,REAL st ( for x being set st x in X holds
g . x <> 0 ) & f is_differentiable_on X & g is_differentiable_on X holds
f / g is_differentiable_on X

proof end;

theorem :: INTEGRA7:9

for X being set
for f being PartFunc of REAL,REAL st ( for x being set st x in X holds
f . x <> 0 ) & f is_differentiable_on X holds
f ^ is_differentiable_on X

proof end;

theorem Th10: :: INTEGRA7:10

for a, b being real number
for X being set
for F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_differentiable_on X & F `| X is_integrable_on ['a,b'] & (F `| X) | ['a,b'] is bounded holds
F . b = (integral ((F `| X),a,b)) + (F . a)

proof end;

begin

definition

let X be set ;
let f be PartFunc of REAL,REAL;
func IntegralFuncs (f,X) -> set means :Def1: :: INTEGRA7:def 1
for x being set holds
( x in it iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) );
existence

proof end;

proof end;

end;

:: deftheorem Def1 defines IntegralFuncs INTEGRA7:def 1 :

definition

let X be set ;
let F, f be PartFunc of REAL,REAL;
pred F is_integral_of f,X means :Def2: :: INTEGRA7:def 2
F in IntegralFuncs (f,X);

end;

:: deftheorem Def2 defines is_integral_of INTEGRA7:def 2 :

Lm1: for X being set
for F, f being PartFunc of REAL,REAL holds
( F is_integral_of f,X iff ( F is_differentiable_on X & F `| X = f | X ) )

proof end;

theorem Th11: :: INTEGRA7:11

for X being set
for F, f being PartFunc of REAL,REAL st F is_integral_of f,X holds
X c= dom F

proof end;

theorem :: INTEGRA7:12

for X being set
for F, f, G, g being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds
( F + G is_integral_of f + g,X & F - G is_integral_of f - g,X )

proof end;

theorem :: INTEGRA7:13

for r being real number
for X being set
for F, f being PartFunc of REAL,REAL st F is_integral_of f,X holds
r (#) F is_integral_of r (#) f,X

proof end;

theorem :: INTEGRA7:14

for X being set
for F, f, G, g being PartFunc of REAL,REAL st F is_integral_of f,X & G is_integral_of g,X holds
F (#) G is_integral_of (f (#) G) + (F (#) g),X

proof end;

theorem :: INTEGRA7:15

for X being set
for G, F, f, g being PartFunc of REAL,REAL st ( for x being set st x in X holds
G . x <> 0 ) & F is_integral_of f,X & G is_integral_of g,X holds
F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X

proof end;

theorem :: INTEGRA7:16

for a, b being real number
for f, F being PartFunc of REAL,REAL st a <= b & ['a,b'] c= dom f & f | ['a,b'] is continuous & ].a,b.[ c= dom F & ( for x being real number st x in ].a,b.[ holds
F . x = (integral (f,a,x)) + (F . a) ) holds
F is_integral_of f,].a,b.[

proof end;

theorem :: INTEGRA7:17

for a, b being real number
for f, F being PartFunc of REAL,REAL
for x, x0 being real number st f | [.a,b.] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds
F . x = (integral (f,x0,x)) + (F . x0)

proof end;

theorem Th18: :: INTEGRA7:18

for a, b being real number
for X being set
for F, f being PartFunc of REAL,REAL st a <= b & ['a,b'] c= X & F is_integral_of f,X & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
F . b = (integral (f,a,b)) + (F . a)

proof end;

theorem Th19: :: INTEGRA7:19

for a, b being real number
for X being set
for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous holds
( f | ['a,b'] is continuous & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded )

proof end;

theorem Th20: :: INTEGRA7:20

for a, b being real number
for X being set
for f, F being PartFunc of REAL,REAL st a <= b & [.a,b.] c= X & X c= dom f & f | X is continuous & F is_integral_of f,X holds
F . b = (integral (f,a,b)) + (F . a)

proof end;

theorem Th21: :: INTEGRA7:21

for b, a being real number
for X being set
for f, g, F, G being PartFunc of REAL,REAL st b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X holds
((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a))

proof end;

theorem :: INTEGRA7:22

for b, a being real number
for X being set
for f, g, F, G being PartFunc of REAL,REAL st b <= a & [.b,a.] c= X & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & F is_integral_of f,X & G is_integral_of g,X holds
((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a))

proof end;

begin

theorem Th23: :: INTEGRA7:23

sin is_integral_of cos , REAL

proof end;

theorem :: INTEGRA7:24

for b, a being real number holds (sin . b) - (sin . a) = integral (cos,a,b)

proof end;

theorem Th25: :: INTEGRA7:25

(- 1) (#) cos is_integral_of sin , REAL

proof end;

theorem :: INTEGRA7:26

for a, b being real number holds (cos . a) - (cos . b) = integral (sin,a,b)

proof end;

theorem Th27: :: INTEGRA7:27

exp_R is_integral_of exp_R , REAL

proof end;

theorem :: INTEGRA7:28

for b, a being real number holds (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)

proof end;

theorem Th29: :: INTEGRA7:29

for n being Element of NAT holds #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL

proof end;

theorem :: INTEGRA7:30

for b, a being real number
for n being Element of NAT holds ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b)

proof end;

begin

theorem :: INTEGRA7:31

for a, b being real number
for H being Functional_Sequence of REAL,REAL
for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) ) ) & H is_unif_conv_on ['a,b'] holds
( (lim (H,['a,b'])) | ['a,b'] is bounded & lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) )

proof end;