The abstract of the Mizar article:

Integrability of Bounded Total Functions

by

Noboru Endou,

Katsumi Wasaki, and

Yasunari Shidama

Received February 1, 2000

MML identifier: INTEGRA4

[ Mizar article, MML identifier index ]

environ

 vocabulary INTEGRA1, MEASURE5, FINSEQ_1, ORDINAL2, ARYTM_1, RELAT_1, BOOLE,
      FUNCT_1, FUNCT_3, RLVECT_1, PARTFUN2, LATTICES, SEQ_2, PARTFUN1, SEQ_1,
      RFUNCT_1, RCOMP_1, ARYTM_3, INTEGRA2, SQUARE_1, FINSEQ_2, FDIFF_1,
      SEQM_3, ABSVALUE, INT_1, RFUNCT_3, INTEGRA4, FINSEQ_4, REALSET1, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, INT_1, REALSET1, FUNCT_1, PSCOMP_1, RELSET_1, FINSEQ_1,
      SEQ_1, PARTFUN2, RFUNCT_1, FINSEQ_2, SEQ_2, SEQM_3, SEQ_4, PRE_CIRC,
      RCOMP_1, FDIFF_1, ABSVALUE, GOBOARD1, SQUARE_1, FINSEQ_4, RVSUM_1,
      INTEGRA1, INTEGRA2, RFUNCT_3, PARTFUN1, FUNCT_2;
 constructors REAL_1, REALSET1, FINSEQOP, PARTFUN2, PRE_CIRC, SFMASTR3,
      FDIFF_1, FINSEQ_4, INTEGRA2, SEQM_3, RFUNCT_3, ABSVALUE, PSCOMP_1, NAT_1;
 clusters XREAL_0, RELSET_1, FINSEQ_2, GOBOARD1, INT_1, INTEGRA1, FUNCT_2,
      SEQ_1, NAT_1, MEMBERED, NUMBERS, ORDINAL2;
 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,b,d,r,x,y for Real;
reserve A for closed-interval Subset of REAL;
reserve C for non empty set;
reserve c for Element of C;
reserve X for set;

theorem :: INTEGRA4:1
for D being Element of divs A st vol(A)=0 holds len D=1;

theorem :: INTEGRA4:2
chi(A,A) is_integrable_on A & 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_on A & integral(f)=r*vol(A);

theorem :: INTEGRA4:5
for r holds
ex f being Function of A,REAL st rng f = {r} & f is_bounded_on A;

theorem :: INTEGRA4:6
for f being PartFunc of A,REAL, D being Element of divs A
st vol(A)=0 holds f is_integrable_on A & integral(f)=0;

theorem :: INTEGRA4:7
  for f being Function of A,REAL st f is_bounded_on A &
f is_integrable_on A holds ex a st inf rng f <= a & a <= sup 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 is_bounded_on A & 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 is_bounded_on A & 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 is_bounded_on A
holds f is_upper_integrable_on A & f is_lower_integrable_on A;

definition let A be closed-interval Subset of REAL,
IT be Element of divs 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=inf 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 is_bounded_on A
holds f is_integrable_on A 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 is_bounded_above_on X holds
max+(f) is_bounded_above_on X;

theorem :: INTEGRA4:15
for f being PartFunc of C,REAL holds max+(f) is_bounded_below_on X;

theorem :: INTEGRA4:16
for f being PartFunc of C,REAL st f is_bounded_below_on X holds
max-(f) is_bounded_above_on X;

theorem :: INTEGRA4:17
for f being PartFunc of C,REAL holds max-(f) is_bounded_below_on X;

theorem :: INTEGRA4:18
for f being PartFunc of A,REAL st f is_bounded_above_on A
holds rng (f|X) is bounded_above;

theorem :: INTEGRA4:19
for f being PartFunc of A,REAL st f is_bounded_below_on A
holds rng (f|X) is bounded_below;

theorem :: INTEGRA4:20
for f being Function of A,REAL st f is_bounded_on A
& f is_integrable_on A holds max+(f) is_integrable_on A;

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 is_bounded_on A
& f is_integrable_on A holds max-(f) is_integrable_on A;

theorem :: INTEGRA4:23
  for f being Function of A,REAL st f is_bounded_on A
& f is_integrable_on A holds abs(f) is_integrable_on A
& abs(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 abs(f.x-f.y)<=a) holds
sup rng f - inf rng f <= a;

theorem :: INTEGRA4:25
for f,g being Function of A,REAL st f is_bounded_on A &
a>=0 & (for x,y st x in A & y in A holds abs(g.x-g.y)<=a*abs(f.x-f.y)) holds
sup rng g - inf rng g <= a*(sup rng f - inf rng f);

theorem :: INTEGRA4:26
for f,g,h being Function of A,REAL st f is_bounded_on A & g is_bounded_on A &
a>=0 &
(for x,y st x in A & y in A holds abs(h.x-h.y)<=a*(abs(f.x-f.y)+abs(g.x-g.y)))
holds
sup rng h - inf rng h <= a*((sup rng f - inf rng f)+(sup rng g - inf rng g));

theorem :: INTEGRA4:27
for f,g being Function of A,REAL st f is_bounded_on A &
f is_integrable_on A & g is_bounded_on A &
a>0 & (for x,y st x in A & y in A holds abs(g.x-g.y)<=a*abs(f.x-f.y)) holds
g is_integrable_on A;

theorem :: INTEGRA4:28
for f,g,h being Function of A,REAL st f is_bounded_on A &
f is_integrable_on A & g is_bounded_on A & g is_integrable_on A &
h is_bounded_on A & a > 0 &
(for x,y st x in A & y in A holds
abs(h.x-h.y)<=a*(abs(f.x-f.y)+abs(g.x-g.y))) holds
h is_integrable_on A;

theorem :: INTEGRA4:29
  for f,g being Function of A,REAL st f is_bounded_on A &
f is_integrable_on A & g is_bounded_on A & g is_integrable_on A
holds f(#)g is_integrable_on A;

theorem :: INTEGRA4:30
  for f being Function of A,REAL st f is_bounded_on A &
f is_integrable_on A & not(0 in rng f) & f^ is_bounded_on A
holds f^ is_integrable_on A;