:: 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-2012 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 &amp; (upper_bound (rng g)) - (upper_bound (rng f)) <= a )
proofend;

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 &amp; rng g is bounded_below &amp; ( 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 &amp; (lower_bound (rng g)) - (lower_bound (rng f)) <= a )
proofend;

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:72;

theorem Th4: :: INTEGRA7:4
for X being set
for f being PartFunc of REAL,REAL
for x being Real st x in X &amp; f | X is_differentiable_in x holds
f is_differentiable_in x
proofend;

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

theorem Th6: :: INTEGRA7:6
for X being set
for f, g being PartFunc of REAL,REAL st f is_differentiable_on X &amp; g is_differentiable_on X holds
( f + g is_differentiable_on X &amp; f - g is_differentiable_on X &amp; f (#) g is_differentiable_on X )
proofend;

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

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 ) &amp; f is_differentiable_on X &amp; g is_differentiable_on X holds
f / g is_differentiable_on X
proofend;

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 ) &amp; f is_differentiable_on X holds
f ^ is_differentiable_on X
proofend;

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

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

definition
let X be set ;
let F, f be PartFunc of REAL,REAL;
predF 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 &amp; F `| X = f | X ) )
proofend;

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

theorem :: INTEGRA7:12
for X being set
for F, f, G, g being PartFunc of REAL,REAL st F is_integral_of f,X &amp; G is_integral_of g,X holds
( F + G is_integral_of f + g,X &amp; F - G is_integral_of f - g,X )
proofend;

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

theorem :: INTEGRA7:14
for X being set
for F, f, G, g being PartFunc of REAL,REAL st F is_integral_of f,X &amp; G is_integral_of g,X holds
F (#) G is_integral_of (f (#) G) + (F (#) g),X
proofend;

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 ) &amp; F is_integral_of f,X &amp; G is_integral_of g,X holds
F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X
proofend;

theorem :: INTEGRA7:16
for a, b being real number
for f, F being PartFunc of REAL,REAL st a <= b &amp; ['a,b'] c= dom f &amp; f | ['a,b'] is continuous &amp; ].a,b.[ c= dom F &amp; ( 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.[
proofend;

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 &amp; [.a,b.] c= dom f &amp; x in ].a,b.[ &amp; x0 in ].a,b.[ &amp; F is_integral_of f,].a,b.[ holds
F . x = (integral (f,x0,x)) + (F . x0)
proofend;

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 &amp; ['a,b'] c= X &amp; F is_integral_of f,X &amp; f is_integrable_on ['a,b'] &amp; f | ['a,b'] is bounded holds
F . b = (integral (f,a,b)) + (F . a)
proofend;

theorem Th19: :: INTEGRA7:19
for a, b being real number
for X being set
for f being PartFunc of REAL,REAL st a <= b &amp; [.a,b.] c= X &amp; X c= dom f &amp; f | X is continuous holds
( f | ['a,b'] is continuous &amp; f is_integrable_on ['a,b'] &amp; f | ['a,b'] is bounded )
proofend;

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 &amp; [.a,b.] c= X &amp; X c= dom f &amp; f | X is continuous &amp; F is_integral_of f,X holds
F . b = (integral (f,a,b)) + (F . a)
proofend;

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 &amp; ['b,a'] c= X &amp; f is_integrable_on ['b,a'] &amp; g is_integrable_on ['b,a'] &amp; f | ['b,a'] is bounded &amp; g | ['b,a'] is bounded &amp; X c= dom f &amp; X c= dom g &amp; F is_integral_of f,X &amp; 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))
proofend;

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 &amp; [.b,a.] c= X &amp; X c= dom f &amp; X c= dom g &amp; f | X is continuous &amp; g | X is continuous &amp; F is_integral_of f,X &amp; 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))
proofend;

begin

theorem Th23: :: INTEGRA7:23
sin is_integral_of cos , REAL
proofend;

theorem :: INTEGRA7:24
for b, a being real number holds (sin . b) - (sin . a) = integral (cos,a,b)
proofend;

theorem Th25: :: INTEGRA7:25
(- 1) (#) cos is_integral_of sin , REAL
proofend;

theorem :: INTEGRA7:26
for a, b being real number holds (cos . a) - (cos . b) = integral (sin,a,b)
proofend;

theorem Th27: :: INTEGRA7:27
exp_R is_integral_of exp_R , REAL
proofend;

theorem :: INTEGRA7:28
for b, a being real number holds (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
proofend;

theorem Th29: :: INTEGRA7:29
for n being Element of NAT holds #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL
proofend;

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

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 &amp; ( for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] &amp; (H . n) | ['a,b'] is bounded &amp; rseq . n = integral ((H . n),a,b) ) ) &amp; H is_unif_conv_on ['a,b'] holds
( (lim (H,['a,b'])) | ['a,b'] is bounded &amp; lim (H,['a,b']) is_integrable_on ['a,b'] &amp; rseq is convergent &amp; lim rseq = integral ((lim (H,['a,b'])),a,b) )
proofend;