:: Improper Integral, Part {II} :: by Noboru Endou :: :: Received December 8, 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, XXREAL_0, NAT_1, XXREAL_2, XBOOLE_0, REAL_1, XXREAL_1, ARYTM_1, COMPLEX1, SEQ_1, PARTFUN1, INTEGRA1, INTEGRA5, VALUED_1, FUNCT_2, LIMFUNC1, INTEGR10, FUNCT_7, INTEGR25; notations TARSKI, XBOOLE_0, SUBSET_1, SEQ_1, FUNCT_1, RELSET_1, PARTFUN1, XXREAL_3, VALUED_1, SEQ_2, FUNCT_2, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, NUMBERS, ORDINAL1, NAT_1, VALUED_0, RCOMP_1, INTEGRA5, LIMFUNC1, INTEGR10; constructors PROB_3, RVSUM_1, SEQ_2, NEWTON, COMSEQ_2, INTEGRA2, INTEGRA5, LIMFUNC1, RELSET_1, INTEGR10; registrations XBOOLE_0, ORDINAL1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, RELSET_1, NAT_1, XXREAL_0, FUNCT_2, XXREAL_3, VALUED_1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin :: Properties of Extended Riemann Integral on Infinite Interval theorem :: INTEGR25:1 for f be PartFunc of REAL,REAL st f is divergent_in-infty_to+infty holds not f is convergent_in-infty & not f is divergent_in-infty_to-infty; theorem :: INTEGR25:2 for f be PartFunc of REAL,REAL st f is divergent_in-infty_to-infty holds not f is convergent_in-infty & not f is divergent_in-infty_to+infty; theorem :: INTEGR25:3 for f be PartFunc of REAL,REAL st f is divergent_in+infty_to+infty holds not f is convergent_in+infty & not f is divergent_in+infty_to-infty; theorem :: INTEGR25:4 for f be PartFunc of REAL,REAL st f is divergent_in+infty_to-infty holds not f is convergent_in+infty & not f is divergent_in+infty_to+infty; theorem :: INTEGR25:5 for f be PartFunc of REAL,REAL st f is convergent_in-infty holds (ex r be Real st f|left_open_halfline r is bounded_below) & (ex r be Real st f|left_open_halfline r is bounded_above); theorem :: INTEGR25:6 for f be PartFunc of REAL,REAL st f is convergent_in+infty holds (ex r be Real st f|right_open_halfline r is bounded_below) & (ex r be Real st f|right_open_halfline r is bounded_above); theorem :: INTEGR25:7 for f be PartFunc of REAL,REAL st f is divergent_in-infty_to+infty holds ex r be Real st f|left_open_halfline r is bounded_below; theorem :: INTEGR25:8 for f be PartFunc of REAL,REAL st f is divergent_in-infty_to-infty holds ex r be Real st f|left_open_halfline r is bounded_above; theorem :: INTEGR25:9 for f be PartFunc of REAL,REAL st f is divergent_in+infty_to+infty holds ex r be Real st f|right_open_halfline r is bounded_below; theorem :: INTEGR25:10 for f be PartFunc of REAL,REAL st f is divergent_in+infty_to-infty holds ex r be Real st f|right_open_halfline r is bounded_above; theorem :: INTEGR25:11 for f1,f2 be PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & (for r be Real ex g be Real st g ExtReal means :: INTEGR25:def 3 ex Intf be PartFunc of REAL,REAL st dom Intf = left_closed_halfline b & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) & (Intf is convergent_in-infty & it = lim_in-infty Intf or Intf is divergent_in-infty_to+infty & it = +infty or Intf is divergent_in-infty_to-infty & it = -infty); end; definition let f be PartFunc of REAL,REAL; let a be Real; assume f is_+infty_improper_integrable_on a; func improper_integral_+infty(f,a) -> ExtReal means :: INTEGR25:def 4 ex Intf be PartFunc of REAL,REAL st dom Intf = right_closed_halfline a & (for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)) & (Intf is convergent_in+infty & it = lim_in+infty Intf or Intf is divergent_in+infty_to+infty & it = +infty or Intf is divergent_in+infty_to-infty & it = -infty); end; theorem :: INTEGR25:20 for f be PartFunc of REAL,REAL, b be Real st f is_-infty_ext_Riemann_integrable_on b holds f is_-infty_improper_integrable_on b; theorem :: INTEGR25:21 for f be PartFunc of REAL,REAL, a be Real st f is_+infty_ext_Riemann_integrable_on a holds f is_+infty_improper_integrable_on a; theorem :: INTEGR25:22 for f be PartFunc of REAL,REAL, b be Real st f is_-infty_improper_integrable_on b holds (f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)) or (not f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty(f,b) = +infty) or (not f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty(f,b) = -infty); theorem :: INTEGR25:23 for f be PartFunc of REAL,REAL, b be Real st ex Intf be PartFunc of REAL,REAL st dom Intf = left_closed_halfline b & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) & (Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty) holds not f is_-infty_ext_Riemann_integrable_on b; theorem :: INTEGR25:24 for f,Intf be PartFunc of REAL,REAL, b be Real st f is_-infty_improper_integrable_on b & dom Intf = left_closed_halfline b & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) & Intf is convergent_in-infty holds improper_integral_-infty(f,b) = lim_in-infty Intf; theorem :: INTEGR25:25 for f be PartFunc of REAL,REAL, b,c be Real st b <= c & left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c holds f is_-infty_improper_integrable_on b & ( improper_integral_-infty(f,c) = infty_ext_left_integral(f,c) implies improper_integral_-infty(f,b) = infty_ext_left_integral(f,b) ) & ( improper_integral_-infty(f,c) = +infty implies improper_integral_-infty(f,b) = +infty ) & ( improper_integral_-infty(f,c) = -infty implies improper_integral_-infty(f,b) = -infty ); theorem :: INTEGR25:26 for f be PartFunc of REAL,REAL, b,c be Real st b <= c & left_closed_halfline c c= dom f & f|['b,c'] is bounded & f is_-infty_improper_integrable_on b & f is_integrable_on ['b,c'] holds f is_-infty_improper_integrable_on c & ( improper_integral_-infty(f,b) = infty_ext_left_integral(f,b) implies improper_integral_-infty(f,c) = improper_integral_-infty(f,b) + integral(f,b,c) ) & ( improper_integral_-infty(f,b) = +infty implies improper_integral_-infty(f,c) = +infty ) & ( improper_integral_-infty(f,b) = -infty implies improper_integral_-infty(f,c) = -infty ); theorem :: INTEGR25:27 for f be PartFunc of REAL,REAL, b be Real st f is_+infty_improper_integrable_on b holds (f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)) or (not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty(f,b) = +infty) or (not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty(f,b) = -infty); theorem :: INTEGR25:28 for f be PartFunc of REAL,REAL, b be Real st ex Intf be PartFunc of REAL,REAL st dom Intf = right_closed_halfline b & (for x be Real st x in dom Intf holds Intf.x = integral(f,b,x)) & (Intf is divergent_in+infty_to+infty or Intf is divergent_in+infty_to-infty) holds not f is_+infty_ext_Riemann_integrable_on b; theorem :: INTEGR25:29 for f,Intf be PartFunc of REAL,REAL, b be Real st f is_+infty_improper_integrable_on b & dom Intf = right_closed_halfline b & (for x be Real st x in dom Intf holds Intf.x = integral(f,b,x)) & Intf is convergent_in+infty holds improper_integral_+infty(f,b) = lim_in+infty Intf; theorem :: INTEGR25:30 for f be PartFunc of REAL,REAL, b,c be Real st b >= c & right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c holds f is_+infty_improper_integrable_on b & ( improper_integral_+infty(f,c) = infty_ext_right_integral(f,c) implies improper_integral_+infty(f,b) = infty_ext_right_integral(f,b) ) & ( improper_integral_+infty(f,c) = +infty implies improper_integral_+infty(f,b) = +infty ) & ( improper_integral_+infty(f,c) = -infty implies improper_integral_+infty(f,b) = -infty ); theorem :: INTEGR25:31 for f be PartFunc of REAL,REAL, b,c be Real st b >= c & right_closed_halfline c c= dom f & f|['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] holds f is_+infty_improper_integrable_on c & ( improper_integral_+infty(f,b) = infty_ext_right_integral(f,b) implies improper_integral_+infty(f,c) = improper_integral_+infty(f,b) + integral(f,c,b) ) & ( improper_integral_+infty(f,b) = +infty implies improper_integral_+infty(f,c) = +infty ) & ( improper_integral_+infty(f,b) = -infty implies improper_integral_+infty(f,c) = -infty ); definition let f be PartFunc of REAL,REAL; pred f is_improper_integrable_on_REAL means :: INTEGR25:def 5 ex r be Real st f is_-infty_improper_integrable_on r & f is_+infty_improper_integrable_on r & not (improper_integral_-infty(f,r) = -infty & improper_integral_+infty(f,r) = +infty) & not (improper_integral_-infty(f,r) = +infty & improper_integral_+infty(f,r) = -infty); end; theorem :: INTEGR25:32 for f be PartFunc of REAL,REAL st f is_improper_integrable_on_REAL holds ex b be Real st ( (improper_integral_-infty(f,b) = infty_ext_left_integral(f,b) & improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)) or improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = +infty or improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = -infty); theorem :: INTEGR25:33 for f be PartFunc of REAL,REAL, b be Real st dom f = REAL & f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & not (improper_integral_-infty(f,b) = -infty & improper_integral_+infty(f,b) = +infty) & not (improper_integral_-infty(f,b) = +infty & improper_integral_+infty(f,b) = -infty) holds for b1 be Real st b1 <= b holds improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1); theorem :: INTEGR25:34 for f be PartFunc of REAL,REAL, b be Real st dom f = REAL & f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & not (improper_integral_-infty(f,b) = -infty & improper_integral_+infty(f,b) = +infty) & not (improper_integral_-infty(f,b) = +infty & improper_integral_+infty(f,b) = -infty) holds for b2 be Real st b <= b2 holds improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = improper_integral_-infty(f,b2)+improper_integral_+infty(f,b2); theorem :: INTEGR25:35 for f be PartFunc of REAL,REAL st dom f = REAL & f is_improper_integrable_on_REAL holds for b1,b2 be Real holds improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1) = improper_integral_-infty(f,b2)+improper_integral_+infty(f,b2); definition let f be PartFunc of REAL,REAL; assume dom f = REAL & f is_improper_integrable_on_REAL; func improper_integral_on_REAL f -> ExtReal means :: INTEGR25:def 6 ex c be Real st f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & it = improper_integral_-infty(f,c) + improper_integral_+infty(f,c); end; theorem :: INTEGR25:36 for f be PartFunc of REAL,REAL, b be Real st dom f = REAL & f is_improper_integrable_on_REAL holds f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = improper_integral_-infty(f,b) + improper_integral_+infty(f,b); begin :: Linearity of Improper Integral on Infinite Interval theorem :: INTEGR25:37 for f be PartFunc of REAL,REAL, b be Real st f is_-infty_improper_integrable_on b & improper_integral_-infty(f,b) = +infty holds for Intf be PartFunc of REAL,REAL st dom Intf = left_closed_halfline b & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) holds Intf is divergent_in-infty_to+infty; theorem :: INTEGR25:38 for f be PartFunc of REAL,REAL, b be Real st f is_-infty_improper_integrable_on b & improper_integral_-infty(f,b) = -infty holds for Intf be PartFunc of REAL,REAL st dom Intf = left_closed_halfline b & (for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)) holds Intf is divergent_in-infty_to-infty; theorem :: INTEGR25:39 for f be PartFunc of REAL,REAL, a be Real st f is_+infty_improper_integrable_on a & improper_integral_+infty(f,a) = +infty holds for Intf be PartFunc of REAL,REAL st dom Intf = right_closed_halfline a & (for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)) holds Intf is divergent_in+infty_to+infty; theorem :: INTEGR25:40 for f be PartFunc of REAL,REAL, a be Real st f is_+infty_improper_integrable_on a & improper_integral_+infty(f,a) = -infty holds for Intf be PartFunc of REAL,REAL st dom Intf = right_closed_halfline a & (for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)) holds Intf is divergent_in+infty_to-infty; theorem :: INTEGR25:41 for f be PartFunc of REAL,REAL, b,r be Real st left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b holds r(#)f is_-infty_improper_integrable_on b & improper_integral_-infty(r(#)f,b) = r * improper_integral_-infty(f,b); theorem :: INTEGR25:42 for f be PartFunc of REAL,REAL, a,r be Real st right_closed_halfline a c= dom f & f is_+infty_improper_integrable_on a holds r(#)f is_+infty_improper_integrable_on a & improper_integral_+infty(r(#)f,a) = r * improper_integral_+infty(f,a); theorem :: INTEGR25:43 for f be PartFunc of REAL,REAL, b be Real st left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b holds -f is_-infty_improper_integrable_on b & improper_integral_-infty(-f,b) = - improper_integral_-infty(f,b); theorem :: INTEGR25:44 for f be PartFunc of REAL,REAL, a be Real st right_closed_halfline a c= dom f & f is_+infty_improper_integrable_on a holds -f is_+infty_improper_integrable_on a & improper_integral_+infty(-f,a) = - improper_integral_+infty(f,a); theorem :: INTEGR25:45 for f,g be PartFunc of REAL,REAL, b be Real st left_closed_halfline b c= dom f & left_closed_halfline b c= dom g & f is_-infty_improper_integrable_on b & g is_-infty_improper_integrable_on b & not (improper_integral_-infty(f,b) = +infty & improper_integral_-infty(g,b) = -infty) & not (improper_integral_-infty(f,b) = -infty & improper_integral_-infty(g,b) = +infty) holds f+g is_-infty_improper_integrable_on b & improper_integral_-infty(f+g,b) = improper_integral_-infty(f,b) + improper_integral_-infty(g,b); theorem :: INTEGR25:46 for f,g be PartFunc of REAL,REAL, a be Real st right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_improper_integrable_on a & g is_+infty_improper_integrable_on a & not (improper_integral_+infty(f,a) = +infty & improper_integral_+infty(g,a) = -infty) & not (improper_integral_+infty(f,a) = -infty & improper_integral_+infty(g,a) = +infty) holds f+g is_+infty_improper_integrable_on a & improper_integral_+infty(f+g,a) = improper_integral_+infty(f,a) + improper_integral_+infty(g,a); theorem :: INTEGR25:47 for f,g be PartFunc of REAL,REAL, b be Real st left_closed_halfline b c= dom f & left_closed_halfline b c= dom g & f is_-infty_improper_integrable_on b & g is_-infty_improper_integrable_on b & not (improper_integral_-infty(f,b) = +infty & improper_integral_-infty(g,b) = +infty) & not (improper_integral_-infty(f,b) = -infty & improper_integral_-infty(g,b) = -infty) holds f-g is_-infty_improper_integrable_on b & improper_integral_-infty(f-g,b) = improper_integral_-infty(f,b) - improper_integral_-infty(g,b); theorem :: INTEGR25:48 for f,g be PartFunc of REAL,REAL, a be Real st right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_improper_integrable_on a & g is_+infty_improper_integrable_on a & not (improper_integral_+infty(f,a) = +infty & improper_integral_+infty(g,a) = +infty) & not (improper_integral_+infty(f,a) = -infty & improper_integral_+infty(g,a) = -infty) holds f-g is_+infty_improper_integrable_on a & improper_integral_+infty(f-g,a) = improper_integral_+infty(f,a) - improper_integral_+infty(g,a); theorem :: INTEGR25:49 for f be PartFunc of REAL,REAL, r be Real st dom f = REAL & f is_improper_integrable_on_REAL holds r(#)f is_improper_integrable_on_REAL & improper_integral_on_REAL (r(#)f) = r * improper_integral_on_REAL(f); theorem :: INTEGR25:50 for f be PartFunc of REAL,REAL, r be Real st dom f = REAL & f is_improper_integrable_on_REAL holds -f is_improper_integrable_on_REAL & improper_integral_on_REAL -f = - improper_integral_on_REAL f; theorem :: INTEGR25:51 for f,g be PartFunc of REAL,REAL st dom f = REAL & dom g = REAL & f is_improper_integrable_on_REAL & g is_improper_integrable_on_REAL & not (improper_integral_on_REAL f = +infty & improper_integral_on_REAL g = -infty) & not (improper_integral_on_REAL f = -infty & improper_integral_on_REAL g = +infty) holds f+g is_improper_integrable_on_REAL & improper_integral_on_REAL (f+g) = improper_integral_on_REAL f + improper_integral_on_REAL g; theorem :: INTEGR25:52 for f,g be PartFunc of REAL,REAL st dom f = REAL & dom g = REAL & f is_improper_integrable_on_REAL & g is_improper_integrable_on_REAL & not (improper_integral_on_REAL f = +infty & improper_integral_on_REAL g = +infty) & not (improper_integral_on_REAL f = -infty & improper_integral_on_REAL g = -infty) holds f-g is_improper_integrable_on_REAL & improper_integral_on_REAL (f-g) = improper_integral_on_REAL f - improper_integral_on_REAL g;