:: Improper Integral, Part {II}
:: by Noboru Endou
::
:: Received December 8, 2021
:: Copyright (c) 2021-2026 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;
equalities XCMPLX_0, LIMFUNC1, PROB_1, VALUED_1;
expansions MEMBERED;
theorems FUNCT_1, FUNCT_2, NAT_1, XBOOLE_0, XBOOLE_1, XXREAL_0, ORDINAL1,
XXREAL_3, XXREAL_1, XREAL_1, XREAL_0, VALUED_0, PARTFUN1, RELAT_1,
INTEGRA5, RFUNCT_1, VALUED_1, SEQ_2, ABSVALUE, RELSET_1, INTEGR10,
INTEGRA6, LIMFUNC1, RFUNCT_2, INTEGR24;
schemes FUNCT_2;
begin :: Properties of Extended Riemann Integral on Infinite Interval
theorem Th1:
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
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is divergent_in-infty_to+infty;
hereby assume f is convergent_in-infty; then
consider g be Real such that
A2: for g1 be Real st 0 < g1 ex r be Real st for r1 be Real st r1 < r &
r1 in dom f holds |. f.r1 - g .| < g1 by LIMFUNC1:45;
consider R1 be Real such that
A3: for r1 be Real st r1 < R1 & r1 in dom f holds |. f.r1 - g .| < 1 by A2;
consider R2 be Real such that
A4: for r1 be Real st r1 < R2 & r1 in dom f holds g+1 < f.r1
by A1,LIMFUNC1:48;
set R = min(R1,R2);
A5: R <= R1 & R <= R2 by XXREAL_0:17;
consider r be Real such that
A6: r < R & r in dom f by A1,LIMFUNC1:48;
A7: r < R1 by A5,A6,XXREAL_0:2;
r < R2 by A5,A6,XXREAL_0:2; then
A8: 1 < f.r - g by A4,A6,XREAL_1:20;
f.r - g <= |. f.r - g .| by ABSVALUE:4; then
1 < |. f.r - g .| by A8,XXREAL_0:2;
hence contradiction by A3,A6,A7;
end;
hereby assume f is divergent_in-infty_to-infty; then
consider R1 be Real such that
A9: for r1 be Real st r1 < R1 & r1 in dom f holds f.r1 < 0 by LIMFUNC1:49;
consider R2 be Real such that
A10: for r1 be Real st r1 < R2 & r1 in dom f holds 0 < f.r1 by A1,LIMFUNC1:48;
set R = min(R1,R2);
A11: R <= R1 & R <= R2 by XXREAL_0:17;
consider r be Real such that
A12: r < R & r in dom f by A1,LIMFUNC1:48;
A13: r < R1 & r < R2 by A11,A12,XXREAL_0:2; then
f.r > 0 by A10,A12;
hence contradiction by A9,A12,A13;
end;
end;
theorem Th2:
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
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is divergent_in-infty_to-infty;
hereby assume f is convergent_in-infty; then
consider g be Real such that
A2: for g1 be Real st 0 < g1 ex r be Real st for r1 be Real st r1 < r &
r1 in dom f holds |. f.r1 - g .| < g1 by LIMFUNC1:45;
consider R1 be Real such that
A3: for r1 be Real st r1 < R1 & r1 in dom f holds |. f.r1 - g .| < 1 by A2;
consider R2 be Real such that
A4: for r1 be Real st r1 < R2 & r1 in dom f holds g-1 > f.r1
by A1,LIMFUNC1:49;
set R = min(R1,R2);
A5: R <= R1 & R <= R2 by XXREAL_0:17;
consider r be Real such that
A6: r < R & r in dom f by A1,LIMFUNC1:49;
A7: r < R1 by A5,A6,XXREAL_0:2;
r < R2 by A5,A6,XXREAL_0:2; then
g-1 > f.r by A4,A6; then
A8: -1 > f.r - g by XREAL_1:19;
f.r - g >= -|. f.r - g .| by ABSVALUE:4; then
-1 > -|. f.r - g .| by A8,XXREAL_0:2;
hence contradiction by A3,A6,A7,XREAL_1:24;
end;
hereby assume f is divergent_in-infty_to+infty; then
consider R1 be Real such that
A9: for r1 be Real st r1 < R1 & r1 in dom f holds 0 < f.r1 by LIMFUNC1:48;
consider R2 be Real such that
A10: for r1 be Real st r1 < R2 & r1 in dom f holds f.r1 < 0 by A1,LIMFUNC1:49;
set R = min(R1,R2);
A11: R <= R1 & R <= R2 by XXREAL_0:17;
consider r be Real such that
A12: r < R & r in dom f by A1,LIMFUNC1:49;
A13: r < R1 & r < R2 by A11,A12,XXREAL_0:2; then
f.r < 0 by A10,A12;
hence contradiction by A9,A12,A13;
end;
end;
theorem Th3:
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
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is divergent_in+infty_to+infty;
hereby assume f is convergent_in+infty; then
consider g be Real such that
A2: for g1 be Real st 0 < g1 ex r be Real st for r1 be Real st r < r1 &
r1 in dom f holds |. f.r1 - g .| < g1 by LIMFUNC1:44;
consider R1 be Real such that
A3: for r1 be Real st R1 < r1 & r1 in dom f holds |. f.r1 - g .| < 1 by A2;
consider R2 be Real such that
A4: for r1 be Real st R2 < r1 & r1 in dom f holds g+1 < f.r1
by A1,LIMFUNC1:46;
set R = max(R1,R2);
A5: R >= R1 & R >= R2 by XXREAL_0:25;
consider r be Real such that
A6: r > R & r in dom f by A1,LIMFUNC1:46;
A7: r > R1 by A5,A6,XXREAL_0:2;
r > R2 by A5,A6,XXREAL_0:2; then
g+1 < f.r by A4,A6; then
A8: 1 < f.r - g by XREAL_1:20;
f.r - g <= |. f.r - g .| by ABSVALUE:4; then
1 < |. f.r - g .| by A8,XXREAL_0:2;
hence contradiction by A3,A6,A7;
end;
hereby assume f is divergent_in+infty_to-infty; then
consider R1 be Real such that
A9: for r1 be Real st r1 > R1 & r1 in dom f holds f.r1 < 0 by LIMFUNC1:47;
consider R2 be Real such that
A10: for r1 be Real st r1 > R2 & r1 in dom f holds 0 < f.r1 by A1,LIMFUNC1:46;
set R = max(R1,R2);
A11: R >= R1 & R >= R2 by XXREAL_0:25;
consider r be Real such that
A12: r > R & r in dom f by A1,LIMFUNC1:46;
A13: r > R1 & r > R2 by A11,A12,XXREAL_0:2; then
f.r > 0 by A10,A12;
hence contradiction by A9,A12,A13;
end;
end;
theorem Th4:
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
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is divergent_in+infty_to-infty;
hereby assume f is convergent_in+infty; then
consider g be Real such that
A2: for g1 be Real st 0 < g1 ex r be Real st for r1 be Real st r1 > r &
r1 in dom f holds |. f.r1 - g .| < g1 by LIMFUNC1:44;
consider R1 be Real such that
A3: for r1 be Real st r1 > R1 & r1 in dom f holds |. f.r1 - g .| < 1 by A2;
consider R2 be Real such that
A4: for r1 be Real st r1 > R2 & r1 in dom f holds g-1 > f.r1
by A1,LIMFUNC1:47;
set R = max(R1,R2);
A5: R >= R1 & R >= R2 by XXREAL_0:25;
consider r be Real such that
A6: r > R & r in dom f by A1,LIMFUNC1:47;
A7: r > R1 by A5,A6,XXREAL_0:2;
r > R2 by A5,A6,XXREAL_0:2; then
A8: -1 > f.r - g by A4,A6,XREAL_1:19;
f.r - g >= -|. f.r - g .| by ABSVALUE:4; then
-1 > -|. f.r - g .| by A8,XXREAL_0:2;
hence contradiction by A3,A6,A7,XREAL_1:24;
end;
hereby assume f is divergent_in+infty_to+infty; then
consider R1 be Real such that
A9: for r1 be Real st r1 > R1 & r1 in dom f holds 0 < f.r1 by LIMFUNC1:46;
consider R2 be Real such that
A10: for r1 be Real st r1 > R2 & r1 in dom f holds f.r1 < 0 by A1,LIMFUNC1:47;
set R = max(R1,R2);
A11: R >= R1 & R >= R2 by XXREAL_0:25;
consider r be Real such that
A12: r > R & r in dom f by A1,LIMFUNC1:47;
A13: r > R1 & r > R2 by A11,A12,XXREAL_0:2; then
f.r < 0 by A10,A12;
hence contradiction by A9,A12,A13;
end;
end;
theorem Th5:
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)
proof
let f be PartFunc of REAL,REAL;
assume f is convergent_in-infty; then
consider g be Real such that
A1: for g1 be Real st 0 < g1 ex r be Real st for r1 be Real st
r1<r & r1 in dom f holds |.f.r1-g.| < g1 by LIMFUNC1:45;
consider r be Real such that
A2: for r1 be Real st r1<r & r1 in dom f holds |.f.r1-g.| < 1 by A1;
for r1 be object st r1 in dom(f|left_open_halfline r)
holds -1+g < (f|left_open_halfline r).r1
proof
let r1 be object;
assume A3: r1 in dom(f|left_open_halfline r); then
reconsider r1 as Real;
r1 in dom f /\ left_open_halfline r by A3,RELAT_1:61; then
A4: r1 in dom f & r1 in left_open_halfline r by XBOOLE_0:def 4; then
|. f.r1 - g .| < 1 by A2,XXREAL_1:233; then
A5: -1 <= f.r1 - g by ABSVALUE:5;
now assume -1 = f.r1 - g; then
|. f.r1 - g .| = -(-1) by ABSVALUE:def 1;
hence contradiction by A2,A4,XXREAL_1:233;
end; then
-1 < f.r1-g by A5,XXREAL_0:1; then
-1+g < f.r1 by XREAL_1:20;
hence thesis by A4,FUNCT_1:49;
end; then
f|left_open_halfline r is bounded_below by SEQ_2:def 2;
hence ex r be Real st f|left_open_halfline r is bounded_below;
consider r be Real such that
A6: for r1 be Real st r1<r & r1 in dom f holds |.f.r1-g.| < 1 by A1;
for r1 be object st r1 in dom(f|left_open_halfline r)
holds (f|left_open_halfline r).r1 < g+1
proof
let r1 be object;
assume A7: r1 in dom(f|left_open_halfline r); then
reconsider r1 as Real;
r1 in dom f /\ left_open_halfline r by A7,RELAT_1:61; then
A8: r1 in dom f & r1 in left_open_halfline r by XBOOLE_0:def 4; then
|. f.r1 - g .| < 1 by A6,XXREAL_1:233; then
f.r1-g < 1 by ABSVALUE:def 1; then
f.r1 < g+1 by XREAL_1:19;
hence thesis by A8,FUNCT_1:49;
end; then
f|left_open_halfline r is bounded_above by SEQ_2:def 1;
hence ex r be Real st f|left_open_halfline r is bounded_above;
end;
theorem Th6:
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)
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is convergent_in+infty;
consider g be Real such that
A2: for g1 be Real st 0 < g1 ex r be Real st for r1 be Real st
r<r1 & r1 in dom f holds |.f.r1-g.| < g1 by A1,LIMFUNC1:44;
consider r be Real such that
A3: for r1 be Real st r<r1 & r1 in dom f holds |.f.r1-g.| < 1 by A2;
for r1 be object st r1 in dom(f|right_open_halfline r)
holds -1+g < (f|right_open_halfline r).r1
proof
let r1 be object;
assume A4: r1 in dom(f|right_open_halfline r); then
reconsider r1 as Real;
r1 in dom f /\ right_open_halfline r by A4,RELAT_1:61; then
A5: r1 in dom f & r1 in right_open_halfline r by XBOOLE_0:def 4; then
|. f.r1 - g .| < 1 by A3,XXREAL_1:235; then
A6: -1 <= f.r1 - g by ABSVALUE:5;
now assume -1 = f.r1 - g; then
|. f.r1 - g .| = -(-1) by ABSVALUE:def 1;
hence contradiction by A3,A5,XXREAL_1:235;
end; then
-1 < f.r1-g by A6,XXREAL_0:1; then
-1+g < f.r1 by XREAL_1:20;
hence thesis by A5,FUNCT_1:49;
end; then
f|right_open_halfline r is bounded_below by SEQ_2:def 2;
hence ex r be Real st f|right_open_halfline r is bounded_below;
consider r be Real such that
A7: for r1 be Real st r<r1 & r1 in dom f holds |.f.r1-g.| < 1 by A2;
for r1 be object st r1 in dom(f|right_open_halfline r)
holds (f|right_open_halfline r).r1 < g+1
proof
let r1 be object;
assume A8: r1 in dom(f|right_open_halfline r); then
reconsider r1 as Real;
r1 in dom f /\ right_open_halfline r by A8,RELAT_1:61; then
A9: r1 in dom f & r1 in right_open_halfline r by XBOOLE_0:def 4; then
|. f.r1 - g .| < 1 by A7,XXREAL_1:235; then
f.r1-g < 1 by ABSVALUE:def 1; then
f.r1 < g+1 by XREAL_1:19;
hence thesis by A9,FUNCT_1:49;
end; then
f|right_open_halfline r is bounded_above by SEQ_2:def 1;
hence ex r be Real st f|right_open_halfline r is bounded_above;
end;
theorem Th7:
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
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is divergent_in-infty_to+infty;
consider r be Real such that
A2: for r1 be Real st r1 < r & r1 in dom f holds 1 < f.r1
by A1,LIMFUNC1:48;
for r1 be object st r1 in dom(f|left_open_halfline r)
holds 1 < (f|left_open_halfline r).r1
proof
let r1 be object;
assume A3: r1 in dom(f|left_open_halfline r); then
reconsider r1 as Real;
r1 in dom f /\ left_open_halfline r by A3,RELAT_1:61; then
A4: r1 in dom f & r1 in left_open_halfline r by XBOOLE_0:def 4; then
r1 < r by XXREAL_1:4; then
1 < f.r1 by A2,A4;
hence thesis by A4,FUNCT_1:49;
end; then
f|left_open_halfline r is bounded_below by SEQ_2:def 2;
hence ex r be Real st f|left_open_halfline r is bounded_below;
end;
theorem Th8:
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
proof
let f be PartFunc of REAL,REAL;
assume
A1: f is divergent_in-infty_to-infty;
consider r be Real such that
A2: for r1 be Real st r1 < r & r1 in dom f holds f.r1 < 1
by A1,LIMFUNC1:49;
for r1 be object st r1 in dom(f|left_open_halfline r)
holds (f|left_open_halfline r).r1 < 1
proof
let r1 be object;
assume A3: r1 in dom(f|left_open_halfline r); then
reconsider r1 as Real;
r1 in dom f /\ left_open_halfline r by A3,RELAT_1:61; then
A4: r1 in dom f & r1 in left_open_halfline r by XBOOLE_0:def 4; then
r1 < r by XXREAL_1:4; then
f.r1 < 1 by A2,A4;
hence thesis by A4,FUNCT_1:49;
end; then
f|left_open_halfline r is bounded_above by SEQ_2:def 1;
hence ex r be Real st f|left_open_halfline r is bounded_above;
end;
theorem Th9:
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
proof
let f be PartFunc of REAL,REAL;
assume f is divergent_in+infty_to+infty; then
consider r be Real such that
A1: for r1 be Real st r < r1 & r1 in dom f holds 1 < f.r1 by LIMFUNC1:46;
for r1 be object st r1 in dom(f|right_open_halfline r)
holds 1 < (f|right_open_halfline r).r1
proof
let r1 be object;
assume A2: r1 in dom(f|right_open_halfline r); then
reconsider r1 as Real;
r1 in dom f /\ right_open_halfline r by A2,RELAT_1:61; then
A3: r1 in dom f & r1 in right_open_halfline r by XBOOLE_0:def 4; then
r < r1 by XXREAL_1:4; then
1 < f.r1 by A1,A3;
hence thesis by A3,FUNCT_1:49;
end; then
f|right_open_halfline r is bounded_below by SEQ_2:def 2;
hence ex r be Real st f|right_open_halfline r is bounded_below;
end;
theorem Th10:
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
proof
let f be PartFunc of REAL,REAL;
assume f is divergent_in+infty_to-infty; then
consider r be Real such that
A1: for r1 be Real st r < r1 & r1 in dom f holds f.r1 < 1 by LIMFUNC1:47;
for r1 be object st r1 in dom(f|right_open_halfline r)
holds (f|right_open_halfline r).r1 < 1
proof
let r1 be object;
assume A2: r1 in dom(f|right_open_halfline r); then
reconsider r1 as Real;
r1 in dom f /\ right_open_halfline r by A2,RELAT_1:61; then
A3: r1 in dom f & r1 in right_open_halfline r by XBOOLE_0:def 4; then
r < r1 by XXREAL_1:4; then
f.r1 < 1 by A1,A3;
hence thesis by A3,FUNCT_1:49;
end; then
f|right_open_halfline r is bounded_above by SEQ_2:def 1;
hence ex r be Real st f|right_open_halfline r is bounded_above;
end;
Lm1:
for seq be Real_Sequence, f1,f2 be PartFunc of REAL,REAL st
rng seq c=dom(f1+f2) holds dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1
& rng seq c=dom f2
proof
let seq be Real_Sequence, f1,f2 be PartFunc of REAL,REAL;
assume
A1: rng seq c=dom(f1+f2);
thus dom(f1+f2)=dom f1/\dom f2 by VALUED_1:def 1;
then dom(f1+f2)c=dom f1 & dom(f1+f2)c=dom f2 by XBOOLE_1:17;
hence thesis by A1;
end;
theorem Th11:
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<r & g in dom(f1+f2))
& (ex r be Real st f2|left_open_halfline r is bounded_above)
holds f1+f2 is divergent_in-infty_to-infty
proof
let f1,f2 be PartFunc of REAL,REAL;
assume that
A1: f1 is divergent_in-infty_to-infty and
A2: for r be Real ex g be Real st g<r & g in dom(f1+f2);
given r1 be Real such that
A3: f2|left_open_halfline r1 is bounded_above;
now
let seq be Real_Sequence;
assume that
A4: seq is divergent_to-infty and
A5: rng seq c=dom(f1+f2);
consider k be Nat such that
A6: for n be Nat st k<=n holds seq.n<r1 by A4,LIMFUNC1:def 5;
A7: rng(seq^\k)c=rng seq by VALUED_0:21;
dom(f1+f2)=dom f1/\dom f2 by A5,Lm1;
then rng(seq^\k)c=dom f1/\dom f2 by A5,A7;
then
A8: f1/*(seq^\k)+f2/*(seq^\k)=(f1+f2)/*(seq^\k) by RFUNCT_2:8
.=((f1+f2)/*seq)^\k by A5,VALUED_0:27;
consider r2 be Real such that
A9: for g being object st g in left_open_halfline(r1)/\dom f2 holds r2>=
f2.g by A3,RFUNCT_1:70;
A10: rng seq c=dom f2 by A5,Lm1;
then
A11: rng(seq^\k)c=dom f2 by A7;
now
let n be Nat;
A12: n in NAT by ORDINAL1:def 12;
seq.(n+k)<r1 by A6,NAT_1:12;
then (seq^\k).n<r1 by NAT_1:def 3;
then (seq^\k).n in {g2 where g2 is Real: g2<r1};
then
(seq^\k).n in rng(seq^\k) & (seq^\k).n in left_open_halfline(r1) by
VALUED_0:28,XXREAL_1:229;
then (seq^\k).n in left_open_halfline(r1)/\dom f2 by A11,XBOOLE_0:def 4;
then r2>=f2.((seq^\k).n) by A9;
then
A13: r2>=(f2/*(seq^\k)).n by A10,A7,FUNCT_2:108,XBOOLE_1:1,A12;
r2 <= |.r2.| & |.r2.| < |.r2.| + 1 by ABSVALUE:4,XREAL_1:29; then
r2 < |.r2.|+1 by XXREAL_0:2;
hence |.r2.|+1>(f2/*(seq^\k)).n by A13,XXREAL_0:2;
end;
then
A14: f2/*(seq^\k) is bounded_above by SEQ_2:def 3;
rng seq c=dom f1 by A5,Lm1;
then
A15: rng(seq^\k)c=dom f1 by A7;
seq^\k is divergent_to-infty by A4,LIMFUNC1:27;
then f1/*(seq^\k)+f2/*(seq^\k) is divergent_to-infty
by A1,A14,A15,LIMFUNC1:def 11,12;
hence (f1+f2)/*seq is divergent_to-infty by A8,LIMFUNC1:7;
end;
hence thesis by A2,LIMFUNC1:def 11;
end;
theorem Th12:
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 r<g & g in dom(f1+f2))
& (ex r be Real st f2|right_open_halfline r is bounded_above)
holds f1+f2 is divergent_in+infty_to-infty
proof
let f1,f2 be PartFunc of REAL,REAL;
assume that
A1: f1 is divergent_in+infty_to-infty and
A2: for r be Real ex g be Real st r<g & g in dom(f1+f2);
given r1 be Real such that
A3: f2|right_open_halfline r1 is bounded_above;
now
let seq be Real_Sequence;
assume that
A4: seq is divergent_to+infty and
A5: rng seq c=dom(f1+f2);
consider k be Nat such that
A6: for n be Nat st k<=n holds r1<seq.n by A4,LIMFUNC1:def 4;
A7: rng(seq^\k)c=rng seq by VALUED_0:21;
dom(f1+f2)=dom f1/\dom f2 by A5,Lm1;
then rng(seq^\k)c=dom f1/\dom f2 by A5,A7;
then
A8: f1/*(seq^\k)+f2/*(seq^\k)=(f1+f2)/*(seq^\k) by RFUNCT_2:8
.=((f1+f2)/*seq)^\k by A5,VALUED_0:27;
consider r2 be Real such that
A9: for g being object st g in right_open_halfline(r1)/\dom f2 holds r2
>=f2.g by A3,RFUNCT_1:70;
A10: rng seq c=dom f2 by A5,Lm1;
then
A11: rng(seq^\k)c=dom f2 by A7;
now
let n be Nat;
A12: n in NAT by ORDINAL1:def 12;
reconsider nk = n+k, nn=n as Element of NAT by ORDINAL1:def 12;
r1<seq.(nk) by A6,NAT_1:12;
then (seq^\k).nn < +infty & r1<(seq^\k).nn
by NAT_1:def 3,XXREAL_0:9;
then (seq^\k).n in rng(seq^\k) & (seq^\k).n in right_open_halfline(r1)
by VALUED_0:28,XXREAL_1:4;
then (seq^\k).n in right_open_halfline(r1)/\dom f2 by A11,XBOOLE_0:def 4;
then r2>=f2.((seq^\k).n) by A9;
then
A13: r2>=(f2/*(seq^\k)).n by A10,A7,FUNCT_2:108,XBOOLE_1:1,A12;
r2 <= |.r2.| & |.r2.| < |.r2.| + 1 by ABSVALUE:4,XREAL_1:29; then
r2 < |.r2.|+1 by XXREAL_0:2;
hence |.r2.|+1>(f2/*(seq^\k)).n by A13,XXREAL_0:2;
end;
then
A14: f2/*(seq^\k) is bounded_above by SEQ_2:def 3;
rng seq c=dom f1 by A5,Lm1;
then
A15: rng(seq^\k)c=dom f1 by A7;
seq^\k is divergent_to+infty by A4,LIMFUNC1:26;
then f1/*(seq^\k)+f2/*(seq^\k) is divergent_to-infty
by A1,A14,A15,LIMFUNC1:def 8,12;
hence (f1+f2)/*seq is divergent_to-infty by A8,LIMFUNC1:7;
end;
hence thesis by A2,LIMFUNC1:def 8;
end;
theorem
for f be PartFunc of REAL,REAL, d be Real st
left_closed_halfline(d) c= dom f & f is_-infty_ext_Riemann_integrable_on d
holds for b,c be Real st b < c <= d holds
f is_right_ext_Riemann_integrable_on b,c
& f is_left_ext_Riemann_integrable_on b,c
proof
let f be PartFunc of REAL,REAL, d be Real;
assume that
A1: left_closed_halfline(d) c= dom f and
A2: f is_-infty_ext_Riemann_integrable_on d;
hereby let b,c be Real;
assume A3: b < c <= d; then
b < d by XXREAL_0:2; then
A4: f is_integrable_on ['b,d'] & f|['b,d'] is bounded by A2,INTEGR10:def 6;
['b,d'] = [.b,d.] by A3,XXREAL_0:2,INTEGRA5:def 3; then
['b,d'] c= ].-infty,d.] by XXREAL_1:265; then
['b,d'] c= dom f by A1; then
f is_integrable_on ['b,c'] & f|['b,c'] is bounded & ['b,c'] c= dom f
by A3,A4,INTEGRA6:18;
hence f is_right_ext_Riemann_integrable_on b,c &
f is_left_ext_Riemann_integrable_on b,c by A3,INTEGR24:19,18;
end;
end;
theorem
for f be PartFunc of REAL,REAL, a be Real st
right_closed_halfline(a) c= dom f & f is_+infty_ext_Riemann_integrable_on a
holds for b,c be Real st a <= b < c holds
f is_right_ext_Riemann_integrable_on b,c
& f is_left_ext_Riemann_integrable_on b,c
proof
let f be PartFunc of REAL,REAL, a be Real;
assume that
A1: right_closed_halfline(a) c= dom f and
A2: f is_+infty_ext_Riemann_integrable_on a;
hereby let b,c be Real;
assume A3: a <= b < c; then
a < c by XXREAL_0:2; then
A4: f is_integrable_on ['a,c'] & f|['a,c'] is bounded by A2,INTEGR10:def 5;
['a,c'] = [.a,c.] by A3,XXREAL_0:2,INTEGRA5:def 3; then
['a,c'] c= [.a,+infty.[ by XXREAL_1:251; then
['a,c'] c= dom f by A1; then
f is_integrable_on ['b,c'] & f|['b,c'] is bounded & ['b,c'] c= dom f
by A3,A4,INTEGRA6:18;
hence f is_right_ext_Riemann_integrable_on b,c &
f is_left_ext_Riemann_integrable_on b,c by A3,INTEGR24:19,18;
end;
end;
theorem Th15:
for f be PartFunc of REAL,REAL, a be Real
st left_closed_halfline(a) c= dom f & f is_-infty_ext_Riemann_integrable_on a
holds for b be Real st b <= a holds f is_-infty_ext_Riemann_integrable_on b
proof
let f be PartFunc of REAL,REAL, a be Real;
assume that
A1: left_closed_halfline(a) c= dom f and
A2: f is_-infty_ext_Riemann_integrable_on a;
hereby let b be Real;
assume A3: b <= a;
A4: for c be Real st c <= b holds
f is_integrable_on ['c,b'] & f|['c,b'] is bounded
proof
let c be Real;
assume A5: c <= b; then
c <= a by A3,XXREAL_0:2; then
A6: f is_integrable_on ['c,a'] & f|['c,a'] is bounded by A2,INTEGR10:def 6;
['c,a'] = [.c,a.] by A5,A3,XXREAL_0:2,INTEGRA5:def 3; then
['c,a'] c= ].-infty,a.] by XXREAL_1:265; then
['c,a'] c= dom f by A1;
hence thesis by A3,A5,A6,INTEGRA6:18;
end;
consider I be PartFunc of REAL,REAL such that
A7: dom I = left_closed_halfline(a) and
A8: for x be Real st x in dom I holds I.x = integral(f,x,a) and
A9: I is convergent_in-infty by A2,INTEGR10:def 6;
-infty < b by XREAL_0:def 1,XXREAL_0:12; then
reconsider B = ].-infty,b.] as non empty Subset of REAL by XXREAL_1:2;
deffunc F(Element of B) = In(integral(f,$1,b),REAL);
consider Intf be Function of B, REAL such that
A10: for x being Element of B holds Intf.x = F(x) from FUNCT_2:sch 4;
A11: dom Intf = B by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A12: dom Intf = left_closed_halfline(b) by FUNCT_2:def 1;
A13: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,x,b),REAL) by A10,A11;
hence Intf.x = integral(f,x,b);
end;
A14: for r be Real ex g be Real st g<r & g in dom Intf
proof
let r be Real;
consider g be Real such that
A15: g < min(b,r) by XREAL_1:2;
A16: -infty < g by XREAL_0:def 1,XXREAL_0:12;
r >= min(b,r) & b >= min(b,r) by XXREAL_0:17; then
A17: g < r & g < b by A15,XXREAL_0:2; then
g in ].-infty,b.] by A16,XXREAL_1:2;
hence thesis by A11,A17;
end;
consider G be Real such that
A18: for g1 be Real st 0<g1
ex r be Real st
for r1 be Real st r1<r & r1 in dom I holds |. I.r1-G .| < g1
by A9,LIMFUNC1:45;
set G1=G-integral(f,b,a);
for g1 be Real st 0<g1
ex r be Real st
for r1 be Real st r1<r & r1 in dom Intf holds
|. Intf.r1 - G1 .| < g1
proof
let g1 be Real;
assume 0 < g1; then
consider R be Real such that
A19: for r1 be Real st r1 < R & r1 in dom I holds |. I.r1-G .| < g1
by A18;
take R;
thus for r1 be Real st r1<R & r1 in dom Intf holds
|. Intf.r1 - G1 .| < g1
proof
let r1 be Real;
assume that
A20: r1 < R and
A21: r1 in dom Intf;
A22: ].-infty,b.] c= ].-infty,a.] by A3,XXREAL_1:42;
A23: r1 <= b by A21,A11,XXREAL_1:2; then
A24: r1 <= a by A3,XXREAL_0:2; then
A25: f is_integrable_on ['r1,a'] & f|['r1,a'] is bounded
by A2,INTEGR10:def 6;
A26: ['r1,a'] = [.r1,a.] by A23,A3,XXREAL_0:2,INTEGRA5:def 3; then
['r1,a'] c= ].-infty,a.] by XXREAL_1:265; then
A27: ['r1,a'] c= dom f by A1;
A28: b in ['r1,a'] by A3,A23,A26,XXREAL_1:1;
A29: integral(f,r1,b) + integral(f,b,a) = integral(f,r1,a)
by A24,A25,A27,A28,INTEGRA6:17;
Intf.r1 - G1 = integral(f,r1,b) - (G - integral(f,b,a)) by A13,A21; then
Intf.r1 - G1 = integral(f,r1,a) - G by A29; then
Intf.r1 - G1 = I.r1 - G by A22,A21,A11,A7,A8;
hence thesis by A19,A20,A22,A21,A11,A7;
end;
end;
hence f is_-infty_ext_Riemann_integrable_on b
by A4,A12,A13,A14,INTEGR10:def 6,LIMFUNC1:45;
end;
end;
theorem Th16:
for f be PartFunc of REAL,REAL, a be Real
st right_closed_halfline(a) c= dom f & f is_+infty_ext_Riemann_integrable_on a
holds for b be Real st a <= b holds f is_+infty_ext_Riemann_integrable_on b
proof
let f be PartFunc of REAL,REAL, a be Real;
assume that
A1: right_closed_halfline(a) c= dom f and
A2: f is_+infty_ext_Riemann_integrable_on a;
hereby let b be Real;
assume A3: a <= b;
A4: for c be Real st b <= c holds
f is_integrable_on ['b,c'] & f|['b,c'] is bounded
proof
let c be Real;
assume A5: b <= c; then
a <= c by A3,XXREAL_0:2; then
A6: f is_integrable_on ['a,c'] & f|['a,c'] is bounded by A2,INTEGR10:def 5;
['a,c'] = [.a,c.] by A5,A3,XXREAL_0:2,INTEGRA5:def 3; then
['a,c'] c= [.a,+infty.[ by XXREAL_1:251; then
['a,c'] c= dom f by A1;
hence thesis by A3,A5,A6,INTEGRA6:18;
end;
consider I be PartFunc of REAL,REAL such that
A7: dom I = right_closed_halfline(a) and
A8: for x be Real st x in dom I holds I.x = integral(f,a,x) and
A9: I is convergent_in+infty by A2,INTEGR10:def 5;
b < +infty by XREAL_0:def 1,XXREAL_0:9; then
reconsider B = [.b,+infty.[ as non empty Subset of REAL
by XXREAL_1:3;
deffunc F(Element of B) = In(integral(f,b,$1),REAL);
consider Intf be Function of B, REAL such that
A10: for x being Element of B holds Intf.x = F(x) from FUNCT_2:sch 4;
A11: dom Intf = B by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A12: dom Intf = right_closed_halfline(b) by FUNCT_2:def 1;
A13: for x be Real st x in dom Intf holds Intf.x = integral(f,b,x)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,b,x),REAL) by A10,A11;
hence Intf.x = integral(f,b,x);
end;
A14: for r be Real ex g be Real st r<g & g in dom Intf
proof
let r be Real;
consider g be Real such that
A15: max(b,r) < g by XREAL_1:1;
A16: g < +infty by XXREAL_0:9,XREAL_0:def 1;
r <= max(b,r) & b <= max(b,r) by XXREAL_0:25; then
A17: r < g & b < g by A15,XXREAL_0:2; then
g in [.b,+infty.[ by A16,XXREAL_1:3;
hence thesis by A11,A17;
end;
consider G be Real such that
A18: for g1 be Real st 0<g1
ex r be Real st
for r1 be Real st r<r1 & r1 in dom I holds |. I.r1-G .| < g1
by A9,LIMFUNC1:44;
set G1=G-integral(f,a,b);
for g1 be Real st 0<g1
ex r be Real st
for r1 be Real st r<r1 & r1 in dom Intf holds
|. Intf.r1 - G1 .| < g1
proof
let g1 be Real;
assume 0 < g1; then
consider R be Real such that
A19: for r1 be Real st R < r1 & r1 in dom I holds |. I.r1-G .| < g1
by A18;
take R;
thus for r1 be Real st R<r1 & r1 in dom Intf holds
|. Intf.r1 - G1 .| < g1
proof
let r1 be Real;
assume that
A20: R < r1 and
A21: r1 in dom Intf;
A22: [.b,+infty.[ c= [.a,+infty.[ by A3,XXREAL_1:38;
A23: b <= r1 by A21,A11,XXREAL_1:3; then
A24: a <= r1 by A3,XXREAL_0:2; then
A25: f is_integrable_on ['a,r1'] & f|['a,r1'] is bounded
by A2,INTEGR10:def 5;
A26: ['a,r1'] = [.a,r1.] by A23,A3,XXREAL_0:2,INTEGRA5:def 3; then
['a,r1'] c= [.a,+infty.[ by XXREAL_1:251; then
A27: ['a,r1'] c= dom f by A1;
A28: b in ['a,r1'] by A3,A23,A26,XXREAL_1:1;
A29: integral(f,a,b) + integral(f,b,r1) = integral(f,a,r1)
by A24,A25,A27,A28,INTEGRA6:17;
Intf.r1 - G1 = integral(f,b,r1) - (G - integral(f,a,b)) by A13,A21; then
Intf.r1 - G1 = integral(f,a,r1) - G by A29; then
Intf.r1 - G1 = I.r1 - G by A22,A21,A11,A7,A8;
hence thesis by A19,A20,A22,A21,A11,A7;
end;
end;
hence f is_+infty_ext_Riemann_integrable_on b
by A4,A12,A13,A14,LIMFUNC1:44,INTEGR10:def 5;
end;
end;
theorem Th17:
for f be PartFunc of REAL,REAL, a,b be Real st a <= b
& left_closed_halfline(b) c= dom f & f is_integrable_on ['a,b']
& f|['a,b'] is bounded & f is_-infty_ext_Riemann_integrable_on a
holds f is_-infty_ext_Riemann_integrable_on b
& infty_ext_left_integral(f,b) = infty_ext_left_integral(f,a) + integral(f,a,b)
proof
let f be PartFunc of REAL,REAL, a,b be Real;
assume that
A1: a <= b and
A2: left_closed_halfline(b) c= dom f and
A3: f is_integrable_on ['a,b'] and
A4: f|['a,b'] is bounded and
A5: f is_-infty_ext_Riemann_integrable_on a;
A6: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
A7: for c be Real st c <= b holds
f is_integrable_on ['c,b'] & f|['c,b'] is bounded
proof
let c be Real;
assume A8: c <= b; then
A9: ['c,b'] = [.c,b.] by INTEGRA5:def 3;
per cases;
suppose A10: a <= c;
['a,b'] c= ].-infty,b.] by A6,XXREAL_1:265; then
A11: ['a,b'] c= dom f by A2;
c in ['a,b'] by A8,A10,A6,XXREAL_1:1;
hence f is_integrable_on ['c,b'] by A1,A3,A4,A11,INTEGRA6:17;
thus f|['c,b'] is bounded by A4,A6,A9,A10,XXREAL_1:34,RFUNCT_1:74;
end;
suppose A12: c < a; then
A13: f is_integrable_on ['c,a'] & f|['c,a'] is bounded by A5,INTEGR10:def 6;
['c,b'] c= ].-infty,b.] by A9,XXREAL_1:265; then
['c,b'] c= dom f by A2;
hence f is_integrable_on ['c,b'] by A1,A12,A4,A13,A3,INTEGR24:1;
['c,a'] = [.c,a.] by A12,INTEGRA5:def 3; then
['c,b'] = ['c,a'] \/ ['a,b'] by A1,A6,A9,A12,XXREAL_1:165;
hence f|['c,b'] is bounded by A4,A13,RFUNCT_1:87;
end;
end;
consider I be PartFunc of REAL,REAL such that
A14: dom I = left_closed_halfline(a) and
A15: for x be Real st x in dom I holds I.x = integral(f,x,a) and
A16: I is convergent_in-infty by A5,INTEGR10:def 6;
b > -infty by XREAL_0:def 1,XXREAL_0:12; then
reconsider B = ].-infty,b.] as non empty Subset of REAL
by XXREAL_1:2;
deffunc F(Element of B) = In(integral(f,$1,b),REAL);
consider Intf be Function of B, REAL such that
A17: for x being Element of B holds Intf.x = F(x) from FUNCT_2:sch 4;
A18:dom Intf = B by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A19: dom Intf = left_closed_halfline(b) by FUNCT_2:def 1;
A20: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,x,b),REAL) by A17,A18;
hence Intf.x = integral(f,x,b);
end;
A21: for r be Real ex g be Real st g<r & g in dom Intf
proof
let r be Real;
consider g be Real such that
A22: g < min(b,r) by XREAL_1:2;
A23: -infty < g by XREAL_0:def 1,XXREAL_0:12;
min(b,r) <= r & min(b,r) <= b by XXREAL_0:17; then
A24: g < r & g < b by A22,XXREAL_0:2; then
g in ].-infty,b.] by A23,XXREAL_1:2;
hence thesis by A18,A24;
end;
consider G be Real such that
A25: for g1 be Real st 0<g1
ex r be Real st
for r1 be Real st r1<r & r1 in dom I holds |. I.r1-G .| < g1
by A16,LIMFUNC1:45;
G = lim_in-infty I by A25,A16,LIMFUNC1:78; then
A26: G = infty_ext_left_integral(f,a) by A5,A14,A15,A16,INTEGR10:def 8;
set G1=G+integral(f,a,b);
A27:for g1 be Real st 0<g1
ex r be Real st
for r1 be Real st r1<r & r1 in dom Intf holds
|. Intf.r1 - G1 .| < g1
proof
let g1 be Real;
assume 0 < g1; then
consider R be Real such that
A28: for r1 be Real st r1< R & r1 in dom I holds |. I.r1-G .| < g1
by A25;
set R1=min(R,a);
take R1;
thus for r1 be Real st r1<R1 & r1 in dom Intf holds
|. Intf.r1 - G1 .| < g1
proof
let r1 be Real;
assume that
A29: r1 < R1 and
A30: r1 in dom Intf;
A31: R1 <= R & R1 <= a by XXREAL_0:17; then
A32: r1 < a & r1 < R by A29,XXREAL_0:2;
A33: r1 in dom I by A14,A31,A29,XXREAL_0:2,XXREAL_1:234;
A34: r1 <= b by A1,A32,XXREAL_0:2; then
A35: f is_integrable_on ['r1,b'] & f|['r1,b'] is bounded by A7;
A36: ['r1,b'] = [.r1,b.] by A1,A32,XXREAL_0:2,INTEGRA5:def 3; then
['r1,b'] c= ].-infty,b.] by XXREAL_1:265; then
A37: ['r1,b'] c= dom f by A2;
a in ['r1,b'] by A1,A32,A36,XXREAL_1:1; then
A38: integral(f,a,b) + integral(f,r1,a) = integral(f,r1,b)
by A34,A35,A37,INTEGRA6:17;
Intf.r1 - G1 = integral(f,r1,b) - (G + integral(f,a,b)) by A20,A30; then
Intf.r1 - G1 = integral(f,r1,a) - G by A38; then
Intf.r1 - G1 = I.r1 - G by A32,A15,A14,XXREAL_1:234;
hence thesis by A28,A33,A32;
end;
end;
hence
A39: f is_-infty_ext_Riemann_integrable_on b
by A7,A19,A20,A21,LIMFUNC1:45,INTEGR10:def 6;
A40:Intf is convergent_in-infty by A21,A27,LIMFUNC1:45; then
infty_ext_left_integral(f,b) = lim_in-infty Intf
by A19,A20,A39,INTEGR10:def 8;
hence infty_ext_left_integral(f,b)
= infty_ext_left_integral(f,a) + integral(f,a,b)
by A40,A26,A27,LIMFUNC1:78;
end;
theorem Th18:
for f be PartFunc of REAL,REAL, a,b be Real st a <= b
& right_closed_halfline a c= dom f & f is_integrable_on ['a,b']
& f|['a,b'] is bounded & f is_+infty_ext_Riemann_integrable_on b
holds f is_+infty_ext_Riemann_integrable_on a
& infty_ext_right_integral(f,a)
= infty_ext_right_integral(f,b) + integral(f,a,b)
proof
let f be PartFunc of REAL,REAL, a,b be Real;
assume that
A1: a <= b and
A2: right_closed_halfline(a) c= dom f and
A3: f is_integrable_on ['a,b'] and
A4: f|['a,b'] is bounded and
A5: f is_+infty_ext_Riemann_integrable_on b;
A6: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
A7: for c be Real st a <= c holds
f is_integrable_on ['a,c'] & f|['a,c'] is bounded
proof
let c be Real;
assume A8: a <= c; then
A9: ['a,c'] = [.a,c.] by INTEGRA5:def 3;
per cases;
suppose A10: c <= b;
['a,b'] c= [.a,+infty.[ by A6,XXREAL_1:251; then
A11: ['a,b'] c= dom f by A2;
c in ['a,b'] by A8,A10,A6,XXREAL_1:1;
hence f is_integrable_on ['a,c'] by A1,A3,A4,A11,INTEGRA6:17;
thus f|['a,c'] is bounded by A4,A6,A9,A10,XXREAL_1:34,RFUNCT_1:74;
end;
suppose A12: b < c; then
A13: f is_integrable_on ['b,c'] & f|['b,c'] is bounded by A5,INTEGR10:def 5;
['a,c'] c= [.a,+infty.[ by A9,XXREAL_1:251; then
['a,c'] c= dom f by A2;
hence f is_integrable_on ['a,c'] by A1,A12,A4,A13,A3,INTEGR24:1;
['b,c'] = [.b,c.] by A12,INTEGRA5:def 3; then
['a,c'] = ['a,b'] \/ ['b,c'] by A1,A6,A9,A12,XXREAL_1:165;
hence f|['a,c'] is bounded by A4,A13,RFUNCT_1:87;
end;
end;
consider I be PartFunc of REAL,REAL such that
A14: dom I = right_closed_halfline(b) and
A15: for x be Real st x in dom I holds I.x = integral(f,b,x) and
A16: I is convergent_in+infty by A5,INTEGR10:def 5;
a < +infty by XREAL_0:def 1,XXREAL_0:9; then
reconsider A = [.a,+infty.[ as non empty Subset of REAL
by XXREAL_1:3;
deffunc F(Element of A) = In(integral(f,a,$1),REAL);
consider Intf be Function of A, REAL such that
A17: for x being Element of A holds Intf.x = F(x) from FUNCT_2:sch 4;
A18:dom Intf = A by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A19: dom Intf = right_closed_halfline(a) by FUNCT_2:def 1;
A20: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,a,x),REAL) by A17,A18;
hence Intf.x = integral(f,a,x);
end;
A21: for r be Real ex g be Real st r<g & g in dom Intf
proof
let r be Real;
consider g be Real such that
A22: max(a,r) < g by XREAL_1:1;
A23: g < +infty by XREAL_0:def 1,XXREAL_0:9;
r <= max(a,r) & a <= max(a,r) by XXREAL_0:25; then
A24: r < g & a < g by A22,XXREAL_0:2; then
g in [.a,+infty.[ by A23,XXREAL_1:3;
hence thesis by A18,A24;
end;
consider G be Real such that
A25: for g1 be Real st 0<g1
ex r be Real st
for r1 be Real st r<r1 & r1 in dom I holds |. I.r1-G .| < g1
by A16,LIMFUNC1:44;
G = lim_in+infty I by A25,A16,LIMFUNC1:79; then
A26: G = infty_ext_right_integral(f,b) by A5,A14,A15,A16,INTEGR10:def 7;
set G1=G+integral(f,a,b);
A27:for g1 be Real st 0<g1
ex r be Real st
for r1 be Real st r<r1 & r1 in dom Intf holds
|. Intf.r1 - G1 .| < g1
proof
let g1 be Real;
assume 0 < g1; then
consider R be Real such that
A28: for r1 be Real st R < r1 & r1 in dom I holds |. I.r1-G .| < g1
by A25;
set R1=max(R,b);
take R1;
thus for r1 be Real st R1<r1 & r1 in dom Intf holds
|. Intf.r1 - G1 .| < g1
proof
let r1 be Real;
assume that
A29: R1 < r1 and
A30: r1 in dom Intf;
A31: b <= R1 & R <= R1 by XXREAL_0:25; then
A32: b < r1 & R < r1 by A29,XXREAL_0:2;
A33: r1 in dom I by A14,A31,A29,XXREAL_0:2,XXREAL_1:236;
A34: a <= r1 by A1,A32,XXREAL_0:2; then
A35: f is_integrable_on ['a,r1'] & f|['a,r1'] is bounded by A7;
A36: ['a,r1'] = [.a,r1.] by A1,A32,XXREAL_0:2,INTEGRA5:def 3; then
['a,r1'] c= [.a,+infty.[ by XXREAL_1:251; then
A37: ['a,r1'] c= dom f by A2;
A38: b in ['a,r1'] by A1,A32,A36,XXREAL_1:1;
A39: integral(f,a,b) + integral(f,b,r1) = integral(f,a,r1)
by A34,A35,A37,A38,INTEGRA6:17;
Intf.r1 - G1 = integral(f,a,r1) - (G + integral(f,a,b)) by A20,A30; then
Intf.r1 - G1 = integral(f,b,r1) - G by A39; then
Intf.r1 - G1 = I.r1 - G by A32,A15,A14,XXREAL_1:236;
hence thesis by A28,A33,A32;
end;
end;
hence
A40: f is_+infty_ext_Riemann_integrable_on a
by A7,A19,A20,A21,LIMFUNC1:44,INTEGR10:def 5;
A41: Intf is convergent_in+infty by A21,A27,LIMFUNC1:44; then
infty_ext_right_integral(f,a) = lim_in+infty Intf
by A19,A20,A40,INTEGR10:def 7;
hence infty_ext_right_integral(f,a)
= infty_ext_right_integral(f,b) + integral(f,a,b)
by A41,A26,A27,LIMFUNC1:79;
end;
theorem
for f be PartFunc of REAL,REAL st dom f = REAL holds
f is infty_ext_Riemann_integrable iff
for a be Real holds f is_+infty_ext_Riemann_integrable_on a
& f is_-infty_ext_Riemann_integrable_on a
proof
let f be PartFunc of REAL,REAL;
assume A1: dom f = REAL;
hereby assume
A2: f is infty_ext_Riemann_integrable; then
A3: f is_+infty_ext_Riemann_integrable_on 0
& f is_-infty_ext_Riemann_integrable_on 0 by INTEGR10:def 9;
thus for a be Real holds f is_+infty_ext_Riemann_integrable_on a
& f is_-infty_ext_Riemann_integrable_on a
proof
let a be Real;
per cases;
suppose A4: 0 <= a;
right_closed_halfline(0) c= dom f by A1;
hence f is_+infty_ext_Riemann_integrable_on a
by A2,A4,Th16,INTEGR10:def 9;
A5: left_closed_halfline(a) c= dom f by A1;
f is_integrable_on ['0,a'] & f|['0,a'] is bounded
by A3,A4,INTEGR10:def 5;
hence f is_-infty_ext_Riemann_integrable_on a by A3,A4,A5,Th17;
end;
suppose A6: a < 0;
A7: right_closed_halfline(a) c= dom f by A1;
f is_integrable_on ['a,0'] & f|['a,0'] is bounded
by A3,A6,INTEGR10:def 6;
hence f is_+infty_ext_Riemann_integrable_on a by A3,A6,A7,Th18;
left_closed_halfline(0) c= dom f by A1;
hence f is_-infty_ext_Riemann_integrable_on a
by A2,A6,Th15,INTEGR10:def 9;
end;
end;
end;
assume for a be Real holds f is_+infty_ext_Riemann_integrable_on a
& f is_-infty_ext_Riemann_integrable_on a; then
f is_+infty_ext_Riemann_integrable_on 0 &
f is_-infty_ext_Riemann_integrable_on 0;
hence f is infty_ext_Riemann_integrable by INTEGR10:def 9;
end;
begin :: Improper Integral on Infinite Inteval
definition
let f be PartFunc of REAL,REAL;
let b be Real;
pred f is_-infty_improper_integrable_on b means
(for a be Real st
a <= b holds f is_integrable_on [' a,b '] & f|[' a,b '] is bounded) &
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
or Intf is divergent_in-infty_to+infty
or Intf is divergent_in-infty_to-infty);
end;
definition
let f be PartFunc of REAL,REAL;
let a be Real;
pred f is_+infty_improper_integrable_on a means
(for b be Real st
a <= b holds f is_integrable_on [' a,b '] & f|[' a,b '] is bounded) &
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
or Intf is divergent_in+infty_to+infty
or Intf is divergent_in+infty_to-infty);
end;
definition
let f be PartFunc of REAL,REAL;
let b be Real;
assume
A1: f is_-infty_improper_integrable_on b;
func improper_integral_-infty(f,b) -> ExtReal means
:Def3:
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);
existence
proof
consider Intf be PartFunc of REAL,REAL such that
A2: dom Intf = left_closed_halfline b and
A3: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
A4: Intf is convergent_in-infty or Intf is divergent_in-infty_to+infty
or Intf is divergent_in-infty_to-infty by A1;
per cases by A4;
suppose A5: Intf is convergent_in-infty;
reconsider IT = lim_in-infty Intf as ExtReal;
take IT;
thus thesis by A2,A3,A5;
end;
suppose A6: Intf is divergent_in-infty_to+infty;
take +infty;
thus thesis by A2,A3,A6;
end;
suppose A7: Intf is divergent_in-infty_to-infty;
take -infty;
thus thesis by A2,A3,A7;
end;
end;
uniqueness
proof
let y1,y2 be ExtReal;
assume that
A8: 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 & y1 = lim_in-infty Intf
or Intf is divergent_in-infty_to+infty & y1 = +infty
or Intf is divergent_in-infty_to-infty & y1 = -infty) and
A9: 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 & y2 = lim_in-infty Intf
or Intf is divergent_in-infty_to+infty & y2 = +infty
or Intf is divergent_in-infty_to-infty & y2 = -infty);
consider I1 be PartFunc of REAL,REAL such that
A10: dom I1 = left_closed_halfline b and
A11: for x be Real st x in dom I1 holds I1.x = integral(f,x,b) and
A12: (I1 is convergent_in-infty & y1 = lim_in-infty I1)
or (I1 is divergent_in-infty_to+infty & y1 = +infty)
or (I1 is divergent_in-infty_to-infty & y1 = -infty) by A8;
consider I2 be PartFunc of REAL,REAL such that
A13: dom I2 = left_closed_halfline b and
A14: for x be Real st x in dom I2 holds I2.x = integral(f,x,b) and
A15: (I2 is convergent_in-infty & y2 = lim_in-infty I2)
or (I2 is divergent_in-infty_to+infty & y2 = +infty)
or (I2 is divergent_in-infty_to-infty & y2 = -infty) by A9;
now let x be Element of REAL;
assume A16: x in dom I1; then
I1.x = integral(f,x,b) by A11;
hence I1.x = I2.x by A10,A16,A13,A14;
end; then
I1 = I2 by A10,A13,PARTFUN1:5;
hence y1 = y2 by A12,A15,Th1,Th2;
end;
end;
definition
let f be PartFunc of REAL,REAL;
let a be Real;
assume
A1: f is_+infty_improper_integrable_on a;
func improper_integral_+infty(f,a) -> ExtReal means
:Def4:
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);
existence
proof
consider Intf be PartFunc of REAL,REAL such that
A2: dom Intf = right_closed_halfline a and
A3: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x) and
A4: Intf is convergent_in+infty or Intf is divergent_in+infty_to+infty
or Intf is divergent_in+infty_to-infty by A1;
per cases by A4;
suppose A5: Intf is convergent_in+infty;
reconsider IT = lim_in+infty Intf as ExtReal;
take IT;
thus thesis by A2,A3,A5;
end;
suppose A6: Intf is divergent_in+infty_to+infty;
take +infty;
thus thesis by A2,A3,A6;
end;
suppose A7: Intf is divergent_in+infty_to-infty;
take -infty;
thus thesis by A2,A3,A7;
end;
end;
uniqueness
proof
let y1,y2 be ExtReal;
assume that
A8: 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 & y1 = lim_in+infty Intf
or Intf is divergent_in+infty_to+infty & y1 = +infty
or Intf is divergent_in+infty_to-infty & y1 = -infty) and
A9: 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 & y2 = lim_in+infty Intf
or Intf is divergent_in+infty_to+infty & y2 = +infty
or Intf is divergent_in+infty_to-infty & y2 = -infty);
consider I1 be PartFunc of REAL,REAL such that
A10: dom I1 = right_closed_halfline a and
A11: for x be Real st x in dom I1 holds I1.x = integral(f,a,x) and
A12: (I1 is convergent_in+infty & y1 = lim_in+infty I1)
or (I1 is divergent_in+infty_to+infty & y1 = +infty)
or (I1 is divergent_in+infty_to-infty & y1 = -infty) by A8;
consider I2 be PartFunc of REAL,REAL such that
A13: dom I2 = right_closed_halfline a and
A14: for x be Real st x in dom I2 holds I2.x = integral(f,a,x) and
A15: (I2 is convergent_in+infty & y2 = lim_in+infty I2)
or (I2 is divergent_in+infty_to+infty & y2 = +infty)
or (I2 is divergent_in+infty_to-infty & y2 = -infty) by A9;
now let x be Element of REAL;
assume A16: x in dom I1; then
I1.x = integral(f,a,x) by A11;
hence I1.x = I2.x by A10,A16,A13,A14;
end; then
I1 = I2 by A10,A13,PARTFUN1:5;
hence y1 = y2 by A12,A15,Th3,Th4;
end;
end;
theorem Th20:
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
proof
let f be PartFunc of REAL,REAL, b be Real;
assume
A1: f is_-infty_ext_Riemann_integrable_on b; then
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 by INTEGR10:def 6;
hence f is_-infty_improper_integrable_on b by A1,INTEGR10:def 6;
end;
theorem Th21:
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
proof
let f be PartFunc of REAL,REAL, a be Real;
assume
A1: f is_+infty_ext_Riemann_integrable_on a; then
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 by INTEGR10:def 5;
hence f is_+infty_improper_integrable_on a by A1,INTEGR10:def 5;
end;
theorem Th22:
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)
proof
let f be PartFunc of REAL,REAL, b be Real;
assume
A1: f is_-infty_improper_integrable_on b; then
consider Intf be PartFunc of REAL,REAL such that
A2: dom Intf = left_closed_halfline b and
A3: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
A4: Intf is convergent_in-infty or Intf is divergent_in-infty_to+infty
or Intf is divergent_in-infty_to-infty;
per cases by A4;
suppose A5: Intf is convergent_in-infty; then
A6: f is_-infty_ext_Riemann_integrable_on b by A1,A2,A3,INTEGR10:def 6;
improper_integral_-infty(f,b) = lim_in-infty Intf by A1,A2,A3,A5,Def3
.= infty_ext_left_integral(f,b) by A6,A2,A3,A5,INTEGR10:def 8;
hence thesis by A5,A1,A2,A3,INTEGR10:def 6;
end;
suppose A7: Intf is divergent_in-infty_to+infty;
for I be PartFunc of REAL,REAL st
dom I = left_closed_halfline b
& (for x be Real st x in dom I holds I.x = integral(f,x,b))
holds not I is convergent_in-infty
proof
let I be PartFunc of REAL,REAL;
assume that
A8: dom I = left_closed_halfline b and
A9: for x be Real st x in dom I holds I.x = integral(f,x,b);
now let x be Element of REAL;
assume A10: x in dom Intf; then
Intf.x = integral(f,x,b) by A3;
hence Intf.x = I.x by A2,A8,A9,A10;
end; then
Intf = I by A2,A8,PARTFUN1:5;
hence not I is convergent_in-infty by A7,Th1;
end;
hence thesis by A1,Def3,INTEGR10:def 6;
end;
suppose A11: Intf is divergent_in-infty_to-infty;
for I be PartFunc of REAL,REAL st
dom I = left_closed_halfline b
& (for x be Real st x in dom I holds I.x = integral(f,x,b))
holds not I is convergent_in-infty
proof
let I be PartFunc of REAL,REAL;
assume that
A12: dom I = left_closed_halfline b and
A13: for x be Real st x in dom I holds I.x = integral(f,x,b);
now let x be Element of REAL;
assume A14: x in dom Intf; then
Intf.x = integral(f,x,b) by A3;
hence Intf.x = I.x by A2,A12,A13,A14;
end; then
Intf = I by A2,A12,PARTFUN1:5;
hence not I is convergent_in-infty by A11,Th2;
end;
hence thesis by A1,Def3,INTEGR10:def 6;
end;
end;
theorem Th23:
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
proof
let f be PartFunc of REAL,REAL, b be Real;
assume 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); then
consider Intf be PartFunc of REAL,REAL such that
A1: dom Intf = left_closed_halfline b and
A2: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
A3: Intf is divergent_in-infty_to+infty
or Intf is divergent_in-infty_to-infty;
hereby assume f is_-infty_ext_Riemann_integrable_on b; then
consider I be PartFunc of REAL,REAL such that
A4: dom I = left_closed_halfline b and
A5: for x be Real st x in dom I holds I.x = integral(f,x,b) and
A6: I is convergent_in-infty by INTEGR10:def 6;
now let x be Element of REAL;
assume A7: x in dom Intf; then
Intf.x = integral(f,x,b) by A2;
hence Intf.x = I.x by A1,A4,A5,A7;
end; then
Intf = I by A1,A4,PARTFUN1:5;
hence contradiction by A3,A6,Th1,Th2;
end;
end;
theorem
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
proof
let f,Intf be PartFunc of REAL,REAL, b be Real;
assume that
A1: f is_-infty_improper_integrable_on b and
A2: dom Intf = left_closed_halfline b and
A3: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
A4: Intf is convergent_in-infty;
A5: f is_-infty_ext_Riemann_integrable_on b by A1,A2,A3,A4,INTEGR10:def 6;
then
A6: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b) by A1,Th22;
consider I be PartFunc of REAL,REAL such that
A7: dom I = left_closed_halfline b and
A8: for x be Real st x in dom I holds I.x = integral(f,x,b) and
I is convergent_in-infty and
A9: infty_ext_left_integral(f,b) = lim_in-infty I by A5,INTEGR10:def 8;
now let x be Element of REAL;
assume A10: x in dom Intf; then
Intf.x = integral(f,x,b) by A3;
hence Intf.x = I.x by A2,A7,A8,A10;
end;
hence improper_integral_-infty(f,b) = lim_in-infty Intf
by A6,A9,A2,A7,PARTFUN1:5;
end;
Lm2:
for f be PartFunc of REAL,REAL, c be Real st
left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c
holds
for b be Real st b <= c holds
for d be Real st d <= b holds
f is_integrable_on ['d,b'] & f|['d,b'] is bounded
proof
let f be PartFunc of REAL,REAL, c be Real;
assume that
A1: left_closed_halfline c c= dom f and
A2: f is_-infty_improper_integrable_on c;
let b be Real;
assume
A3: b <= c;
thus for d be Real st d <= b holds
f is_integrable_on ['d,b'] & f|['d,b'] is bounded
proof
let d be Real;
assume A4: d <= b; then
A5: d <= c by A3,XXREAL_0:2; then
A6: f is_integrable_on ['d,c'] & f|['d,c'] is bounded by A2;
A7: [.d,c.] = ['d,c'] by A4,A3,XXREAL_0:2,INTEGRA5:def 3; then
['d,c'] c= ].-infty,c.] by XXREAL_1:265; then
A8: ['d,c'] c= dom f by A1;
b in ['d,c'] by A7,A4,A3,XXREAL_1:1;
hence f is_integrable_on ['d,b'] by A6,A5,A8,INTEGRA6:17;
[.d,b.] = ['d,b'] by A4,INTEGRA5:def 3;
hence f|['d,b'] is bounded by A6,A3,A7,XXREAL_1:34,RFUNCT_1:74;
end;
end;
Lm3:
for f be PartFunc of REAL,REAL, c be Real st
left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c
& improper_integral_-infty(f,c) = infty_ext_left_integral(f,c) holds
for b be Real st b <= c holds
f is_-infty_improper_integrable_on b
& improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
proof
let f be PartFunc of REAL,REAL, c be Real;
assume that
A1: left_closed_halfline c c= dom f and
A2: f is_-infty_improper_integrable_on c and
A3: improper_integral_-infty(f,c) = infty_ext_left_integral(f,c);
let b be Real;
assume
A4: b <= c;
consider I be PartFunc of REAL,REAL such that
A5: dom I = left_closed_halfline c and
A6: for x be Real st x in dom I holds I.x = integral(f,x,c) and
A7: (I is convergent_in-infty or I is divergent_in-infty_to+infty
or I is divergent_in-infty_to-infty) by A2;
A8: now assume I is divergent_in-infty_to+infty; then
not f is_-infty_ext_Riemann_integrable_on c by A5,A6,Th23;
hence contradiction by A2,A3,Th22;
end;
A9: now assume I is divergent_in-infty_to-infty; then
not f is_-infty_ext_Riemann_integrable_on c by A5,A6,Th23;
hence contradiction by A2,A3,Th22;
end;
-infty < b by XREAL_0:def 1,XXREAL_0:12; then
reconsider LB = ].-infty,b.] as non empty Subset of REAL by XXREAL_1:2;
deffunc F(Element of LB) = In(integral(f,$1,b),REAL);
consider Intf be Function of LB,REAL such that
A10: for x be Element of LB holds Intf.x = F(x) from FUNCT_2:sch 4;
A11: dom Intf = LB by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A12: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,x,b),REAL) by A10,A11;
hence thesis;
end;
A13: for r be Real ex g be Real st g < r & g in dom Intf
proof
let r be Real;
set R = min(b,r);
consider g be Real such that
A14: g < R & g in dom I by A7,A8,A9,LIMFUNC1:45;
A15:R <= b & R <= r by XXREAL_0:17; then
A16: g < b & g < r by A14,XXREAL_0:2;
g in ].-infty,b.] by A15,A14,XXREAL_0:2,XXREAL_1:234;
hence thesis by A11,A16;
end;
consider g be Real such that
A17: for g1 be Real st 0 < g1
ex r be Real st for r1 be Real st r1 < r & r1 in dom I
holds |. I.r1-g .| < g1 by A7,A8,A9,LIMFUNC1:45;
set G = g-integral(f,b,c);
A18: for g1 be Real st 0 <g1
ex r be Real st
for r1 be Real st r1 < r & r1 in dom Intf holds
|. Intf.r1-G .| < g1
proof
let g1 be Real;
assume 0 < g1; then
consider r be Real such that
A19: for r1 be Real st r1 < r & r1 in dom I holds |. I.r1-g .| < g1
by A17;
set R = min(b,r);
for r1 be Real st r1 < R & r1 in dom Intf holds
|. Intf.r1-G .| < g1
proof
let r1 be Real;
assume that
A20: r1 < R and
A21: r1 in dom Intf;
R <= r & R <= b by XXREAL_0:17; then
A22: r1 < r & r1 < b by A20,XXREAL_0:2;
A23: dom Intf c= dom I by A4,A5,A11,XXREAL_1:42; then
A24: |. I.r1 - g .| < g1 by A22,A19,A21;
A25: r1 <= c by A5,A21,A23,XXREAL_1:2; then
A26: f is_integrable_on ['r1,c'] & f|['r1,c'] is bounded by A2;
A27: [.r1,c.] = ['r1,c'] by A25,INTEGRA5:def 3; then
['r1,c'] c= ].-infty,c.] by XXREAL_1:265; then
A28: ['r1,c'] c= dom f by A1;
A29: b in ['r1,c'] by A22,A4,A27,XXREAL_1:1;
I.r1 - g = integral(f,r1,c) - g by A6,A21,A23
.= integral(f,r1,b)+integral(f,b,c) - g by A25,A26,A28,A29,INTEGRA6:17
.= integral(f,r1,b) - (g - integral(f,b,c));
hence |. Intf.r1 - G .| < g1 by A21,A24,A12;
end;
hence thesis;
end;
hence A30: f is_-infty_improper_integrable_on b
by A11,A12,A13,A1,A2,A4,Lm2,LIMFUNC1:45; then
f is_-infty_ext_Riemann_integrable_on b
by A11,A12,A13,A18,LIMFUNC1:45,INTEGR10:def 6;
hence improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
by A30,Th22;
end;
Lm4:
for f be PartFunc of REAL,REAL, c be Real
st left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c
& improper_integral_-infty(f,c) = +infty
holds for b be Real st b <= c holds
f is_-infty_improper_integrable_on b & improper_integral_-infty(f,b) = +infty
proof
let f be PartFunc of REAL,REAL, c be Real;
assume that
A1: left_closed_halfline c c= dom f and
A2: f is_-infty_improper_integrable_on c and
A3: improper_integral_-infty(f,c) = +infty;
let b be Real;
assume
A4: b <= c;
consider I be PartFunc of REAL,REAL such that
A5: dom I = ].-infty,c.] and
A6: for x be Real st x in dom I holds I.x = integral(f,x,c) and
A7: (I is convergent_in-infty or I is divergent_in-infty_to+infty
or I is divergent_in-infty_to-infty) by A2;
improper_integral_-infty(f,c) <> infty_ext_left_integral(f,c)
by A3; then
A8: not f is_-infty_ext_Riemann_integrable_on c by A2,Th22;
-infty < b by XREAL_0:def 1,XXREAL_0:12; then
reconsider LB = ].-infty,b.] as non empty Subset of REAL by XXREAL_1:2;
deffunc F(Element of LB) = In(integral(f,$1,b),REAL);
consider Intf be Function of LB,REAL such that
A9: for x be Element of LB holds Intf.x = F(x) from FUNCT_2:sch 4;
A10: dom Intf = LB by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A11: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,x,b),REAL) by A9,A10;
hence thesis;
end;
A12: for r be Real ex g be Real st g < r & g in dom Intf
proof
let r be Real;
set R = min(b,r);
consider g be Real such that
A13: g < R & g in dom I
by A8,A3,A2,A5,Def3,INTEGR10:def 6,LIMFUNC1:48;
A14:R <= b & R <= r by XXREAL_0:17; then
A15: g < b & g < r by A13,XXREAL_0:2;
g in dom Intf by A10,A14,A13,XXREAL_0:2,XXREAL_1:234;
hence thesis by A15;
end;
A16: for g1 be Real ex r be Real st for r1 be Real st r1 < r &
r1 in dom Intf holds g1 < Intf.r1
proof
let g1 be Real;
consider r be Real such that
A17: for r1 be Real st r1 < r & r1 in dom I
holds g1+integral(f,b,c) < I.r1
by A8,A7,A3,A2,A5,A6,Def3,INTEGR10:def 6,LIMFUNC1:48;
set R = min(b,r);
take R;
thus for r1 be Real st r1 < R & r1 in dom Intf holds g1 < Intf.r1
proof
let r1 be Real;
assume A18: r1 < R & r1 in dom Intf;
R <= b & R <= r by XXREAL_0:17; then
A19: r1 < b & r1 < r by A18,XXREAL_0:2; then
A20: r1 < c by A4,XXREAL_0:2;
r1 in dom I by A5,A19,A4,XXREAL_0:2,XXREAL_1:234; then
g1+integral(f,b,c) < I.r1 by A17,A19; then
A21: g1 + integral(f,b,c) < integral(f,r1,c) by A6,A20,A5,XXREAL_1:234;
A22: f is_integrable_on ['r1,c'] & f|['r1,c'] is bounded by A20,A2;
A23: ['r1,c'] = [.r1,c.] by A19,A4,XXREAL_0:2,INTEGRA5:def 3; then
['r1,c'] c= ].-infty,c.] by XXREAL_1:265; then
A24: ['r1,c'] c= dom f by A1;
b in ['r1,c'] by A23,A19,A4,XXREAL_1:1; then
integral(f,r1,c) = integral(f,r1,b) + integral(f,b,c)
by A20,A22,A24,INTEGRA6:17; then
g1 < integral(f,r1,b) by A21,XREAL_1:6;
hence g1 < Intf.r1 by A11,A18;
end;
end;
hence
A25: f is_-infty_improper_integrable_on b
by A10,A11,A1,A2,A4,Lm2,A12,LIMFUNC1:48;
Intf is divergent_in-infty_to+infty by A12,A16,LIMFUNC1:48;
hence improper_integral_-infty(f,b) = +infty by A10,A11,A25,Def3;
end;
Lm5:
for f be PartFunc of REAL,REAL, c be Real st
left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c
& improper_integral_-infty(f,c) = -infty holds
for b be Real st b <= c holds
f is_-infty_improper_integrable_on b & improper_integral_-infty(f,b) = -infty
proof
let f be PartFunc of REAL,REAL, c be Real;
assume that
A1: left_closed_halfline c c= dom f and
A2: f is_-infty_improper_integrable_on c and
A3: improper_integral_-infty(f,c) = -infty;
let b be Real;
assume
A4: b <= c;
consider I be PartFunc of REAL,REAL such that
A5: dom I = ].-infty,c.] and
A6: for x be Real st x in dom I holds I.x = integral(f,x,c) and
A7: (I is convergent_in-infty or I is divergent_in-infty_to+infty
or I is divergent_in-infty_to-infty) by A2;
improper_integral_-infty(f,c) <> infty_ext_left_integral(f,c)
by A3; then
A8: not f is_-infty_ext_Riemann_integrable_on c by A2,Th22;
-infty < b by XREAL_0:def 1,XXREAL_0:12; then
reconsider LB = ].-infty,b.] as non empty Subset of REAL by XXREAL_1:2;
deffunc F(Element of LB) = In(integral(f,$1,b),REAL);
consider Intf be Function of LB,REAL such that
A9: for x be Element of LB holds Intf.x = F(x) from FUNCT_2:sch 4;
A10: dom Intf = LB by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A11: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,x,b),REAL) by A9,A10;
hence thesis;
end;
A12: for r be Real ex g be Real st g < r & g in dom Intf
proof
let r be Real;
set R = min(b,r);
consider g be Real such that
A13: g < R & g in dom I
by A8,A3,A2,A5,Def3,INTEGR10:def 6,LIMFUNC1:49;
A14: R <= b & R <= r by XXREAL_0:17; then
A15: g < b & g < r by A13,XXREAL_0:2;
g in dom Intf by A10,A14,A13,XXREAL_0:2,XXREAL_1:234;
hence thesis by A15;
end;
A16: for g1 be Real ex r be Real st for r1 be Real st r1 < r &
r1 in dom Intf holds g1 > Intf.r1
proof
let g1 be Real;
consider r be Real such that
A17: for r1 be Real st r1 < r & r1 in dom I
holds g1+integral(f,b,c) > I.r1
by A8,A7,A3,A2,A5,A6,Def3,INTEGR10:def 6,LIMFUNC1:49;
set R = min(b,r);
take R;
thus for r1 be Real st r1 < R & r1 in dom Intf holds g1 > Intf.r1
proof
let r1 be Real;
assume A18: r1 < R & r1 in dom Intf;
R <= b & R <= r by XXREAL_0:17; then
A19: r1 < b & r1 < r by A18,XXREAL_0:2; then
A20: r1 < c by A4,XXREAL_0:2;
r1 in dom I by A19,A5,A4,XXREAL_0:2,XXREAL_1:234; then
g1+integral(f,b,c) > I.r1 by A17,A19; then
A21: g1 + integral(f,b,c) > integral(f,r1,c) by A6,A20,A5,XXREAL_1:234;
A22: f is_integrable_on ['r1,c'] & f|['r1,c'] is bounded by A20,A2;
A23: ['r1,c'] = [.r1,c.] by A19,A4,XXREAL_0:2,INTEGRA5:def 3; then
['r1,c'] c= ].-infty,c.] by XXREAL_1:265; then
A24: ['r1,c'] c= dom f by A1;
b in ['r1,c'] by A23,A19,A4,XXREAL_1:1; then
integral(f,r1,c) = integral(f,r1,b) + integral(f,b,c)
by A20,A22,A24,INTEGRA6:17; then
g1 > integral(f,r1,b) by A21,XREAL_1:6;
hence g1 > Intf.r1 by A11,A18;
end;
end;
hence
A25: f is_-infty_improper_integrable_on b
by A10,A11,A1,A2,A4,Lm2,A12,LIMFUNC1:49;
Intf is divergent_in-infty_to-infty by A12,A16,LIMFUNC1:49;
hence improper_integral_-infty(f,b) = -infty by A10,A11,A25,Def3;
end;
theorem Th25:
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 )
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b <= c and
A2: left_closed_halfline c c= dom f and
A3: f is_-infty_improper_integrable_on c;
per cases;
suppose f is_-infty_ext_Riemann_integrable_on c; then
improper_integral_-infty(f,c) = infty_ext_left_integral(f,c)
by A3,Th22;
hence thesis by A1,A2,A3,Lm3;
end;
suppose not f is_-infty_ext_Riemann_integrable_on c; then
per cases by A3,Th22;
suppose improper_integral_-infty(f,c) = +infty;
hence thesis by A1,A2,A3,Lm4;
end;
suppose improper_integral_-infty(f,c) = -infty;
hence thesis by A1,A2,A3,Lm5;
end;
end;
end;
Lm6:
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 for d be Real st d <= c holds
f is_integrable_on ['d,c'] & f|['d,c'] is bounded
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b <= c and
A2: left_closed_halfline c c= dom f and
A3: f|['b,c'] is bounded and
A4: f is_-infty_improper_integrable_on b and
A5: f is_integrable_on ['b,c'];
hereby let d be Real;
assume
A6: d <= c; then
['d,c'] = [.d,c.] by INTEGRA5:def 3; then
['d,c'] c= ].-infty,c.] by XXREAL_1:265; then
A7: ['d,c'] c= dom f by A2;
A8: ['b,c'] = [.b,c.] & ['d,c'] = [.d,c.] by A1,A6,INTEGRA5:def 3;
per cases;
suppose A9: d <= b; then
A10: f is_integrable_on ['d,b'] & f|['d,b'] is bounded by A4;
hence f is_integrable_on ['d,c'] by A9,A1,A7,A3,A5,INTEGR24:1;
['d,b'] = [.d,b.] by A9,INTEGRA5:def 3; then
['d,b'] \/ ['b,c'] = [.d,c.] by A9,A1,A8,XXREAL_1:165;
hence f|['d,c'] is bounded by A10,A3,A8,RFUNCT_1:87;
end;
suppose A11: b < d;
[.b,c.] c= ].-infty,c.] by XXREAL_1:265; then
A12: ['b,c'] c= dom f by A2,A8;
d in ['b,c'] by A8,A11,A6,XXREAL_1:1;
hence f is_integrable_on ['d,c'] by A1,A3,A5,A12,INTEGRA6:17;
thus f|['d,c'] is bounded by A3,A11,A8,XXREAL_1:34,RFUNCT_1:74;
end;
end;
end;
Lm7:
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']
& improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
holds f is_-infty_improper_integrable_on c
& improper_integral_-infty(f,c)
= improper_integral_-infty(f,b) + integral(f,b,c)
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b <= c and
A2: left_closed_halfline c c= dom f and
A3: f|['b,c'] is bounded and
A4: f is_-infty_improper_integrable_on b and
A5: f is_integrable_on ['b,c'] and
A6: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b);
consider I be PartFunc of REAL,REAL such that
A7: dom I = left_closed_halfline b and
A8: for x be Real st x in dom I holds I.x = integral(f,x,b) and
A9: (I is convergent_in-infty or I is divergent_in-infty_to+infty
or I is divergent_in-infty_to-infty) by A4;
A10: now assume I is divergent_in-infty_to+infty; then
not f is_-infty_ext_Riemann_integrable_on b by A7,A8,Th23;
hence contradiction by A4,A6,Th22;
end;
now assume I is divergent_in-infty_to-infty; then
not f is_-infty_ext_Riemann_integrable_on b by A7,A8,Th23;
hence contradiction by A4,A6,Th22;
end; then
f is_-infty_ext_Riemann_integrable_on b
by A4,A7,A8,A9,A10,INTEGR10:def 6; then
A11: f is_-infty_ext_Riemann_integrable_on c
& infty_ext_left_integral(f,c)
= infty_ext_left_integral(f,b) + integral(f,b,c)
by A1,A2,A3,A5,Th17;
ex Intf be PartFunc of REAL,REAL st dom Intf = left_closed_halfline c &
(for x be Real st x in dom Intf holds Intf.x = integral(f,x,c)) &
Intf is convergent_in-infty by A11,INTEGR10:def 6;
hence f is_-infty_improper_integrable_on c by A1,A2,A3,A4,A5,Lm6; then
improper_integral_-infty(f,c)
= infty_ext_left_integral(f,b) + integral(f,b,c) by A11,Th22;
hence improper_integral_-infty(f,c)
= improper_integral_-infty(f,b) + integral(f,b,c)
by A6,XXREAL_3:def 2;
end;
Lm8:
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']
& improper_integral_-infty(f,b) = +infty
holds f is_-infty_improper_integrable_on c
& improper_integral_-infty(f,c) = +infty
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b <= c and
A2: left_closed_halfline c c= dom f and
A3: f|['b,c'] is bounded and
A4: f is_-infty_improper_integrable_on b and
A5: f is_integrable_on ['b,c'] and
A6: improper_integral_-infty(f,b) = +infty;
consider I be PartFunc of REAL,REAL such that
A7: dom I = left_closed_halfline b and
A8: for x be Real st x in dom I holds I.x = integral(f,x,b) and
A9: (I is convergent_in-infty or I is divergent_in-infty_to+infty
or I is divergent_in-infty_to-infty) by A4;
improper_integral_-infty(f,b) <> infty_ext_left_integral(f,b)
by A6; then
A10: not f is_-infty_ext_Riemann_integrable_on b by A4,Th22;
-infty < c by XREAL_0:def 1,XXREAL_0:12; then
reconsider AC = ].-infty,c.] as non empty Subset of REAL by XXREAL_1:2;
deffunc F(Element of AC) = In(integral(f,$1,c),REAL);
consider Intf be Function of AC,REAL such that
A11: for x be Element of AC holds Intf.x = F(x) from FUNCT_2:sch 4;
A12: dom Intf = AC by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A13: for x be Real st x in dom Intf holds Intf.x = integral(f,x,c)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,x,c),REAL) by A11,A12;
hence thesis;
end;
A14: for r be Real ex g be Real st g < r & g in dom Intf
proof
let r be Real;
consider g be Real such that
A15: g < r & g in dom I
by A10,A6,A7,Def3,INTEGR10:def 6,A4,LIMFUNC1:48;
].-infty,b.] c= ].-infty,c.] by A1,XXREAL_1:42;
hence thesis by A15,A7,A12;
end;
A16: for g1 be Real ex r be Real st for r1 be Real st r1 < r &
r1 in dom Intf holds g1 < Intf.r1
proof
let g1 be Real;
consider r be Real such that
A17: for r1 be Real st r1 < r & r1 in dom I
holds g1-integral(f,b,c) < I.r1
by A10,A9,A4,A6,A7,A8,Def3,INTEGR10:def 6,LIMFUNC1:48;
set R = min(b,r);
take R;
thus for r1 be Real st r1 < R & r1 in dom Intf holds g1 < Intf.r1
proof
let r1 be Real;
assume A18: r1 < R & r1 in dom Intf;
A19: R <= b & R <= r by XXREAL_0:17; then
A20: r1 < b & r1 < r by A18,XXREAL_0:2; then
A21: r1 < c by A1,XXREAL_0:2;
r1 in dom I by A7,A19,A18,XXREAL_0:2,XXREAL_1:234; then
g1-integral(f,b,c) < I.r1 by A17,A20; then
A22: g1-integral(f,b,c) < integral(f,r1,b) by A8,A20,A7,XXREAL_1:234;
A23: f is_integrable_on ['r1,c'] & f|['r1,c'] is bounded
by A21,A1,A2,A3,A4,A5,Lm6;
A24: ['r1,c'] = [.r1,c.] by A20,A1,XXREAL_0:2,INTEGRA5:def 3; then
['r1,c'] c= ].-infty,c.] by XXREAL_1:265; then
A25: ['r1,c'] c= dom f by A2;
b in ['r1,c'] by A24,A20,A1,XXREAL_1:1; then
integral(f,r1,c) = integral(f,r1,b) + integral(f,b,c)
by A21,A23,A25,INTEGRA6:17; then
integral(f,r1,b) = integral(f,r1,c) - integral(f,b,c); then
g1 < integral(f,r1,c) by A22,XREAL_1:9;
hence g1 < Intf.r1 by A13,A18;
end;
end;
hence
A26: f is_-infty_improper_integrable_on c
by A12,A13,A14,A1,A2,A3,A4,A5,Lm6,LIMFUNC1:48;
Intf is divergent_in-infty_to+infty by A14,A16,LIMFUNC1:48;
hence improper_integral_-infty(f,c) = +infty by A12,A13,A26,Def3;
end;
Lm9:
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']
& improper_integral_-infty(f,b) = -infty
holds f is_-infty_improper_integrable_on c
& improper_integral_-infty(f,c) = -infty
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b <= c and
A2: left_closed_halfline c c= dom f and
A3: f|['b,c'] is bounded and
A4: f is_-infty_improper_integrable_on b and
A5: f is_integrable_on ['b,c'] and
A6: improper_integral_-infty(f,b) = -infty;
consider I be PartFunc of REAL,REAL such that
A7: dom I = left_closed_halfline b and
A8: for x be Real st x in dom I holds I.x = integral(f,x,b) and
A9: (I is convergent_in-infty or I is divergent_in-infty_to+infty
or I is divergent_in-infty_to-infty) by A4;
improper_integral_-infty(f,b) <> infty_ext_left_integral(f,b)
by A6; then
A10: not f is_-infty_ext_Riemann_integrable_on b by A4,Th22;
-infty < c by XREAL_0:def 1,XXREAL_0:12; then
reconsider AC = ].-infty,c.] as non empty Subset of REAL by XXREAL_1:2;
deffunc F(Element of AC) = In(integral(f,$1,c),REAL);
consider Intf be Function of AC,REAL such that
A11: for x be Element of AC holds Intf.x = F(x) from FUNCT_2:sch 4;
A12: dom Intf = AC by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A13: for x be Real st x in dom Intf holds Intf.x = integral(f,x,c)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,x,c),REAL) by A11,A12;
hence thesis;
end;
A14: for r be Real ex g be Real st g < r & g in dom Intf
proof
let r be Real;
consider g be Real such that
A15: g < r & g in dom I
by A10,A6,A7,Def3,INTEGR10:def 6,A4,LIMFUNC1:49;
].-infty,b.] c= ].-infty,c.] by A1,XXREAL_1:42;
hence thesis by A15,A7,A12;
end;
A16: for g1 be Real ex r be Real st for r1 be Real st r1 < r &
r1 in dom Intf holds g1 > Intf.r1
proof
let g1 be Real;
consider r be Real such that
A17: for r1 be Real st r1 < r & r1 in dom I
holds g1-integral(f,b,c) > I.r1
by A10,A9,A4,A6,A7,A8,Def3,INTEGR10:def 6,LIMFUNC1:49;
set R = min(b,r);
take R;
thus for r1 be Real st r1 < R & r1 in dom Intf holds g1 > Intf.r1
proof
let r1 be Real;
assume A18: r1 < R & r1 in dom Intf;
A19: R <= b & R <= r by XXREAL_0:17; then
A20: r1 < b & r1 < r by A18,XXREAL_0:2; then
A21: r1 < c by A1,XXREAL_0:2;
r1 in dom I by A7,A19,A18,XXREAL_0:2,XXREAL_1:234; then
g1-integral(f,b,c) > I.r1 by A17,A20; then
A22: g1-integral(f,b,c) > integral(f,r1,b) by A8,A20,A7,XXREAL_1:234;
A23: f is_integrable_on ['r1,c'] & f|['r1,c'] is bounded
by A21,A1,A2,A3,A4,A5,Lm6;
A24: ['r1,c'] = [.r1,c.] by A20,A1,XXREAL_0:2,INTEGRA5:def 3; then
['r1,c'] c= ].-infty,c.] by XXREAL_1:265; then
A25: ['r1,c'] c= dom f by A2;
b in ['r1,c'] by A24,A20,A1,XXREAL_1:1; then
integral(f,r1,c) = integral(f,r1,b) + integral(f,b,c)
by A21,A23,A25,INTEGRA6:17; then
integral(f,r1,b) = integral(f,r1,c) - integral(f,b,c); then
g1 > integral(f,r1,c) by A22,XREAL_1:9;
hence g1 > Intf.r1 by A13,A18;
end;
end;
hence
A26: f is_-infty_improper_integrable_on c
by A12,A13,A14,A1,A2,A3,A4,A5,Lm6,LIMFUNC1:49;
Intf is divergent_in-infty_to-infty by A14,A16,LIMFUNC1:49;
hence improper_integral_-infty(f,c) = -infty by A12,A13,A26,Def3;
end;
theorem Th26:
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 )
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b <= c and
A2: left_closed_halfline c c= dom f and
A3: f|['b,c'] is bounded and
A4: f is_-infty_improper_integrable_on b and
A5: f is_integrable_on ['b,c'];
per cases;
suppose f is_-infty_ext_Riemann_integrable_on b; then
improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
by A4,Th22;
hence thesis by A1,A2,A3,A4,A5,Lm7;
end;
suppose A6: not f is_-infty_ext_Riemann_integrable_on b;
per cases by A4,A6,Th22;
suppose improper_integral_-infty(f,b) = +infty;
hence thesis by A1,A2,A3,A4,A5,Lm8;
end;
suppose improper_integral_-infty(f,b) = -infty;
hence thesis by A1,A2,A3,A4,A5,Lm9;
end;
end;
end;
theorem Th27:
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)
proof
let f be PartFunc of REAL,REAL, b be Real;
assume
A1: f is_+infty_improper_integrable_on b; then
consider Intf be PartFunc of REAL,REAL such that
A2: dom Intf = right_closed_halfline b and
A3: for x be Real st x in dom Intf holds Intf.x = integral(f,b,x) and
A4: Intf is convergent_in+infty or Intf is divergent_in+infty_to+infty
or Intf is divergent_in+infty_to-infty;
per cases by A4;
suppose A5: Intf is convergent_in+infty; then
A6: f is_+infty_ext_Riemann_integrable_on b by A1,A2,A3,INTEGR10:def 5;
improper_integral_+infty(f,b) = lim_in+infty Intf by A1,A2,A3,A5,Def4
.= infty_ext_right_integral(f,b) by A6,A2,A3,A5,INTEGR10:def 7;
hence thesis by A5,A1,A2,A3,INTEGR10:def 5;
end;
suppose A7: Intf is divergent_in+infty_to+infty;
for I be PartFunc of REAL,REAL st
dom I = right_closed_halfline b
& (for x be Real st x in dom I holds I.x = integral(f,b,x))
holds not I is convergent_in+infty
proof
let I be PartFunc of REAL,REAL;
assume that
A8: dom I = right_closed_halfline b and
A9: for x be Real st x in dom I holds I.x = integral(f,b,x);
now let x be Element of REAL;
assume A10: x in dom Intf; then
Intf.x = integral(f,b,x) by A3;
hence Intf.x = I.x by A2,A8,A9,A10;
end; then
Intf = I by A2,A8,PARTFUN1:5;
hence not I is convergent_in+infty by A7,Th3;
end;
hence thesis by A1,Def4,INTEGR10:def 5;
end;
suppose A11: Intf is divergent_in+infty_to-infty;
for I be PartFunc of REAL,REAL st
dom I = right_closed_halfline b
& (for x be Real st x in dom I holds I.x = integral(f,b,x))
holds not I is convergent_in+infty
proof
let I be PartFunc of REAL,REAL;
assume that
A12: dom I = right_closed_halfline b and
A13: for x be Real st x in dom I holds I.x = integral(f,b,x);
now let x be Element of REAL;
assume A14: x in dom Intf; then
Intf.x = integral(f,b,x) by A3;
hence Intf.x = I.x by A2,A12,A13,A14;
end; then
Intf = I by A2,A12,PARTFUN1:5;
hence not I is convergent_in+infty by A11,Th4;
end;
hence thesis by A1,Def4,INTEGR10:def 5;
end;
end;
theorem Th28:
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
proof
let f be PartFunc of REAL,REAL, b be Real;
assume 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); then
consider Intf be PartFunc of REAL,REAL such that
A1: dom Intf = right_closed_halfline b and
A2: for x be Real st x in dom Intf holds Intf.x = integral(f,b,x) and
A3: Intf is divergent_in+infty_to+infty
or Intf is divergent_in+infty_to-infty;
hereby assume f is_+infty_ext_Riemann_integrable_on b; then
consider I be PartFunc of REAL,REAL such that
A4: dom I = right_closed_halfline b and
A5: for x be Real st x in dom I holds I.x = integral(f,b,x) and
A6: I is convergent_in+infty by INTEGR10:def 5;
now let x be Element of REAL;
assume A7: x in dom Intf; then
Intf.x = integral(f,b,x) by A2;
hence Intf.x = I.x by A1,A4,A5,A7;
end; then
Intf = I by A1,A4,PARTFUN1:5;
hence contradiction by A3,A6,Th3,Th4;
end;
end;
theorem
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
proof
let f,Intf be PartFunc of REAL,REAL, b be Real;
assume that
A1: f is_+infty_improper_integrable_on b and
A2: dom Intf = right_closed_halfline b and
A3: for x be Real st x in dom Intf holds Intf.x = integral(f,b,x) and
A4: Intf is convergent_in+infty;
A5: f is_+infty_ext_Riemann_integrable_on b by A1,A2,A3,A4,INTEGR10:def 5;
then
A6: improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A1,Th27;
consider I be PartFunc of REAL,REAL such that
A7: dom I = right_closed_halfline b and
A8: for x be Real st x in dom I holds I.x = integral(f,b,x) and
I is convergent_in+infty and
A9: infty_ext_right_integral(f,b) = lim_in+infty I by A5,INTEGR10:def 7;
now let x be Element of REAL;
assume A10: x in dom Intf; then
Intf.x = integral(f,b,x) by A3;
hence Intf.x = I.x by A2,A7,A8,A10;
end;
hence improper_integral_+infty(f,b) = lim_in+infty Intf
by A6,A9,A2,A7,PARTFUN1:5;
end;
Lm10:
for f be PartFunc of REAL,REAL, c be Real st
right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c
holds
for b be Real st b >= c holds
for d be Real st d >= b holds
f is_integrable_on ['b,d'] & f|['b,d'] is bounded
proof
let f be PartFunc of REAL,REAL, c be Real;
assume that
A1: right_closed_halfline c c= dom f and
A2: f is_+infty_improper_integrable_on c;
let b be Real;
assume
A3: b >= c;
thus for d be Real st d >= b holds
f is_integrable_on ['b,d'] & f|['b,d'] is bounded
proof
let d be Real;
assume A4: d >= b; then
A5: d >= c by A3,XXREAL_0:2; then
A6: f is_integrable_on ['c,d'] & f|['c,d'] is bounded by A2;
A7: [.c,d.] = ['c,d'] by A4,A3,XXREAL_0:2,INTEGRA5:def 3; then
['c,d'] c= [.c,+infty.[ by XXREAL_1:251; then
A8: ['c,d'] c= dom f by A1;
b in ['c,d'] by A7,A4,A3,XXREAL_1:1;
hence f is_integrable_on ['b,d'] by A6,A5,A8,INTEGRA6:17;
[.b,d.] = ['b,d'] by A4,INTEGRA5:def 3;
hence f|['b,d'] is bounded by A6,A3,A7,XXREAL_1:34,RFUNCT_1:74;
end;
end;
Lm11:
for f be PartFunc of REAL,REAL, c be Real st
right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c
& improper_integral_+infty(f,c) = infty_ext_right_integral(f,c) holds
for b be Real st b >= c holds
f is_+infty_improper_integrable_on b
& improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
proof
let f be PartFunc of REAL,REAL, c be Real;
assume that
A1: right_closed_halfline c c= dom f and
A2: f is_+infty_improper_integrable_on c and
A3: improper_integral_+infty(f,c) = infty_ext_right_integral(f,c);
let b be Real;
assume
A4: b >= c;
consider I be PartFunc of REAL,REAL such that
A5: dom I = right_closed_halfline c and
A6: for x be Real st x in dom I holds I.x = integral(f,c,x) and
A7: (I is convergent_in+infty or I is divergent_in+infty_to+infty
or I is divergent_in+infty_to-infty) by A2;
A8: now assume I is divergent_in+infty_to+infty; then
not f is_+infty_ext_Riemann_integrable_on c by A5,A6,Th28;
hence contradiction by A2,A3,Th27;
end;
A9: now assume I is divergent_in+infty_to-infty; then
not f is_+infty_ext_Riemann_integrable_on c by A5,A6,Th28;
hence contradiction by A2,A3,Th27;
end;
+infty > b by XREAL_0:def 1,XXREAL_0:9; then
reconsider LB = [.b,+infty.[ as non empty Subset of REAL by XXREAL_1:3;
deffunc F(Element of LB) = In(integral(f,b,$1),REAL);
consider Intf be Function of LB,REAL such that
A10: for x be Element of LB holds Intf.x = F(x) from FUNCT_2:sch 4;
A11: dom Intf = LB by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A12: for x be Real st x in dom Intf holds Intf.x = integral(f,b,x)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,b,x),REAL) by A10,A11;
hence thesis;
end;
A13: for r be Real ex g be Real st g > r & g in dom Intf
proof
let r be Real;
set R = max(b,r);
consider g be Real such that
A14: g > R & g in dom I by A7,A8,A9,LIMFUNC1:44;
A15:R >= b & R >= r by XXREAL_0:25; then
A16: g > b & g > r by A14,XXREAL_0:2;
g in [.b,+infty.[ by A15,A14,XXREAL_0:2,XXREAL_1:236;
hence thesis by A11,A16;
end;
consider g be Real such that
A17: for g1 be Real st 0 < g1
ex r be Real st for r1 be Real st r1 > r & r1 in dom I
holds |. I.r1-g .| < g1 by A7,A8,A9,LIMFUNC1:44;
set G = g-integral(f,c,b);
A18: for g1 be Real st 0 <g1
ex r be Real st
for r1 be Real st r1 > r & r1 in dom Intf holds
|. Intf.r1-G .| < g1
proof
let g1 be Real;
assume 0 < g1; then
consider r be Real such that
A19: for r1 be Real st r1 > r & r1 in dom I holds |. I.r1-g .| < g1
by A17;
set R = max(b,r);
for r1 be Real st r1 > R & r1 in dom Intf holds
|. Intf.r1-G .| < g1
proof
let r1 be Real;
assume that
A20: r1 > R and
A21: r1 in dom Intf;
R >= r & R >= b by XXREAL_0:25; then
A22: r1 > r & r1 > b by A20,XXREAL_0:2;
A23: dom Intf c= dom I by A4,A5,A11,XXREAL_1:38; then
A24: |. I.r1 - g .| < g1 by A22,A19,A21;
A25: r1 >= c by A5,A21,A23,XXREAL_1:3; then
A26: f is_integrable_on ['c,r1'] & f|['c,r1'] is bounded by A2;
A27: [.c,r1.] = ['c,r1'] by A25,INTEGRA5:def 3; then
['c,r1'] c= [.c,+infty.[ by XXREAL_1:251; then
A28: ['c,r1'] c= dom f by A1;
A29: b in ['c,r1'] by A22,A4,A27,XXREAL_1:1;
I.r1 - g = integral(f,c,r1) - g by A6,A21,A23
.= integral(f,b,r1)+integral(f,c,b) - g by A25,A26,A28,A29,INTEGRA6:17
.= integral(f,b,r1) - (g - integral(f,c,b));
hence |. Intf.r1 - G .| < g1 by A21,A24,A12;
end;
hence thesis;
end;
hence A30: f is_+infty_improper_integrable_on b
by A11,A12,A13,A1,A2,A4,Lm10,LIMFUNC1:44; then
f is_+infty_ext_Riemann_integrable_on b
by A11,A12,A13,A18,LIMFUNC1:44,INTEGR10:def 5;
hence improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A30,Th27;
end;
Lm12:
for f be PartFunc of REAL,REAL, c be Real st
right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c
& improper_integral_+infty(f,c) = +infty holds
for b be Real st b >= c holds
f is_+infty_improper_integrable_on b & improper_integral_+infty(f,b) = +infty
proof
let f be PartFunc of REAL,REAL, c be Real;
assume that
A1: right_closed_halfline c c= dom f and
A2: f is_+infty_improper_integrable_on c and
A3: improper_integral_+infty(f,c) = +infty;
let b be Real;
assume
A4: b >= c;
consider I be PartFunc of REAL,REAL such that
A5: dom I = [.c,+infty.[ and
A6: for x be Real st x in dom I holds I.x = integral(f,c,x) and
A7: (I is convergent_in+infty or I is divergent_in+infty_to+infty
or I is divergent_in+infty_to-infty) by A2;
improper_integral_+infty(f,c) <> infty_ext_right_integral(f,c)
by A3; then
A8: not f is_+infty_ext_Riemann_integrable_on c by A2,Th27;
+infty > b by XREAL_0:def 1,XXREAL_0:9; then
reconsider LB = [.b,+infty.[ as non empty Subset of REAL by XXREAL_1:3;
deffunc F(Element of LB) = In(integral(f,b,$1),REAL);
consider Intf be Function of LB,REAL such that
A9: for x be Element of LB holds Intf.x = F(x) from FUNCT_2:sch 4;
A10: dom Intf = LB by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A11: for x be Real st x in dom Intf holds Intf.x = integral(f,b,x)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,b,x),REAL) by A9,A10;
hence thesis;
end;
A12: for r be Real ex g be Real st g > r & g in dom Intf
proof
let r be Real;
set R = max(b,r);
consider g be Real such that
A13: g > R & g in dom I
by A8,A3,A2,A5,Def4,INTEGR10:def 5,LIMFUNC1:46;
A14: R >= b & R >= r by XXREAL_0:25; then
A15: g > b & g > r by A13,XXREAL_0:2;
g in dom Intf by A10,A14,A13,XXREAL_0:2,XXREAL_1:236;
hence thesis by A15;
end;
A16: for g1 be Real ex r be Real st for r1 be Real st r1 > r &
r1 in dom Intf holds g1 < Intf.r1
proof
let g1 be Real;
consider r be Real such that
A17: for r1 be Real st r1 > r & r1 in dom I
holds g1+integral(f,c,b) < I.r1
by A8,A7,A3,A2,A5,A6,Def4,INTEGR10:def 5,LIMFUNC1:46;
set R = max(b,r);
take R;
thus for r1 be Real st r1 > R & r1 in dom Intf holds g1 < Intf.r1
proof
let r1 be Real;
assume A18: r1 > R & r1 in dom Intf;
R >= b & R >= r by XXREAL_0:25; then
A19: r1 > b & r1 > r by A18,XXREAL_0:2; then
A20: r1 > c by A4,XXREAL_0:2;
r1 in dom I by A19,A5,A4,XXREAL_0:2,XXREAL_1:236; then
g1+integral(f,c,b) < I.r1 by A17,A19; then
A21: g1 + integral(f,c,b) < integral(f,c,r1) by A6,A20,A5,XXREAL_1:236;
A22: f is_integrable_on ['c,r1'] & f|['c,r1'] is bounded by A20,A2;
A23: ['c,r1'] = [.c,r1.] by A19,A4,XXREAL_0:2,INTEGRA5:def 3; then
['c,r1'] c= [.c,+infty.[ by XXREAL_1:251; then
A24: ['c,r1'] c= dom f by A1;
b in ['c,r1'] by A23,A19,A4,XXREAL_1:1; then
integral(f,c,r1) = integral(f,b,r1) + integral(f,c,b)
by A20,A22,A24,INTEGRA6:17; then
g1 < integral(f,b,r1) by A21,XREAL_1:6;
hence g1 < Intf.r1 by A11,A18;
end;
end;
hence
A25: f is_+infty_improper_integrable_on b
by A10,A11,A1,A2,A4,Lm10,A12,LIMFUNC1:46;
Intf is divergent_in+infty_to+infty by A12,A16,LIMFUNC1:46;
hence improper_integral_+infty(f,b) = +infty by A10,A11,A25,Def4;
end;
Lm13:
for f be PartFunc of REAL,REAL, c be Real st
right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c
& improper_integral_+infty(f,c) = -infty holds
for b be Real st b >= c holds
f is_+infty_improper_integrable_on b & improper_integral_+infty(f,b) = -infty
proof
let f be PartFunc of REAL,REAL, c be Real;
assume that
A1: right_closed_halfline c c= dom f and
A2: f is_+infty_improper_integrable_on c and
A3: improper_integral_+infty(f,c) = -infty;
let b be Real;
assume
A4: b >= c;
consider I be PartFunc of REAL,REAL such that
A5: dom I = [.c,+infty.[ and
A6: for x be Real st x in dom I holds I.x = integral(f,c,x) and
A7: (I is convergent_in+infty or I is divergent_in+infty_to+infty
or I is divergent_in+infty_to-infty) by A2;
improper_integral_+infty(f,c) <> infty_ext_right_integral(f,c)
by A3; then
A8: not f is_+infty_ext_Riemann_integrable_on c by A2,Th27;
+infty > b by XREAL_0:def 1,XXREAL_0:9; then
reconsider LB = [.b,+infty.[ as non empty Subset of REAL by XXREAL_1:3;
deffunc F(Element of LB) = In(integral(f,b,$1),REAL);
consider Intf be Function of LB,REAL such that
A9: for x be Element of LB holds Intf.x = F(x) from FUNCT_2:sch 4;
A10: dom Intf = LB by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A11: for x be Real st x in dom Intf holds Intf.x = integral(f,b,x)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,b,x),REAL) by A9,A10;
hence thesis;
end;
A12: for r be Real ex g be Real st g > r & g in dom Intf
proof
let r be Real;
set R = max(b,r);
consider g be Real such that
A13: g > R & g in dom I
by A8,A3,A2,A5,Def4,INTEGR10:def 5,LIMFUNC1:47;
A14: R >= b & R >= r by XXREAL_0:25; then
A15: g > b & g > r by A13,XXREAL_0:2;
g in dom Intf by A10,A14,A13,XXREAL_0:2,XXREAL_1:236;
hence thesis by A15;
end;
A16: for g1 be Real ex r be Real st for r1 be Real st r1 > r &
r1 in dom Intf holds g1 > Intf.r1
proof
let g1 be Real;
consider r be Real such that
A17: for r1 be Real st r1 > r & r1 in dom I
holds g1+integral(f,c,b) > I.r1
by A8,A7,A3,A2,A5,A6,Def4,INTEGR10:def 5,LIMFUNC1:47;
set R = max(b,r);
take R;
thus for r1 be Real st r1 > R & r1 in dom Intf holds g1 > Intf.r1
proof
let r1 be Real;
assume A18: r1 > R & r1 in dom Intf;
R >= b & R >= r by XXREAL_0:25; then
A19: r1 > b & r1 > r by A18,XXREAL_0:2; then
A20: r1 > c by A4,XXREAL_0:2;
r1 in dom I by A5,A19,A4,XXREAL_0:2,XXREAL_1:236; then
g1+integral(f,c,b) > I.r1 by A17,A19; then
A21: g1 + integral(f,c,b) > integral(f,c,r1) by A6,A20,A5,XXREAL_1:236;
A22: f is_integrable_on ['c,r1'] & f|['c,r1'] is bounded by A20,A2;
A23: ['c,r1'] = [.c,r1.] by A19,A4,XXREAL_0:2,INTEGRA5:def 3; then
['c,r1'] c= [.c,+infty.[ by XXREAL_1:251; then
A24: ['c,r1'] c= dom f by A1;
b in ['c,r1'] by A23,A19,A4,XXREAL_1:1; then
integral(f,c,r1) = integral(f,b,r1) + integral(f,c,b)
by A20,A22,A24,INTEGRA6:17; then
g1 > integral(f,b,r1) by A21,XREAL_1:6;
hence g1 > Intf.r1 by A11,A18;
end;
end;
hence
A25: f is_+infty_improper_integrable_on b
by A10,A11,A1,A2,A4,Lm10,A12,LIMFUNC1:47;
Intf is divergent_in+infty_to-infty by A12,A16,LIMFUNC1:47;
hence improper_integral_+infty(f,b) = -infty by A10,A11,A25,Def4;
end;
theorem Th30:
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 )
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b >= c and
A2: right_closed_halfline c c= dom f and
A3: f is_+infty_improper_integrable_on c;
per cases;
suppose f is_+infty_ext_Riemann_integrable_on c; then
improper_integral_+infty(f,c) = infty_ext_right_integral(f,c)
by A3,Th27;
hence thesis by A1,A2,A3,Lm11;
end;
suppose not f is_+infty_ext_Riemann_integrable_on c; then
per cases by A3,Th27;
suppose improper_integral_+infty(f,c) = +infty;
hence thesis by A1,A2,A3,Lm12;
end;
suppose improper_integral_+infty(f,c) = -infty;
hence thesis by A1,A2,A3,Lm13;
end;
end;
end;
Lm14:
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 for d be Real st d >= c holds
f is_integrable_on ['c,d'] & f|['c,d'] is bounded
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b >= c and
A2: right_closed_halfline c c= dom f and
A3: f|['c,b'] is bounded and
A4: f is_+infty_improper_integrable_on b and
A5: f is_integrable_on ['c,b'];
hereby let d be Real;
assume
A6: d >= c; then
['c,d'] = [.c,d.] by INTEGRA5:def 3; then
['c,d'] c= [.c,+infty.[ by XXREAL_1:251; then
A7: ['c,d'] c= dom f by A2;
A8: ['c,b'] = [.c,b.] & ['c,d'] = [.c,d.] by A1,A6,INTEGRA5:def 3;
per cases;
suppose A9: d >= b; then
A10: f is_integrable_on ['b,d'] & f|['b,d'] is bounded by A4;
hence f is_integrable_on ['c,d'] by A9,A1,A7,A3,A5,INTEGR24:1;
['b,d'] = [.b,d.] by A9,INTEGRA5:def 3; then
['b,d'] \/ ['c,b'] = [.c,d.] by A9,A1,A8,XXREAL_1:165;
hence f|['c,d'] is bounded by A10,A3,A8,RFUNCT_1:87;
end;
suppose A11: b > d;
[.c,b.] c= [.c,+infty.[ by XXREAL_1:251; then
A12: ['c,b'] c= dom f by A2,A8;
d in ['c,b'] by A8,A11,A6,XXREAL_1:1;
hence f is_integrable_on ['c,d'] by A1,A3,A5,A12,INTEGRA6:17;
thus f|['c,d'] is bounded by A3,A11,A8,XXREAL_1:34,RFUNCT_1:74;
end;
end;
end;
Lm15:
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']
& improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
holds f is_+infty_improper_integrable_on c
& improper_integral_+infty(f,c)
= improper_integral_+infty(f,b) + integral(f,c,b)
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b >= c and
A2: right_closed_halfline c c= dom f and
A3: f|['c,b'] is bounded and
A4: f is_+infty_improper_integrable_on b and
A5: f is_integrable_on ['c,b'] and
A6: improper_integral_+infty(f,b) = infty_ext_right_integral(f,b);
consider I be PartFunc of REAL,REAL such that
A7: dom I = right_closed_halfline b and
A8: for x be Real st x in dom I holds I.x = integral(f,b,x) and
A9: (I is convergent_in+infty or I is divergent_in+infty_to+infty
or I is divergent_in+infty_to-infty) by A4;
A10: now assume I is divergent_in+infty_to+infty; then
not f is_+infty_ext_Riemann_integrable_on b by A7,A8,Th28;
hence contradiction by A4,A6,Th27;
end;
now assume I is divergent_in+infty_to-infty; then
not f is_+infty_ext_Riemann_integrable_on b by A7,A8,Th28;
hence contradiction by A4,A6,Th27;
end; then
f is_+infty_ext_Riemann_integrable_on b
by A4,A7,A8,A9,A10,INTEGR10:def 5; then
A11: f is_+infty_ext_Riemann_integrable_on c
& infty_ext_right_integral(f,c)
= infty_ext_right_integral(f,b) + integral(f,c,b)
by A1,A2,A3,A5,Th18;
ex Intf be PartFunc of REAL,REAL st dom Intf = right_closed_halfline c &
(for x be Real st x in dom Intf holds Intf.x = integral(f,c,x)) &
Intf is convergent_in+infty by A11,INTEGR10:def 5;
hence f is_+infty_improper_integrable_on c by A1,A2,A3,A4,A5,Lm14; then
improper_integral_+infty(f,c)
= infty_ext_right_integral(f,b) + integral(f,c,b) by A11,Th27;
hence improper_integral_+infty(f,c)
= improper_integral_+infty(f,b) + integral(f,c,b)
by A6,XXREAL_3:def 2;
end;
Lm16:
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']
& improper_integral_+infty(f,b) = +infty
holds f is_+infty_improper_integrable_on c
& improper_integral_+infty(f,c) = +infty
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b >= c and
A2: right_closed_halfline c c= dom f and
A3: f|['c,b'] is bounded and
A4: f is_+infty_improper_integrable_on b and
A5: f is_integrable_on ['c,b'] and
A6: improper_integral_+infty(f,b) = +infty;
consider I be PartFunc of REAL,REAL such that
A7: dom I = right_closed_halfline b and
A8: for x be Real st x in dom I holds I.x = integral(f,b,x) and
A9: (I is convergent_in+infty or I is divergent_in+infty_to+infty
or I is divergent_in+infty_to-infty) by A4;
improper_integral_+infty(f,b) <> infty_ext_right_integral(f,b)
by A6; then
A10: not f is_+infty_ext_Riemann_integrable_on b by A4,Th27;
+infty > c by XREAL_0:def 1,XXREAL_0:9; then
reconsider AC = [.c,+infty.[ as non empty Subset of REAL by XXREAL_1:3;
deffunc F(Element of AC) = In(integral(f,c,$1),REAL);
consider Intf be Function of AC,REAL such that
A11: for x be Element of AC holds Intf.x = F(x) from FUNCT_2:sch 4;
A12: dom Intf = AC by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A13: for x be Real st x in dom Intf holds Intf.x = integral(f,c,x)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,c,x),REAL) by A11,A12;
hence thesis;
end;
A14: for r be Real ex g be Real st g > r & g in dom Intf
proof
let r be Real;
consider g be Real such that
A15: g > r & g in dom I
by A10,A6,A7,Def4,INTEGR10:def 5,A4,LIMFUNC1:46;
[.b,+infty.[ c= [.c,+infty.[ by A1,XXREAL_1:38;
hence thesis by A15,A7,A12;
end;
A16: for g1 be Real ex r be Real st for r1 be Real st r1 > r &
r1 in dom Intf holds g1 < Intf.r1
proof
let g1 be Real;
consider r be Real such that
A17: for r1 be Real st r1 > r & r1 in dom I
holds g1-integral(f,c,b) < I.r1
by A10,A9,A4,A6,A7,A8,Def4,INTEGR10:def 5,LIMFUNC1:46;
set R = max(b,r);
take R;
thus for r1 be Real st r1 > R & r1 in dom Intf holds g1 < Intf.r1
proof
let r1 be Real;
assume A18: r1 > R & r1 in dom Intf;
A19: R >= b & R >= r by XXREAL_0:25; then
A20: r1 > b & r1 > r by A18,XXREAL_0:2; then
A21: r1 > c by A1,XXREAL_0:2;
r1 in dom I by A7,A19,A18,XXREAL_0:2,XXREAL_1:236; then
g1-integral(f,c,b) < I.r1 by A17,A20; then
A22: g1-integral(f,c,b) < integral(f,b,r1) by A8,A20,A7,XXREAL_1:236;
A23: f is_integrable_on ['c,r1'] & f|['c,r1'] is bounded
by A21,A1,A2,A3,A4,A5,Lm14;
A24: ['c,r1'] = [.c,r1.] by A20,A1,XXREAL_0:2,INTEGRA5:def 3; then
['c,r1'] c= [.c,+infty.[ by XXREAL_1:251; then
A25: ['c,r1'] c= dom f by A2;
b in ['c,r1'] by A24,A20,A1,XXREAL_1:1; then
integral(f,c,r1) = integral(f,b,r1) + integral(f,c,b)
by A21,A23,A25,INTEGRA6:17; then
integral(f,b,r1) = integral(f,c,r1) - integral(f,c,b); then
g1 < integral(f,c,r1) by A22,XREAL_1:9;
hence g1 < Intf.r1 by A13,A18;
end;
end;
hence
A26: f is_+infty_improper_integrable_on c
by A12,A13,A14,A1,A2,A3,A4,A5,Lm14,LIMFUNC1:46;
Intf is divergent_in+infty_to+infty by A14,A16,LIMFUNC1:46;
hence improper_integral_+infty(f,c) = +infty by A12,A13,A26,Def4;
end;
Lm17:
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']
& improper_integral_+infty(f,b) = -infty
holds f is_+infty_improper_integrable_on c
& improper_integral_+infty(f,c) = -infty
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b >= c and
A2: right_closed_halfline c c= dom f and
A3: f|['c,b'] is bounded and
A4: f is_+infty_improper_integrable_on b and
A5: f is_integrable_on ['c,b'] and
A6: improper_integral_+infty(f,b) = -infty;
consider I be PartFunc of REAL,REAL such that
A7: dom I = right_closed_halfline b and
A8: for x be Real st x in dom I holds I.x = integral(f,b,x) and
A9: (I is convergent_in+infty or I is divergent_in+infty_to+infty
or I is divergent_in+infty_to-infty) by A4;
improper_integral_+infty(f,b) <> infty_ext_right_integral(f,b)
by A6; then
A10: not f is_+infty_ext_Riemann_integrable_on b by A4,Th27;
+infty > c by XREAL_0:def 1,XXREAL_0:9; then
reconsider AC = [.c,+infty.[ as non empty Subset of REAL by XXREAL_1:3;
deffunc F(Element of AC) = In(integral(f,c,$1),REAL);
consider Intf be Function of AC,REAL such that
A11: for x be Element of AC holds Intf.x = F(x) from FUNCT_2:sch 4;
A12: dom Intf = AC by FUNCT_2:def 1; then
reconsider Intf as PartFunc of REAL,REAL by RELSET_1:5;
A13: for x be Real st x in dom Intf holds Intf.x = integral(f,c,x)
proof
let x be Real;
assume x in dom Intf; then
Intf.x = In(integral(f,c,x),REAL) by A11,A12;
hence thesis;
end;
A14: for r be Real ex g be Real st g > r & g in dom Intf
proof
let r be Real;
consider g be Real such that
A15: g > r & g in dom I
by A10,A6,A7,Def4,INTEGR10:def 5,A4,LIMFUNC1:47;
[.b,+infty.[ c= [.c,+infty.[ by A1,XXREAL_1:38;
hence thesis by A15,A7,A12;
end;
A16: for g1 be Real ex r be Real st for r1 be Real st r1 > r &
r1 in dom Intf holds g1 > Intf.r1
proof
let g1 be Real;
consider r be Real such that
A17: for r1 be Real st r1 > r & r1 in dom I
holds g1-integral(f,c,b) > I.r1
by A10,A9,A4,A6,A7,A8,Def4,INTEGR10:def 5,LIMFUNC1:47;
set R = max(b,r);
take R;
thus for r1 be Real st r1 > R & r1 in dom Intf holds g1 > Intf.r1
proof
let r1 be Real;
assume A18: r1 > R & r1 in dom Intf;
A19: R >= b & R >= r by XXREAL_0:25; then
A20: r1 > b & r1 > r by A18,XXREAL_0:2; then
A21: r1 > c by A1,XXREAL_0:2;
r1 in dom I by A7,A19,A18,XXREAL_0:2,XXREAL_1:236; then
g1-integral(f,c,b) > I.r1 by A17,A20; then
A22: g1-integral(f,c,b) > integral(f,b,r1) by A8,A20,A7,XXREAL_1:236;
A23: f is_integrable_on ['c,r1'] & f|['c,r1'] is bounded
by A21,A1,A2,A3,A4,A5,Lm14;
A24: ['c,r1'] = [.c,r1.] by A20,A1,XXREAL_0:2,INTEGRA5:def 3; then
['c,r1'] c= [.c,+infty.[ by XXREAL_1:251; then
A25: ['c,r1'] c= dom f by A2;
b in ['c,r1'] by A24,A20,A1,XXREAL_1:1; then
integral(f,c,r1) = integral(f,b,r1) + integral(f,c,b)
by A21,A23,A25,INTEGRA6:17; then
integral(f,b,r1) = integral(f,c,r1) - integral(f,c,b); then
g1 > integral(f,c,r1) by A22,XREAL_1:9;
hence g1 > Intf.r1 by A13,A18;
end;
end;
hence
A26: f is_+infty_improper_integrable_on c
by A12,A13,A14,A1,A2,A3,A4,A5,Lm14,LIMFUNC1:47;
Intf is divergent_in+infty_to-infty by A14,A16,LIMFUNC1:47;
hence improper_integral_+infty(f,c) = -infty by A12,A13,A26,Def4;
end;
theorem Th31:
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 )
proof
let f be PartFunc of REAL,REAL, b,c be Real;
assume that
A1: b >= c and
A2: right_closed_halfline c c= dom f and
A3: f|['c,b'] is bounded and
A4: f is_+infty_improper_integrable_on b and
A5: f is_integrable_on ['c,b'];
per cases;
suppose f is_+infty_ext_Riemann_integrable_on b; then
improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A4,Th27;
hence thesis by A1,A2,A3,A4,A5,Lm15;
end;
suppose A6: not f is_+infty_ext_Riemann_integrable_on b;
per cases by A4,A6,Th27;
suppose improper_integral_+infty(f,b) = +infty;
hence thesis by A1,A2,A3,A4,A5,Lm16;
end;
suppose improper_integral_+infty(f,b) = -infty;
hence thesis by A1,A2,A3,A4,A5,Lm17;
end;
end;
end;
definition
let f be PartFunc of REAL,REAL;
pred f is_improper_integrable_on_REAL means
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
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)
proof
let f be PartFunc of REAL,REAL;
assume f is_improper_integrable_on_REAL; then
consider b be Real such that
A1: f is_-infty_improper_integrable_on b and
A2: f is_+infty_improper_integrable_on b and
A3: not(improper_integral_-infty(f,b) = -infty &
improper_integral_+infty(f,b) = +infty) and
A4: not(improper_integral_-infty(f,b) = +infty &
improper_integral_+infty(f,b) = -infty);
consider IL be PartFunc of REAL,REAL such that
A5: dom IL = left_closed_halfline b and
A6: for x be Real st x in dom IL holds IL.x = integral(f,x,b) and
A7: IL is convergent_in-infty or IL is divergent_in-infty_to+infty
or IL is divergent_in-infty_to-infty by A1;
consider IR be PartFunc of REAL,REAL such that
A8: dom IR = right_closed_halfline b and
A9: for x be Real st x in dom IR holds IR.x = integral(f,b,x) and
A10: IR is convergent_in+infty or IR is divergent_in+infty_to+infty
or IR is divergent_in+infty_to-infty by A2;
per cases by A7;
suppose IL is convergent_in-infty; then
f is_-infty_ext_Riemann_integrable_on b
by A1,A5,A6,INTEGR10:def 6; then
A11: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
by A1,Th22;
per cases by A10;
suppose IR is convergent_in+infty; then
f is_+infty_ext_Riemann_integrable_on b
by A2,A8,A9,INTEGR10:def 5; then
improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A2,Th27;
hence thesis by A11;
end;
suppose IR is divergent_in+infty_to+infty; then
improper_integral_+infty(f,b) = +infty by A2,A8,A9,Def4; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = +infty
by A11,XXREAL_3:def 2;
hence thesis;
end;
suppose IR is divergent_in+infty_to-infty; then
improper_integral_+infty(f,b) = -infty by A2,A8,A9,Def4; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = -infty
by A11,XXREAL_3:def 2;
hence thesis;
end;
end;
suppose A12: IL is divergent_in-infty_to+infty; then
A13: improper_integral_-infty(f,b) = +infty by A1,A5,A6,Def3;
per cases by A10,A2,A8,A9,A12,A4,A1,A5,A6,Def3,Def4;
suppose IR is convergent_in+infty; then
f is_+infty_ext_Riemann_integrable_on b
by A2,A8,A9,INTEGR10:def 5; then
improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A2,Th27; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = +infty
by A13,XXREAL_3:def 2;
hence thesis;
end;
suppose IR is divergent_in+infty_to+infty; then
improper_integral_+infty(f,b) = +infty by A2,A8,A9,Def4; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = +infty
by A13,XXREAL_3:def 2;
hence thesis;
end;
end;
suppose A14: IL is divergent_in-infty_to-infty; then
A15: improper_integral_-infty(f,b) = -infty by A1,A5,A6,Def3;
per cases by A10,A2,A8,A9,A14,A3,A1,A5,A6,Def3,Def4;
suppose IR is convergent_in+infty; then
f is_+infty_ext_Riemann_integrable_on b
by A2,A8,A9,INTEGR10:def 5; then
improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A2,Th27; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = -infty
by A15,XXREAL_3:def 2;
hence thesis;
end;
suppose IR is divergent_in+infty_to-infty; then
improper_integral_+infty(f,b) = -infty by A2,A8,A9,Def4; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b) = -infty
by A15,XXREAL_3:def 2;
hence thesis;
end;
end;
end;
theorem Th33:
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)
proof
let f be PartFunc of REAL,REAL, b be Real;
assume that
A1: dom f = REAL and
A2: f is_-infty_improper_integrable_on b and
A3: f is_+infty_improper_integrable_on b and
A4: not (improper_integral_-infty(f,b) = -infty
& improper_integral_+infty(f,b) = +infty) and
A5: not (improper_integral_-infty(f,b) = +infty
& improper_integral_+infty(f,b) = -infty);
A6: left_closed_halfline b c= dom f & right_closed_halfline b c= dom f by A1;
let b1 be Real;
assume
A7: b1 <= b; then
A8: f is_integrable_on ['b1,b'] & f|['b1,b'] is bounded by A2;
A9: right_closed_halfline b1 c= dom f & [.b1,b.] c= dom f by A1;
per cases by A2,Th22;
suppose f is_-infty_ext_Riemann_integrable_on b; then
A10: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
by A2,Th22; then
A11: f is_-infty_improper_integrable_on b1
& improper_integral_-infty(f,b1) = infty_ext_left_integral(f,b1)
by A1,A7,A2,Lm3;
A12: improper_integral_-infty(f,b)
= improper_integral_-infty(f,b1)+integral(f,b1,b)
by A7,A6,A8,A11,Lm7
.= infty_ext_left_integral(f,b1) +integral(f,b1,b) by A11,XXREAL_3:def 2;
per cases by A3,Th27;
suppose A13: f is_+infty_ext_Riemann_integrable_on b; then
A14: improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A3,Th27; then
improper_integral_+infty(f,b1)
= improper_integral_+infty(f,b) + integral(f,b1,b)
by A7,A9,A8,A3,Th31
.= infty_ext_right_integral(f,b) + integral(f,b1,b)
by A14,XXREAL_3:def 2; then
improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1)
= infty_ext_left_integral(f,b1)
+ (infty_ext_right_integral(f,b) + integral(f,b1,b))
by A11,XXREAL_3:def 2
.= infty_ext_left_integral(f,b1)
+ integral(f,b1,b) + infty_ext_right_integral(f,b)
.= improper_integral_-infty(f,b) + infty_ext_right_integral(f,b)
by A12,XXREAL_3:def 2;
hence thesis by A13,A3,Th27;
end;
suppose A15: improper_integral_+infty(f,b) = +infty;
improper_integral_+infty(f,b1) = +infty
by A7,A9,A8,A3,A15,Th31; then
improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1)
= +infty by A11,XXREAL_3:def 2;
hence thesis by A15,A10,XXREAL_3:def 2;
end;
suppose A16: improper_integral_+infty(f,b) = -infty;
improper_integral_+infty(f,b1) = -infty
by A7,A9,A8,A3,A16,Th31; then
improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1)
= -infty by A11,XXREAL_3:def 2;
hence thesis by A16,A10,XXREAL_3:def 2;
end;
end;
suppose A17: improper_integral_-infty(f,b) = +infty;
A18: improper_integral_-infty(f,b1) = +infty by A1,A2,A17,A7,Lm4;
per cases;
suppose f is_+infty_ext_Riemann_integrable_on b; then
A19: improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A3,Th27; then
improper_integral_+infty(f,b1)
= improper_integral_+infty(f,b) + integral(f,b1,b)
by A7,A9,A8,A3,Th31
.= infty_ext_right_integral(f,b) + integral(f,b1,b)
by A19,XXREAL_3:def 2; then
improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1)
= +infty by A18,XXREAL_3:def 2;
hence thesis by A17,A19,XXREAL_3:def 2;
end;
suppose not f is_+infty_ext_Riemann_integrable_on b; then
improper_integral_+infty(f,b) = +infty by A17,A5,A3,Th27;
hence thesis by A17,A18,A7,A9,A8,A3,Th31;
end;
end;
suppose A20: improper_integral_-infty(f,b) = -infty;
A21: improper_integral_-infty(f,b1) = -infty by A1,A2,A20,A7,Lm5;
per cases;
suppose f is_+infty_ext_Riemann_integrable_on b; then
A22: improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A3,Th27; then
improper_integral_+infty(f,b1)
= improper_integral_+infty(f,b) + integral(f,b1,b)
by A7,A9,A8,A3,Th31
.= infty_ext_right_integral(f,b) + integral(f,b1,b)
by A22,XXREAL_3:def 2; then
improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1)
= -infty by A21,XXREAL_3:def 2;
hence thesis by A20,A22,XXREAL_3:def 2;
end;
suppose not f is_+infty_ext_Riemann_integrable_on b; then
improper_integral_+infty(f,b) = -infty by A20,A4,A3,Th27;
hence thesis by A20,A21,A7,A9,A8,A3,Th31;
end;
end;
end;
theorem Th34:
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)
proof
let f be PartFunc of REAL,REAL, b be Real;
assume that
A1: dom f = REAL and
A2: f is_-infty_improper_integrable_on b and
A3: f is_+infty_improper_integrable_on b and
A4: not (improper_integral_-infty(f,b) = -infty
& improper_integral_+infty(f,b) = +infty) and
A5: not (improper_integral_-infty(f,b) = +infty
& improper_integral_+infty(f,b) = -infty);
let b2 be Real;
assume
A6: b <= b2;
A7: left_closed_halfline b c= dom f & right_closed_halfline b c= dom f by A1;
A8: left_closed_halfline b2 c= dom f & [.b,b2.] c= dom f by A1;
A9: f is_integrable_on ['b,b2'] & f|['b,b2'] is bounded by A6,A3;
per cases by A3,Th27;
suppose f is_+infty_ext_Riemann_integrable_on b; then
A10: improper_integral_+infty(f,b) = infty_ext_right_integral(f,b)
by A3,Th27; then
A11: f is_+infty_improper_integrable_on b2
& improper_integral_+infty(f,b2) = infty_ext_right_integral(f,b2)
by A6,A1,A3,Th30;
A12: improper_integral_+infty(f,b)
= improper_integral_+infty(f,b2)+integral(f,b,b2)
by A6,A7,A9,A11,Th31
.= infty_ext_right_integral(f,b2) +integral(f,b,b2)
by A11,XXREAL_3:def 2;
per cases by A2,Th22;
suppose A13: f is_-infty_ext_Riemann_integrable_on b; then
A14: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
by A2,Th22; then
improper_integral_-infty(f,b2)
= improper_integral_-infty(f,b) + integral(f,b,b2)
by A6,A8,A9,A2,Lm7
.= infty_ext_left_integral(f,b) + integral(f,b,b2)
by A14,XXREAL_3:def 2; then
improper_integral_+infty(f,b2)+improper_integral_-infty(f,b2)
= infty_ext_right_integral(f,b2)
+ (infty_ext_left_integral(f,b) + integral(f,b,b2))
by A11,XXREAL_3:def 2
.= infty_ext_right_integral(f,b2)
+ integral(f,b,b2) + infty_ext_left_integral(f,b)
.= improper_integral_+infty(f,b) + infty_ext_left_integral(f,b)
by A12,XXREAL_3:def 2;
hence thesis by A13,A2,Th22;
end;
suppose A15: improper_integral_-infty(f,b) = +infty;
improper_integral_-infty(f,b2) = +infty
by A6,A8,A9,A2,A15,Lm8; then
improper_integral_+infty(f,b2)+improper_integral_-infty(f,b2)
= +infty by A11,XXREAL_3:def 2;
hence thesis by A15,A10,XXREAL_3:def 2;
end;
suppose A16: improper_integral_-infty(f,b) = -infty;
improper_integral_-infty(f,b2) = -infty
by A6,A8,A9,A2,A16,Lm9; then
improper_integral_+infty(f,b2)+improper_integral_-infty(f,b2)
= -infty by A11,XXREAL_3:def 2;
hence thesis by A16,A10,XXREAL_3:def 2;
end;
end;
suppose A17: improper_integral_+infty(f,b) = +infty;
A18: improper_integral_+infty(f,b2) = +infty by A1,A3,A17,A6,Th30;
per cases;
suppose f is_-infty_ext_Riemann_integrable_on b; then
A19: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
by A2,Th22; then
improper_integral_-infty(f,b2)
= improper_integral_-infty(f,b) + integral(f,b,b2)
by A6,A8,A9,A2,Lm7
.= infty_ext_left_integral(f,b) + integral(f,b,b2)
by A19,XXREAL_3:def 2; then
improper_integral_+infty(f,b2)+improper_integral_-infty(f,b2)
= +infty by A18,XXREAL_3:def 2;
hence thesis by A17,A19,XXREAL_3:def 2;
end;
suppose not f is_-infty_ext_Riemann_integrable_on b; then
improper_integral_-infty(f,b) = +infty by A17,A4,A2,Th22;
hence thesis by A17,A18,A6,A8,A9,A2,Lm8;
end;
end;
suppose A20: improper_integral_+infty(f,b) = -infty;
A21: improper_integral_+infty(f,b2) = -infty by A1,A3,A20,A6,Th30;
per cases;
suppose f is_-infty_ext_Riemann_integrable_on b; then
A22: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
by A2,Th22; then
improper_integral_-infty(f,b2)
= improper_integral_-infty(f,b) + integral(f,b,b2)
by A6,A8,A9,A2,Lm7
.= infty_ext_left_integral(f,b) + integral(f,b,b2)
by A22,XXREAL_3:def 2; then
improper_integral_+infty(f,b2)+improper_integral_-infty(f,b2)
= -infty by A21,XXREAL_3:def 2;
hence thesis by A20,A22,XXREAL_3:def 2;
end;
suppose not f is_-infty_ext_Riemann_integrable_on b; then
improper_integral_-infty(f,b) = -infty by A20,A5,A2,Th22;
hence thesis by A20,A21,A6,A8,A9,A2,Lm9;
end;
end;
end;
theorem Th35:
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)
proof
let f be PartFunc of REAL,REAL;
assume that
A1: dom f = REAL and
A2: f is_improper_integrable_on_REAL;
let b1,b2 be Real;
consider b be Real such that
A3: f is_-infty_improper_integrable_on b and
A4: f is_+infty_improper_integrable_on b and
A5: not (improper_integral_-infty(f,b) = -infty
& improper_integral_+infty(f,b) = +infty) and
A6: not (improper_integral_-infty(f,b) = +infty
& improper_integral_+infty(f,b) = -infty) by A2;
per cases;
suppose b1 < b & b2 < b; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b)
= improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1)
& improper_integral_-infty(f,b)+improper_integral_+infty(f,b)
= improper_integral_-infty(f,b2)+improper_integral_+infty(f,b2)
by A1,A3,A4,A5,A6,Th33;
hence thesis;
end;
suppose b1 < b & b <= b2; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b)
= improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1)
& improper_integral_-infty(f,b)+improper_integral_+infty(f,b)
= improper_integral_-infty(f,b2)+improper_integral_+infty(f,b2)
by A1,A3,A4,A5,A6,Th33,Th34;
hence thesis;
end;
suppose b <= b1 & b2 < b; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b)
= improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1)
& improper_integral_-infty(f,b)+improper_integral_+infty(f,b)
= improper_integral_-infty(f,b2)+improper_integral_+infty(f,b2)
by A1,A3,A4,A5,A6,Th33,Th34;
hence thesis;
end;
suppose b <= b1 & b <= b2; then
improper_integral_-infty(f,b)+improper_integral_+infty(f,b)
= improper_integral_-infty(f,b1)+improper_integral_+infty(f,b1)
& improper_integral_-infty(f,b)+improper_integral_+infty(f,b)
= improper_integral_-infty(f,b2)+improper_integral_+infty(f,b2)
by A1,A3,A4,A5,A6,Th34;
hence thesis;
end;
end;
definition
let f be PartFunc of REAL,REAL;
assume
A1: dom f = REAL & f is_improper_integrable_on_REAL;
func improper_integral_on_REAL f -> ExtReal means
:Def6:
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);
existence
proof
consider c be Real such that
A2: f is_-infty_improper_integrable_on c and
A3: f is_+infty_improper_integrable_on c and
A4: not (improper_integral_-infty(f,c) = -infty
& improper_integral_+infty(f,c) = +infty) and
A5: not (improper_integral_-infty(f,c) = +infty
& improper_integral_+infty(f,c) = -infty) by A1;
per cases by A2,Th22;
suppose
A6: f is_-infty_ext_Riemann_integrable_on c &
improper_integral_-infty(f,c) = infty_ext_left_integral(f,c);
per cases by A3,Th27;
suppose
A7: f is_+infty_ext_Riemann_integrable_on c &
improper_integral_+infty(f,c) = infty_ext_right_integral(f,c);
reconsider
IT = infty_ext_left_integral(f,c) + infty_ext_right_integral(f,c)
as ExtReal;
take IT;
IT = improper_integral_-infty(f,c)+improper_integral_+infty(f,c)
by A6,A7,XXREAL_3:def 2;
hence thesis by A2,A3;
end;
suppose improper_integral_+infty(f,c) = +infty; then
A8: improper_integral_-infty(f,c) + improper_integral_+infty(f,c) = +infty
by A4,XXREAL_3:def 2;
take IT = +infty;
thus thesis by A2,A3,A8;
end;
suppose improper_integral_+infty(f,c) = -infty; then
A9: improper_integral_-infty(f,c) + improper_integral_+infty(f,c) = -infty
by A5,XXREAL_3:def 2;
take IT = -infty;
thus thesis by A2,A3,A9;
end;
end;
suppose
A10: improper_integral_-infty(f,c) = +infty;
per cases by A3,A5,A10,Th27;
suppose
f is_+infty_ext_Riemann_integrable_on c &
improper_integral_+infty(f,c) = infty_ext_right_integral(f,c); then
A11: improper_integral_-infty(f,c) + improper_integral_+infty(f,c) = +infty
by A10,XXREAL_3:def 2;
take IT = +infty;
thus thesis by A2,A3,A11;
end;
suppose
improper_integral_+infty(f,c) = +infty; then
A12: improper_integral_-infty(f,c) + improper_integral_+infty(f,c) = +infty
by A10,XXREAL_3:def 2;
take IT = +infty;
thus thesis by A2,A3,A12;
end;
end;
suppose
A13: improper_integral_-infty(f,c) = -infty;
per cases by A3,A4,A13,Th27;
suppose
f is_+infty_ext_Riemann_integrable_on c &
improper_integral_+infty(f,c) = infty_ext_right_integral(f,c); then
A14: improper_integral_-infty(f,c) + improper_integral_+infty(f,c) = -infty
by A13,XXREAL_3:def 2;
take IT = -infty;
thus thesis by A2,A3,A14;
end;
suppose
improper_integral_+infty(f,c) = -infty; then
A15: improper_integral_-infty(f,c) + improper_integral_+infty(f,c) = -infty
by A13,XXREAL_3:def 2;
take IT = -infty;
thus thesis by A2,A3,A15;
end;
end;
end;
uniqueness by A1,Th35;
end;
theorem Th36:
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)
proof
let f be PartFunc of REAL,REAL, b be Real;
assume that
A1: dom f = REAL and
A2: f is_improper_integrable_on_REAL;
consider b1 be Real such that
A3: f is_-infty_improper_integrable_on b1 and
A4: f is_+infty_improper_integrable_on b1 and
A5: improper_integral_on_REAL f
= improper_integral_-infty(f,b1) + improper_integral_+infty(f,b1)
by A1,A2,Def6;
per cases;
suppose A6: b < b1;
hence f is_-infty_improper_integrable_on b by A3,A1,Th25;
A7: right_closed_halfline b c= dom f by A1;
f|['b,b1'] is bounded & f is_integrable_on ['b,b1'] by A3,A6;
hence f is_+infty_improper_integrable_on b by A6,A4,A7,Th31;
thus thesis by A1,A2,A5,Th35;
end;
suppose A8: b >= b1;
A9: left_closed_halfline b c= dom f by A1;
f|['b1,b'] is bounded & f is_integrable_on ['b1,b'] by A4,A8;
hence f is_-infty_improper_integrable_on b by A3,A8,A9,Th26;
thus f is_+infty_improper_integrable_on b by A8,A1,A4,Th30;
thus thesis by A1,A2,A5,Th35;
end;
end;
begin :: Linearity of Improper Integral on Infinite Interval
theorem Th37:
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
proof
let f be PartFunc of REAL,REAL, b be Real;
assume that
A1: f is_-infty_improper_integrable_on b and
A2: improper_integral_-infty(f,b) = +infty;
let Intf be PartFunc of REAL,REAL;
assume that
A3: dom Intf = left_closed_halfline b and
A4: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b);
consider I be PartFunc of REAL,REAL such that
A5: dom I = left_closed_halfline b &
(for x be Real st x in dom I holds I.x = integral(f,x,b))
& (I is convergent_in-infty
& improper_integral_-infty(f,b) = lim_in-infty I
or I is divergent_in-infty_to+infty
& improper_integral_-infty(f,b) = +infty
or I is divergent_in-infty_to-infty
& improper_integral_-infty(f,b) = -infty) by A1,Def3;
for x be Element of REAL st x in dom I holds I.x = Intf.x
proof
let x be Element of REAL;
assume x in dom I; then
I.x = integral(f,x,b) & Intf.x = integral(f,x,b) by A3,A4,A5;
hence thesis;
end;
hence Intf is divergent_in-infty_to+infty by A2,A3,A5,PARTFUN1:5;
end;
theorem Th38:
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
proof
let f be PartFunc of REAL,REAL, b be Real;
assume that
A1: f is_-infty_improper_integrable_on b and
A2: improper_integral_-infty(f,b) = -infty;
let Intf be PartFunc of REAL,REAL;
assume that
A3: dom Intf = left_closed_halfline b and
A4: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b);
consider I be PartFunc of REAL,REAL such that
A5: dom I = left_closed_halfline b &
(for x be Real st x in dom I holds I.x = integral(f,x,b))
& (I is convergent_in-infty
& improper_integral_-infty(f,b) = lim_in-infty I
or I is divergent_in-infty_to+infty
& improper_integral_-infty(f,b) = +infty
or I is divergent_in-infty_to-infty
& improper_integral_-infty(f,b) = -infty) by A1,Def3;
for x be Element of REAL st x in dom I holds I.x = Intf.x
proof
let x be Element of REAL;
assume x in dom I; then
I.x = integral(f,x,b) & Intf.x = integral(f,x,b) by A3,A4,A5;
hence thesis;
end;
hence Intf is divergent_in-infty_to-infty by A2,A3,A5,PARTFUN1:5;
end;
theorem Th39:
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
proof
let f be PartFunc of REAL,REAL, a be Real;
assume that
A1: f is_+infty_improper_integrable_on a and
A2: improper_integral_+infty(f,a) = +infty;
let Intf be PartFunc of REAL,REAL;
assume that
A3: dom Intf = right_closed_halfline a and
A4: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x);
consider I be PartFunc of REAL,REAL such that
A5: dom I = right_closed_halfline a &
(for x be Real st x in dom I holds I.x = integral(f,a,x))
& (I is convergent_in+infty
& improper_integral_+infty(f,a) = lim_in+infty I
or I is divergent_in+infty_to+infty
& improper_integral_+infty(f,a) = +infty
or I is divergent_in+infty_to-infty
& improper_integral_+infty(f,a) = -infty) by A1,Def4;
for x be Element of REAL st x in dom I holds I.x = Intf.x
proof
let x be Element of REAL;
assume x in dom I; then
I.x = integral(f,a,x) & Intf.x = integral(f,a,x) by A3,A4,A5;
hence thesis;
end;
hence Intf is divergent_in+infty_to+infty by A2,A3,A5,PARTFUN1:5;
end;
theorem Th40:
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
proof
let f be PartFunc of REAL,REAL, a be Real;
assume that
A1: f is_+infty_improper_integrable_on a and
A2: improper_integral_+infty(f,a) = -infty;
let Intf be PartFunc of REAL,REAL;
assume that
A3: dom Intf = right_closed_halfline a and
A4: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x);
consider I be PartFunc of REAL,REAL such that
A5: dom I = right_closed_halfline a &
(for x be Real st x in dom I holds I.x = integral(f,a,x))
& (I is convergent_in+infty
& improper_integral_+infty(f,a) = lim_in+infty I
or I is divergent_in+infty_to+infty
& improper_integral_+infty(f,a) = +infty
or I is divergent_in+infty_to-infty
& improper_integral_+infty(f,a) = -infty) by A1,Def4;
for x be Element of REAL st x in dom I holds I.x = Intf.x
proof
let x be Element of REAL;
assume x in dom I; then
I.x = integral(f,a,x) & Intf.x = integral(f,a,x) by A3,A4,A5;
hence thesis;
end;
hence Intf is divergent_in+infty_to-infty by A2,A3,A5,PARTFUN1:5;
end;
theorem Th41:
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)
proof
let f be PartFunc of REAL,REAL, b,r be Real;
assume that
A1: left_closed_halfline b c= dom f and
A2: f is_-infty_improper_integrable_on b;
A3: for d be Real st d <= b holds r(#)f is_integrable_on [' d,b ']
& (r(#)f)|[' d,b '] is bounded
proof
let d be Real;
assume
A4: d <= b;
[.d,b.] c= ].-infty,b.] by XXREAL_1:265; then
[.d,b.] c= dom f by A1; then
A5: ['d,b'] c= dom f by A4,INTEGRA5:def 3;
A6: f is_integrable_on ['d,b'] & f|['d,b'] is bounded by A2,A4;
hence r(#)f is_integrable_on ['d,b'] by A5,INTEGRA6:9;
thus (r(#)f)|['d,b'] is bounded by A6,RFUNCT_1:80;
end;
per cases;
suppose A7: f is_-infty_ext_Riemann_integrable_on b; then
A8: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
by A2,Th22;
A9: r(#)f is_-infty_ext_Riemann_integrable_on b &
infty_ext_left_integral(r(#)f,b) = r*infty_ext_left_integral(f,b)
by A1,A7,INTEGR10:11;
thus r(#)f is_-infty_improper_integrable_on b
by A1,A7,INTEGR10:11,Th20; then
improper_integral_-infty(r(#)f,b) = infty_ext_left_integral(r(#)f,b)
by A9,Th22;
hence improper_integral_-infty(r(#)f,b)
= r * improper_integral_-infty(f,b) by A8,A9,XXREAL_3:def 5;
end;
suppose A10: not f is_-infty_ext_Riemann_integrable_on b;
consider Intf be PartFunc of REAL,REAL such that
A11: dom Intf = left_closed_halfline b and
A12: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)
by A2;
A13: dom(r(#)Intf) = left_closed_halfline b by A11,VALUED_1:def 5;
A14: for x be Real st x in dom(r(#)Intf) holds
(r(#)Intf).x = integral(r(#)f,x,b)
proof
let x be Real;
assume A15: x in dom(r(#)Intf); then
A16: (r(#)Intf).x = r*(Intf.x) by VALUED_1:def 5
.= r*integral(f,x,b) by A15,A13,A12,A11;
A17: x <= b by A13,A15,XXREAL_1:2;
[.x,b.] c= ].-infty,b.] by XXREAL_1:265; then
[.x,b.] c= dom f by A1; then
A18: ['x,b'] c= dom f by A17,INTEGRA5:def 3;
f is_integrable_on ['x,b'] & f|['x,b'] is bounded by A2,A17;
hence (r(#)Intf).x = integral(r(#)f,x,b) by A16,A17,A18,INTEGRA6:10;
end;
per cases by A2,A10,Th22;
suppose A19: improper_integral_-infty(f,b) = +infty; then
A20: Intf is divergent_in-infty_to+infty by A2,A11,A12,Th37;
per cases;
suppose A21: r > 0; then
A22: r(#)Intf is divergent_in-infty_to+infty
by A19,A2,A11,A12,Th37,LIMFUNC1:59;
thus r(#)f is_-infty_improper_integrable_on b
by A3,A13,A14,A21,A20,LIMFUNC1:59; then
improper_integral_-infty(r(#)f,b) = +infty by A13,A14,A22,Def3;
hence improper_integral_-infty(r(#)f,b)
= r * improper_integral_-infty(f,b) by A19,A21,XXREAL_3:def 5;
end;
suppose A23: r < 0; then
A24: r(#)Intf is divergent_in-infty_to-infty
by A19,A2,A11,A12,Th37,LIMFUNC1:59;
thus r(#)f is_-infty_improper_integrable_on b
by A3,A13,A14,A23,A20,LIMFUNC1:59; then
improper_integral_-infty(r(#)f,b) = -infty by A13,A14,A24,Def3;
hence improper_integral_-infty(r(#)f,b)
= r * improper_integral_-infty(f,b) by A19,A23,XXREAL_3:def 5;
end;
suppose A25: r = 0;
A26: for R be Real
ex g be Real st g < R & g in dom(r(#)Intf)
by A11,A13,A20,LIMFUNC1:48;
A27: for g1 be Real st 0 < g1
ex R be Real st for r1 be Real st r1 < R
& r1 in dom(r(#)Intf) holds |. (r(#)Intf).r1 - 0 .| < g1
proof
let g1 be Real;
assume A28: 0 < g1;
now let r1 be Real;
assume r1 < b & r1 in dom(r(#)Intf); then
(r(#)Intf).r1 = r * Intf.r1 by VALUED_1:def 5 .= 0 by A25;
hence |. (r(#)Intf).r1 - 0 .| < g1 by A28,ABSVALUE:2;
end;
hence thesis;
end; then
A29: r(#)Intf is convergent_in-infty by A26,LIMFUNC1:45; then
A30: lim_in-infty (r(#)Intf) = 0 by A27,LIMFUNC1:78;
thus r(#)f is_-infty_improper_integrable_on b
by A3,A13,A14,A27,A26,LIMFUNC1:45; then
improper_integral_-infty(r(#)f,b) = 0 by A13,A14,A29,A30,Def3;
hence improper_integral_-infty(r(#)f,b)
= r * improper_integral_-infty(f,b) by A25;
end;
end;
suppose A31: improper_integral_-infty(f,b) = -infty; then
A32: Intf is divergent_in-infty_to-infty by A2,A11,A12,Th38;
per cases;
suppose A33: r > 0; then
A34: r(#)Intf is divergent_in-infty_to-infty
by A31,A2,A11,A12,Th38,LIMFUNC1:59;
thus r(#)f is_-infty_improper_integrable_on b
by A3,A13,A14,A33,A32,LIMFUNC1:59; then
improper_integral_-infty(r(#)f,b) = -infty by A13,A14,A34,Def3;
hence improper_integral_-infty(r(#)f,b)
= r * improper_integral_-infty(f,b) by A31,A33,XXREAL_3:def 5;
end;
suppose A35: r < 0; then
A36: r(#)Intf is divergent_in-infty_to+infty
by A31,A2,A11,A12,Th38,LIMFUNC1:59;
thus r(#)f is_-infty_improper_integrable_on b
by A3,A13,A14,A35,A32,LIMFUNC1:59; then
improper_integral_-infty(r(#)f,b) = +infty by A13,A14,A36,Def3;
hence improper_integral_-infty(r(#)f,b)
= r * improper_integral_-infty(f,b) by A31,A35,XXREAL_3:def 5;
end;
suppose A37: r = 0;
A38: for R be Real
ex g be Real st g < R & g in dom(r(#)Intf)
by A11,A13,A32,LIMFUNC1:49;
A39: for g1 be Real st 0 < g1
ex R be Real st for r1 be Real st r1 < R
& r1 in dom(r(#)Intf) holds |. (r(#)Intf).r1 - 0 .| < g1
proof
let g1 be Real;
assume A40: 0 < g1;
now let r1 be Real;
assume r1 < b & r1 in dom(r(#)Intf); then
(r(#)Intf).r1 = r * Intf.r1 by VALUED_1:def 5 .= 0 by A37;
hence |. (r(#)Intf).r1 - 0 .| < g1 by A40,ABSVALUE:2;
end;
hence thesis;
end; then
A41: r(#)Intf is convergent_in-infty by A38,LIMFUNC1:45; then
A42: lim_in-infty (r(#)Intf) = 0 by A39,LIMFUNC1:78;
thus r(#)f is_-infty_improper_integrable_on b
by A3,A13,A14,A39,A38,LIMFUNC1:45; then
improper_integral_-infty(r(#)f,b) = 0 by A13,A14,A41,A42,Def3;
hence improper_integral_-infty(r(#)f,b)
= r * improper_integral_-infty(f,b) by A37;
end;
end;
end;
end;
theorem Th42:
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)
proof
let f be PartFunc of REAL,REAL, a,r be Real;
assume that
A1: right_closed_halfline a c= dom f and
A2: f is_+infty_improper_integrable_on a;
A3: for d be Real st a <= d holds r(#)f is_integrable_on [' a,d ']
& (r(#)f)|[' a,d '] is bounded
proof
let d be Real;
assume
A4: a <= d;
[.a,d.] c= [.a,+infty.[ by XXREAL_1:251; then
[.a,d.] c= dom f by A1; then
A5: ['a,d'] c= dom f by A4,INTEGRA5:def 3;
A6: f is_integrable_on ['a,d'] & f|['a,d'] is bounded by A2,A4;
hence r(#)f is_integrable_on ['a,d'] by A5,INTEGRA6:9;
thus (r(#)f)|['a,d'] is bounded by A6,RFUNCT_1:80;
end;
per cases;
suppose A7: f is_+infty_ext_Riemann_integrable_on a; then
A8: improper_integral_+infty(f,a) = infty_ext_right_integral(f,a)
by A2,Th27;
A9: r(#)f is_+infty_ext_Riemann_integrable_on a &
infty_ext_right_integral(r(#)f,a) = r*infty_ext_right_integral(f,a)
by A1,A7,INTEGR10:9;
thus r(#)f is_+infty_improper_integrable_on a
by A1,A7,INTEGR10:9,Th21; then
improper_integral_+infty(r(#)f,a) = infty_ext_right_integral(r(#)f,a)
by A9,Th27;
hence improper_integral_+infty(r(#)f,a)
= r * improper_integral_+infty(f,a) by A8,A9,XXREAL_3:def 5;
end;
suppose A10: not f is_+infty_ext_Riemann_integrable_on a;
consider Intf be PartFunc of REAL,REAL such that
A11: dom Intf = right_closed_halfline a and
A12: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)
by A2;
A13: dom(r(#)Intf) = right_closed_halfline a by A11,VALUED_1:def 5;
A14: for x be Real st x in dom(r(#)Intf) holds
(r(#)Intf).x = integral(r(#)f,a,x)
proof
let x be Real;
assume A15: x in dom(r(#)Intf); then
A16: (r(#)Intf).x = r*(Intf.x) by VALUED_1:def 5
.= r*integral(f,a,x) by A15,A13,A12,A11;
A17: a <= x by A13,A15,XXREAL_1:3;
[.a,x.] c= [.a,+infty.[ by XXREAL_1:251; then
[.a,x.] c= dom f by A1; then
A18: ['a,x'] c= dom f by A17,INTEGRA5:def 3;
f is_integrable_on ['a,x'] & f|['a,x'] is bounded by A2,A17;
hence (r(#)Intf).x = integral(r(#)f,a,x) by A16,A17,A18,INTEGRA6:10;
end;
per cases by A2,A10,Th27;
suppose A19: improper_integral_+infty(f,a) = +infty; then
A20: Intf is divergent_in+infty_to+infty by A2,A11,A12,Th39;
per cases;
suppose A21: r > 0; then
A22: r(#)Intf is divergent_in+infty_to+infty
by A19,A2,A11,A12,Th39,LIMFUNC1:58;
thus r(#)f is_+infty_improper_integrable_on a
by A3,A13,A14,A21,A20,LIMFUNC1:58; then
improper_integral_+infty(r(#)f,a) = +infty by A13,A14,A22,Def4;
hence improper_integral_+infty(r(#)f,a)
= r * improper_integral_+infty(f,a) by A19,A21,XXREAL_3:def 5;
end;
suppose A23: r < 0; then
A24: r(#)Intf is divergent_in+infty_to-infty
by A19,A2,A11,A12,Th39,LIMFUNC1:58;
thus r(#)f is_+infty_improper_integrable_on a
by A3,A13,A14,A23,A20,LIMFUNC1:58; then
improper_integral_+infty(r(#)f,a) = -infty by A13,A14,A24,Def4;
hence improper_integral_+infty(r(#)f,a)
= r * improper_integral_+infty(f,a) by A19,A23,XXREAL_3:def 5;
end;
suppose A25: r = 0;
A26: for R be Real
ex g be Real st R < g & g in dom(r(#)Intf)
by A11,A13,A20,LIMFUNC1:46;
A27: for g1 be Real st 0 < g1
ex R be Real st for r1 be Real st R < r1
& r1 in dom(r(#)Intf) holds |. (r(#)Intf).r1 - 0 .| < g1
proof
let g1 be Real;
assume A28: 0 < g1;
now let r1 be Real;
assume a < r1 & r1 in dom(r(#)Intf); then
(r(#)Intf).r1 = r * Intf.r1 by VALUED_1:def 5 .= 0 by A25;
hence |. (r(#)Intf).r1 - 0 .| < g1 by A28,ABSVALUE:2;
end;
hence thesis;
end; then
A29: r(#)Intf is convergent_in+infty by A26,LIMFUNC1:44; then
A30: lim_in+infty (r(#)Intf) = 0 by A27,LIMFUNC1:79;
thus r(#)f is_+infty_improper_integrable_on a
by A3,A13,A14,A27,A26,LIMFUNC1:44; then
improper_integral_+infty(r(#)f,a) = 0 by A13,A14,A29,A30,Def4;
hence improper_integral_+infty(r(#)f,a)
= r * improper_integral_+infty(f,a) by A25;
end;
end;
suppose A31: improper_integral_+infty(f,a) = -infty; then
A32: Intf is divergent_in+infty_to-infty by A2,A11,A12,Th40;
per cases;
suppose A33: r > 0; then
A34: r(#)Intf is divergent_in+infty_to-infty
by A31,A2,A11,A12,Th40,LIMFUNC1:58;
thus r(#)f is_+infty_improper_integrable_on a
by A3,A13,A14,A33,A32,LIMFUNC1:58; then
improper_integral_+infty(r(#)f,a) = -infty by A13,A14,A34,Def4;
hence improper_integral_+infty(r(#)f,a)
= r * improper_integral_+infty(f,a) by A31,A33,XXREAL_3:def 5;
end;
suppose A35: r < 0; then
A36: r(#)Intf is divergent_in+infty_to+infty
by A31,A2,A11,A12,Th40,LIMFUNC1:58;
thus r(#)f is_+infty_improper_integrable_on a
by A3,A13,A14,A35,A32,LIMFUNC1:58; then
improper_integral_+infty(r(#)f,a) = +infty by A13,A14,A36,Def4;
hence improper_integral_+infty(r(#)f,a)
= r * improper_integral_+infty(f,a) by A31,A35,XXREAL_3:def 5;
end;
suppose A37: r = 0;
A38: for R be Real
ex g be Real st R < g & g in dom(r(#)Intf)
by A11,A13,A32,LIMFUNC1:47;
A39: for g1 be Real st 0 < g1
ex R be Real st for r1 be Real st R < r1
& r1 in dom(r(#)Intf) holds |. (r(#)Intf).r1 - 0 .| < g1
proof
let g1 be Real;
assume A40: 0 < g1;
now let r1 be Real;
assume a < r1 & r1 in dom(r(#)Intf); then
(r(#)Intf).r1 = r * Intf.r1 by VALUED_1:def 5 .= 0 by A37;
hence |. (r(#)Intf).r1 - 0 .| < g1 by A40,ABSVALUE:2;
end;
hence thesis;
end; then
A41: r(#)Intf is convergent_in+infty by A38,LIMFUNC1:44; then
A42: lim_in+infty (r(#)Intf) = 0 by A39,LIMFUNC1:79;
thus r(#)f is_+infty_improper_integrable_on a
by A3,A13,A14,A39,A38,LIMFUNC1:44; then
improper_integral_+infty(r(#)f,a) = 0 by A13,A14,A41,A42,Def4;
hence improper_integral_+infty(r(#)f,a)
= r * improper_integral_+infty(f,a) by A37;
end;
end;
end;
end;
theorem Th43:
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)
proof
let f be PartFunc of REAL,REAL, b be Real;
assume A1: left_closed_halfline b c= dom f
& f is_-infty_improper_integrable_on b;
hence -f is_-infty_improper_integrable_on b by Th41;
improper_integral_-infty(-f,b) = (-1) * improper_integral_-infty(f,b)
by A1,Th41;
hence improper_integral_-infty(-f,b) = - improper_integral_-infty(f,b)
by XXREAL_3:91;
end;
theorem Th44:
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)
proof
let f be PartFunc of REAL,REAL, a be Real;
assume A1: right_closed_halfline a c= dom f
& f is_+infty_improper_integrable_on a;
hence -f is_+infty_improper_integrable_on a by Th42;
improper_integral_+infty(-f,a) = (-1) * improper_integral_+infty(f,a)
by A1,Th42;
hence improper_integral_+infty(-f,a) = - improper_integral_+infty(f,a)
by XXREAL_3:91;
end;
theorem Th45:
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)
proof
let f,g be PartFunc of REAL,REAL, b be Real;
assume that
A1: left_closed_halfline b c= dom f and
A2: left_closed_halfline b c= dom g and
A3: f is_-infty_improper_integrable_on b and
A4: g is_-infty_improper_integrable_on b and
A5: not (improper_integral_-infty(f,b) = +infty
& improper_integral_-infty(g,b) = -infty) and
A6: not (improper_integral_-infty(f,b) = -infty
& improper_integral_-infty(g,b) = +infty);
A7: for d be Real st d<=b holds
f+g is_integrable_on ['d,b'] & (f+g)|['d,b'] is bounded
proof
let d be Real;
assume
A8: d<=b;
A9: f is_integrable_on ['d,b'] & f|['d,b'] is bounded &
g is_integrable_on ['d,b'] & g|['d,b'] is bounded by A3,A4,A8;
[.d,b.] c= ].-infty,b.] by XXREAL_1:265; then
['d,b'] c= ].-infty,b.] by A8,INTEGRA5:def 3; then
['d,b'] c= dom f & ['d,b'] c= dom g by A1,A2;
hence f+g is_integrable_on ['d,b'] by A9,INTEGRA6:11;
(f+g)|(['d,b'] /\ ['d,b']) is bounded by A9,RFUNCT_1:83;
hence (f+g)|['d,b'] is bounded;
end;
per cases;
suppose A10: f is_-infty_ext_Riemann_integrable_on b
& g is_-infty_ext_Riemann_integrable_on b; then
A11: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
& improper_integral_-infty(g,b) = infty_ext_left_integral(g,b)
by A3,A4,Th22;
A12: f+g is_-infty_ext_Riemann_integrable_on b
& infty_ext_left_integral(f+g,b)
= infty_ext_left_integral(f,b) + infty_ext_left_integral(g,b)
by A1,A2,A10,INTEGR10:10;
thus f+g is_-infty_improper_integrable_on b
by A1,A2,A10,INTEGR10:10,Th20; then
improper_integral_-infty(f+g,b) = infty_ext_left_integral(f+g,b)
by A12,Th22;
hence improper_integral_-infty(f+g,b)
= improper_integral_-infty(f,b) + improper_integral_-infty(g,b)
by A11,A12,XXREAL_3:def 2;
end;
suppose A13: f is_-infty_ext_Riemann_integrable_on b &
not g is_-infty_ext_Riemann_integrable_on b; then
A14: improper_integral_-infty(f,b) = infty_ext_left_integral(f,b)
by A3,Th22;
consider Intf be PartFunc of REAL,REAL such that
A15: dom Intf = left_closed_halfline b and
A16: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
A17: Intf is convergent_in-infty by A13,INTEGR10:def 6;
consider Intg be PartFunc of REAL,REAL such that
A18: dom Intg = left_closed_halfline b and
A19: for x be Real st x in dom Intg holds Intg.x = integral(g,x,b) and
(Intg is convergent_in-infty or Intg is divergent_in-infty_to+infty
or Intg is divergent_in-infty_to-infty) by A4;
A20: dom(Intf+Intg) = left_closed_halfline b /\ left_closed_halfline b
by A15,A18,VALUED_1:def 1
.= left_closed_halfline b;
A21: for x be Real st x in dom(Intf+Intg) holds
(Intf+Intg).x = integral(f+g,x,b)
proof
let x be Real;
assume A22: x in dom(Intf+Intg); then
A23: x <= b by A20,XXREAL_1:2;
[.x,b.] c= left_closed_halfline b by XXREAL_1:265; then
A24: [.x,b.] c= dom f & [.x,b.] c= dom g by A1,A2;
A25: ['x,b'] = [.x,b.] by A23,INTEGRA5:def 3;
f is_integrable_on ['x,b'] & f|['x,b'] is bounded &
g is_integrable_on ['x,b'] & g|['x,b'] is bounded by A3,A4,A23; then
integral(f+g,['x,b']) = integral(f,['x,b'])+integral(g,['x,b'])
by A24,A25,INTEGRA6:11; then
A26: integral(f+g,x,b)
= integral(f,['x,b'])+integral(g,['x,b']) by A23,INTEGRA5:def 4
.= integral(f,x,b) + integral(g,['x,b']) by A23,INTEGRA5:def 4
.= integral(f,x,b) + integral(g,x,b) by A23,INTEGRA5:def 4;
(Intf+Intg).x = Intf.x + Intg.x by A22,VALUED_1:def 1
.= integral(f,x,b) + Intg.x by A22,A20,A15,A16
.= integral(f,x,b) + integral(g,x,b) by A22,A20,A18,A19;
hence (Intf+Intg).x = integral(f+g,x,b) by A26;
end;
A27: for r be Real
ex g be Real st g < r & g in dom(Intf+Intg)
proof
let r be Real;
consider g be Real such that
A28: g < min(b,r) by XREAL_1:2;
take g;
min(b,r) <= b & min(b,r) <= r by XXREAL_0:17;
hence thesis by A20,A28,XXREAL_0:2,XXREAL_1:234;
end;
per cases by A4,A13,Th22;
suppose A29: improper_integral_-infty(g,b) = +infty; then
A30: Intg is divergent_in-infty_to+infty by A4,A18,A19,Th37;
A31: ex r be Real st Intf|left_open_halfline r is bounded_below
by A17,Th5; then
A32: Intf+Intg is divergent_in-infty_to+infty
by A29,A27,A4,A18,A19,Th37,LIMFUNC1:56;
thus f+g is_-infty_improper_integrable_on b
by A7,A20,A21,A31,A30,A27,LIMFUNC1:56; then
improper_integral_-infty(f+g,b) = +infty by A20,A21,A32,Def3;
hence improper_integral_-infty(f+g,b)
= improper_integral_-infty(f,b) + improper_integral_-infty(g,b)
by A14,A29,XXREAL_3:def 2;
end;
suppose A33: improper_integral_-infty(g,b) = -infty; then
A34: Intg is divergent_in-infty_to-infty by A4,A18,A19,Th38;
A35: ex r be Real st Intf|left_open_halfline r is bounded_above
by A17,Th5; then
A36: Intf+Intg is divergent_in-infty_to-infty
by A33,A27,A4,A18,A19,Th38,Th11;
thus f+g is_-infty_improper_integrable_on b
by A7,A20,A21,A35,A34,A27,Th11; then
improper_integral_-infty(f+g,b) = -infty by A20,A21,A36,Def3;
hence improper_integral_-infty(f+g,b)
= improper_integral_-infty(f,b) + improper_integral_-infty(g,b)
by A14,A33,XXREAL_3:def 2;
end;
end;
suppose A37: not f is_-infty_ext_Riemann_integrable_on b &
g is_-infty_ext_Riemann_integrable_on b; then
A38: improper_integral_-infty(g,b) = infty_ext_left_integral(g,b)
by A4,Th22;
consider Intg be PartFunc of REAL,REAL such that
A39: dom Intg = left_closed_halfline b and
A40: for x be Real st x in dom Intg holds Intg.x = integral(g,x,b) and
A41: Intg is convergent_in-infty by A37,INTEGR10:def 6;
consider Intf be PartFunc of REAL,REAL such that
A42: dom Intf = left_closed_halfline b and
A43: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
(Intf is convergent_in-infty or Intf is divergent_in-infty_to+infty
or Intf is divergent_in-infty_to-infty) by A3;
A44: dom(Intf+Intg) = left_closed_halfline b /\ left_closed_halfline b
by A39,A42,VALUED_1:def 1
.= left_closed_halfline b;
A45: for x be Real st x in dom(Intf+Intg) holds
(Intf+Intg).x = integral(f+g,x,b)
proof
let x be Real;
assume A46: x in dom(Intf+Intg); then
A47: x <= b by A44,XXREAL_1:2;
[.x,b.] c= left_closed_halfline b by XXREAL_1:265; then
A48: [.x,b.] c= dom f & [.x,b.] c= dom g by A1,A2;
A49: ['x,b'] = [.x,b.] by A47,INTEGRA5:def 3;
f is_integrable_on ['x,b'] & f|['x,b'] is bounded &
g is_integrable_on ['x,b'] & g|['x,b'] is bounded by A3,A4,A47; then
integral(f+g,['x,b']) = integral(f,['x,b'])+integral(g,['x,b'])
by A48,A49,INTEGRA6:11; then
A50: integral(f+g,x,b)
= integral(f,['x,b'])+integral(g,['x,b']) by A47,INTEGRA5:def 4
.= integral(f,x,b) + integral(g,['x,b']) by A47,INTEGRA5:def 4
.= integral(f,x,b) + integral(g,x,b) by A47,INTEGRA5:def 4;
(Intf+Intg).x = Intf.x + Intg.x by A46,VALUED_1:def 1
.= integral(f,x,b) + Intg.x by A46,A44,A42,A43
.= integral(f,x,b) + integral(g,x,b) by A46,A44,A39,A40;
hence (Intf+Intg).x = integral(f+g,x,b) by A50;
end;
A51: for r be Real
ex g be Real st g < r & g in dom(Intf+Intg)
proof
let r be Real;
consider g be Real such that
A52: g < min(b,r) by XREAL_1:2;
take g;
min(b,r) <= b & min(b,r) <= r by XXREAL_0:17;
hence thesis by A44,A52,XXREAL_0:2,XXREAL_1:234;
end;
per cases by A3,A37,Th22;
suppose A53: improper_integral_-infty(f,b) = +infty;
ex r be Real st Intg|left_open_halfline r is bounded_below
by A41,Th5; then
A54: Intf+Intg is divergent_in-infty_to+infty
by A53,A51,A3,A42,A43,Th37,LIMFUNC1:56;
hence f+g is_-infty_improper_integrable_on b by A7,A44,A45; then
improper_integral_-infty(f+g,b) = +infty by A44,A45,A54,Def3;
hence improper_integral_-infty(f+g,b)
= improper_integral_-infty(f,b) + improper_integral_-infty(g,b)
by A38,A53,XXREAL_3:def 2;
end;
suppose A55: improper_integral_-infty(f,b) = -infty;
ex r be Real st Intg|left_open_halfline r is bounded_above
by A41,Th5; then
A56: Intf+Intg is divergent_in-infty_to-infty
by A55,A51,A3,A42,A43,Th38,Th11;
hence f+g is_-infty_improper_integrable_on b by A7,A44,A45; then
improper_integral_-infty(f+g,b) = -infty by A44,A45,A56,Def3;
hence improper_integral_-infty(f+g,b)
= improper_integral_-infty(f,b) + improper_integral_-infty(g,b)
by A38,A55,XXREAL_3:def 2;
end;
end;
suppose A57: not f is_-infty_ext_Riemann_integrable_on b &
not g is_-infty_ext_Riemann_integrable_on b;
consider Intf be PartFunc of REAL,REAL such that
A58: dom Intf = left_closed_halfline b and
A59: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
(Intf is convergent_in-infty or Intf is divergent_in-infty_to+infty
or Intf is divergent_in-infty_to-infty) by A3;
consider Intg be PartFunc of REAL,REAL such that
A60: dom Intg = left_closed_halfline b and
A61: for x be Real st x in dom Intg holds Intg.x = integral(g,x,b) and
(Intg is convergent_in-infty or Intg is divergent_in-infty_to+infty
or Intg is divergent_in-infty_to-infty) by A4;
A62: dom(Intf+Intg) = left_closed_halfline b /\ left_closed_halfline b
by A60,A58,VALUED_1:def 1
.= left_closed_halfline b;
A63: for x be Real st x in dom(Intf+Intg) holds
(Intf+Intg).x = integral(f+g,x,b)
proof
let x be Real;
assume A64: x in dom(Intf+Intg); then
A65: x <= b by A62,XXREAL_1:2;
[.x,b.] c= left_closed_halfline b by XXREAL_1:265; then
A66: [.x,b.] c= dom f & [.x,b.] c= dom g by A1,A2;
A67: ['x,b'] = [.x,b.] by A65,INTEGRA5:def 3;
f is_integrable_on ['x,b'] & f|['x,b'] is bounded &
g is_integrable_on ['x,b'] & g|['x,b'] is bounded by A3,A4,A65; then
integral(f+g,['x,b']) = integral(f,['x,b'])+integral(g,['x,b'])
by A66,A67,INTEGRA6:11; then
A68: integral(f+g,x,b)
= integral(f,['x,b'])+integral(g,['x,b']) by A65,INTEGRA5:def 4
.= integral(f,x,b) + integral(g,['x,b']) by A65,INTEGRA5:def 4
.= integral(f,x,b) + integral(g,x,b) by A65,INTEGRA5:def 4;
(Intf+Intg).x = Intf.x + Intg.x by A64,VALUED_1:def 1
.= integral(f,x,b) + Intg.x by A64,A62,A58,A59
.= integral(f,x,b) + integral(g,x,b) by A64,A62,A60,A61;
hence (Intf+Intg).x = integral(f+g,x,b) by A68;
end;
A69: for r be Real
ex g be Real st g < r & g in dom(Intf+Intg)
proof
let r be Real;
consider g be Real such that
A70: g < min(b,r) by XREAL_1:2;
take g;
min(b,r) <= b & min(b,r) <= r by XXREAL_0:17;
hence thesis by A62,A70,XXREAL_0:2,XXREAL_1:234;
end;
per cases by A3,A57,Th22;
suppose A71: improper_integral_-infty(f,b) = +infty; then
A72: Intf is divergent_in-infty_to+infty by A3,A58,A59,Th37;
improper_integral_-infty(g,b) = +infty by A71,A4,A57,A5,Th22; then
A73: ex r be Real st Intg|left_open_halfline r is bounded_below
by A4,A60,A61,Th37,Th7; then
A74: Intf+Intg is divergent_in-infty_to+infty
by A69,A71,A3,A58,A59,Th37,LIMFUNC1:56;
thus f+g is_-infty_improper_integrable_on b
by A7,A62,A63,A73,A72,A69,LIMFUNC1:56; then
improper_integral_-infty(f+g,b) = +infty by A62,A63,A74,Def3;
hence improper_integral_-infty(f+g,b)
= improper_integral_-infty(f,b) + improper_integral_-infty(g,b)
by A5,A71,XXREAL_3:def 2;
end;
suppose A75: improper_integral_-infty(f,b) = -infty; then
A76: Intf is divergent_in-infty_to-infty by A3,A58,A59,Th38;
improper_integral_-infty(g,b) = -infty by A75,A4,A57,A6,Th22; then
A77: ex r be Real st Intg|left_open_halfline r is bounded_above
by A4,A60,A61,Th38,Th8; then
A78: Intf+Intg is divergent_in-infty_to-infty
by A75,A69,A3,A58,A59,Th38,Th11;
thus f+g is_-infty_improper_integrable_on b
by A7,A62,A63,A76,A69,A77,Th11; then
improper_integral_-infty(f+g,b) = -infty by A62,A63,A78,Def3;
hence improper_integral_-infty(f+g,b)
= improper_integral_-infty(f,b) + improper_integral_-infty(g,b)
by A6,A75,XXREAL_3:def 2;
end;
end;
end;
theorem Th46:
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)
proof
let f,g be PartFunc of REAL,REAL, a be Real;
assume that
A1: right_closed_halfline a c= dom f and
A2: right_closed_halfline a c= dom g and
A3: f is_+infty_improper_integrable_on a and
A4: g is_+infty_improper_integrable_on a and
A5: not (improper_integral_+infty(f,a) = +infty
& improper_integral_+infty(g,a) = -infty) and
A6: not (improper_integral_+infty(f,a) = -infty
& improper_integral_+infty(g,a) = +infty);
A7: for d be Real st a<=d holds
f+g is_integrable_on ['a,d'] & (f+g)|['a,d'] is bounded
proof
let d be Real;
assume
A8: a<=d;
A9: f is_integrable_on ['a,d'] & f|['a,d'] is bounded &
g is_integrable_on ['a,d'] & g|['a,d'] is bounded by A3,A4,A8;
[.a,d.] c= [.a,+infty.[ by XXREAL_1:251; then
['a,d'] c= [.a,+infty.[ by A8,INTEGRA5:def 3; then
['a,d'] c= dom f & ['a,d'] c= dom g by A1,A2;
hence f+g is_integrable_on ['a,d'] by A9,INTEGRA6:11;
(f+g)|(['a,d'] /\ ['a,d']) is bounded by A9,RFUNCT_1:83;
hence (f+g)|['a,d'] is bounded;
end;
per cases;
suppose A10: f is_+infty_ext_Riemann_integrable_on a
& g is_+infty_ext_Riemann_integrable_on a; then
A11: improper_integral_+infty(f,a) = infty_ext_right_integral(f,a)
& improper_integral_+infty(g,a) = infty_ext_right_integral(g,a)
by A3,A4,Th27;
A12: f+g is_+infty_ext_Riemann_integrable_on a
& infty_ext_right_integral(f+g,a)
= infty_ext_right_integral(f,a) + infty_ext_right_integral(g,a)
by A1,A2,A10,INTEGR10:8;
thus f+g is_+infty_improper_integrable_on a
by A1,A2,A10,Th21,INTEGR10:8; then
improper_integral_+infty(f+g,a) = infty_ext_right_integral(f+g,a)
by A12,Th27;
hence improper_integral_+infty(f+g,a)
= improper_integral_+infty(f,a) + improper_integral_+infty(g,a)
by A11,A12,XXREAL_3:def 2;
end;
suppose A13: f is_+infty_ext_Riemann_integrable_on a &
not g is_+infty_ext_Riemann_integrable_on a; then
A14: improper_integral_+infty(f,a) = infty_ext_right_integral(f,a)
by A3,Th27;
consider Intf be PartFunc of REAL,REAL such that
A15: dom Intf = right_closed_halfline a and
A16: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x) and
A17: Intf is convergent_in+infty by A13,INTEGR10:def 5;
consider Intg be PartFunc of REAL,REAL such that
A18: dom Intg = right_closed_halfline a and
A19: for x be Real st x in dom Intg holds Intg.x = integral(g,a,x) and
(Intg is convergent_in+infty or Intg is divergent_in+infty_to+infty
or Intg is divergent_in+infty_to-infty) by A4;
A20: dom(Intf+Intg) = right_closed_halfline a /\ right_closed_halfline a
by A15,A18,VALUED_1:def 1
.= right_closed_halfline a;
A21: for x be Real st x in dom(Intf+Intg) holds
(Intf+Intg).x = integral(f+g,a,x)
proof
let x be Real;
assume A22: x in dom(Intf+Intg); then
A23: a <= x by A20,XXREAL_1:3;
[.a,x.] c= right_closed_halfline a by XXREAL_1:251; then
A24: [.a,x.] c= dom f & [.a,x.] c= dom g by A1,A2;
A25: ['a,x'] = [.a,x.] by A23,INTEGRA5:def 3;
f is_integrable_on ['a,x'] & f|['a,x'] is bounded &
g is_integrable_on ['a,x'] & g|['a,x'] is bounded by A3,A4,A23; then
integral(f+g,['a,x']) = integral(f,['a,x'])+integral(g,['a,x'])
by A24,A25,INTEGRA6:11; then
A26: integral(f+g,a,x)
= integral(f,['a,x'])+integral(g,['a,x']) by A23,INTEGRA5:def 4
.= integral(f,a,x) + integral(g,['a,x']) by A23,INTEGRA5:def 4
.= integral(f,a,x) + integral(g,a,x) by A23,INTEGRA5:def 4;
(Intf+Intg).x = Intf.x + Intg.x by A22,VALUED_1:def 1
.= integral(f,a,x) + Intg.x by A22,A20,A15,A16
.= integral(f,a,x) + integral(g,a,x) by A22,A20,A18,A19;
hence (Intf+Intg).x = integral(f+g,a,x) by A26;
end;
A27: for r be Real
ex g be Real st r < g & g in dom(Intf+Intg)
proof
let r be Real;
consider g be Real such that
A28: max(a,r) < g by XREAL_1:1;
take g;
max(a,r) >= a & max(a,r) >= r by XXREAL_0:25;
hence thesis by A20,A28,XXREAL_0:2,XXREAL_1:236;
end;
A29: (ex r be Real st Intf|right_open_halfline r is bounded_below)
& (ex r be Real st Intf|right_open_halfline r is bounded_above)
by A17,Th6;
per cases by A4,A13,Th27;
suppose A30: improper_integral_+infty(g,a) = +infty; then
A31: Intf+Intg is divergent_in+infty_to+infty
by A27,A4,A18,A19,A29,Th39,LIMFUNC1:54;
hence f+g is_+infty_improper_integrable_on a by A7,A20,A21; then
improper_integral_+infty(f+g,a) = +infty by A20,A21,A31,Def4;
hence improper_integral_+infty(f+g,a)
= improper_integral_+infty(f,a) + improper_integral_+infty(g,a)
by A14,A30,XXREAL_3:def 2;
end;
suppose A32: improper_integral_+infty(g,a) = -infty; then
A33: Intf+Intg is divergent_in+infty_to-infty
by A27,A4,A18,A19,A29,Th40,Th12;
hence f+g is_+infty_improper_integrable_on a by A7,A20,A21; then
improper_integral_+infty(f+g,a) = -infty by A20,A21,A33,Def4;
hence improper_integral_+infty(f+g,a)
= improper_integral_+infty(f,a) + improper_integral_+infty(g,a)
by A14,A32,XXREAL_3:def 2;
end;
end;
suppose A34: not f is_+infty_ext_Riemann_integrable_on a &
g is_+infty_ext_Riemann_integrable_on a; then
A35: improper_integral_+infty(g,a) = infty_ext_right_integral(g,a)
by A4,Th27;
consider Intg be PartFunc of REAL,REAL such that
A36: dom Intg = right_closed_halfline a and
A37: for x be Real st x in dom Intg holds Intg.x = integral(g,a,x) and
A38: Intg is convergent_in+infty by A34,INTEGR10:def 5;
consider Intf be PartFunc of REAL,REAL such that
A39: dom Intf = right_closed_halfline a and
A40: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x) and
(Intf is convergent_in+infty or Intf is divergent_in+infty_to+infty
or Intf is divergent_in+infty_to-infty) by A3;
A41: dom(Intf+Intg) = right_closed_halfline a /\ right_closed_halfline a
by A36,A39,VALUED_1:def 1
.= right_closed_halfline a;
A42: for x be Real st x in dom(Intf+Intg) holds
(Intf+Intg).x = integral(f+g,a,x)
proof
let x be Real;
assume A43: x in dom(Intf+Intg); then
A44: a <= x by A41,XXREAL_1:3;
[.a,x.] c= [.a,+infty.[ by XXREAL_1:251; then
A45: [.a,x.] c= dom f & [.a,x.] c= dom g by A1,A2;
A46: ['a,x'] = [.a,x.] by A44,INTEGRA5:def 3;
f is_integrable_on ['a,x'] & f|['a,x'] is bounded &
g is_integrable_on ['a,x'] & g|['a,x'] is bounded by A3,A4,A44; then
integral(f+g,['a,x']) = integral(f,['a,x'])+integral(g,['a,x'])
by A45,A46,INTEGRA6:11; then
A47: integral(f+g,a,x)
= integral(f,['a,x'])+integral(g,['a,x']) by A44,INTEGRA5:def 4
.= integral(f,a,x) + integral(g,['a,x']) by A44,INTEGRA5:def 4
.= integral(f,a,x) + integral(g,a,x) by A44,INTEGRA5:def 4;
(Intf+Intg).x = Intf.x + Intg.x by A43,VALUED_1:def 1
.= integral(f,a,x) + Intg.x by A43,A41,A39,A40
.= integral(f,a,x) + integral(g,a,x) by A43,A41,A36,A37;
hence (Intf+Intg).x = integral(f+g,a,x) by A47;
end;
A48: for r be Real
ex g be Real st r < g & g in dom(Intf+Intg)
proof
let r be Real;
consider g be Real such that
A49: max(a,r) < g by XREAL_1:1;
take g;
max(a,r) >= a & max(a,r) >= r by XXREAL_0:25;
hence thesis by A41,A49,XXREAL_0:2,XXREAL_1:236;
end;
A50: (ex r be Real st Intg|right_open_halfline r is bounded_below)
& (ex r be Real st Intg|right_open_halfline r is bounded_above)
by A38,Th6;
per cases by A3,A34,Th27;
suppose A51: improper_integral_+infty(f,a) = +infty; then
A52: Intf+Intg is divergent_in+infty_to+infty
by A48,A3,A39,A40,A50,Th39,LIMFUNC1:54;
hence f+g is_+infty_improper_integrable_on a by A7,A41,A42; then
improper_integral_+infty(f+g,a) = +infty by A41,A42,A52,Def4;
hence improper_integral_+infty(f+g,a)
= improper_integral_+infty(f,a) + improper_integral_+infty(g,a)
by A35,A51,XXREAL_3:def 2;
end;
suppose A53: improper_integral_+infty(f,a) = -infty; then
A54: Intf+Intg is divergent_in+infty_to-infty
by A48,A3,A39,A40,A50,Th40,Th12;
hence f+g is_+infty_improper_integrable_on a by A7,A41,A42; then
improper_integral_+infty(f+g,a) = -infty by A41,A42,A54,Def4;
hence improper_integral_+infty(f+g,a)
= improper_integral_+infty(f,a) + improper_integral_+infty(g,a)
by A35,A53,XXREAL_3:def 2;
end;
end;
suppose A55: not f is_+infty_ext_Riemann_integrable_on a &
not g is_+infty_ext_Riemann_integrable_on a;
consider Intf be PartFunc of REAL,REAL such that
A56: dom Intf = right_closed_halfline a and
A57: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x) and
(Intf is convergent_in+infty or Intf is divergent_in+infty_to+infty
or Intf is divergent_in+infty_to-infty) by A3;
consider Intg be PartFunc of REAL,REAL such that
A58: dom Intg = right_closed_halfline a and
A59: for x be Real st x in dom Intg holds Intg.x = integral(g,a,x) and
(Intg is convergent_in+infty or Intg is divergent_in+infty_to+infty
or Intg is divergent_in+infty_to-infty) by A4;
A60: dom(Intf+Intg) = right_closed_halfline a /\ right_closed_halfline a
by A58,A56,VALUED_1:def 1
.= right_closed_halfline a;
A61: for x be Real st x in dom(Intf+Intg) holds
(Intf+Intg).x = integral(f+g,a,x)
proof
let x be Real;
assume A62: x in dom(Intf+Intg); then
A63: a <= x by A60,XXREAL_1:3;
[.a,x.] c= [.a,+infty.[ by XXREAL_1:251; then
A64: [.a,x.] c= dom f & [.a,x.] c= dom g by A1,A2;
A65: ['a,x'] = [.a,x.] by A63,INTEGRA5:def 3;
f is_integrable_on ['a,x'] & f|['a,x'] is bounded &
g is_integrable_on ['a,x'] & g|['a,x'] is bounded by A3,A4,A63; then
integral(f+g,['a,x']) = integral(f,['a,x'])+integral(g,['a,x'])
by A64,A65,INTEGRA6:11; then
A66: integral(f+g,a,x)
= integral(f,['a,x'])+integral(g,['a,x']) by A63,INTEGRA5:def 4
.= integral(f,a,x) + integral(g,['a,x']) by A63,INTEGRA5:def 4
.= integral(f,a,x) + integral(g,a,x) by A63,INTEGRA5:def 4;
(Intf+Intg).x = Intf.x + Intg.x by A62,VALUED_1:def 1
.= integral(f,a,x) + Intg.x by A62,A60,A56,A57
.= integral(f,a,x) + integral(g,a,x) by A62,A60,A58,A59;
hence (Intf+Intg).x = integral(f+g,a,x) by A66;
end;
A67: for r be Real
ex g be Real st r < g & g in dom(Intf+Intg)
proof
let r be Real;
consider g be Real such that
A68: max(a,r) < g by XREAL_1:1;
take g;
max(a,r) >= a & max(a,r) >= r by XXREAL_0:25;
hence thesis by A60,A68,XXREAL_0:2,XXREAL_1:236;
end;
per cases by A3,A55,Th27;
suppose A69: improper_integral_+infty(f,a) = +infty; then
improper_integral_+infty(g,a) = +infty by A4,A55,Th27,A5; then
ex r be Real st Intg|right_open_halfline r is bounded_below
by A4,A58,A59,Th39,Th9; then
A70: Intf+Intg is divergent_in+infty_to+infty
by A69,A67,A3,A56,A57,Th39,LIMFUNC1:54;
hence f+g is_+infty_improper_integrable_on a by A7,A60,A61; then
improper_integral_+infty(f+g,a) = +infty by A60,A61,A70,Def4;
hence improper_integral_+infty(f+g,a)
= improper_integral_+infty(f,a) + improper_integral_+infty(g,a)
by A69,A5,XXREAL_3:def 2;
end;
suppose A71: improper_integral_+infty(f,a) = -infty; then
improper_integral_+infty(g,a) = -infty by A4,A55,Th27,A6; then
ex r be Real st Intg|right_open_halfline r is bounded_above
by A4,A58,A59,Th40,Th10; then
A72: Intf+Intg is divergent_in+infty_to-infty
by A71,A67,A3,A56,A57,Th40,Th12;
hence f+g is_+infty_improper_integrable_on a by A7,A60,A61; then
improper_integral_+infty(f+g,a) = -infty by A60,A61,A72,Def4;
hence improper_integral_+infty(f+g,a)
= improper_integral_+infty(f,a) + improper_integral_+infty(g,a)
by A71,A6,XXREAL_3:def 2;
end;
end;
end;
theorem
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)
proof
let f,g be PartFunc of REAL,REAL, b be Real;
assume that
A1: left_closed_halfline b c= dom f and
A2: left_closed_halfline b c= dom g and
A3: f is_-infty_improper_integrable_on b and
A4: g is_-infty_improper_integrable_on b and
A5: not (improper_integral_-infty(f,b) = +infty
& improper_integral_-infty(g,b) = +infty) and
A6: not (improper_integral_-infty(f,b) = -infty
& improper_integral_-infty(g,b) = -infty);
A7: dom(-g) = dom g by VALUED_1:8;
A8: -g is_-infty_improper_integrable_on b by A2,A4,Th43;
A9:now assume A10: improper_integral_-infty(f,b) = +infty &
improper_integral_-infty(-g,b) = -infty; then
-improper_integral_-infty(g,b) = -(+infty) by A2,A4,Th43,XXREAL_3:6;
hence contradiction by A5,A10,XXREAL_3:10;
end;
A11:now assume A12: improper_integral_-infty(f,b) = -infty &
improper_integral_-infty(-g,b) = +infty; then
-improper_integral_-infty(g,b) = -(-infty)
by A2,A4,Th43,XXREAL_3:5;
hence contradiction by A6,A12,XXREAL_3:10;
end;
hence f-g is_-infty_improper_integrable_on b
by A1,A2,A7,A3,A8,A9,Th45;
improper_integral_-infty(f-g,b)
= improper_integral_-infty(f,b) + improper_integral_-infty(-g,b)
by A1,A2,A7,A3,A8,A9,A11,Th45
.= improper_integral_-infty(f,b) + (-improper_integral_-infty(g,b))
by A2,A4,Th43;
hence improper_integral_-infty(f-g,b)
= improper_integral_-infty(f,b) - improper_integral_-infty(g,b)
by XXREAL_3:def 4;
end;
theorem
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)
proof
let f,g be PartFunc of REAL,REAL, a be Real;
assume that
A1: right_closed_halfline a c= dom f and
A2: right_closed_halfline a c= dom g and
A3: f is_+infty_improper_integrable_on a and
A4: g is_+infty_improper_integrable_on a and
A5: not (improper_integral_+infty(f,a) = +infty
& improper_integral_+infty(g,a) = +infty) and
A6: not (improper_integral_+infty(f,a) = -infty
& improper_integral_+infty(g,a) = -infty);
A7: dom(-g) = dom g by VALUED_1:8;
A8: -g is_+infty_improper_integrable_on a by A2,A4,Th44;
A9:now assume A10: improper_integral_+infty(f,a) = +infty &
improper_integral_+infty(-g,a) = -infty; then
-improper_integral_+infty(g,a) = -(+infty)
by A2,A4,Th44,XXREAL_3:6;
hence contradiction by A5,A10,XXREAL_3:10;
end;
A11:now assume A12: improper_integral_+infty(f,a) = -infty &
improper_integral_+infty(-g,a) = +infty; then
-improper_integral_+infty(g,a) = -(-infty)
by A2,A4,Th44,XXREAL_3:5;
hence contradiction by A6,A12,XXREAL_3:10;
end;
hence f-g is_+infty_improper_integrable_on a
by A1,A2,A7,A3,A8,A9,Th46;
improper_integral_+infty(f-g,a)
= improper_integral_+infty(f,a) + improper_integral_+infty(-g,a)
by A1,A2,A7,A3,A8,A9,A11,Th46
.= improper_integral_+infty(f,a) + (-improper_integral_+infty(g,a))
by A2,A4,Th44;
hence improper_integral_+infty(f-g,a)
= improper_integral_+infty(f,a) - improper_integral_+infty(g,a)
by XXREAL_3:def 4;
end;
theorem Th49:
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)
proof
let f be PartFunc of REAL,REAL, r be Real;
assume that
A1: dom f = REAL and
A2: f is_improper_integrable_on_REAL;
consider c be Real such that
f is_-infty_improper_integrable_on c and
f is_+infty_improper_integrable_on c and
A3: not (improper_integral_-infty(f,c) = -infty
& improper_integral_+infty(f,c) = +infty) and
A4: not (improper_integral_-infty(f,c) = +infty
& improper_integral_+infty(f,c) = -infty) by A2;
f is_-infty_improper_integrable_on c
& f is_+infty_improper_integrable_on c by A1,A2,Th36; then
A5: r(#)f is_-infty_improper_integrable_on c
& r(#)f is_+infty_improper_integrable_on c
& improper_integral_-infty(r(#)f,c) = r * improper_integral_-infty(f,c)
& improper_integral_+infty(r(#)f,c) = r * improper_integral_+infty(f,c)
by A1,Th41,Th42;
A6: improper_integral_-infty(r(#)f,c) + improper_integral_+infty(r(#)f,c)
= r * (improper_integral_-infty(f,c) + improper_integral_+infty(f,c))
by A5,XXREAL_3:95
.= r * improper_integral_on_REAL f by A1,A2,Th36;
A7: dom(r(#)f) = dom f by VALUED_1:def 5;
per cases;
suppose r = 0;
hence r(#)f is_improper_integrable_on_REAL by A5;
hence improper_integral_on_REAL (r(#)f) = r * improper_integral_on_REAL f
by A1,A6,A7,Th36;
end;
suppose A8: r > 0;
A9: now assume A10: improper_integral_-infty(r(#)f,c) = -infty
& improper_integral_+infty(r(#)f,c) = +infty; then
improper_integral_-infty(f,c) = +infty or
improper_integral_-infty(f,c) = -infty by A5,XXREAL_3:70;
hence contradiction by A3,A10,A5,A8,XXREAL_3:69;
end;
A11: now assume A12: improper_integral_-infty(r(#)f,c) = +infty
& improper_integral_+infty(r(#)f,c) = -infty; then
improper_integral_-infty(f,c) = +infty or
improper_integral_-infty(f,c) = -infty by A5,XXREAL_3:69;
hence contradiction by A4,A12,A5,A8,XXREAL_3:70;
end;
thus r(#)f is_improper_integrable_on_REAL by A5,A9,A11;
hence improper_integral_on_REAL (r(#)f)
= r * improper_integral_on_REAL f
by A1,A6,A7,Th36;
end;
suppose A13: r < 0;
A14: now assume A15: improper_integral_-infty(r(#)f,c) = -infty
& improper_integral_+infty(r(#)f,c) = +infty; then
improper_integral_-infty(f,c) = +infty or
improper_integral_-infty(f,c) = -infty by A5,XXREAL_3:70;
hence contradiction by A4,A15,A5,A13,XXREAL_3:69;
end;
A16: now assume A17: improper_integral_-infty(r(#)f,c) = +infty
& improper_integral_+infty(r(#)f,c) = -infty; then
improper_integral_-infty(f,c) = +infty or
improper_integral_-infty(f,c) = -infty by A5,XXREAL_3:69;
hence contradiction by A3,A17,A5,A13,XXREAL_3:70;
end;
thus r(#)f is_improper_integrable_on_REAL by A5,A14,A16;
hence improper_integral_on_REAL (r(#)f)
= r * improper_integral_on_REAL f
by A1,A6,A7,Th36;
end;
end;
theorem Th50:
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
proof
let f be PartFunc of REAL,REAL, r be Real;
assume dom f = REAL & f is_improper_integrable_on_REAL; then
(-1)(#)f is_improper_integrable_on_REAL &
improper_integral_on_REAL ((-1)(#)f) = (-1) * improper_integral_on_REAL f
by Th49;
hence thesis by XXREAL_3:91;
end;
theorem Th51:
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
proof
let f,g be PartFunc of REAL,REAL;
assume that
A1: dom f = REAL and
A2: dom g = REAL and
A3: f is_improper_integrable_on_REAL and
A4: g is_improper_integrable_on_REAL and
A5: not (improper_integral_on_REAL f = +infty
& improper_integral_on_REAL g = -infty) and
A6: not (improper_integral_on_REAL f = -infty
& improper_integral_on_REAL g = +infty);
consider c be Real such that
A7: f is_-infty_improper_integrable_on c and
A8: f is_+infty_improper_integrable_on c and
A9: not (improper_integral_-infty(f,c) = -infty
& improper_integral_+infty(f,c) = +infty) and
A10: not (improper_integral_-infty(f,c) = +infty
& improper_integral_+infty(f,c) = -infty) by A3;
consider c1 be Real such that
A11: g is_-infty_improper_integrable_on c1 and
A12: g is_+infty_improper_integrable_on c1 and
A13: not (improper_integral_-infty(g,c1) = -infty
& improper_integral_+infty(g,c1) = +infty) and
A14: not (improper_integral_-infty(g,c1) = +infty
& improper_integral_+infty(g,c1) = -infty) by A4;
A15: left_closed_halfline c c= dom g by A2;
A16: right_closed_halfline c c= dom g by A2;
A17: left_closed_halfline c1 c= dom g by A2;
A18: right_closed_halfline c1 c= dom g by A2;
A19:g is_-infty_improper_integrable_on c
proof
per cases;
suppose c < c1;
hence g is_-infty_improper_integrable_on c by A2,A11,Th25;
end;
suppose A20: c1 <= c; then
g|['c1,c'] is bounded & g is_integrable_on ['c1,c'] by A12;
hence g is_-infty_improper_integrable_on c
by A20,A15,A11,Th26;
end;
end;
A21:g is_+infty_improper_integrable_on c
proof
per cases;
suppose A22: c < c1;
g|['c,c1'] is bounded & g is_integrable_on ['c,c1'] by A22,A11;
hence g is_+infty_improper_integrable_on c
by A22,A16,A12,Th31;
end;
suppose c1 <= c;
hence g is_+infty_improper_integrable_on c by A2,A12,Th30;
end;
end;
A23:not (improper_integral_-infty(g,c) = -infty
& improper_integral_+infty(g,c) = +infty)
proof
per cases;
suppose A24: c < c1; then
A25: g|['c,c1'] is bounded & g is_integrable_on ['c,c1'] by A11;
A26: g is_-infty_improper_integrable_on c
by A24,A2,A11,Th25;
g is_+infty_improper_integrable_on c
by A24,A16,A25,A12,Th31;
hence thesis by A13,A2,A17,A24,A25,A26,Th26,Th30;
end;
suppose A27: c1 <= c; then
A28: g|['c1,c'] is bounded & g is_integrable_on ['c1,c'] by A12; then
A29: g is_-infty_improper_integrable_on c
by A27,A15,A11,Th26;
g is_+infty_improper_integrable_on c
by A27,A2,A12,Th30;
hence thesis by A13,A2,A18,A28,A27,A29,Th25,Th31;
end;
end;
A30:not (improper_integral_-infty(g,c) = +infty
& improper_integral_+infty(g,c) = -infty)
proof
per cases;
suppose A31: c < c1;
A32: g|['c,c1'] is bounded & g is_integrable_on ['c,c1'] by A31,A11;
A33: g is_-infty_improper_integrable_on c
by A31,A2,A11,Th25;
g is_+infty_improper_integrable_on c
by A31,A16,A32,A12,Th31;
hence thesis by A14,A2,A17,A31,A32,A33,Th26,Th30;
end;
suppose A34: c1 <= c;
A35: g|['c1,c'] is bounded & g is_integrable_on ['c1,c'] by A34,A12;
A36: g is_-infty_improper_integrable_on c
by A34,A35,A15,A11,Th26;
g is_+infty_improper_integrable_on c
by A34,A2,A12,Th30;
hence thesis by A14,A2,A18,A35,A34,A36,Th25,Th31;
end;
end;
A37: improper_integral_on_REAL f
= improper_integral_-infty(f,c)+improper_integral_+infty(f,c)
by A1,A3,Th36;
A38: improper_integral_on_REAL g
= improper_integral_-infty(g,c)+improper_integral_+infty(g,c)
by A2,A4,Th36;
A39:not (improper_integral_-infty(f,c) = +infty &
improper_integral_-infty(g,c) = -infty)
by A5,A37,A38,A10,A23,XXREAL_3:def 2;
A40:not (improper_integral_-infty(f,c) = -infty &
improper_integral_-infty(g,c) = +infty)
by A6,A37,A38,A9,A30,XXREAL_3:def 2;
A41:not (improper_integral_+infty(f,c) = +infty &
improper_integral_+infty(g,c) = -infty)
by A5,A37,A38,A9,A30,XXREAL_3:def 2;
A42:not (improper_integral_+infty(f,c) = -infty &
improper_integral_+infty(g,c) = +infty)
by A6,A37,A38,A10,A23,XXREAL_3:def 2;
A43:f+g is_-infty_improper_integrable_on c
by A7,A19,A1,A2,A39,A40,Th45;
A44:improper_integral_-infty(f+g,c)
= improper_integral_-infty(f,c) + improper_integral_-infty(g,c)
by A1,A2,A7,A19,A39,A40,Th45;
A45:f+g is_+infty_improper_integrable_on c
by A1,A2,A8,A21,A41,A42,Th46;
A46:improper_integral_+infty(f+g,c)
= improper_integral_+infty(f,c) + improper_integral_+infty(g,c)
by A1,A2,A8,A21,A41,A42,Th46;
A47:now assume A48: improper_integral_-infty(f+g,c) = -infty &
improper_integral_+infty(f+g,c) = +infty;
per cases by A9,A23,A44,A46,A48,XXREAL_3:16,17;
suppose improper_integral_-infty(f,c) = -infty &
improper_integral_+infty(g,c) = +infty;
hence contradiction
by A6,A9,A37,A38,A23,XXREAL_3:def 2;
end;
suppose improper_integral_-infty(g,c) = -infty &
improper_integral_+infty(f,c) = +infty;
hence contradiction
by A5,A9,A37,A38,A23,XXREAL_3:def 2;
end;
end;
A49:now assume A50: improper_integral_-infty(f+g,c) = +infty &
improper_integral_+infty(f+g,c) = -infty;
per cases by A10,A30,A46,A50,A44,XXREAL_3:16,17;
suppose improper_integral_-infty(f,c) = +infty &
improper_integral_+infty(g,c) = -infty;
hence contradiction by A5,A10,A37,A38,A30,XXREAL_3:def 2;
end;
suppose improper_integral_-infty(g,c) = +infty &
improper_integral_+infty(f,c) = -infty;
hence contradiction by A6,A10,A37,A38,A30,XXREAL_3:def 2;
end;
end;
hence
A51: f+g is_improper_integrable_on_REAL by A43,A45,A47;
dom(f+g) = dom f /\ dom g by VALUED_1:def 1; then
A52:improper_integral_on_REAL (f+g)
= improper_integral_-infty(f+g,c) + improper_integral_+infty(f+g,c)
by A1,A2,A51,Th36;
per cases by XXREAL_0:14;
suppose A53: improper_integral_-infty(f+g,c) = +infty; then
A54: improper_integral_on_REAL (f+g) = +infty by A49,A52,XXREAL_3:def 2;
per cases by A53,A44,XXREAL_3:16;
suppose improper_integral_-infty(f,c) = +infty; then
improper_integral_on_REAL f = +infty by A10,A37,XXREAL_3:def 2;
hence improper_integral_on_REAL (f+g)
= improper_integral_on_REAL f + improper_integral_on_REAL g
by A5,A54,XXREAL_3:def 2;
end;
suppose improper_integral_-infty(g,c) = +infty; then
improper_integral_on_REAL g = +infty by A38,A30,XXREAL_3:def 2;
hence improper_integral_on_REAL (f+g)
= improper_integral_on_REAL f + improper_integral_on_REAL g
by A6,A54,XXREAL_3:def 2;
end;
end;
suppose A55: improper_integral_-infty(f+g,c) = -infty; then
A56: improper_integral_on_REAL (f+g) = -infty by A47,A52,XXREAL_3:def 2;
per cases by A55,A44,XXREAL_3:17;
suppose improper_integral_-infty(f,c) = -infty; then
improper_integral_on_REAL f = -infty by A9,A37,XXREAL_3:def 2;
hence improper_integral_on_REAL (f+g)
= improper_integral_on_REAL f + improper_integral_on_REAL g
by A6,A56,XXREAL_3:def 2;
end;
suppose improper_integral_-infty(g,c) = -infty; then
improper_integral_on_REAL g = -infty by A23,A38,XXREAL_3:def 2;
hence improper_integral_on_REAL(f+g)
= improper_integral_on_REAL f+improper_integral_on_REAL g
by A5,A56,XXREAL_3:def 2;
end;
end;
suppose A57: improper_integral_-infty(f+g,c) in REAL; then
A58: improper_integral_-infty(f,c) in REAL &
improper_integral_-infty(g,c) in REAL
by A39,A40,A44,XXREAL_3:20; then
reconsider lf = improper_integral_-infty(f,c),
lg = improper_integral_-infty(g,c) as Real;
per cases by XXREAL_0:14;
suppose A59: improper_integral_+infty(f+g,c) = +infty; then
improper_integral_+infty(f,c) = +infty or
improper_integral_+infty(g,c) = +infty by A46,XXREAL_3:16; then
improper_integral_on_REAL f = +infty or
improper_integral_on_REAL g = +infty by A58,A37,A38,XXREAL_3:def 2; then
improper_integral_on_REAL f + improper_integral_on_REAL g = +infty
by A5,A6,XXREAL_3:def 2;
hence improper_integral_on_REAL (f+g)
= improper_integral_on_REAL f+improper_integral_on_REAL g
by A57,A59,A52,XXREAL_3:def 2;
end;
suppose A60: improper_integral_+infty(f+g,c) = -infty; then
improper_integral_+infty(f,c) = -infty or
improper_integral_+infty(g,c) = -infty by A46,XXREAL_3:17; then
improper_integral_on_REAL f = -infty or
improper_integral_on_REAL g = -infty by A58,A37,A38,XXREAL_3:def 2; then
improper_integral_on_REAL f + improper_integral_on_REAL g = -infty
by A5,A6,XXREAL_3:def 2;
hence improper_integral_on_REAL(f+g)
= improper_integral_on_REAL f+improper_integral_on_REAL g
by A57,A60,A52,XXREAL_3:def 2;
end;
suppose improper_integral_+infty(f+g,c) in REAL; then
improper_integral_+infty(f,c) in REAL &
improper_integral_+infty(g,c) in REAL
by A41,A42,A46,XXREAL_3:20; then
reconsider rf = improper_integral_+infty(f,c),
rg = improper_integral_+infty(g,c) as Real;
improper_integral_on_REAL f = lf+rf &
improper_integral_on_REAL g = lg+rg by A37,A38,XXREAL_3:def 2; then
A61: improper_integral_on_REAL f+improper_integral_on_REAL g
= lf+rf + (lg+rg) by XXREAL_3:def 2;
improper_integral_-infty(f+g,c) = lf+lg &
improper_integral_+infty(f+g,c) = rf+rg
by A44,A46,XXREAL_3:def 2; then
improper_integral_on_REAL(f+g) = lf+lg + (rf+rg) by A52,XXREAL_3:def 2;
hence improper_integral_on_REAL(f+g)
= improper_integral_on_REAL f+improper_integral_on_REAL g by A61;
end;
end;
end;
theorem
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
proof
let f,g be PartFunc of REAL,REAL;
assume that
A1: dom f = REAL and
A2: dom g = REAL and
A3: f is_improper_integrable_on_REAL and
A4: g is_improper_integrable_on_REAL and
A5: not (improper_integral_on_REAL f = +infty
& improper_integral_on_REAL g = +infty) and
A6: not (improper_integral_on_REAL f = -infty
& improper_integral_on_REAL g = -infty);
A7: dom(-g) = dom g by VALUED_1:8;
A8: -g is_improper_integrable_on_REAL by A2,A4,Th50;
A9:improper_integral_on_REAL (-g) = -improper_integral_on_REAL g by A2,A4,Th50;
A10: improper_integral_on_REAL f <> +infty
or improper_integral_on_REAL(-g) <> -infty
by A5,A9,XXREAL_3:23;
A11: improper_integral_on_REAL f <> -infty
or improper_integral_on_REAL(-g) <> +infty
by A6,A9,XXREAL_3:23;
hence f-g is_improper_integrable_on_REAL by A1,A2,A3,A7,A8,A10,Th51;
improper_integral_on_REAL(f-g)
= improper_integral_on_REAL f + improper_integral_on_REAL (-g)
by A1,A2,A3,A7,A8,A10,A11,Th51; then
improper_integral_on_REAL(f-g)
=improper_integral_on_REAL f + -improper_integral_on_REAL g by A2,A4,Th50;
hence improper_integral_on_REAL (f-g)
= improper_integral_on_REAL f-improper_integral_on_REAL g
by XXREAL_3:def 4;
end;