:: Integrability and the Integral of Partial Functions from $\Bbb R$ into :: $\Bbb R$ :: by Noboru Endou , Yasunari Shidama and Masahiko Yamazaki :: :: Received November 17, 2006 :: Copyright (c) 2006-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, PARTFUN1, XXREAL_0, ARYTM_3, XXREAL_1, ARYTM_1, TARSKI, RELAT_1, FUNCT_3, XBOOLE_0, FUNCT_1, MEASURE7, INTEGRA5, ORDINAL2, COMPLEX1, CARD_1, REALSET1, XXREAL_2, REAL_1, VALUED_1, FINSEQ_1, NAT_1, INTEGRA2, SEQ_2, INTEGRA4, INT_1, RFINSEQ, ORDINAL4, CARD_3, FCONT_1, FDIFF_1, SEQ_1, FUNCT_2, FUNCOP_1, RCOMP_1, VALUED_0, SEQ_4, MEASURE5, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, INT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, RCOMP_1, FINSEQ_1, VALUED_0, VALUED_1, SEQ_1, RFUNCT_1, SEQ_2, FDIFF_1, RFINSEQ, XXREAL_2, RVSUM_1, MEASURE5, INTEGRA1, INTEGRA2, FCONT_1, INTEGRA3, INTEGRA4, INTEGRA5, XXREAL_0, SEQ_4; constructors REAL_1, BINOP_2, COMPLEX1, RFUNCT_1, FCONT_1, FDIFF_1, RFINSEQ, RSSPACE, INTEGRA2, INTEGRA4, INTEGRA5, RVSUM_1, SEQ_4, RELSET_1, FUNCOP_1, SEQ_2, INTEGRA3, COMSEQ_2; registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, RCOMP_1, FDIFF_1, SEQM_3, INTEGRA1, VALUED_0, VALUED_1, FINSET_1, XXREAL_2, CARD_1, RELSET_1, MEASURE5; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin :: Preliminaries reserve a,b,c,d,e,x,r for Real, A for non empty closed_interval Subset of REAL, f,g for PartFunc of REAL,REAL; theorem :: INTEGRA6:1 ::: XREAL_0 a <= b & c <= d & a+c = b+d implies a = b & c = d; theorem :: INTEGRA6:2 ::: XXREAL_1 a <= b implies ].x-a,x+a.[ c= ].x-b,x+b.[; theorem :: INTEGRA6:3 for R be Relation, A,B,C be set st A c= B & A c= C holds (R|B)|A = (R|C)|A; theorem :: INTEGRA6:4 for A,B,C be set st A c= B & A c= C holds chi(B,B)|A = chi(C,C)|A; theorem :: INTEGRA6:5 a <= b implies vol([' a,b '])=b-a; theorem :: INTEGRA6:6 vol([' min(a,b),max(a,b) ']) = |.b-a.|; begin theorem :: INTEGRA6:7 A c= dom f & f is_integrable_on A & f|A is bounded implies abs f is_integrable_on A & |.integral(f,A).| <= integral(abs f,A); theorem :: INTEGRA6:8 a<=b & [' a,b '] c= dom f & f is_integrable_on [' a,b '] & f|[' a ,b '] is bounded implies |.integral(f,a,b).| <=integral(abs f,a,b); theorem :: INTEGRA6:9 A c= dom f & f is_integrable_on A & f|A is bounded implies r(#)f is_integrable_on A & integral(r(#)f,A)=r*integral(f,A); theorem :: INTEGRA6:10 a<=b & [' a,b '] c= dom f & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded implies integral(c(#)f,a,b) =c*integral(f,a,b); theorem :: INTEGRA6:11 A c= dom f & A c= dom g & f is_integrable_on A & f|A is bounded & g is_integrable_on A & g|A is bounded implies f+g is_integrable_on A & f-g is_integrable_on A & integral(f+g,A) = integral(f,A) + integral(g,A) & integral (f-g,A) = integral(f,A) - integral(g,A); theorem :: INTEGRA6:12 a<=b & [' a,b '] c= dom f & [' a,b '] c= dom g & f is_integrable_on [' a,b '] & g is_integrable_on [' a,b '] & f|[' a,b '] is bounded & g|[' a,b '] is bounded implies integral(f+g,a,b) =integral(f,a,b) + integral(g,a,b) & integral(f-g,a,b) =integral(f,a,b) - integral(g,a,b); theorem :: INTEGRA6:13 f|A is bounded & g|A is bounded implies (f(#)g)|A is bounded; theorem :: INTEGRA6:14 A c= dom f & A c= dom g & f is_integrable_on A & f|A is bounded & g is_integrable_on A & g|A is bounded implies f(#)g is_integrable_on A; theorem :: INTEGRA6:15 for n be Nat st n > 0 & vol A > 0 holds ex D being Division of A st len D = n & for i be Nat st i in dom D holds D.i= lower_bound A + vol(A)/n*i; begin :: Integrability on a Subinterval theorem :: INTEGRA6:16 vol A > 0 implies ex T being DivSequence of A st delta T is convergent & lim delta T = 0 & for n be Element of NAT holds ex Tn being Division of A st Tn divide_into_equal n+1 & T.n =Tn; theorem :: INTEGRA6:17 a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f & c in [' a,b '] implies 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 :: INTEGRA6:18 a <= c & c <= d & d <= b & f is_integrable_on [' a,b '] & f|[' a ,b '] is bounded & [' a,b '] c= dom f implies f is_integrable_on ['c,d '] & f| [' c,d '] is bounded & ['c,d '] c= dom f; theorem :: INTEGRA6:19 a <= c & c <= d & d <= b & f is_integrable_on [' a,b '] & g is_integrable_on [' a,b '] & f|[' a,b '] is bounded & g|[' a,b '] is bounded & [' a,b '] c= dom f & [' a,b '] c= dom g implies f+g is_integrable_on ['c,d '] & (f+g)|[' c,d '] is bounded; theorem :: INTEGRA6:20 a<=b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] implies integral(f,a,d)= integral(f,a,c)+integral(f,c,d); theorem :: INTEGRA6:21 a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] implies [' min(c,d),max(c, d) '] c= dom (abs f) & abs f is_integrable_on [' min(c,d),max(c,d) '] & abs f| [' min(c,d),max(c,d) '] is bounded & |.integral(f,c,d).| <= integral(abs f,min( c,d),max(c,d)); theorem :: INTEGRA6:22 a <= b & c <= d & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] implies [' c,d '] c= dom (abs f) & abs f is_integrable_on [' c,d '] & abs f|[' c,d '] is bounded & |.integral(f,c,d).| <= integral(abs f,c,d) & |.integral(f,d,c).| <= integral(abs f,c,d); theorem :: INTEGRA6:23 ( a<=b & c <= d & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f & c in [' a,b '] & d in [' a,b '] & for x be Real st x in [' c,d '] holds |.f.x.| <= e ) implies |.integral(f,c,d).| <= e * (d-c) & |.integral(f,d,c).| <= e * (d-c); theorem :: INTEGRA6:24 a <= b & f is_integrable_on [' a,b '] & g is_integrable_on [' a, b '] & f|[' a,b '] is bounded & g|[' a,b '] is bounded & [' a,b '] c= dom f & [' a,b '] c= dom g & c in ['a,b '] & d in ['a,b '] implies integral(f+g,c,d) = integral(f,c,d) + integral(g,c,d) & integral(f-g,c,d) = integral(f,c,d) - integral(g,c,d); theorem :: INTEGRA6:25 a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a, b '] c= dom f & c in ['a,b '] & d in ['a,b '] implies integral(e(#)f,c,d)=e* integral(f,c,d); theorem :: INTEGRA6:26 ( a <= b & [' a,b '] c= dom f & for x be Real st x in [' a,b '] holds f.x=e ) implies f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & integral(f,a,b) = e*(b-a); theorem :: INTEGRA6:27 a <= b & (for x be Real st x in [' a,b '] holds f.x=e) & [' a,b '] c= dom f & c in ['a,b '] & d in ['a,b '] implies integral(f,c,d) = e* (d-c); begin :: Fundamental Theorem of Calculus theorem :: INTEGRA6:28 for x0 be Real, F be PartFunc of REAL,REAL st a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f & ].a, b.[ c= dom F & (for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x )) & x0 in ].a,b.[ & f is_continuous_in x0 holds F is_differentiable_in x0 & diff(F,x0)=f.x0; theorem :: INTEGRA6:29 for x0 be Real st a <= b & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded & [' a,b '] c= dom f & x0 in ].a,b.[ & f is_continuous_in x0 holds ex F be PartFunc of REAL,REAL st ].a,b.[ c= dom F & (for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x)) & F is_differentiable_in x0 & diff (F,x0)=f.x0;