:: Scalar Multiple of Riemann Definite Integral
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-2019 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, REAL_1, SUBSET_1, FINSEQ_1, INTEGRA1, SEQ_4, XXREAL_0,
XXREAL_1, VALUED_0, RELAT_1, ARYTM_3, FUNCT_1, CARD_1, NAT_1, CLASSES1,
FINSEQ_5, ARYTM_1, ORDINAL4, XBOOLE_0, JORDAN3, MEMBERED, MEMBER_1,
TARSKI, PARTFUN1, XXREAL_2, VALUED_1, MEASURE7, CARD_3, SEQ_1, INTEGRA2,
MEASURE5, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0,
XREAL_0, XXREAL_2, XXREAL_3, MEMBERED, MEMBER_1, XCMPLX_0, REAL_1, NAT_1,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, RFUNCT_1,
RVSUM_1, INTEGRA1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4,
FINSEQ_6, RCOMP_1, FINSEQ_5, CLASSES1, RFINSEQ, MEASURE5, MEASURE6;
constructors PARTFUN1, REAL_1, NAT_1, SEQM_3, VALUED_0, RFUNCT_1, RFINSEQ,
BINARITH, FINSEQ_5, FINSEQ_6, INTEGRA1, XXREAL_2, NAT_D, RVSUM_1, SEQ_4,
CLASSES1, RELSET_1, SEQ_2, MEMBER_1, MEASURE6, COMSEQ_2;
registrations RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED,
FINSEQ_1, INTEGRA1, VALUED_0, VALUED_1, XXREAL_2, CARD_1, SEQ_2,
RELSET_1, XXREAL_3, MEMBER_1, MEASURE5, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Lemmas of Finite Sequence
reserve a,b,r,x,y for Real,
i,j,k,n for Nat,
x1 for set,
p for FinSequence of REAL;
theorem :: INTEGRA2:1
for A be non empty closed_interval Subset of REAL, x being Real holds
x in A iff lower_bound A <= x & x <= upper_bound A;
definition
let IT be FinSequence of REAL;
redefine 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;
registration
cluster non-decreasing for 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 Subset of REAL;
end;
theorem :: INTEGRA2:5
for X,Y be non empty set, f be PartFunc of X,REAL st
f|X is bounded_above & Y c= X holds f|Y|Y is bounded_above;
theorem :: INTEGRA2:6
for X,Y be non empty set, f be PartFunc of X,REAL st
f|X is bounded_below & Y c= X holds f|Y|Y is bounded_below;
theorem :: INTEGRA2:7
for X being real-membered set, a being Real holds
X is empty iff a ** X is 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 upper_bound(r**X) = r*(upper_bound X);
theorem :: INTEGRA2:14
for X be non empty Subset of REAL st X is bounded_above & r<=0
holds lower_bound(r**X) = r*(upper_bound X);
theorem :: INTEGRA2:15
for X be non empty Subset of REAL st X is bounded_below & 0<=r
holds lower_bound(r**X) = r*(lower_bound X);
theorem :: INTEGRA2:16
for X be non empty Subset of REAL st X is bounded_below & r<=0
holds upper_bound(r**X) = r*(lower_bound 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);
reserve A, B for non empty closed_interval Subset of REAL;
reserve f, g for Function of A,REAL;
reserve D, D1, D2 for Division of A;
theorem :: INTEGRA2:19
f|A is bounded & r >= 0 implies (upper_sum_set(r(#)f)).D >= r*(
lower_bound rng f)*vol(A);
theorem :: INTEGRA2:20
f|A is bounded & r <= 0 implies (upper_sum_set(r(#)f)).D >= r*(
upper_bound rng f)*vol(A);
theorem :: INTEGRA2:21
f|A is bounded & r >= 0 implies (lower_sum_set(r(#)f)).D <= r*(
upper_bound rng f)*vol(A);
theorem :: INTEGRA2:22
f|A is bounded & r <= 0 implies (lower_sum_set(r(#)f)).D <= r*(
lower_bound rng f)*vol(A);
theorem :: INTEGRA2:23
i in dom D & f|A is bounded_above & r >= 0 implies upper_volume(
r(#)f,D).i = r*upper_volume(f,D).i;
theorem :: INTEGRA2:24
i in dom D & f|A is bounded_above & r <= 0 implies lower_volume(
r(#)f,D).i = r*upper_volume(f,D).i;
theorem :: INTEGRA2:25
i in dom D & f|A is bounded_below & r >= 0 implies lower_volume(
r(#)f,D).i = r*lower_volume(f,D).i;
theorem :: INTEGRA2:26
i in dom D & f|A is bounded_below & r <= 0 implies upper_volume(
r(#)f,D).i = r*lower_volume(f,D).i;
theorem :: INTEGRA2:27
f|A is bounded_above & r >= 0 implies upper_sum(r(#)f,D) = r*
upper_sum(f,D);
theorem :: INTEGRA2:28
f|A is bounded_above & r <= 0 implies lower_sum(r(#)f,D) = r*
upper_sum(f,D);
theorem :: INTEGRA2:29
f|A is bounded_below & r >= 0 implies lower_sum(r(#)f,D) = r*
lower_sum(f,D);
theorem :: INTEGRA2:30
f|A is bounded_below & r <= 0 implies upper_sum(r(#)f,D) = r*
lower_sum(f,D);
theorem :: INTEGRA2:31
f|A is bounded & f is integrable implies r(#)f is integrable &
integral(r(#)f) = r*integral(f);
begin :: Monotonicity of Integral
theorem :: INTEGRA2:32
f|A is bounded & (for x st x in A holds f.x >= 0) implies
integral(f) >= 0;
theorem :: INTEGRA2:33
f|A is bounded & f is integrable & g|A is bounded & g is
integrable implies f-g is integrable & integral(f-g) = integral(f)-integral(g);
theorem :: INTEGRA2:34
f|A is bounded & f is integrable & g|A is bounded & g is integrable &
(for x st x in A holds f.x >= g.x) implies integral(f) >= integral(g);
begin :: Definition of Division Sequence
theorem :: INTEGRA2:35
f|A is bounded implies rng upper_sum_set(f) is bounded_below;
theorem :: INTEGRA2:36
f|A is bounded implies rng lower_sum_set(f) is bounded_above;
definition
let A be non empty closed_interval Subset of REAL;
mode DivSequence of A is sequence of divs A;
end;
definition
let A;
let T be DivSequence of A;
let i;
redefine func T.i -> Division of A;
end;
definition
let A be non empty 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 2
for i holds it.i = upper_sum(f,T.i);
func lower_sum(f,T) -> Real_Sequence means
:: INTEGRA2:def 3
for i holds it.i = lower_sum(f,T.
i);
end;
theorem :: INTEGRA2:37
D1 <= D2 implies 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
A c= B implies vol(A) <= vol(B);
theorem :: INTEGRA2:39
for A being Subset of REAL,
a,x being Real st x in a ** A holds
ex b being Real st b in A & x = a * b;
begin :: Addenda
:: missing, 2008.06.10
theorem :: INTEGRA2:40
for A being non empty ext-real-membered set holds 0 ** A = {0};