:: The Linearity of Riemann Integral on Functions from $\mathbbbR$ into Real :: {B}anach Space :: by Keiko Narita , Noboru Endou and Yasunari Shidama :: :: Received October 7, 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_2, LOPBAN_1, STRUCT_0, COMPLEX1, VALUED_1, SUPINF_2, XBOOLE_0, INTEGRA1, INTEGRA2, FINSEQ_1, TARSKI, INTEGRA5, INTEGR15, INTEGRA4, MEASURE7, CARD_3, XXREAL_1, PARTFUN1, SEQ_4, XXREAL_2, MEASURE5, FUNCT_3, ORDINAL4, RFINSEQ; notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, SEQ_2, RFUNCT_1, RVSUM_1, RFINSEQ, SEQ_4, RCOMP_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA4, INTEGRA5, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, LOPBAN_1, INTEGR15, INTEGR18, NFCONT_3, INTEGR19; constructors ABIAN, SEQ_2, RELSET_1, SEQ_4, VFUNCT_1, PDIFF_1, RLSUB_1, FCONT_1, NFCONT_1, INTEGRA3, INTEGRA4, NDIFF_3, INTEGR18, RVSUM_1, INTEGR19, INTEGR15, COMSEQ_2, VALUED_2, BINOM, FDIFF_1, NFCONT_2, C0SP2, ORDEQ_01, RFINSEQ, RFUNCT_1, RFINSEQ2, SQUARE_1, PDIFF_7, NDIFF_5, INTEGR20, NEWTON; registrations STRUCT_0, NAT_1, XXREAL_0, NUMBERS, XBOOLE_0, FUNCT_2, XREAL_0, MEMBERED, NORMSP_1, RELAT_1, RELSET_1, INTEGRA1, ORDINAL1, NFCONT_3, XXREAL_2, RLVECT_1, VALUED_0, FINSEQ_1, FINSET_1, MEASURE5, SEQM_3, INT_1, CARD_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Some Properties of Bounded Functions reserve Z for RealNormSpace; reserve a,b,c,d,e,r for Real; reserve A,B for non empty closed_interval Subset of REAL; theorem :: INTEGR21:1 for f be PartFunc of REAL,the carrier of Z st f is bounded & A c= dom f holds f|A is bounded; theorem :: INTEGR21:2 for f be PartFunc of REAL,the carrier of Z st f|A is bounded & B c= A & B c= dom (f|A) holds f|B is bounded; theorem :: INTEGR21:3 for f be PartFunc of REAL,the carrier of Z st a <= c & c <= d & d <= b & f| ['a,b'] is bounded & ['a,b'] c= dom f holds f| ['c,d'] is bounded; theorem :: INTEGR21:4 for X,Y be set, f1,f2 be PartFunc of REAL,the carrier of Z st f1|X is bounded & f2|Y is bounded holds (f1+f2) | (X /\ Y) is bounded & (f1-f2) | (X /\ Y) is bounded; theorem :: INTEGR21:5 for X be set, f be PartFunc of REAL,the carrier of Z st f|X is bounded holds (r(#)f)|X is bounded; theorem :: INTEGR21:6 for X be set, f be PartFunc of REAL,the carrier of Z st f|X is bounded holds (-f)|X is bounded; theorem :: INTEGR21:7 for f be Function of A,the carrier of Z holds f is bounded iff ||.f.|| is bounded; theorem :: INTEGR21:8 for f be PartFunc of REAL,the carrier of Z st A c= dom f holds ||.f|A.|| = (||.f.||) |A; theorem :: INTEGR21:9 for g be PartFunc of REAL,the carrier of Z st A c= dom g & g|A is bounded holds (||.g.||) |A is bounded; begin :: Some Properties of Integral of Continuous Functions reserve X,Y for RealBanachSpace; reserve E for Point of Y; theorem :: INTEGR21:10 for Y be RealNormSpace, f be continuous PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f holds ||.f.|| | ['a,b'] is bounded; theorem :: INTEGR21:11 for Y be RealNormSpace, f be continuous PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f holds f|['a,b'] is bounded; theorem :: INTEGR21:12 for Y be RealNormSpace, f be continuous PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f holds ||.f.|| is_integrable_on ['a,b']; theorem :: INTEGR21:13 for f be continuous PartFunc of REAL,the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f holds f is_integrable_on ['c,d']; theorem :: INTEGR21:14 for f be PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f holds integral(f,b,a) = - integral(f,a,b); theorem :: INTEGR21:15 for f be continuous PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] holds f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral(f,a,b) = integral(f,a,c) + integral(f,c,b); theorem :: INTEGR21:16 for f,g be continuous PartFunc of REAL,the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds f+g is_integrable_on ['c,d'] & (f+g) | ['c,d'] is bounded; theorem :: INTEGR21:17 for f be continuous PartFunc of REAL,the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f holds r(#)f is_integrable_on ['c,d'] & (r(#)f) | ['c,d'] is bounded; theorem :: INTEGR21:18 for f be continuous PartFunc of REAL,the carrier of Y st a <= c & c <= d & d <= b & f is_integrable_on ['a,b'] & f| ['a,b'] is bounded & ['a,b'] c= dom f holds -f is_integrable_on ['c,d'] & (-f) | ['c,d'] is bounded; theorem :: INTEGR21:19 for f,g be continuous PartFunc of REAL,the carrier of Y st a <= c & c <= d & d <= b & ['a,b'] c= dom f & ['a,b'] c= dom g holds f-g is_integrable_on ['c,d'] & (f-g) | ['c,d'] is bounded; theorem :: INTEGR21:20 for f be PartFunc of REAL,the carrier of Y st A c= dom f & f|A is bounded & f is_integrable_on A & ||.f.|| is_integrable_on A holds ||.integral(f,A).|| <= integral(||.f.||,A); theorem :: INTEGR21:21 for f be PartFunc of REAL,the carrier of Y st a<=b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & ||.f.|| is_integrable_on ['a,b'] & f| ['a ,b'] is bounded holds ||.integral(f,a,b).|| <= integral(||.f.||,a,b); theorem :: INTEGR21:22 for f be continuous PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds ||.f.|| is_integrable_on ['min(c,d),max(c,d)'] & ||.f.|| | ['min(c,d),max(c,d)'] is bounded & ||. integral(f,c,d) .|| <= integral(||.f.||,min(c,d),max(c,d)); theorem :: INTEGR21:23 for f be continuous PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral(r(#)f,c,d) = r*integral(f,c,d); theorem :: INTEGR21:24 for f be continuous PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral(-f,c,d) = -integral(f,c,d); theorem :: INTEGR21:25 for f be continuous PartFunc of REAL,the carrier of Y st ( a<=b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] & for x be Real st x in ['min(c,d),max(c,d)'] holds ||. f/.x .|| <= e ) holds ||.integral(f,c,d).|| <= e * |.d-c.|; theorem :: INTEGR21:26 for Y be RealNormSpace, A be non empty closed_interval Subset of REAL, f be Function of A,the carrier of Y, E be Point of Y st rng f = {E} holds f is integrable & integral f = (vol A) * E; theorem :: INTEGR21:27 for f be PartFunc of REAL,the carrier of Y, E be Point of Y st ( a <= b & ['a,b'] c= dom f & for x be Real st x in ['a,b'] holds f/.x = E ) holds f is_integrable_on ['a,b'] & integral(f,a,b) = (b-a)*E; theorem :: INTEGR21:28 for f be PartFunc of REAL,the carrier of Y st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= dom f & for x be Real st x in ['a,b'] holds f/.x = E holds integral(f,c,d) = (d-c)*E; theorem :: INTEGR21:29 for f be continuous PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds integral(f,a,d) = integral(f,a,c) + integral(f,c,d); theorem :: INTEGR21:30 for f,g be continuous PartFunc of REAL,the carrier of Y st a <= b & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds integral(f-g,c,d) = integral(f,c,d) - integral(g,c,d);