The Mizar abstract of INTEGRA2

Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users
The abstract of the Mizar article:: Scalar Multiple of Riemann Definite Integral
by
Noboru Endou,
Katsumi Wasaki, and
Yasunari Shidama
Received December 7, 1999
MML identifier: INTEGRA2
[ Mizar article, MML identifier index ]
environ

 vocabulary FINSEQ_1, INTEGRA1, ARYTM, ORDINAL2, RCOMP_1, PROB_1, RELAT_1,
      FUNCT_1, RFINSEQ, FINSEQ_5, ARYTM_1, BOOLE, CARD_1, JORDAN3, PARTFUN1,
      RFUNCT_1, SEQ_2, ARYTM_3, SEQ_1, MEASURE5, RLVECT_1, FUNCT_3, SQUARE_1,
      FINSET_1, INTEGRA2;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, FUNCT_1, RELSET_1, SEQ_4, PARTFUN1, FUNCT_2, PSCOMP_1,
      FINSEQ_1, TOPREAL1, RFUNCT_1, RVSUM_1, INTEGRA1, SEQ_1, JORDAN3,
      PRE_CIRC, CQC_SIM1, RCOMP_1, FINSET_1, CARD_1, FINSEQ_5, RFINSEQ,
      BINARITH;
 constructors REAL_1, INTEGRA1, PRE_CIRC, CQC_SIM1, PARTFUN1, RFUNCT_1,
      FINSEQ_5, RFINSEQ, TOPREAL1, BINARITH, JORDAN3, PSCOMP_1;
 clusters XREAL_0, RELAT_1, RELSET_1, FINSEQ_1, GROUP_2, INTEGRA1, RFINSEQ,
      ARYTM_3, FUNCT_2, MEMBERED, ORDINAL2, NUMBERS;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Lemmas of Finite Sequence

reserve a,b,r,x,y,z for Real,
        i,j,k,n,m for Nat,
        x1 for set,
        p for FinSequence of REAL;

theorem :: INTEGRA2:1
for A be closed-interval Subset of REAL, x being real number
holds x in A iff inf A <= x & x <= sup A;

definition let IT be FinSequence of REAL;
attr IT is non-decreasing means
:: INTEGRA2:def 1
 for n be Nat st n in dom IT & n+1 in dom IT holds IT.n <= IT.(n+1);
end;

definition
cluster non-decreasing FinSequence of REAL;
end;

theorem :: INTEGRA2:2
for p be non-decreasing FinSequence of REAL,
i,j st i in dom p & j in dom p & i <= j holds p.i <= p.j;

theorem :: INTEGRA2:3
for p ex q be non-decreasing FinSequence of REAL
st p,q are_fiberwise_equipotent;

theorem :: INTEGRA2:4
for D be non empty set, f be FinSequence of D, k1,k2,k3 be Nat st
1<=k1 & k3<=len f & k1<=k2 & k2<k3 holds
mid(f,k1,k2)^mid(f,k2+1,k3)=mid(f,k1,k3);

begin :: Scalar Product of Real Subset

definition
   let A be Subset of REAL;
   let x be real number;
   func x * A -> Subset of REAL means
:: INTEGRA2:def 2
for y being Real holds
       y in it iff ex z being Real st z in A & y = x * z;
end;

theorem :: INTEGRA2:5
for X,Y be non empty set, f be PartFunc of X,REAL
st f is_bounded_above_on X & Y c= X holds f|Y is_bounded_above_on Y;

theorem :: INTEGRA2:6
for X,Y be non empty set, f be PartFunc of X,REAL
st f is_bounded_below_on X & Y c= X holds f|Y is_bounded_below_on Y;

theorem :: INTEGRA2:7
for X be non empty Subset of REAL holds r*X is non empty;

theorem :: INTEGRA2:8
  for X be Subset of REAL holds r*X = {r*x : x in X};

