:: 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
ex b1 being set st
for x being set holds
( x in b1 iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) & ( for x being set holds
( x in b2 iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines IntegralFuncs INTEGRA7:def 1 :
for X being set
for f being PartFunc of REAL,REAL
for b3 being set holds
( b3 = IntegralFuncs (f,X) iff for x being set holds
( x in b3 iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) );

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 :
for X being set
for F, f being PartFunc of REAL,REAL holds
( F is_integral_of f,X iff F in IntegralFuncs (f,X) );

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;