:: Riemann Integral of Functions $\mathbbbR$ into $\mathbbbR^n$ :: by Keiichi Miyajima and Yasunari Shidama :: :: Received May 5, 2009 :: Copyright (c) 2009-2021 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, INTEGRA1, SUBSET_1, FUNCT_1, FINSEQ_1, NAT_1, RELAT_1, MEASURE7, XBOOLE_0, XXREAL_2, XXREAL_0, SEQ_4, CARD_1, REAL_1, ARYTM_3, ARYTM_1, CARD_3, FINSEQ_2, INTEGRA2, SEQ_1, SEQ_2, ORDINAL2, COMPLEX1, XXREAL_1, FUNCT_3, REAL_NS1, STRUCT_0, PARTFUN1, VALUED_1, TARSKI, PRE_TOPC, INTEGRA5, REALSET1, INTEGR15, VALUED_2, MEASURE5, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, XCMPLX_0, COMPLEX1, XXREAL_2, NAT_1, FUNCT_1, FUNCT_2, STRUCT_0, REAL_1, RCOMP_1, VALUED_1, RELSET_1, PARTFUN1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, FINSEQ_1, FINSEQ_2, FINSEQOP, VALUED_2, RVSUM_1, PRE_TOPC, XXREAL_0, EUCLID, PDIFF_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA5, NORMSP_0, NORMSP_1, REAL_NS1; constructors REAL_1, FINSEQOP, MONOID_0, SEQ_4, PSCOMP_1, NAT_D, VFUNCT_1, PDIFF_1, BINOP_2, INTEGRA2, INTEGRA5, RELSET_1, SEQ_2, INTEGRA3, VALUED_2, COMSEQ_2; registrations NUMBERS, XREAL_0, SEQ_2, INTEGRA1, FUNCT_2, NAT_1, MEMBERED, XXREAL_0, ORDINAL1, VALUED_0, VALUED_1, REAL_NS1, RELSET_1, EUCLID, VALUED_2, CARD_1, MEASURE5, FINSEQ_1, FINSEQ_2, RELAT_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve Z for set; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL; let D be Division of A; mode middle_volume of f,D -> FinSequence of REAL means :: INTEGR15:def 1 len it = len D & for i be Nat st i in dom D holds ex r be Element of REAL st r in rng (f| divset(D,i)) & it.i=r*vol divset(D,i); end; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL; let D be Division of A; let F be middle_volume of f,D; func middle_sum(f,F) -> Real equals :: INTEGR15:def 2 Sum(F); end; theorem :: INTEGR15:1 for A be non empty closed_interval Subset of REAL, f be Function of A,REAL, D be Division of A, F be middle_volume of f,D st f|A is bounded_below holds lower_sum (f,D) <= middle_sum(f,F); theorem :: INTEGR15:2 for A be non empty closed_interval Subset of REAL, f be Function of A,REAL, D be Division of A, F be middle_volume of f,D st f|A is bounded_above holds middle_sum(f,F) <= upper_sum (f,D); theorem :: INTEGR15:3 for A be non empty closed_interval Subset of REAL, f be Function of A,REAL, D be Division of A, e be Real st f|A is bounded_below & 0 < e holds ex F be middle_volume of f,D st middle_sum(f,F) <= lower_sum (f,D) + e; theorem :: INTEGR15:4 for A be non empty closed_interval Subset of REAL, f be Function of A,REAL, D be Division of A, e be Real st f|A is bounded_above & 0 < e holds ex F be middle_volume of f,D st upper_sum (f,D) - e <= middle_sum(f,F); definition let A be non empty closed_interval Subset of REAL, f be Function of A,REAL, T be DivSequence of A; mode middle_volume_Sequence of f,T -> sequence of (REAL)* means :: INTEGR15:def 3 for k be Element of NAT holds it.k is middle_volume of f,T.k; end; definition let A be non empty closed_interval Subset of REAL, f be Function of A,REAL, T be DivSequence of A, S be middle_volume_Sequence of f,T, k be Element of NAT; redefine func S.k -> middle_volume of f,T.k; end; definition let A be non empty closed_interval Subset of REAL, f be Function of A,REAL, T be DivSequence of A, S be middle_volume_Sequence of f,T; func middle_sum(f,S) -> Real_Sequence means :: INTEGR15:def 4 for i be Element of NAT holds it.i = middle_sum(f,S.i); end; theorem :: INTEGR15:5 for A be non empty closed_interval Subset of REAL, f being Function of A, REAL, T being DivSequence of A, S be middle_volume_Sequence of f,T, i be Element of NAT st f|A is bounded_below holds (lower_sum(f,T)).i <= (middle_sum( f,S)).i; theorem :: INTEGR15:6 for A be non empty closed_interval Subset of REAL, f being Function of A, REAL, T being DivSequence of A, S be middle_volume_Sequence of f,T, i be Element of NAT st f|A is bounded_above holds (middle_sum(f,S)).i <= (upper_sum( f,T)).i; theorem :: INTEGR15:7 for A be non empty closed_interval Subset of REAL, f being Function of A, REAL, T being DivSequence of A, e be Element of REAL st 0 < e & f|A is bounded_below holds ex S be middle_volume_Sequence of f,T st for i be Element of NAT holds (middle_sum(f,S)).i <= (lower_sum(f,T)).i + e; theorem :: INTEGR15:8 for A be non empty closed_interval Subset of REAL, f being Function of A, REAL, T being DivSequence of A, e be Element of REAL st 0 < e & f|A is bounded_above holds ex S be middle_volume_Sequence of f,T st for i be Element of NAT holds (upper_sum(f,T)).i - e <= (middle_sum(f,S)).i; theorem :: INTEGR15:9 for A be non empty closed_interval Subset of REAL, f being Function of A, REAL, T being DivSequence of A, S be middle_volume_Sequence of f,T st f is bounded & f is integrable & delta(T) is convergent & lim delta(T)=0 holds middle_sum(f,S) is convergent & lim (middle_sum(f,S))=integral(f); theorem :: INTEGR15:10 for A be non empty closed_interval Subset of REAL, f being Function of A, REAL st f is bounded holds f is integrable iff ex I be Real st for T being DivSequence of A, S be middle_volume_Sequence of f,T st delta(T) is convergent & lim delta(T)=0 holds middle_sum(f,S) is convergent & lim (middle_sum(f,S))=I; definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL n; let D be Division of A; mode middle_volume of f,D -> FinSequence of (REAL n) means :: INTEGR15:def 5 len it = len D & for i be Nat st i in dom D holds ex r be Element of (REAL n) st r in rng (f|divset(D,i)) & it.i=vol divset(D,i)*r; end; definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL n; let D be Division of A; let F be middle_volume of f,D; func middle_sum(f,F) -> Element of (REAL n) means :: INTEGR15:def 6 for i be Element of NAT st i in Seg n holds ex Fi be FinSequence of REAL st Fi=proj(i,n)*F & it.i = Sum(Fi); end; definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL n; let T be DivSequence of A; mode middle_volume_Sequence of f,T -> sequence of (REAL n)* means :: INTEGR15:def 7 for k be Element of NAT holds it.k is middle_volume of f,T.k; end; definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL n; let T be DivSequence of A; let S be middle_volume_Sequence of f,T; let k be Element of NAT; redefine func S.k -> middle_volume of f,T.k; end; definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL n; let T be DivSequence of A; let S be middle_volume_Sequence of f,T; func middle_sum(f,S) -> sequence of (REAL-NS n) means :: INTEGR15:def 8 for i be Element of NAT holds it.i = middle_sum(f,S.i); end; definition let n be Nat; let Z be set; let f,g be PartFunc of Z,REAL n; func f+g -> PartFunc of Z, REAL n equals :: INTEGR15:def 9 f <++> g; func f-g -> PartFunc of Z, REAL n equals :: INTEGR15:def 10 f <--> g; end; definition let n be Nat; let r be Real; let Z be set; let f be PartFunc of Z,REAL n; func r(#)f -> PartFunc of Z, REAL n equals :: INTEGR15:def 11 f [#] r; end; begin :: Definition of Riemann Integral on Functions REAL to REAL n definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL n; attr f is bounded means :: INTEGR15:def 12 for i be Element of NAT st i in Seg n holds (proj(i,n)*f) is bounded; end; definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL n; attr f is integrable means :: INTEGR15:def 13 for i be Element of NAT st i in Seg n holds (proj(i,n)*f) is integrable; end; definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be Function of A,REAL n; func integral(f) -> Element of REAL n means :: INTEGR15:def 14 dom it = Seg n & for i be Element of NAT st i in Seg n holds it.i = integral((proj(i,n)*f)); end; theorem :: INTEGR15:11 for n be Element of NAT, A be non empty closed_interval Subset of REAL, f being Function of A,REAL n, T being DivSequence of A, S be middle_volume_Sequence of f,T st f is bounded & f is integrable & delta(T) is convergent & lim delta(T)=0 holds middle_sum(f,S) is convergent & lim ( middle_sum(f,S))=integral(f); theorem :: INTEGR15:12 for n be Element of NAT, A be non empty closed_interval Subset of REAL, f being Function of A,REAL n st f is bounded holds f is integrable iff ex I be Element of REAL n st for T being DivSequence of A, S be middle_volume_Sequence of f,T st delta(T) is convergent & lim delta(T)=0 holds middle_sum(f,S) is convergent & lim (middle_sum(f,S))=I; definition let n be Element of NAT; let f be PartFunc of REAL,REAL n; attr f is bounded means :: INTEGR15:def 15 for i be Element of NAT st i in Seg n holds (proj(i,n)*f) is bounded; end; definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,REAL n; pred f is_integrable_on A means :: INTEGR15:def 16 for i be Element of NAT st i in Seg n holds (proj(i,n)*f) is_integrable_on A; end; definition let n be Element of NAT; let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,REAL n; func integral(f,A) -> Element of REAL n means :: INTEGR15:def 17 dom it = Seg n & for i be Element of NAT st i in Seg n holds it.i = integral( (proj(i,n)*f), A); end; theorem :: INTEGR15:13 for n be Element of NAT, A be non empty closed_interval Subset of REAL, f be PartFunc of REAL,REAL n, g be Function of A,REAL n st f|A = g holds f is_integrable_on A iff g is integrable; theorem :: INTEGR15:14 for n be Element of NAT, A be non empty closed_interval Subset of REAL, f be PartFunc of REAL,REAL n, g be Function of A,REAL n st f|A = g holds integral(f,A) = integral(g); definition let a,b be Real; let n be Element of NAT; let f be PartFunc of REAL, REAL n; func integral(f,a,b) -> Element of REAL n means :: INTEGR15:def 18 dom it = Seg n & for i be Element of NAT st i in Seg n holds it.i = integral( (proj(i,n)*f) ,a,b); end; begin :: Linearity of the Integration Operator theorem :: INTEGR15:15 for n, i be Element of NAT, f1,f2 be PartFunc of Z, REAL n holds proj(i,n)*(f1+f2) = proj(i,n)*f1 + proj(i,n)*f2 & proj(i,n)*(f1-f2) = proj(i,n)*f1 - proj(i,n)*f2; theorem :: INTEGR15:16 for n,i be Element of NAT, r be Real, f be PartFunc of Z, REAL n holds proj(i,n)*(r(#)f) = r(#)(proj(i,n)*f); theorem :: INTEGR15:17 for n be Element of NAT for A be non empty closed_interval Subset of REAL for f1 ,f2 be PartFunc of REAL, REAL n st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & (f1|A) is bounded & (f2|A) is bounded holds f1+ f2 is_integrable_on A & f1-f2 is_integrable_on A & integral(f1+f2,A)=integral( f1,A)+integral(f2,A) & integral(f1-f2,A)=integral(f1,A)-integral(f2,A); theorem :: INTEGR15:18 for n be Element of NAT for r be Real for A be non empty closed_interval Subset of REAL for f be PartFunc of REAL, REAL n st A c= dom f & f is_integrable_on A & f|A is bounded holds r(#)f is_integrable_on A & integral( (r(#)f) ,A) = r* integral(f,A); theorem :: INTEGR15:19 for n be Element of NAT for f being PartFunc of REAL,REAL n, A being non empty closed_interval Subset of REAL, a,b be Real st A=[.a,b.] holds integral(f,A) = integral(f,a,b); theorem :: INTEGR15:20 for n be Element of NAT for f being PartFunc of REAL,REAL n, A being non empty closed_interval Subset of REAL, a,b be Real st A=[.b,a.] holds -integral(f,A) = integral(f,a,b); theorem :: INTEGR15:21 for n being Nat, Z,x being set, f,g being PartFunc of Z,REAL n st x in dom (f+g) holds (f+g)/.x = (f/.x) + (g/.x); theorem :: INTEGR15:22 for n being Nat, Z,x being set, f,g being PartFunc of Z,REAL n st x in dom (f-g) holds (f-g)/.x = (f/.x) - (g/.x); theorem :: INTEGR15:23 for n being Nat, Z,x being set, f being PartFunc of Z,REAL n for r being Real st x in dom (r(#)f) holds (r(#)f)/.x = r* (f/.x);