:: Definition of Integrability for Partial Functions from REAL to :: REAL and Integrability for Continuous Functions :: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama :: :: Received March 23, 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, FINSEQ_1, ORDINAL4, CARD_3, ARYTM_1, ARYTM_3, BINOP_2, RELAT_1, FUNCT_1, PARTFUN1, XXREAL_0, FINSEQ_2, NAT_1, XBOOLE_0, REALSET1, VALUED_1, TARSKI, XXREAL_2, ORDINAL2, FCONT_2, INTEGRA2, FUNCT_3, SEQ_2, CARD_1, SEQ_1, COMPLEX1, MEASURE7, FDIFF_1, SEQ_4, XXREAL_1, ZFMISC_1, VALUED_0, SEQM_3, RCOMP_1, INTEGRA5, MEASURE5, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, COMPLEX1, XXREAL_2, ZFMISC_1, FUNCT_1, RELSET_1, FUNCT_2, RCOMP_1, PARTFUN1, MEASURE6, FINSEQ_1, FUNCOP_1, VALUED_1, SEQ_1, RFUNCT_1, FINSEQ_2, COMSEQ_2, SEQ_2, SEQ_4, BINOP_2, REAL_1, NAT_1, FDIFF_1, RVSUM_1, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, FCONT_1, FCONT_2, RFUNCT_2, XXREAL_0; constructors PARTFUN1, REAL_1, NAT_1, BINOP_2, COMPLEX1, RFUNCT_1, RFUNCT_2, FCONT_1, FCONT_2, FDIFF_1, ZFMISC_1, MEASURE6, INTEGRA2, XXREAL_2, RVSUM_1, SEQ_4, RELSET_1, FUNCOP_1, SEQ_2, INTEGRA3, COMSEQ_2; registrations XBOOLE_0, RELAT_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1, RCOMP_1, INTEGRA1, VALUED_0, VALUED_1, FUNCT_2, FINSET_1, XXREAL_2, CARD_1, SEQ_2, RELSET_1, MEASURE5, RVSUM_1, ORDINAL1, FINSEQ_2; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin ::Some useful properties of finite sequence reserve i,k,n,m for Element of NAT; reserve a,b,r,r1,r2,s,x,x1,x2 for Real; reserve A for non empty closed_interval Subset of REAL; reserve X for set; theorem :: INTEGRA5:1 for F,F1,F2 being FinSequence of REAL, r1,r2 st (F1=<*r1*>^F or F1=F^<*r1*>) & (F2=<*r2*>^F or F2=F^<*r2*>) holds Sum(F1-F2)=r1-r2; theorem :: INTEGRA5:2 for F1,F2 being FinSequence of REAL st len F1 = len F2 holds len (F1+F2)=len F1 & len (F1-F2)=len F1 & Sum(F1+F2)=Sum F1+Sum F2 & Sum(F1-F2)= Sum F1-Sum F2; theorem :: INTEGRA5:3 for F1,F2 being FinSequence of REAL st len F1 = len F2 & (for i st i in dom F1 holds F1.i <= F2.i) holds Sum F1 <= Sum F2; begin :: Integrability for partial function of REAL,REAL notation let f be PartFunc of REAL,REAL; let C be non empty Subset of REAL; synonym f||C for f|C; end; definition let f be PartFunc of REAL,REAL; let C be non empty Subset of REAL; redefine func f||C -> PartFunc of C,REAL; end; theorem :: INTEGRA5:4 for f,g being PartFunc of REAL,REAL, C being non empty Subset of REAL holds (f||C)(#)(g||C) = (f(#)g)||C; theorem :: INTEGRA5:5 for f,g being PartFunc of REAL,REAL, C being non empty Subset of REAL holds (f+g)||C = f||C + g||C; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,REAL; pred f is_integrable_on A means :: INTEGRA5:def 1 f||A is integrable; end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,REAL; func integral(f,A) -> Real equals :: INTEGRA5:def 2 integral(f||A); end; theorem :: INTEGRA5:6 for f being PartFunc of REAL,REAL st A c= dom f holds f||A is total; theorem :: INTEGRA5:7 for f being PartFunc of REAL,REAL st f|A is bounded_above holds f ||A|A is bounded_above; theorem :: INTEGRA5:8 for f being PartFunc of REAL,REAL st f|A is bounded_below holds f ||A|A is bounded_below; theorem :: INTEGRA5:9 for f being PartFunc of REAL,REAL st f|A is bounded holds f||A|A is bounded; begin :: Integrability for continuous function theorem :: INTEGRA5:10 for f being PartFunc of REAL,REAL st A c= dom f & f|A is continuous holds f|A is bounded; theorem :: INTEGRA5:11 for f being PartFunc of REAL,REAL st A c= dom f & f|A is continuous holds f is_integrable_on A; theorem :: INTEGRA5:12 for f being PartFunc of REAL,REAL, D being Division of A st A c= X & f is_differentiable_on X & (f`|X)|A is bounded holds lower_sum((f`|X)||A,D) <= f.(upper_bound A)-f.(lower_bound A) & f.(upper_bound A)-f.(lower_bound A) <=upper_sum((f`|X)||A,D); ::$N Fundamental Theorem of Integral Calculus theorem :: INTEGRA5:13 for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f`|X is_integrable_on A & (f`|X)|A is bounded holds integral(f`|X,A) = f.(upper_bound A)-f.(lower_bound A); theorem :: INTEGRA5:14 for f being PartFunc of REAL,REAL st f|A is non-decreasing & A c= dom f holds rng (f|A) is real-bounded; theorem :: INTEGRA5:15 for f being PartFunc of REAL,REAL st f|A is non-decreasing & A c= dom f holds lower_bound rng (f|A) = f.(lower_bound A) & upper_bound rng (f|A) = f.(upper_bound A); theorem :: INTEGRA5:16 for f being PartFunc of REAL,REAL st f|A is monotone & A c= dom f holds f is_integrable_on A; theorem :: INTEGRA5:17 for f being PartFunc of REAL,REAL, A,B being non empty closed_interval Subset of REAL st A c= dom f & f|A is continuous & B c= A holds f is_integrable_on B; theorem :: INTEGRA5:18 for f being PartFunc of REAL,REAL, A,B,C being non empty closed_interval Subset of REAL, X st A c= X & f is_differentiable_on X & (f`|X)|A is continuous &lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds B c= A & C c= A & integral(f`|X,A )=integral(f`|X,B)+integral(f`|X,C); definition let a,b be Real; assume a<=b; func [' a,b '] -> non empty closed_interval Subset of REAL equals :: INTEGRA5:def 3 [.a,b.]; end; definition let a,b be Real; let f be PartFunc of REAL,REAL; func integral(f,a,b) -> Real equals :: INTEGRA5:def 4 integral(f,[' a,b ']) if a<=b otherwise -integral(f,[' b,a ']); end; theorem :: INTEGRA5:19 for f being PartFunc of REAL,REAL, A being non empty closed_interval Subset of REAL, a,b st A=[.a,b.] holds integral(f,A)=integral(f,a,b); theorem :: INTEGRA5:20 for f being PartFunc of REAL,REAL, A being non empty closed_interval Subset of REAL, a,b st A=[.b,a.] holds -integral(f,A)=integral(f,a,b); theorem :: INTEGRA5:21 for f,g being PartFunc of REAL,REAL, X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f`|X is_integrable_on A & (f`|X)|A is bounded & g`|X is_integrable_on A & (g`|X)|A is bounded holds integral((f`|X)(#)g,A) = f.(upper_bound A)*g.(upper_bound A)-f.(lower_bound A)*g.(lower_bound A )-integral(f(#)(g`|X),A);