environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PARTFUN1, SUBSET_1, FUNCT_1, RELAT_1, XXREAL_2, COMPLEX1, ARYTM_1, XXREAL_0, SEQ_4, ARYTM_3, REAL_1, FDIFF_1, RCOMP_1, TARSKI, VALUED_1, CARD_1, ORDINAL4, INTEGRA5, INTEGRA1, XXREAL_1, SQUARE_1, ORDINAL2, FUNCOP_1, FCONT_1, REALSET1, SIN_COS, PREPOWER, SEQFUNC, SEQ_1, SEQ_2, INTEGRA2, FUNCT_3, FINSEQ_1, FINSEQ_2, CARD_3, MEASURE7, NAT_1, INTEGRA7, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, XXREAL_2, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCOP_1, RELSET_1, FUNCT_2, RCOMP_1, PARTFUN1, PARTFUN2, FINSEQ_1, VALUED_1, SEQ_1, RFUNCT_1, SEQ_2, SEQ_4, SQUARE_1, PREPOWER, FCONT_1, FDIFF_1, FINSEQ_2, RVSUM_1, INTEGRA1, INTEGRA2, SEQFUNC, SIN_COS, TAYLOR_1, INTEGRA3, INTEGRA5;
definitions FDIFF_1;
theorems TARSKI, PARTFUN1, RVSUM_1, ZFMISC_1, PREPOWER, INTEGRA1, INTEGRA2, RFUNCT_1, FUNCT_1, SEQ_1, SEQ_2, FDIFF_1, SEQFUNC, ABSVALUE, XCMPLX_1, FINSEQ_1, FINSEQ_2, RCOMP_1, FCONT_1, FDIFF_2, RELAT_1, XREAL_0, XXREAL_0, PARTFUN2, FUNCT_2, XBOOLE_0, XBOOLE_1, SEQ_4, XREAL_1, COMPLEX1, INTEGRA4, INTEGRA5, SIN_COS, INTEGRA6, TAYLOR_1, VALUED_1, XXREAL_1, XXREAL_2, FUNCOP_1, ORDINAL1;
schemes FUNCT_2, XBOOLE_0;
registrations XREAL_0, RELSET_1, INTEGRA1, RCOMP_1, INT_1, MEMBERED, PREPOWER, XBOOLE_0, NUMBERS, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, SEQ_2, FCONT_3, MEASURE5, SQUARE_1;
constructors HIDDEN, REAL_1, FDIFF_1, PARTFUN2, RFUNCT_1, INTEGRA2, LIMFUNC1, FCONT_1, BINOP_2, INTEGRA5, SIN_COS, PREPOWER, TAYLOR_1, SQUARE_1, SEQFUNC, RVSUM_1, SEQ_4, RELSET_1, SEQ_2, COMPLEX1, INTEGRA3, COMSEQ_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities XCMPLX_0, SUBSET_1, INTEGRA1, INTEGRA5, VALUED_1, SQUARE_1;
expansions INTEGRA1, INTEGRA5, FDIFF_1;
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
for
a,
b being
Real 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 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 for
f,
F being
PartFunc of
REAL,
REAL for
x,
x0 being
Real 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 Th21:
for
a,
b being
Real 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
for
a,
b being
Real 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
for
a,
b being
Real 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) )