theorem :: INTEGRA2:9
for X be non empty Subset of REAL st
X is bounded_above & 0<=r holds r*X is bounded_above;

theorem :: INTEGRA2:10
for X be non empty Subset of REAL st
 X is bounded_above & r<=0 holds r*X is bounded_below;

theorem :: INTEGRA2:11
for X be non empty Subset of REAL st
X is bounded_below & 0<=r holds r*X is bounded_below;

theorem :: INTEGRA2:12
for X be non empty Subset of REAL st
 X is bounded_below & r<=0 holds r*X is bounded_above;

theorem :: INTEGRA2:13
for X be non empty Subset of REAL st
X is bounded_above & 0<=r holds sup(r*X) = r*(sup X);

theorem :: INTEGRA2:14
for X be non empty Subset of REAL st
 X is bounded_above & r<=0 holds inf(r*X) = r*(sup X);

theorem :: INTEGRA2:15
for X be non empty Subset of REAL st
 X is bounded_below & 0<=r holds inf(r*X) = r*(inf X);

theorem :: INTEGRA2:16
for X be non empty Subset of REAL st
 X is bounded_below & r<=0 holds sup(r*X) = r*(inf X);

begin :: Scalar Multiple of Integral

theorem :: INTEGRA2:17
for X be non empty set, f be Function of X,REAL holds
rng(r(#)f) = r*rng f;

theorem :: INTEGRA2:18
for X,Z be non empty set, f be PartFunc of X,REAL
holds rng(r(#)(f|Z)) = r*rng(f|Z);

theorem :: INTEGRA2:19
for A be closed-interval Subset of REAL, f be Function of A,REAL,
D be Element of divs A st f is_bounded_on A & r >= 0
holds (upper_sum_set(r(#)f)).D >= r*(inf rng f)*vol(A);

theorem :: INTEGRA2:20
for A be closed-interval Subset of REAL, f be Function of A,REAL,
D be Element of divs A st f is_bounded_on A & r <= 0
holds (upper_sum_set(r(#)f)).D >= r*(sup rng f)*vol(A);

theorem :: INTEGRA2:21
for A be closed-interval Subset of REAL, f be Function of A,REAL,
D be Element of divs A st f is_bounded_on A & r >= 0
holds (lower_sum_set(r(#)f)).D <= r*(sup rng f)*vol(A);

theorem :: INTEGRA2:22
for A be closed-interval Subset of REAL, f be Function of A,REAL,
D be Element of divs A st f is_bounded_on A & r <= 0
holds (lower_sum_set(r(#)f)).D <= r*(inf rng f)*vol(A);

theorem :: INTEGRA2:23
for A be closed-interval Subset of REAL, f be Function of A,REAL,
S be non empty Division of A, D be Element of S, i st i in Seg(len D) &
f is_bounded_above_on A & r >= 0 holds
upper_volume(r(#)f,D).i = r*upper_volume(f,D).i;

theorem :: INTEGRA2:24
for A be closed-interval Subset of REAL, f be Function of A,REAL,
S be non empty Division of A, D be Element of S, i st i in Seg(len D) &
f is_bounded_above_on A & r <= 0 holds
lower_volume(r(#)f,D).i = r*upper_volume(f,D).i;

theorem :: INTEGRA2:25
for A be closed-interval Subset of REAL, f be Function of A,REAL,
S be non empty Division of A, D be Element of S, i st i in Seg(len D) &
f is_bounded_below_on A & r >= 0 holds
lower_volume(r(#)f,D).i = r*lower_volume(f,D).i;

theorem :: INTEGRA2:26
for A be closed-interval Subset of REAL, f be Function of A,REAL,
S be non empty Division of A, D be Element of S, i st i in Seg(len D) &
f is_bounded_below_on A & r <= 0 holds
upper_volume(r(#)f,D).i = r*lower_volume(f,D).i;

theorem :: INTEGRA2:27
for A be closed-interval Subset of REAL, f be Function of A,REAL,
S be non empty Division of A, D be Element of S st
f is_bounded_above_on A & r >= 0 holds
upper_sum(r(#)f,D) = r*upper_sum(f,D);

theorem :: INTEGRA2:28
for A be closed-interval Subset of REAL, f be Function of A,REAL,
S be non empty Division of A, D be Element of S st
f is_bounded_above_on A & r <= 0 holds
lower_sum(r(#)f,D) = r*upper_sum(f,D);

theorem :: INTEGRA2:29
for A be closed-interval Subset of REAL, f be Function of A,REAL,
S be non empty Division of A, D be Element of S st
f is_bounded_below_on A & r >= 0 holds
lower_sum(r(#)f,D) = r*lower_sum(f,D);

theorem :: INTEGRA2:30
for A be closed-interval Subset of REAL, f be Function of A,REAL,
S be non empty Division of A, D be Element of S st
f is_bounded_below_on A & r <= 0 holds
upper_sum(r(#)f,D) = r*lower_sum(f,D);

theorem :: INTEGRA2:31
for A be closed-interval Subset of REAL, f be Function of A,REAL
st f is_bounded_on A & f is_integrable_on A
holds r(#)f is_integrable_on A & integral(r(#)f) = r*integral(f);

begin :: Monotonicity of Integral

theorem :: INTEGRA2:32
for A be closed-interval Subset of REAL,
f be Function of A,REAL st f is_bounded_on A &
f is_integrable_on A &(for x st x in A holds f.x >= 0) holds
integral(f) >= 0;

theorem :: INTEGRA2:33
for A be closed-interval Subset of REAL,
f,g be 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 & integral(f-g) = integral(f)-integral(g);

theorem :: INTEGRA2:34
for A be closed-interval Subset of REAL,
f,g be 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 & (for x st x in A holds f.x >= g.x) holds
integral(f) >= integral(g);

begin :: Definition of Division Sequence

theorem :: INTEGRA2:35
  for A be closed-interval Subset of REAL, f be Function of A,REAL
st f is_bounded_on A
holds rng upper_sum_set(f) is bounded_below;

theorem :: INTEGRA2:36
  for A be closed-interval Subset of REAL, f be Function of A,REAL
st f is_bounded_on A
holds rng lower_sum_set(f) is bounded_above;

definition let A be closed-interval Subset of REAL;
 mode DivSequence of A is Function of NAT,divs A;
end;

definition let A be closed-interval Subset of REAL,
T be DivSequence of A;
func delta(T) -> Real_Sequence means
:: INTEGRA2:def 3
  for i holds it.i = delta(T.i);
end;

definition let A be closed-interval Subset of REAL, f be PartFunc of A,REAL,
T be DivSequence of A;
func upper_sum(f,T) -> Real_Sequence means
:: INTEGRA2:def 4
  for i holds it.i = upper_sum(f,T.i);

func lower_sum(f,T) -> Real_Sequence means
:: INTEGRA2:def 5
  for i holds it.i = lower_sum(f,T.i);
end;

theorem :: INTEGRA2:37
for A be closed-interval Subset of REAL,
D1,D2 be Element of divs A st D1 <= D2 holds
(for j st j in dom D2 holds ex i st i in dom D1 & divset(D2,j) c= divset(D1,i))
;

theorem :: INTEGRA2:38
for X,Y be finite non empty Subset of REAL st
X c= Y holds max X <= max Y;

theorem :: INTEGRA2:39
for X,Y be finite non empty Subset of REAL st
(ex y st y in Y & max X <= y) holds max X <= max Y;

theorem :: INTEGRA2:40
for A,B be closed-interval Subset of REAL st
A c= B holds vol(A) <= vol(B);

theorem :: INTEGRA2:41
for A be closed-interval Subset of REAL,
D1,D2 be Element of divs A st D1 <= D2 holds delta(D1) >= delta(D2);
The abstract of the Mizar article:

Scalar Multiple of Riemann Definite Integral
