:: 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 Association of Mizar Users
theorem Th1: :: INTEGRA7:1
theorem Th2: :: INTEGRA7:2
theorem Th3: :: INTEGRA7:3
theorem Th4: :: INTEGRA7:4
theorem :: INTEGRA7:5
theorem Th6: :: INTEGRA7:6
theorem Th7: :: INTEGRA7:7
theorem Th8: :: INTEGRA7:8
theorem :: INTEGRA7:9
theorem Th10: :: INTEGRA7:10
:: deftheorem Def1 defines IntegralFuncs INTEGRA7:def 1 :
:: 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 ) )
theorem Th11: :: INTEGRA7:11
theorem :: INTEGRA7:12
theorem :: INTEGRA7:13
theorem :: INTEGRA7:14
theorem :: INTEGRA7:15
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.[
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)
theorem Th18: :: INTEGRA7:18
theorem Th19: :: INTEGRA7:19
theorem Th20: :: INTEGRA7:20
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)
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)
theorem Th23: :: INTEGRA7:23
theorem :: INTEGRA7:24
theorem Th25: :: INTEGRA7:25
theorem :: INTEGRA7:26
theorem Th27: :: INTEGRA7:27
theorem :: INTEGRA7:28
theorem Th29: :: INTEGRA7:29
theorem :: INTEGRA7:30
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 )