The abstract of the Mizar article:

Definition of Integrability for Partial Functions from $\Bbb R$ to $\Bbb R$ and Integrability for Continuous Functions

by

Noboru Endou,

Katsumi Wasaki, and

Yasunari Shidama

Received March 23, 2000

MML identifier: INTEGRA5

[ Mizar article, MML identifier index ]

environ

 vocabulary INTEGRA1, FINSEQ_1, RLVECT_1, ARYTM_1, RVSUM_1, RELAT_1, FUNCT_1,
      VECTSP_1, FINSEQ_2, PARTFUN1, REALSET1, SEQ_1, BOOLE, RFUNCT_1, FCONT_1,
      FCONT_2, COMPTS_1, LATTICES, SEQ_2, ABSVALUE, INTEGRA2, FUNCT_3,
      ORDINAL2, MEASURE5, ARYTM_3, SQUARE_1, FDIFF_1, RCOMP_1, RFUNCT_2,
      PRE_TOPC, INTEGRA5, FINSEQ_4, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, REALSET1, FUNCT_2, RELSET_1, PARTFUN1, RCOMP_1, PSCOMP_1,
      FINSEQ_1, FUNCOP_1, SEQ_1, RFUNCT_1, FINSEQ_2, SEQ_2, SEQ_4, PRE_CIRC,
      FDIFF_1, ABSVALUE, FINSEQ_4, VECTSP_1, RVSUM_1, INTEGRA1, INTEGRA2,
      FCONT_1, FCONT_2, RFUNCT_2;
 constructors REAL_1, REALSET1, FINSEQOP, PRE_CIRC, FDIFF_1, FINSEQ_4,
      INTEGRA2, RFUNCT_3, FCONT_1, FCONT_2, RFUNCT_2, ABSVALUE, PSCOMP_1,
      NAT_1;
 clusters XREAL_0, RELSET_1, FINSEQ_2, INTEGRA1, SEQ_1, RCOMP_1, ARYTM_3,
      MEMBERED, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin ::Some useful properties of finite sequence

reserve i,k,n,m for Nat;
reserve a,b,r,r1,r2,s,x,x1,x2,y for Real;
reserve A for closed-interval Subset of REAL;
reserve X for set;

theorem :: INTEGRA5:1
for F,F1,F2 being FinSequence of REAL, r1,r2 st
(F1=<*r1*>^F or F1=F^<*r1*>) & (F2=<*r2*>^F or F2=F^<*r2*>)
holds Sum(F1-F2)=r1-r2;

theorem :: INTEGRA5:2
for F1,F2 being FinSequence of REAL st len F1 = len F2 holds
len (F1+F2)=len F1 & len (F1-F2)=len F1 &
Sum(F1+F2)=Sum F1+Sum F2 & Sum(F1-F2)= Sum F1-Sum F2;

theorem :: INTEGRA5:3
for F1,F2 being FinSequence of REAL st len F1 = len F2 &
(for i st i in dom F1 holds F1.i <= F2.i) holds
Sum F1 <= Sum F2;

begin :: Integrability for partial function of REAL,REAL

definition let C be non empty Subset of REAL;
let f be PartFunc of REAL,REAL;
func f||C -> PartFunc of C,REAL equals
:: INTEGRA5:def 1

f|C;
end;

