:: Riemann Indefinite Integral of Functions of Real Variable :: by Yasunari Shidama , Noboru Endou , Katsumi Wasaki and Katuhiko Kanazashi :: :: Received June 6, 2007 :: Copyright (c) 2007-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, XBOOLE_0, PARTFUN1, SUBSET_1, FUNCT_1, RELAT_1, XXREAL_2, COMPLEX1, ARYTM_1, XXREAL_0, SEQ_4, ARYTM_3, REAL_1, FDIFF_1, RCOMP_1, TARSKI, VALUED_1, CARD_1, ORDINAL4, INTEGRA5, INTEGRA1, XXREAL_1, SQUARE_1, ORDINAL2, FUNCOP_1, FCONT_1, REALSET1, SIN_COS, PREPOWER, SEQFUNC, SEQ_1, SEQ_2, INTEGRA2, FUNCT_3, FINSEQ_1, FINSEQ_2, CARD_3, MEASURE7, NAT_1, INTEGRA7, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, XXREAL_2, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCOP_1, RELSET_1, FUNCT_2, RCOMP_1, PARTFUN1, PARTFUN2, FINSEQ_1, VALUED_1, SEQ_1, RFUNCT_1, SEQ_2, SEQ_4, SQUARE_1, PREPOWER, FCONT_1, FDIFF_1, FINSEQ_2, RVSUM_1, INTEGRA1, INTEGRA2, SEQFUNC, SIN_COS, TAYLOR_1, INTEGRA3, INTEGRA5; constructors REAL_1, FDIFF_1, PARTFUN2, RFUNCT_1, INTEGRA2, LIMFUNC1, FCONT_1, BINOP_2, INTEGRA5, SIN_COS, PREPOWER, TAYLOR_1, SQUARE_1, SEQFUNC, RVSUM_1, SEQ_4, RELSET_1, SEQ_2, COMPLEX1, INTEGRA3, COMSEQ_2; registrations XREAL_0, RELSET_1, INTEGRA1, RCOMP_1, INT_1, MEMBERED, PREPOWER, XBOOLE_0, NUMBERS, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, SEQ_2, FCONT_3, SQUARE_1, FINSEQ_2, RELAT_1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin :: Preliminaries reserve a,b,r for Real; reserve A for non empty set; reserve X,x for set; reserve f,g,F,G for PartFunc of REAL,REAL; reserve n for Element of NAT; theorem :: INTEGRA7:1 for f,g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & (for x be set st x in A holds |.f.x-g.x.|<=a) holds upper_bound rng f - upper_bound rng g <= a & upper_bound rng g - upper_bound rng f <= a; theorem :: INTEGRA7:2 for f,g being Function of A,REAL st rng f is bounded_below & rng g is bounded_below & (for x be set st x in A holds |.f.x-g.x.|<=a) holds lower_bound rng f - lower_bound rng g <= a & lower_bound rng g - lower_bound rng f <= a; theorem :: INTEGRA7:3 f|X|X is bounded implies f|X is bounded; theorem :: INTEGRA7:4 for x be Real st x in X & f|X is_differentiable_in x holds f is_differentiable_in x; theorem :: INTEGRA7:5 f|X is_differentiable_on X implies f is_differentiable_on X; theorem :: INTEGRA7:6 f is_differentiable_on X & g is_differentiable_on X implies f+g is_differentiable_on X & f-g is_differentiable_on X & f(#)g is_differentiable_on X; theorem :: INTEGRA7:7 f is_differentiable_on X implies r(#)f is_differentiable_on X; theorem :: INTEGRA7:8 (for x be set st x in X holds g.x <> 0) & f is_differentiable_on X & g is_differentiable_on X implies f/g is_differentiable_on X; theorem :: INTEGRA7:9 (for x be set st x in X holds f.x <> 0) & f is_differentiable_on X implies f^ is_differentiable_on X; theorem :: INTEGRA7:10 a <= b & [' a,b '] c= X & F is_differentiable_on X & F`|X is_integrable_on [' a,b '] & (F`|X)|[' a,b '] is bounded implies F.b = integral (F`|X,a,b) + F.a; begin :: The Definition of Indefinite Integral definition let X be set, f be PartFunc of REAL,REAL; func IntegralFuncs(f,X) -> set means :: INTEGRA7:def 1 x in it iff ex F be PartFunc of REAL,REAL st x = F & F is_differentiable_on X & F`|X = f|X; end; definition let X be set, F,f be PartFunc of REAL,REAL; pred F is_integral_of f,X means :: INTEGRA7:def 2 F in IntegralFuncs(f,X); end; theorem :: INTEGRA7:11 F is_integral_of f,X implies X c= dom F; theorem :: INTEGRA7:12 F is_integral_of f,X & G is_integral_of g,X implies F+G is_integral_of f+g,X & F-G is_integral_of f-g,X; theorem :: INTEGRA7:13 F is_integral_of f,X implies r(#)F is_integral_of r(#)f,X; theorem :: INTEGRA7:14 F is_integral_of f,X & G is_integral_of g,X implies F(#)G is_integral_of f(#)G+F(#)g,X; theorem :: INTEGRA7:15 (for x be set st x in X holds G.x <> 0) & F is_integral_of f,X & G is_integral_of g,X implies F/G is_integral_of (f(#)G-F(#)g)/(G(#)G),X; theorem :: INTEGRA7:16 a <= b & [' a,b '] c= dom f & f|[' a,b '] is continuous & ]. a,b .[ c= dom F & (for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x) + F.a ) implies F is_integral_of f,]. a,b .[; theorem :: INTEGRA7:17 for x,x0 be Real st f| [. a,b .] is continuous & [.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ & F is_integral_of f,].a,b.[ holds F.x = integral(f,x0,x) + F.x0; theorem :: INTEGRA7:18 a <= b & [' a,b '] c= X & F is_integral_of f,X & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded implies F.b = integral(f,a, b) + F.a; theorem :: INTEGRA7:19 a <= b & [. a,b .] c= X & X c= dom f & f|X is continuous implies f|[' a,b '] is continuous & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded; theorem :: INTEGRA7:20 a <= b & [. a,b .] c= X & X c= dom f & f|X is continuous & F is_integral_of f,X implies F.b = integral(f,a,b) + F.a; theorem :: INTEGRA7:21 b <= a & [' b,a '] c= X & f is_integrable_on [' b,a '] & g is_integrable_on [' b,a '] & f|[' b,a '] is bounded & g|[' b,a '] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X implies ( F.a)*(G.a) - (F.b)*(G.b) = integral(f(#)G,b,a) + integral(F(#)g,b,a); theorem :: INTEGRA7:22 b <= a & [. b,a .] c= X & X c= dom f & X c= dom g & f|X is continuous & g|X is continuous & F is_integral_of f,X & G is_integral_of g,X implies (F.a) *(G.a) - (F.b)*(G.b) = integral(f(#)G,b,a)+ integral(F(#)g,b,a); begin :: Examples of Indefinite Integral theorem :: INTEGRA7:23 sin is_integral_of cos,REAL; theorem :: INTEGRA7:24 sin.b-sin.a = integral(cos,a,b); theorem :: INTEGRA7:25 (-1)(#)cos is_integral_of sin,REAL; theorem :: INTEGRA7:26 cos.a - cos.b = integral(sin,a,b); theorem :: INTEGRA7:27 exp_R is_integral_of exp_R,REAL; theorem :: INTEGRA7:28 exp_R.b-exp_R.a = integral(exp_R,a,b); theorem :: INTEGRA7:29 #Z (n+1) is_integral_of (n+1)(#)( #Z n),REAL; theorem :: INTEGRA7:30 ( #Z (n+1)).b - ( #Z (n+1)).a = integral((n+1)(#)( #Z n),a,b); begin :: Uniform Convergent Functional Sequence theorem :: INTEGRA7:31 for H be Functional_Sequence of REAL,REAL, rseq be Real_Sequence st a < b & (for n be Element of NAT holds H.n is_integrable_on [' a,b '] & (H.n)|[' a,b '] is bounded & rseq.n = integral(H.n,a,b) ) & H is_unif_conv_on [' a,b '] holds lim(H,[' a,b '])|[' a,b '] is bounded & lim(H,[' a,b ']) is_integrable_on [' a,b '] & rseq is convergent & lim rseq = integral(lim(H,[' a,b ']),a,b);