:: Improper Integral, Part {I} :: by Noboru Endou :: :: Received September 30, 2021 :: Copyright (c) 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 FUNCT_1, NUMBERS, SUBSET_1, ARYTM_3, CARD_1, RELAT_1, TARSKI, ORDINAL2, XXREAL_0, NAT_1, XXREAL_2, XBOOLE_0, REAL_1, MEASURE7, XXREAL_1, ARYTM_1, CARD_3, FINSEQ_1, ORDINAL4, SEQ_2, COMPLEX1, SEQ_1, PARTFUN1, INTEGRA1, INTEGRA2, INTEGRA4, INTEGRA5, REALSET1, SEQ_4, FUNCT_3, VALUED_1, FUNCT_2, LIMFUNC1, LIMFUNC2, INTEGR10, FUNCT_7, RFINSEQ, INTEGR24; notations TARSKI, XBOOLE_0, SUBSET_1, SEQ_1, FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, XXREAL_3, VALUED_1, FINSEQ_1, RVSUM_1, SEQ_2, SEQ_4, FUNCT_2, XXREAL_2, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, NUMBERS, NAT_1, VALUED_0, RCOMP_1, INTEGRA1, INTEGRA2, RFUNCT_1, INTEGRA3, INTEGRA4, INTEGRA5, RFINSEQ, LIMFUNC1, LIMFUNC2, INTEGR10; constructors PROB_3, RVSUM_1, RFUNCT_1, SEQ_2, SEQ_4, NEWTON, COMSEQ_2, INTEGRA2, INTEGRA4, INTEGRA5, INTEGRA3, LIMFUNC1, LIMFUNC2, RFINSEQ, REAL_1, RELSET_1, INTEGR10; registrations XBOOLE_0, ORDINAL1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, XXREAL_2, RELSET_1, NAT_1, FINSEQ_1, RELAT_1, FINSET_1, XXREAL_0, CARD_1, INTEGRA1, SEQM_3, FUNCT_2, XXREAL_3, SEQ_4, VALUED_1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin theorem :: INTEGR24:1 for f be PartFunc of REAL,REAL, a,b,c be Real st a <= b <= c & ['a,c'] c= dom f & f|['a,b'] is bounded & f|['b,c'] is bounded & f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] holds f is_integrable_on ['a,c'] & integral(f,a,c) = integral(f,a,b) + integral(f,b,c); theorem :: INTEGR24:2 for seq be Real_Sequence st seq is divergent_to+infty holds not seq is divergent_to-infty & not seq is convergent; theorem :: INTEGR24:3 for seq be Real_Sequence st seq is divergent_to-infty holds not seq is divergent_to+infty & not seq is convergent; theorem :: INTEGR24:4 for f be PartFunc of REAL,REAL, x0 be Real st f is_left_convergent_in x0 or f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ex seq be Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= dom f /\ left_open_halfline x0; theorem :: INTEGR24:5 for f be PartFunc of REAL,REAL, x0 be Real st f is_right_convergent_in x0 or f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ex seq be Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= dom f /\ right_open_halfline x0; theorem :: INTEGR24:6 for f be PartFunc of REAL,REAL, x0 be Real st f is_left_divergent_to+infty_in x0 holds not f is_left_divergent_to-infty_in x0 & not f is_left_convergent_in x0; theorem :: INTEGR24:7 for f be PartFunc of REAL,REAL, x0 be Real st f is_left_divergent_to-infty_in x0 holds not f is_left_divergent_to+infty_in x0 & not f is_left_convergent_in x0; theorem :: INTEGR24:8 for f be PartFunc of REAL,REAL, x0 be Real st f is_right_divergent_to+infty_in x0 holds not f is_right_divergent_to-infty_in x0 & not f is_right_convergent_in x0; theorem :: INTEGR24:9 for f be PartFunc of REAL,REAL, x0 be Real st f is_right_divergent_to-infty_in x0 holds not f is_right_divergent_to+infty_in x0 & not f is_right_convergent_in x0; theorem :: INTEGR24:10 for f be PartFunc of REAL,REAL, x0 be Real st f is_right_convergent_in x0 holds (ex r be Real st 0 ExtReal means :: INTEGR24:def 3 ex Intf be PartFunc of REAL,REAL st dom Intf = ].a,b.] & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) & (Intf is_right_convergent_in a & it = lim_right(Intf,a) or Intf is_right_divergent_to+infty_in a & it = +infty or Intf is_right_divergent_to-infty_in a & it = -infty); end; definition let f be PartFunc of REAL,REAL; let a,b be Real; assume f is_right_improper_integrable_on a,b; func right_improper_integral(f,a,b) -> ExtReal means :: INTEGR24:def 4 ex Intf be PartFunc of REAL,REAL st dom Intf = [.a,b.[ & (for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)) & (Intf is_left_convergent_in b & it = lim_left(Intf,b) or Intf is_left_divergent_to+infty_in b & it = +infty or Intf is_left_divergent_to-infty_in b & it = -infty); end; theorem :: INTEGR24:32 for f be PartFunc of REAL,REAL, a,b be Real st f is_left_ext_Riemann_integrable_on a,b holds f is_left_improper_integrable_on a,b; theorem :: INTEGR24:33 for f be PartFunc of REAL,REAL, a,b be Real st f is_right_ext_Riemann_integrable_on a,b holds f is_right_improper_integrable_on a,b; theorem :: INTEGR24:34 for f be PartFunc of REAL,REAL, a,b be Real st f is_left_improper_integrable_on a,b holds (f is_left_ext_Riemann_integrable_on a,b & left_improper_integral(f,a,b) = ext_left_integral(f,a,b)) or (not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral(f,a,b) = +infty) or (not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral(f,a,b) = -infty); theorem :: INTEGR24:35 for f be PartFunc of REAL,REAL, a,b be Real st ex Intf be PartFunc of REAL,REAL st dom Intf = ].a,b.] & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) & (Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a) holds not f is_left_ext_Riemann_integrable_on a,b; theorem :: INTEGR24:36 for f,Intf be PartFunc of REAL,REAL, a,b be Real st f is_left_improper_integrable_on a,b & dom Intf = ].a,b.] & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) & Intf is_right_convergent_in a holds left_improper_integral(f,a,b) = lim_right(Intf,a); theorem :: INTEGR24:37 for f be PartFunc of REAL,REAL, a,b,c be Real st a < b <= c & ].a,c.] c= dom f & f is_left_improper_integrable_on a,c holds f is_left_improper_integrable_on a,b & ( left_improper_integral(f,a,c) = ext_left_integral(f,a,c) implies left_improper_integral(f,a,b) = ext_left_integral(f,a,b) ) & ( left_improper_integral(f,a,c) = +infty implies left_improper_integral(f,a,b) = +infty ) & ( left_improper_integral(f,a,c) = -infty implies left_improper_integral(f,a,b) = -infty ); theorem :: INTEGR24:38 for f be PartFunc of REAL,REAL, a,b,c be Real st a < b <= c & ].a,c.] c= dom f & f|['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] holds f is_left_improper_integrable_on a,c & ( left_improper_integral(f,a,b) = ext_left_integral(f,a,b) implies left_improper_integral(f,a,c) = left_improper_integral(f,a,b) + integral(f,b,c) ) & ( left_improper_integral(f,a,b) = +infty implies left_improper_integral(f,a,c) = +infty ) & ( left_improper_integral(f,a,b) = -infty implies left_improper_integral(f,a,c) = -infty ); theorem :: INTEGR24:39 for f be PartFunc of REAL,REAL, a,b be Real st f is_right_improper_integrable_on a,b holds (f is_right_ext_Riemann_integrable_on a,b & right_improper_integral(f,a,b) = ext_right_integral(f,a,b)) or (not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral(f,a,b) = +infty) or (not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral(f,a,b) = -infty); theorem :: INTEGR24:40 for f be PartFunc of REAL,REAL, a,b be Real st ex Intf be PartFunc of REAL,REAL st dom Intf = [.a,b.[ & (for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)) & (Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b) holds not f is_right_ext_Riemann_integrable_on a,b; theorem :: INTEGR24:41 for f,Intf be PartFunc of REAL,REAL, a,b be Real st f is_right_improper_integrable_on a,b & dom Intf = [.a,b.[ & (for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)) & Intf is_left_convergent_in b holds right_improper_integral(f,a,b) = lim_left(Intf,b); theorem :: INTEGR24:42 for f be PartFunc of REAL,REAL, a,b,c be Real st a <= b < c & [.a,c.[ c= dom f & f is_right_improper_integrable_on a,c holds f is_right_improper_integrable_on b,c & ( right_improper_integral(f,a,c) = ext_right_integral(f,a,c) implies right_improper_integral(f,b,c) = ext_right_integral(f,b,c) ) & ( right_improper_integral(f,a,c) = +infty implies right_improper_integral(f,b,c) = +infty ) & ( right_improper_integral(f,a,c) = -infty implies right_improper_integral(f,b,c) = -infty ); theorem :: INTEGR24:43 for f be PartFunc of REAL,REAL, a,b,c be Real st a <= b < c & [.a,c.[ c= dom f & f|['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] holds f is_right_improper_integrable_on a,c & ( right_improper_integral(f,b,c) = ext_right_integral(f,b,c) implies right_improper_integral(f,a,c) = right_improper_integral(f,b,c) + integral(f,a,b) ) & ( right_improper_integral(f,b,c) = +infty implies right_improper_integral(f,a,c) = +infty ) & ( right_improper_integral(f,b,c) = -infty implies right_improper_integral(f,a,c) = -infty ); definition let f be PartFunc of REAL,REAL; let a,c be Real; pred f is_improper_integrable_on a,c means :: INTEGR24:def 5 ex b be Real st a < b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & not (left_improper_integral(f,a,b) = -infty & right_improper_integral(f,b,c) = +infty) & not (left_improper_integral(f,a,b) = +infty & right_improper_integral(f,b,c) = -infty); end; theorem :: INTEGR24:44 for f be PartFunc of REAL,REAL, a,c be Real st f is_improper_integrable_on a,c holds ex b be Real st a < b < c & ( (left_improper_integral(f,a,b) = ext_left_integral(f,a,b) & right_improper_integral(f,b,c) = ext_right_integral(f,b,c)) or left_improper_integral(f,a,b)+right_improper_integral(f,b,c) = +infty or left_improper_integral(f,a,b)+right_improper_integral(f,b,c) = -infty); theorem :: INTEGR24:45 for f be PartFunc of REAL,REAL, a,b,c be Real st ].a,c.[ c= dom f & a < b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & not (left_improper_integral(f,a,b) = -infty & right_improper_integral(f,b,c) = +infty) & not (left_improper_integral(f,a,b) = +infty & right_improper_integral(f,b,c) = -infty) holds for b1 be Real st a < b1 <= b holds left_improper_integral(f,a,b)+right_improper_integral(f,b,c) = left_improper_integral(f,a,b1)+right_improper_integral(f,b1,c); theorem :: INTEGR24:46 for f be PartFunc of REAL,REAL, a,b,c be Real st ].a,c.[ c= dom f & a < b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & not (left_improper_integral(f,a,b) = -infty & right_improper_integral(f,b,c) = +infty) & not (left_improper_integral(f,a,b) = +infty & right_improper_integral(f,b,c) = -infty) holds for b2 be Real st b <= b2 < c holds left_improper_integral(f,a,b)+right_improper_integral(f,b,c) = left_improper_integral(f,a,b2)+right_improper_integral(f,b2,c); theorem :: INTEGR24:47 for f be PartFunc of REAL,REAL, a,c be Real st ].a,c.[ c= dom f & f is_improper_integrable_on a,c holds for b1,b2 be Real st a < b1 < c & a < b2 < c holds left_improper_integral(f,a,b1)+right_improper_integral(f,b1,c) = left_improper_integral(f,a,b2)+right_improper_integral(f,b2,c); definition let f be PartFunc of REAL,REAL; let a,b be Real; assume ].a,b.[ c= dom f & f is_improper_integrable_on a,b; func improper_integral(f,a,b) -> ExtReal means :: INTEGR24:def 6 ex c be Real st a < c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & it = left_improper_integral(f,a,c) + right_improper_integral(f,c,b); end; theorem :: INTEGR24:48 for f be PartFunc of REAL,REAL, a,c be Real st ].a,c.[ c= dom f & f is_improper_integrable_on a,c holds for b be Real st a < b < c holds f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & improper_integral(f,a,c) = left_improper_integral(f,a,b) + right_improper_integral(f,b,c); begin :: Linearity of Improper Integral theorem :: INTEGR24:49 for f be PartFunc of REAL,REAL, a,b be Real st f is_left_improper_integrable_on a,b & left_improper_integral(f,a,b) = +infty holds for Intf be PartFunc of REAL,REAL st dom Intf = ].a,b.] & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) holds Intf is_right_divergent_to+infty_in a; theorem :: INTEGR24:50 for f be PartFunc of REAL,REAL, a,b be Real st f is_left_improper_integrable_on a,b & left_improper_integral(f,a,b) = -infty holds for Intf be PartFunc of REAL,REAL st dom Intf = ].a,b.] & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) holds Intf is_right_divergent_to-infty_in a; theorem :: INTEGR24:51 for f be PartFunc of REAL,REAL, a,b be Real st f is_right_improper_integrable_on a,b & right_improper_integral(f,a,b) = +infty holds for Intf be PartFunc of REAL,REAL st dom Intf = [.a,b.[ & (for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)) holds Intf is_left_divergent_to+infty_in b; theorem :: INTEGR24:52 for f be PartFunc of REAL,REAL, a,b be Real st f is_right_improper_integrable_on a,b & right_improper_integral(f,a,b) = -infty holds for Intf be PartFunc of REAL,REAL st dom Intf = [.a,b.[ & (for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)) holds Intf is_left_divergent_to-infty_in b; theorem :: INTEGR24:53 for f be PartFunc of REAL,REAL, a,b,r be Real st a < b & ].a,b.] c= dom f & f is_left_improper_integrable_on a,b holds r(#)f is_left_improper_integrable_on a,b & left_improper_integral(r(#)f,a,b) = r * left_improper_integral(f,a,b); theorem :: INTEGR24:54 for f be PartFunc of REAL,REAL, a,b,r be Real st a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b holds r(#)f is_right_improper_integrable_on a,b & right_improper_integral(r(#)f,a,b) = r * right_improper_integral(f,a,b); theorem :: INTEGR24:55 for f be PartFunc of REAL,REAL, a,b be Real st a < b & ].a,b.] c= dom f & f is_left_improper_integrable_on a,b holds -f is_left_improper_integrable_on a,b & left_improper_integral(-f,a,b) = - left_improper_integral(f,a,b); theorem :: INTEGR24:56 for f be PartFunc of REAL,REAL, a,b be Real st a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b holds -f is_right_improper_integrable_on a,b & right_improper_integral(-f,a,b) = - right_improper_integral(f,a,b); theorem :: INTEGR24:57 for f,g be PartFunc of REAL,REAL, a,b be Real st a < b & ].a,b.] c= dom f & ].a,b.] c= dom g & f is_left_improper_integrable_on a,b & g is_left_improper_integrable_on a,b & not (left_improper_integral(f,a,b) = +infty & left_improper_integral(g,a,b) = -infty) & not (left_improper_integral(f,a,b) = -infty & left_improper_integral(g,a,b) = +infty) holds f+g is_left_improper_integrable_on a,b & left_improper_integral(f+g,a,b) = left_improper_integral(f,a,b) + left_improper_integral(g,a,b); theorem :: INTEGR24:58 for f,g be PartFunc of REAL,REAL, a,b be Real st a < b & [.a,b.[ c= dom f & [.a,b.[ c= dom g & f is_right_improper_integrable_on a,b & g is_right_improper_integrable_on a,b & not (right_improper_integral(f,a,b) = +infty & right_improper_integral(g,a,b) = -infty) & not (right_improper_integral(f,a,b) = -infty & right_improper_integral(g,a,b) = +infty) holds f+g is_right_improper_integrable_on a,b & right_improper_integral(f+g,a,b) = right_improper_integral(f,a,b) + right_improper_integral(g,a,b); theorem :: INTEGR24:59 for f,g be PartFunc of REAL,REAL, a,b be Real st a < b & ].a,b.] c= dom f & ].a,b.] c= dom g & f is_left_improper_integrable_on a,b & g is_left_improper_integrable_on a,b & not (left_improper_integral(f,a,b) = +infty & left_improper_integral(g,a,b) = +infty) & not (left_improper_integral(f,a,b) = -infty & left_improper_integral(g,a,b) = -infty) holds f-g is_left_improper_integrable_on a,b & left_improper_integral(f-g,a,b) = left_improper_integral(f,a,b) - left_improper_integral(g,a,b); theorem :: INTEGR24:60 for f,g be PartFunc of REAL,REAL, a,b be Real st a < b & [.a,b.[ c= dom f & [.a,b.[ c= dom g & f is_right_improper_integrable_on a,b & g is_right_improper_integrable_on a,b & not (right_improper_integral(f,a,b) = +infty & right_improper_integral(g,a,b) = +infty) & not (right_improper_integral(f,a,b) = -infty & right_improper_integral(g,a,b) = -infty) holds f-g is_right_improper_integrable_on a,b & right_improper_integral(f-g,a,b) = right_improper_integral(f,a,b) - right_improper_integral(g,a,b); theorem :: INTEGR24:61 for f be PartFunc of REAL,REAL, a,b,r be Real st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds r(#)f is_improper_integrable_on a,b & improper_integral(r(#)f,a,b) = r * improper_integral(f,a,b); theorem :: INTEGR24:62 for f be PartFunc of REAL,REAL, a,b,r be Real st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds -f is_improper_integrable_on a,b & improper_integral(-f,a,b) = - improper_integral(f,a,b); theorem :: INTEGR24:63 for f,g be PartFunc of REAL,REAL, a,b be Real st ].a,b.[ c= dom f & ].a,b.[ c= dom g & f is_improper_integrable_on a,b & g is_improper_integrable_on a,b & not (improper_integral(f,a,b) = +infty & improper_integral(g,a,b) = -infty) & not (improper_integral(f,a,b) = -infty & improper_integral(g,a,b) = +infty) holds f+g is_improper_integrable_on a,b & improper_integral(f+g,a,b) = improper_integral(f,a,b)+improper_integral(g,a,b); theorem :: INTEGR24:64 for f,g be PartFunc of REAL,REAL, a,b be Real st ].a,b.[ c= dom f & ].a,b.[ c= dom g & f is_improper_integrable_on a,b & g is_improper_integrable_on a,b & not (improper_integral(f,a,b) = +infty & improper_integral(g,a,b) = +infty) & not (improper_integral(f,a,b) = -infty & improper_integral(g,a,b) = -infty) holds f-g is_improper_integrable_on a,b & improper_integral(f-g,a,b) = improper_integral(f,a,b)-improper_integral(g,a,b);