:: Integrability of Bounded Total Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received February 1, 2000
:: Copyright (c) 2000-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, INTEGRA1, XBOOLE_0, MEASURE7, CARD_1,
FINSEQ_1, RELAT_1, XXREAL_0, FUNCT_1, SEQ_4, ARYTM_3, ARYTM_1, FUNCT_3,
TARSKI, PARTFUN1, CARD_3, VALUED_1, XXREAL_2, XXREAL_1, INTEGRA2, SEQ_2,
ORDINAL2, FINSET_1, NAT_1, FINSEQ_2, VALUED_0, FDIFF_1, COMPLEX1, INT_1,
ZFMISC_1, RFUNCT_3, SEQ_1, ORDINAL4, SQUARE_1, INTEGRA4, MEASURE5,
FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, NAT_1, INT_1, XXREAL_2, VALUED_0, ZFMISC_1, FUNCT_1,
RELSET_1, FINSET_1, FUNCT_2, FINSEQ_1, VALUED_1, SEQ_1, RFUNCT_1,
FINSEQ_2, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, FDIFF_1, SQUARE_1, RVSUM_1,
MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, RFUNCT_3, PARTFUN1, XXREAL_0;
constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP, FINSOP_1,
PARTFUN2, FDIFF_1, ZFMISC_1, RFUNCT_3, INTEGRA2, XXREAL_2, RVSUM_1,
SEQ_4, RELSET_1, SEQ_2, INTEGRA3, COMSEQ_2;
registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCT_2, FINSET_1, NUMBERS,
XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, INTEGRA1, VALUED_0,
VALUED_1, XXREAL_2, CARD_1, SEQ_2, RELSET_1, SEQM_3, MEASURE5, SQUARE_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Basic integrable functions and first mean value theorem
reserve i,j,k,n,n1,n2,m for Nat;
reserve a,r,x,y for Real;
reserve A for non empty closed_interval Subset of REAL;
reserve C for non empty set;
reserve X for set;
theorem :: INTEGRA4:1
for D being Division of A st vol(A)=0 holds len D=1;
theorem :: INTEGRA4:2
chi(A,A) is integrable & integral(chi(A,A))=vol(A);
theorem :: INTEGRA4:3
for f being PartFunc of A,REAL, r holds f is total & rng f = {r}
iff f=r(#)chi(A,A);
theorem :: INTEGRA4:4
for f being Function of A,REAL, r st rng f = {r} holds f is
integrable & integral(f)=r*vol(A);
theorem :: INTEGRA4:5
for r holds ex f being Function of A,REAL st rng f = {r} & f|A is
bounded;
theorem :: INTEGRA4:6
for f being PartFunc of A,REAL, D being Element of divs A st vol(
A)=0 holds f is integrable & integral(f)=0;
theorem :: INTEGRA4:7
for f being Function of A,REAL st f|A is bounded & f is integrable
holds ex a st lower_bound rng f <= a & a <= upper_bound rng f & integral(f)=a*
vol(A);
begin :: Integrability of Bounded Total Functions
theorem :: INTEGRA4:8
for f being Function of A,REAL, T being DivSequence of A st
f|A is bounded & delta(T) is convergent & lim delta(T)=0 holds
lower_sum(f,T) is convergent & lim lower_sum(f,T) = lower_integral(f);
theorem :: INTEGRA4:9
for f being Function of A,REAL, T being DivSequence of A st f|A
is bounded & delta(T) is convergent & lim delta(T)=0 holds upper_sum(f,T) is
convergent & lim upper_sum(f,T) = upper_integral(f);
theorem :: INTEGRA4:10
for f being Function of A,REAL st f|A is bounded holds f is
upper_integrable & f is lower_integrable;
definition
let A be non empty closed_interval Subset of REAL, IT be Division of A, n;
pred IT divide_into_equal n means
:: INTEGRA4:def 1
len IT = n & for i st i in dom IT
holds IT.i=lower_bound A + vol(A)/(len IT)*i;
end;
theorem :: INTEGRA4:11
ex T being DivSequence of A st delta(T) is convergent & lim
delta(T)=0;
theorem :: INTEGRA4:12
for f being Function of A,REAL st f|A is bounded holds f is
integrable iff for T being DivSequence of A st delta(T) is convergent & lim
delta(T)=0 holds lim upper_sum(f,T)-lim lower_sum(f,T)=0;
theorem :: INTEGRA4:13
for f being Function of C,REAL holds max+(f) is total & max-(f)
is total;
theorem :: INTEGRA4:14
for f being PartFunc of C,REAL st f|X is bounded_above holds (
max+f)|X is bounded_above;
theorem :: INTEGRA4:15
for f being PartFunc of C,REAL holds (max+f)|X is bounded_below;
theorem :: INTEGRA4:16
for f being PartFunc of C,REAL st f|X is bounded_below holds (
max-f)|X is bounded_above;
theorem :: INTEGRA4:17
for f being PartFunc of C,REAL holds (max-f)|X is bounded_below;
theorem :: INTEGRA4:18
for f being PartFunc of A,REAL st f|A is bounded_above holds rng
(f|X) is bounded_above;
theorem :: INTEGRA4:19
for f being PartFunc of A,REAL st f|A is bounded_below holds rng
(f|X) is bounded_below;
theorem :: INTEGRA4:20
for f being Function of A,REAL st f|A is bounded & f is
integrable holds max+(f) is integrable;
theorem :: INTEGRA4:21
for f being PartFunc of C,REAL holds max-(f)=max+(-f);
theorem :: INTEGRA4:22
for f being Function of A,REAL st f|A is bounded & f is
integrable holds max-(f) is integrable;
theorem :: INTEGRA4:23
for f being Function of A,REAL st f|A is bounded & f is integrable
holds abs(f) is integrable & |.integral(f).|<=integral(abs(f));
theorem :: INTEGRA4:24
for f being Function of A,REAL st (for x,y st x in A & y in A
holds |.f.x-f.y.|<=a) holds upper_bound rng f - lower_bound rng f <= a;
theorem :: INTEGRA4:25
for f,g being Function of A,REAL st f|A is bounded & a>=0 & (for
x,y st x in A & y in A holds |.g.x-g.y.|<=a*|.f.x-f.y.|) holds upper_bound
rng g - lower_bound rng g <= a*(upper_bound rng f - lower_bound rng f);
theorem :: INTEGRA4:26
for f,g,h being Function of A,REAL st f|A is bounded & g|A is
bounded & a>=0 & (for x,y st x in A & y in A holds |.h.x-h.y.|<=a*(|.f.x-f.y
.|+|.g.x-g.y.|))
holds upper_bound rng h - lower_bound rng h <= a*((upper_bound
rng f - lower_bound rng f)+(upper_bound rng g - lower_bound rng g));
theorem :: INTEGRA4:27
for f,g being Function of A,REAL st f|A is bounded & f is
integrable & g|A is bounded & a>0 & (for x,y st x in A & y in A holds |.g.x-g
.y.|<=a*|.f.x-f.y.|) holds g is integrable;
theorem :: INTEGRA4:28
for f,g,h being Function of A,REAL st f|A is bounded & f is
integrable & g|A is bounded & g is integrable & h|A is bounded & a > 0 & (for x
,y st x in A & y in A holds |.h.x-h.y.|<=a*(|.f.x-f.y.|+|.g.x-g.y.|)) holds
h is integrable;
theorem :: INTEGRA4:29
for f,g being Function of A,REAL st f|A is bounded & f is integrable &
g|A is bounded & g is integrable holds f(#)g is integrable;
theorem :: INTEGRA4:30
for f being Function of A,REAL st f|A is bounded & f is integrable &
not 0 in rng f & f^|A is bounded holds f^ is integrable;