begin
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
begin
:: 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 , holds
( F is_integral_of f,X iff ( F is_differentiable_on X & F `| X = f | X ) )
theorem Th11:
theorem
theorem
theorem
theorem
theorem
for
a,
b being
real number for
f,
F being
PartFunc of , 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
for
a,
b being
real number for
f,
F being
PartFunc of ,
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:
theorem Th19:
theorem Th20:
theorem Th21:
for
b,
a being
real number for
X being
set for
f,
g,
F,
G being
PartFunc of , 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
for
b,
a being
real number for
X being
set for
f,
g,
F,
G being
PartFunc of , 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)
begin
theorem Th23:
theorem
theorem Th25:
theorem
theorem Th27:
theorem
theorem Th29:
theorem
begin
theorem
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 )