:: Integrability of Bounded Total Functions :: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama :: :: Received February 1, 2000 :: Copyright (c) 2000-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, SUBSET_1, REAL_1, INTEGRA1, XBOOLE_0, MEASURE7, CARD_1, FINSEQ_1, RELAT_1, XXREAL_0, FUNCT_1, SEQ_4, ARYTM_3, ARYTM_1, FUNCT_3, TARSKI, PARTFUN1, CARD_3, VALUED_1, XXREAL_2, XXREAL_1, INTEGRA2, SEQ_2, ORDINAL2, FINSET_1, NAT_1, FINSEQ_2, VALUED_0, FDIFF_1, COMPLEX1, INT_1, ZFMISC_1, RFUNCT_3, SEQ_1, ORDINAL4, SQUARE_1, INTEGRA4, MEASURE5, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, INT_1, XXREAL_2, VALUED_0, ZFMISC_1, FUNCT_1, RELSET_1, FINSET_1, FUNCT_2, FINSEQ_1, VALUED_1, SEQ_1, RFUNCT_1, FINSEQ_2, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, FDIFF_1, SQUARE_1, RVSUM_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, RFUNCT_3, PARTFUN1, XXREAL_0; constructors REAL_1, SQUARE_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP, FINSOP_1, PARTFUN2, FDIFF_1, ZFMISC_1, RFUNCT_3, INTEGRA2, XXREAL_2, RVSUM_1, SEQ_4, RELSET_1, SEQ_2, INTEGRA3, COMSEQ_2; registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_2, INTEGRA1, VALUED_0, VALUED_1, XXREAL_2, CARD_1, SEQ_2, RELSET_1, SEQM_3, MEASURE5, SQUARE_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Basic integrable functions and first mean value theorem reserve i,j,k,n,n1,n2,m for Nat; reserve a,r,x,y for Real; reserve A for non empty closed_interval Subset of REAL; reserve C for non empty set; reserve X for set; theorem :: INTEGRA4:1 for D being Division of A st vol(A)=0 holds len D=1; theorem :: INTEGRA4:2 chi(A,A) is integrable & integral(chi(A,A))=vol(A); theorem :: INTEGRA4:3 for f being PartFunc of A,REAL, r holds f is total & rng f = {r} iff f=r(#)chi(A,A); theorem :: INTEGRA4:4 for f being Function of A,REAL, r st rng f = {r} holds f is integrable & integral(f)=r*vol(A); theorem :: INTEGRA4:5 for r holds ex f being Function of A,REAL st rng f = {r} & f|A is bounded; theorem :: INTEGRA4:6 for f being PartFunc of A,REAL st vol(A)=0 holds f is integrable & integral(f)=0; theorem :: INTEGRA4:7 for f being Function of A,REAL st f|A is bounded & f is integrable holds ex a st lower_bound rng f <= a & a <= upper_bound rng f & integral(f)=a* vol(A); begin :: Integrability of Bounded Total Functions theorem :: INTEGRA4:8 for f being Function of A,REAL, T being DivSequence of A st f|A is bounded & delta(T) is convergent & lim delta(T)=0 holds lower_sum(f,T) is convergent & lim lower_sum(f,T) = lower_integral(f); theorem :: INTEGRA4:9 for f being Function of A,REAL, T being DivSequence of A st f|A is bounded & delta(T) is convergent & lim delta(T)=0 holds upper_sum(f,T) is convergent & lim upper_sum(f,T) = upper_integral(f); theorem :: INTEGRA4:10 for f being Function of A,REAL st f|A is bounded holds f is upper_integrable & f is lower_integrable; definition let A be non empty closed_interval Subset of REAL, IT be Division of A, n; pred IT divide_into_equal n means :: INTEGRA4:def 1 len IT = n & for i st i in dom IT holds IT.i=lower_bound A + vol(A)/(len IT)*i; end; theorem :: INTEGRA4:11 ex T being DivSequence of A st delta(T) is convergent & lim delta(T)=0; theorem :: INTEGRA4:12 for f being Function of A,REAL st f|A is bounded holds f is integrable iff for T being DivSequence of A st delta(T) is convergent & lim delta(T)=0 holds lim upper_sum(f,T)-lim lower_sum(f,T)=0; theorem :: INTEGRA4:13 for f being Function of C,REAL holds max+(f) is total & max-(f) is total; theorem :: INTEGRA4:14 for f being PartFunc of C,REAL st f|X is bounded_above holds ( max+f)|X is bounded_above; theorem :: INTEGRA4:15 for f being PartFunc of C,REAL holds (max+f)|X is bounded_below; theorem :: INTEGRA4:16 for f being PartFunc of C,REAL st f|X is bounded_below holds ( max-f)|X is bounded_above; theorem :: INTEGRA4:17 for f being PartFunc of C,REAL holds (max-f)|X is bounded_below; theorem :: INTEGRA4:18 for f being PartFunc of A,REAL st f|A is bounded_above holds rng (f|X) is bounded_above; theorem :: INTEGRA4:19 for f being PartFunc of A,REAL st f|A is bounded_below holds rng (f|X) is bounded_below; theorem :: INTEGRA4:20 for f being Function of A,REAL st f|A is bounded & f is integrable holds max+(f) is integrable; theorem :: INTEGRA4:21 for f being PartFunc of C,REAL holds max-(f)=max+(-f); theorem :: INTEGRA4:22 for f being Function of A,REAL st f|A is bounded & f is integrable holds max-(f) is integrable; theorem :: INTEGRA4:23 for f being Function of A,REAL st f|A is bounded & f is integrable holds abs(f) is integrable & |.integral(f).|<=integral(abs(f)); theorem :: INTEGRA4:24 for f being Function of A,REAL st (for x,y st x in A & y in A holds |.f.x-f.y.|<=a) holds upper_bound rng f - lower_bound rng f <= a; theorem :: INTEGRA4:25 for f,g being Function of A,REAL st f|A is bounded & a>=0 & (for x,y st x in A & y in A holds |.g.x-g.y.|<=a*|.f.x-f.y.|) holds upper_bound rng g - lower_bound rng g <= a*(upper_bound rng f - lower_bound rng f); theorem :: INTEGRA4:26 for f,g,h being Function of A,REAL st f|A is bounded & g|A is bounded & a>=0 & (for x,y st x in A & y in A holds |.h.x-h.y.|<=a*(|.f.x-f.y .|+|.g.x-g.y.|)) holds upper_bound rng h - lower_bound rng h <= a*((upper_bound rng f - lower_bound rng f)+(upper_bound rng g - lower_bound rng g)); theorem :: INTEGRA4:27 for f,g being Function of A,REAL st f|A is bounded & f is integrable & g|A is bounded & a>0 & (for x,y st x in A & y in A holds |.g.x-g .y.|<=a*|.f.x-f.y.|) holds g is integrable; theorem :: INTEGRA4:28 for f,g,h being Function of A,REAL st f|A is bounded & f is integrable & g|A is bounded & g is integrable & h|A is bounded & a > 0 & (for x ,y st x in A & y in A holds |.h.x-h.y.|<=a*(|.f.x-f.y.|+|.g.x-g.y.|)) holds h is integrable; theorem :: INTEGRA4:29 for f,g being Function of A,REAL st f|A is bounded & f is integrable & g|A is bounded & g is integrable holds f(#)g is integrable; theorem :: INTEGRA4:30 for f being Function of A,REAL st f|A is bounded & f is integrable & not 0 in rng f & f^|A is bounded holds f^ is integrable;