:: Riemann Integral of Functions from $\mathbbbR$ into Real {B}anach Space :: by Keiko Narita , Noboru Endou and Yasunari Shidama :: :: Received June 18, 2013 :: Copyright (c) 2013-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 PRE_TOPC, NORMSP_1, FUNCT_1, ARYTM_1, NAT_1, SUBSET_1, NUMBERS, CARD_1, XXREAL_0, REAL_1, ARYTM_3, RELAT_1, ORDINAL2, SEQ_1, SEQ_2, LOPBAN_1, STRUCT_0, COMPLEX1, VALUED_1, SUPINF_2, XBOOLE_0, ABIAN, INTEGRA1, INTEGRA2, FINSEQ_1, TARSKI, INTEGRA5, INTEGR15, MEASURE7, CARD_3, XXREAL_1, PARTFUN1, SEQ_4, FUNCT_2, RCOMP_1, VALUED_0, XXREAL_2, FCONT_1, MEASURE5, FUNCOP_1, FINSEQ_2, FUNCT_3, ORDINAL4, FCONT_2, ZFMISC_1, INTEGR20; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, BINOP_1, VALUED_1, SEQ_1, SEQ_2, RFUNCT_1, RVSUM_1, SEQ_4, RCOMP_1, ABIAN, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA5, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, LOPBAN_1, BINOM, INTEGR18, NFCONT_3; constructors ABIAN, SEQ_2, RSSPACE3, RELSET_1, SEQ_4, VFUNCT_1, NEWTON, INTEGRA3, INTEGR18, RVSUM_1, COMSEQ_2, BINOM, ORDEQ_01, RFUNCT_1, NDIFF_5; registrations STRUCT_0, NAT_1, VALUED_1, NORMSP_0, NUMBERS, XBOOLE_0, FUNCT_2, XREAL_0, MEMBERED, RELAT_1, RELSET_1, INTEGRA1, ORDINAL1, NFCONT_3, XXREAL_2, RLVECT_1, VALUED_0, FINSEQ_1, FINSET_1, MEASURE5, ABIAN, SEQM_3, INT_1, CARD_1, SUBSET_1, FINSEQ_2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Some Properties of Continuous Functions reserve s1,s2,q1 for Real_Sequence; definition let X be RealNormSpace; let f be PartFunc of REAL,the carrier of X; attr f is uniformly_continuous means :: INTEGR20:def 1 for r be Real st 0 Real equals :: INTEGR20:def 2 0 if A is empty otherwise vol A; end; reserve n for Element of NAT; reserve a,b for Real; theorem :: INTEGR20:5 for A be real-bounded Subset of REAL holds 0 <= xvol A; theorem :: INTEGR20:6 for A be non empty closed_interval Subset of REAL, D be Division of A, q be FinSequence of REAL st dom q = Seg len D & for i be Nat st i in Seg len D holds q.i = vol divset(D,i) holds Sum q = vol A; theorem :: INTEGR20:7 for Y be RealNormSpace, E be Point of Y, q be FinSequence of REAL, S be FinSequence of Y st len S = len q & for i be Nat st i in dom S holds ex r be Real st r = q.i & S.i= r * E holds Sum S = (Sum q)*E; theorem :: INTEGR20:8 for A being non empty closed_interval Subset of REAL, D being Division of A, B be non empty closed_interval Subset of REAL, v be FinSequence of REAL st B c= A & len D = len v & for i be Nat st i in dom v holds v.i = xvol (B /\ divset(D,i)) holds Sum v = vol B; theorem :: INTEGR20:9 for Y be RealNormSpace, xseq be FinSequence of Y, yseq be FinSequence of REAL st len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds ex v be Point of Y st v = xseq/.i & yseq.i = ||.v.|| ) holds ||.Sum xseq.|| <= Sum yseq; theorem :: INTEGR20:10 for Y be RealNormSpace, p be FinSequence of Y, q be FinSequence of REAL st len p = len q & (for j be Nat st j in dom p holds ||. p/.j .|| <= q.j) holds ||. Sum(p) .|| <= Sum(q); theorem :: INTEGR20:11 for j being Element of NAT for A being non empty closed_interval Subset of REAL for D1 being Division of A st j in dom D1 holds vol (divset (D1,j)) <= delta D1; theorem :: INTEGR20:12 for A being non empty closed_interval Subset of REAL, D being Division of A, r be Real st delta(D) < r holds for i be Nat, s,t be Real st i in dom D & s in divset(D,i) & t in divset(D,i) holds |.s-t.| < r; theorem :: INTEGR20:13 for X be RealBanachSpace, A be non empty closed_interval Subset of REAL, h be Function of A,the carrier of X st for r be Real st 0non empty set, F,G(set)->Element of D() }: ex s being sequence of D() st for n be Nat holds s.(2*n) = F(n) & s.(2*n+1) = G(n); theorem :: INTEGR20:14 for n be Nat holds ex k be Nat st n=2*k or n=2*k+1; theorem :: INTEGR20:15 for A be non empty closed_interval Subset of REAL, T0,T be DivSequence of A holds ex T1 be DivSequence of A st for i be Nat holds T1.(2*i) = T0.i & T1.(2*i+1) = T.i; theorem :: INTEGR20:16 for A be non empty closed_interval Subset of REAL, T0,T,T1 be DivSequence of A st delta T0 is convergent & lim delta T0 = 0 & delta T is convergent & lim delta T = 0 & for i be Nat holds T1.(2*i) = T0.i & T1.(2*i+1) = T.i holds delta T1 is convergent & lim delta T1 = 0; theorem :: INTEGR20:17 for X be RealNormSpace, A be non empty closed_interval Subset of REAL, h be Function of A,the carrier of X, T0,T,T1 be DivSequence of A, S0 be middle_volume_Sequence of h,T0, S be middle_volume_Sequence of h,T st for i be Nat holds T1.(2*i) = T0.i & T1.(2*i+1) = T.i ex S1 be middle_volume_Sequence of h,T1 st for i be Nat holds S1.(2*i) = S0.i & S1.(2*i+1) = S.i; theorem :: INTEGR20:18 for X be RealNormSpace, Sq0,Sq,Sq1 be sequence of X st Sq1 is convergent & for i be Nat holds Sq1.(2*i) = Sq0.i & Sq1.(2*i+1) = Sq.i holds Sq0 is convergent & lim Sq0=lim Sq1 & Sq is convergent & lim Sq=lim Sq1; theorem :: INTEGR20:19 for X be RealBanachSpace, f be continuous PartFunc of REAL,the carrier of X st a <= b & [' a,b '] c= dom f holds f is_integrable_on [' a,b '];