theorem :: INTEGRA5:4
for f,g being PartFunc of REAL,REAL, C being non empty Subset of REAL
holds (f||C)(#)(g||C) = (f(#)g)||C;

theorem :: INTEGRA5:5
for f,g being PartFunc of REAL,REAL, C being non empty Subset of REAL
holds (f+g)||C = f||C + g||C;

definition let A be closed-interval Subset of REAL;
let f be PartFunc of REAL,REAL;
pred f is_integrable_on A means
:: INTEGRA5:def 2

f||A is_integrable_on A;
end;

definition let A be closed-interval Subset of REAL;
let f be PartFunc of REAL,REAL;
func integral(f,A) -> Real equals
:: INTEGRA5:def 3

integral(f||A);
end;

theorem :: INTEGRA5:6
for f being PartFunc of REAL,REAL st A c= dom f holds f||A is total;

theorem :: INTEGRA5:7
for f being PartFunc of REAL,REAL st f is_bounded_above_on A holds
f||A is_bounded_above_on A;

theorem :: INTEGRA5:8
for f being PartFunc of REAL,REAL st f is_bounded_below_on A holds
f||A is_bounded_below_on A;

theorem :: INTEGRA5:9
for f being PartFunc of REAL,REAL st f is_bounded_on A
holds f||A is_bounded_on A;

begin :: Integrability for continuous function

theorem :: INTEGRA5:10
for f being PartFunc of REAL,REAL st f is_continuous_on A
holds f is_bounded_on A;

theorem :: INTEGRA5:11
for f being PartFunc of REAL,REAL st f is_continuous_on A
holds f is_integrable_on A;

theorem :: INTEGRA5:12
for f being PartFunc of REAL,REAL, D being Element of divs A
st A c= X & f is_differentiable_on X & f`|X is_bounded_on A
holds lower_sum((f`|X)||A,D) <= f.(sup A)-f.(inf A) &
f.(sup A)-f.(inf A)<=upper_sum((f`|X)||A,D);

theorem :: INTEGRA5:13
for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X &
f`|X is_integrable_on A & f`|X is_bounded_on A holds
integral(f`|X,A) = f.(sup A)-f.(inf A);

theorem :: INTEGRA5:14
for f being PartFunc of REAL,REAL st f is_non_decreasing_on A &
A c= dom f holds rng (f|A) is bounded;

theorem :: INTEGRA5:15
for f being PartFunc of REAL,REAL st f is_non_decreasing_on A & A c= dom f
holds inf rng (f|A) = f.(inf A) & sup rng (f|A) = f.(sup A);

theorem :: INTEGRA5:16
  for f being PartFunc of REAL,REAL st f is_monotone_on A & A c= dom f
holds f is_integrable_on A;

theorem :: INTEGRA5:17
for f being PartFunc of REAL,REAL, A,B being closed-interval Subset of REAL st
f is_continuous_on A & B c= A holds f is_integrable_on B;

theorem :: INTEGRA5:18
  for f being PartFunc of REAL,REAL, A,B,C being closed-interval Subset of REAL
,
X st A c= X & f is_differentiable_on X &f`|X is_continuous_on A &inf A = inf B
& sup B = inf C & sup C = sup A holds
B c= A & C c= A & integral(f`|X,A)=integral(f`|X,B)+integral(f`|X,C);

definition let a,b be real number;
assume a<=b;
func [' a,b '] -> closed-interval Subset of REAL equals
:: INTEGRA5:def 4
[.a,b.];
end;

definition let a,b be real number;
let f be PartFunc of REAL,REAL;
func integral(f,a,b) -> Real equals
:: INTEGRA5:def 5
integral(f,[' a,b ']) if a<=b otherwise -integral(f,[' b,a ']);
end;

theorem :: INTEGRA5:19
  for f being PartFunc of REAL,REAL, A being closed-interval Subset of REAL,
a,b st A=[.a,b.] holds
integral(f,A)=integral(f,a,b);

theorem :: INTEGRA5:20
  for f being PartFunc of REAL,REAL, A being closed-interval Subset of REAL,
a,b st A=[.b,a.] holds
-integral(f,A)=integral(f,a,b);

theorem :: INTEGRA5:21
  for f,g being PartFunc of REAL,REAL, X being open Subset of REAL
st f is_differentiable_on X & g is_differentiable_on X & A c= X &
f`|X is_integrable_on A & f`|X is_bounded_on A & g`|X is_integrable_on A &
g`|X is_bounded_on A holds
integral((f`|X)(#)g,A)
=f.(sup A)*g.(sup A)-f.(inf A)*g.(inf A)-integral(f(#)(g`|X),A);