:: Extended {R}iemann Integral of Functions of Real Variable and One-sided
:: {L}aplace Transform
:: by Masahiko Yamazaki , Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura
::
:: Received July 22, 2008
:: Copyright (c) 2008-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 NUMBERS, SUBSET_1, ARYTM_3, CARD_1, ARYTM_1, RELAT_1, XXREAL_0,
REAL_1, SIN_COS, FUNCT_1, INTEGRA1, XXREAL_1, TARSKI, ORDINAL2, INTEGRA5,
PARTFUN1, XXREAL_2, LIMFUNC2, LIMFUNC1, XBOOLE_0, VALUED_1, COMPLEX1,
INTEGR10, FUNCT_7;
notations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, XXREAL_0, COMPLEX1,
XCMPLX_0, REAL_1, FUNCT_1, RELSET_1, FUNCT_2, RCOMP_1, PARTFUN1, SEQ_2,
LIMFUNC1, LIMFUNC2, MEMBERED, INTEGRA5, SIN_COS, VALUED_1, FCONT_1;
constructors REAL_1, LIMFUNC1, LIMFUNC2, SEQ_2, FCONT_1, INTEGRA5, COMSEQ_3,
SIN_COS, INTEGRA7, RELSET_1, RCOMP_1, COMSEQ_2, BINOP_2;
registrations XREAL_0, NUMBERS, MEMBERED, NAT_1, XBOOLE_0, VALUED_0, SIN_COS,
FCONT_1, RELSET_1, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions MEMBERED;
equalities XCMPLX_0, LIMFUNC1;
expansions MEMBERED;
theorems LIMFUNC1, LIMFUNC2, PARTFUN1, RFUNCT_1, COMPLEX1, RCOMP_1, XREAL_0,
XXREAL_0, FUNCT_2, XBOOLE_1, XREAL_1, INTEGRA5, INTEGRA6, INTEGRA7,
VALUED_1, XXREAL_1, SIN_COS, RELSET_1;
schemes FUNCT_2, PARTFUN2;
begin :: Preliminaries
reserve a,b,r,g for Real;
theorem Th1:
for a,b,g1,M be Real st a < b & 0 < g1 & 0 < M holds ex r
st a < r & r < b & (b - r)*M < g1
proof
let a,b,g1,M be Real such that
A1: a < b and
A2: 0 < g1 and
A3: 0 < M;
set r3 = max(a,b - g1/M);
b - g1/M < b by A2,A3,XREAL_1:44,139;
then r3 < b by A1,XXREAL_0:16;
then consider q be Real such that
A4: r3 < q and
A5: q < b by XREAL_1:5;
reconsider r = q as Real;
take r;
b - g1/M <= r3 by XXREAL_0:25;
then b - g1/M < r by A4,XXREAL_0:2;
then b - g1/M - (r - g1/M) < r - (r - g1/M) by XREAL_1:14;
then (b - r)*1 < g1/M;
then a <= r3 & (b - r)*M < g1/1 by A3,XREAL_1:111,XXREAL_0:25;
hence thesis by A4,A5,XXREAL_0:2;
end;
theorem Th2:
for a,b,g1,M be Real st a < b & 0 < g1 & 0 < M holds ex r
st a < r & r < b & (r - a)*M < g1
proof
let a,b,g1,M be Real such that
A1: a < b and
A2: 0 < g1 & 0 < M;
(-b) < (-a) by A1,XREAL_1:24;
then consider r1 be Real such that
A3: (-b) < r1 & r1 < (-a) and
A4: ((-a) - r1)*M < g1 by A2,Th1;
reconsider r= -r1 as Real;
take r;
-(-b) > -r1 & -r1 > -(-a) by A3,XREAL_1:24;
hence thesis by A4;
end;
theorem
exp_R.b - exp_R.a = integral(exp_R,a,b)
proof
A1: min(a,b) <= a by XXREAL_0:17;
A2: [. min(a,b),max(a,b) .] c= REAL;
exp_R|REAL is continuous & a <= max(a,b) by XXREAL_0:25;
then
A3: exp_R.max(a,b) = integral(exp_R,min(a,b),max(a,b)) + exp_R.min(a,b) by A1
,A2,INTEGRA7:20,27,SIN_COS:47,XXREAL_0:2;
A4: min(a,b) = a implies exp_R.b - exp_R.a = integral(exp_R,a,b)
proof
assume
A5: min(a,b) = a;
then max(a,b) = b by XXREAL_0:36;
hence thesis by A3,A5;
end;
min(a,b) = b implies exp_R.b - exp_R.a = integral(exp_R,a,b)
proof
assume
A6: min(a,b) = b;
then
A7: max(a,b) = a by XXREAL_0:36;
b < a implies exp_R.b - exp_R.a = integral(exp_R,a,b)
proof
assume b < a;
then integral(exp_R,a,b) = -integral(exp_R,[' b,a ']) by INTEGRA5:def 4;
then exp_R.a = -integral(exp_R,a,b) + exp_R.b by A1,A3,A6,A7,
INTEGRA5:def 4;
hence thesis;
end;
hence thesis by A1,A4,A6,XXREAL_0:1;
end;
hence thesis by A4,XXREAL_0:15;
end;
begin :: The Definition of Extended Riemann Integral
definition
let f be PartFunc of REAL,REAL;
let a,b be Real;
pred f is_right_ext_Riemann_integrable_on a,b means
(for d be Real st
a <= d & d < b holds f is_integrable_on [' a,d '] & f|[' a,d '] is bounded) &
ex Intf be PartFunc of REAL,REAL st dom Intf = [.a,b.[ &
(for x be Real st x in
dom Intf holds Intf.x = integral(f,a,x)) & Intf is_left_convergent_in b;
end;
definition
let f be PartFunc of REAL,REAL;
let a,b be Real;
pred f is_left_ext_Riemann_integrable_on a,b means
(for d be Real st
a < d & d <= b holds f is_integrable_on [' d,b '] & f|[' d,b '] is bounded) &
ex Intf be PartFunc of REAL,REAL st dom Intf = ].a,b.] &
(for x be Real st x in
dom Intf holds Intf.x = integral(f,x,b)) & Intf is_right_convergent_in a;
end;
definition
let f be PartFunc of REAL,REAL;
let a,b be Real;
assume
A1: f is_right_ext_Riemann_integrable_on a,b;
func ext_right_integral(f,a,b) -> Real means
:Def3:
ex Intf be PartFunc of
REAL,REAL st dom Intf = [.a,b.[ &
(for x be Real st x in dom Intf holds Intf.x
= integral(f,a,x)) & Intf is_left_convergent_in b & it = lim_left(Intf,b);
existence
proof
consider Intf be PartFunc of REAL,REAL such that
A2: ( dom Intf = [.a,b.[ &
for x be Real st x in dom Intf holds Intf.x
= integral( f,a,x) )& Intf is_left_convergent_in b by A1;
take lim_left(Intf,b);
thus thesis by A2;
end;
uniqueness
proof
let y1,y2 be Real;
assume ex Intf1 be PartFunc of REAL,REAL st dom Intf1 = [.a,b.[ & (for x
be Real st x in dom Intf1 holds Intf1.x = integral(f,a,x)) & Intf1
is_left_convergent_in b & y1 = lim_left(Intf1,b);
then consider Intf1 be PartFunc of REAL,REAL such that
A3: dom Intf1 = [.a,b.[ and
A4: for x be Real st x in dom Intf1 holds Intf1.x = integral(f,a,x) and
Intf1 is_left_convergent_in b and
A5: y1 = lim_left(Intf1,b);
assume ex Intf2 be PartFunc of REAL,REAL st dom Intf2 = [.a,b.[ & (for x
be Real st x in dom Intf2 holds Intf2.x = integral(f,a,x)) & Intf2
is_left_convergent_in b & y2 = lim_left(Intf2,b);
then consider Intf2 be PartFunc of REAL,REAL such that
A6: dom Intf2 = [.a,b.[ and
A7: for x be Real st x in dom Intf2 holds Intf2.x = integral(f,a,x) and
Intf2 is_left_convergent_in b and
A8: y2 = lim_left(Intf2,b);
now
let x be Element of REAL;
assume
A9: x in dom Intf1;
hence Intf1.x = integral(f,a,x) by A4
.= Intf2.x by A3,A6,A7,A9;
end;
hence thesis by A3,A5,A6,A8,PARTFUN1:5;
end;
end;
definition
let f be PartFunc of REAL,REAL;
let a,b be Real;
assume
A1: f is_left_ext_Riemann_integrable_on a,b;
func ext_left_integral(f,a,b) -> Real means
:Def4:
ex Intf be PartFunc of
REAL,REAL st dom Intf = ].a,b.] &
(for x be Real st x in dom Intf holds Intf.x
= integral(f,x,b)) & Intf is_right_convergent_in a & it = lim_right(Intf,a);
existence
proof
consider Intf be PartFunc of REAL,REAL such that
A2: ( dom Intf = ].a,b.] &
for x be Real st x in dom Intf holds Intf.x
= integral( f,x,b) )& Intf is_right_convergent_in a by A1;
take lim_right(Intf,a);
thus thesis by A2;
end;
uniqueness
proof
let y1,y2 be Real;
assume ex Intf1 be PartFunc of REAL,REAL st dom Intf1 = ].a,b.] & (for x
be Real st x in dom Intf1 holds Intf1.x = integral(f,x,b)) & Intf1
is_right_convergent_in a & y1 = lim_right(Intf1,a);
then consider Intf1 be PartFunc of REAL,REAL such that
A3: dom Intf1 = ].a,b.] and
A4: for x be Real st x in dom Intf1 holds Intf1.x = integral(f,x,b) and
Intf1 is_right_convergent_in a and
A5: y1 = lim_right(Intf1,a);
assume ex Intf2 be PartFunc of REAL,REAL st dom Intf2 = ].a,b.] & (for x
be Real st x in dom Intf2 holds Intf2.x = integral(f,x,b)) & Intf2
is_right_convergent_in a & y2 = lim_right(Intf2,a);
then consider Intf2 be PartFunc of REAL,REAL such that
A6: dom Intf2 = ].a,b.] and
A7: for x be Real st x in dom Intf2 holds Intf2.x = integral(f,x,b) and
Intf2 is_right_convergent_in a and
A8: y2 = lim_right(Intf2,a);
now
let x be Element of REAL;
assume
A9: x in dom Intf1;
hence Intf1.x = integral(f,x,b) by A4
.= Intf2.x by A3,A6,A7,A9;
end;
hence thesis by A3,A5,A6,A8,PARTFUN1:5;
end;
end;
definition
let f be PartFunc of REAL,REAL;
let a be Real;
pred f is_+infty_ext_Riemann_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;
end;
definition
let f be PartFunc of REAL,REAL;
let b be Real;
pred f is_-infty_ext_Riemann_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;
end;
definition
let f be PartFunc of REAL,REAL;
let a be Real;
assume
A1: f is_+infty_ext_Riemann_integrable_on a;
func infty_ext_right_integral(f,a) -> Real means
:Def7:
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;
existence
proof
consider Intf be PartFunc of REAL,REAL such that
A2: ( 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 A1;
take lim_in+infty Intf;
thus thesis by A2;
end;
uniqueness
proof
let L1,L2 be Real;
assume ex Intf1 be PartFunc of REAL,REAL st dom Intf1 =
right_closed_halfline(a) & (for x be Real st x in dom Intf1 holds Intf1.x =
integral(f,a,x)) & Intf1 is convergent_in+infty & L1 = lim_in+infty Intf1;
then consider Intf1 be PartFunc of REAL,REAL such that
A3: dom Intf1 = right_closed_halfline(a) and
A4: for x be Real st x in dom Intf1 holds Intf1.x = integral(f,a,x) and
Intf1 is convergent_in+infty and
A5: L1 = lim_in+infty Intf1;
assume ex Intf2 be PartFunc of REAL,REAL st dom Intf2 =
right_closed_halfline(a) & (for x be Real st x in dom Intf2 holds Intf2.x =
integral(f,a,x)) & Intf2 is convergent_in+infty & L2 = lim_in+infty Intf2;
then consider Intf2 be PartFunc of REAL,REAL such that
A6: dom Intf2 = right_closed_halfline(a) and
A7: for x be Real st x in dom Intf2 holds Intf2.x = integral(f,a,x) and
Intf2 is convergent_in+infty and
A8: L2 = lim_in+infty Intf2;
now
let x be Element of REAL;
assume
A9: x in dom Intf1;
hence Intf1.x = integral(f,a,x) by A4
.= Intf2.x by A3,A6,A7,A9;
end;
hence thesis by A3,A5,A6,A8,PARTFUN1:5;
end;
end;
definition
let f be PartFunc of REAL,REAL;
let b be Real;
assume
A1: f is_-infty_ext_Riemann_integrable_on b;
func infty_ext_left_integral(f,b) -> Real means
:Def8:
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;
existence
proof
consider Intf be PartFunc of REAL,REAL such that
A2: ( 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 A1;
take lim_in-infty Intf;
thus thesis by A2;
end;
uniqueness
proof
let L1,L2 be Real;
assume ex Intf1 be PartFunc of REAL,REAL st dom Intf1 =
left_closed_halfline(b) & (for x be Real st x in dom Intf1 holds Intf1.x =
integral(f,x,b)) & Intf1 is convergent_in-infty & L1 = lim_in-infty Intf1;
then consider Intf1 be PartFunc of REAL,REAL such that
A3: dom Intf1 = left_closed_halfline(b) and
A4: for x be Real st x in dom Intf1 holds Intf1.x = integral(f,x,b) and
Intf1 is convergent_in-infty and
A5: L1 = lim_in-infty Intf1;
assume ex Intf2 be PartFunc of REAL,REAL st dom Intf2 =
left_closed_halfline(b) & (for x be Real st x in dom Intf2 holds Intf2.x =
integral(f,x,b)) & Intf2 is convergent_in-infty & L2 = lim_in-infty Intf2;
then consider Intf2 be PartFunc of REAL,REAL such that
A6: dom Intf2 = left_closed_halfline(b) and
A7: for x be Real st x in dom Intf2 holds Intf2.x = integral(f,x,b) and
Intf2 is convergent_in-infty and
A8: L2 = lim_in-infty Intf2;
now
let x be Element of REAL;
assume
A9: x in dom Intf1;
hence Intf1.x = integral(f,x,b) by A4
.= Intf2.x by A3,A6,A7,A9;
end;
hence thesis by A3,A5,A6,A8,PARTFUN1:5;
end;
end;
definition
let f be PartFunc of REAL,REAL;
attr f is infty_ext_Riemann_integrable means
f
is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0
;
end;
definition
let f be PartFunc of REAL,REAL;
func infty_ext_integral(f) -> Real equals
infty_ext_right_integral(f,0) +
infty_ext_left_integral(f,0);
coherence;
end;
begin :: Linearity of Extended Riemann Integral
theorem
for f,g be PartFunc of REAL,REAL, a,b be Real st a < b & [' a,b '] c=
dom f & [' a,b '] c= dom g & f is_right_ext_Riemann_integrable_on a,b & g
is_right_ext_Riemann_integrable_on a,b holds f + g
is_right_ext_Riemann_integrable_on a,b & ext_right_integral(f + g,a,b) =
ext_right_integral(f,a,b) + ext_right_integral(g,a,b)
proof
let f,g be PartFunc of REAL,REAL, a,b be Real such that
A1: a < b and
A2: [' a,b '] c= dom f & [' a,b '] c= dom g and
A3: f is_right_ext_Riemann_integrable_on a,b and
A4: g is_right_ext_Riemann_integrable_on a,b;
consider Intg be PartFunc of REAL,REAL such that
A5: dom Intg = [.a,b.[ and
A6: for x be Real st x in dom Intg holds Intg.x = integral(g,a,x) and
A7: Intg is_left_convergent_in b and
A8: ext_right_integral(g,a,b) = lim_left(Intg,b) by A4,Def3;
consider Intf be PartFunc of REAL,REAL such that
A9: dom Intf = [.a,b.[ and
A10: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x) and
A11: Intf is_left_convergent_in b and
A12: ext_right_integral(f,a,b) = lim_left(Intf,b) by A3,Def3;
set Intfg = Intf + Intg;
A13: dom Intfg = [.a,b.[ &
for x be Real st x in dom Intfg holds Intfg.x =
integral(f + g,a,x)
proof
A14: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
thus
A15: dom Intfg = dom Intf /\ dom Intg by VALUED_1:def 1
.= [.a,b.[ by A9,A5;
let x be Real;
assume
A16: x in dom Intfg;
then
A17: x < b by A15,XXREAL_1:3;
then
A18: [.a,x.] c= [.a,b.] by XXREAL_1:34;
A19: a <= x by A15,A16,XXREAL_1:3;
then
A20: f is_integrable_on [' a,x '] & f|[' a,x '] is bounded by A3,A17;
[' a,x '] = [.a,x.] by A19,INTEGRA5:def 3;
then
A21: [' a,x '] c= dom f & [' a,x '] c= dom g by A2,A14,A18;
A22: g is_integrable_on [' a,x '] & g|[' a,x '] is bounded by A4,A19,A17;
thus Intfg.x = Intf.x + Intg.x by A16,VALUED_1:def 1
.= integral(f,a,x) + Intg.x by A9,A10,A15,A16
.= integral(f,a,x) + integral(g,a,x) by A5,A6,A15,A16
.= integral(f + g,a,x) by A19,A21,A20,A22,INTEGRA6:12;
end;
A23: for r st r < b ex g st r < g & g < b & g in dom(Intf + Intg)
proof
let r be Real such that
A24: r < b;
per cases;
suppose
A25: r < a;
reconsider g = a as Real;
take g;
thus thesis by A1,A13,A25,XXREAL_1:3;
end;
suppose
not r < a;
then
A26: a - a <= r - a by XREAL_1:9;
reconsider g = r + (b - r)/2 as Real;
take g;
A27: 0 < b - r by A24,XREAL_1:50;
then (b - r)/2 < b - r by XREAL_1:216;
then
A28: (b - r)/2 + r < b - r + r by XREAL_1:8;
r < g by A27,XREAL_1:29,215;
then
A29: r - (r - a) < g - 0 by A26,XREAL_1:14;
0 < (b - r)/2 by A27,XREAL_1:215;
hence thesis by A13,A29,A28,XREAL_1:8,XXREAL_1:3;
end;
end;
then
A30: Intfg is_left_convergent_in b by A11,A7,LIMFUNC2:45;
for d be Real st a <= d & d < b
holds f + g is_integrable_on [' a,d '] &
(f+g)|[' a,d '] is bounded
proof
let d be Real;
assume
A31: a <= d & d < b;
then
A32: [' a,d '] = [.a,d.] & [.a,d.] c= [.a,b.] by INTEGRA5:def 3,XXREAL_1:34;
[' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A33: [' a,d '] c= dom f & [' a,d '] c= dom g by A2,A32;
A34: f is_integrable_on [' a,d '] & g is_integrable_on [' a,d '] by A3,A4,A31;
A35: f|[' a,d '] is bounded & g|[' a,d '] is bounded by A3,A4,A31;
then (f + g)|([' a,d '] /\ [' a,d ']) is bounded by RFUNCT_1:83;
hence thesis by A33,A34,A35,INTEGRA6:11;
end;
hence
A36: f + g is_right_ext_Riemann_integrable_on a,b by A13,A30;
lim_left(Intfg,b) = ext_right_integral(f,a,b) + ext_right_integral(g,a
,b) by A11,A12,A7,A8,A23,LIMFUNC2:45;
hence thesis by A13,A30,A36,Def3;
end;
theorem
for f be PartFunc of REAL,REAL, a,b be Real st a < b & [' a,b '] c=
dom f & f is_right_ext_Riemann_integrable_on a,b holds for r be Real holds r(#)
f is_right_ext_Riemann_integrable_on a,b & ext_right_integral(r(#)f,a,b) = r*
ext_right_integral(f,a,b)
proof
let f be PartFunc of REAL,REAL, a,b be Real such that
A1: a < b and
A2: [' a,b '] c= dom f and
A3: f is_right_ext_Riemann_integrable_on a,b;
for r be Real holds r(#)f is_right_ext_Riemann_integrable_on a,b &
ext_right_integral(r(#)f,a,b) = r*ext_right_integral(f,a,b)
proof
let r be Real;
consider Intf be PartFunc of REAL,REAL such that
A4: dom Intf = [.a,b.[ and
A5: for x be Real st x in dom Intf holds Intf.x =integral(f,a,x) and
A6: Intf is_left_convergent_in b and
A7: ext_right_integral(f,a,b) = lim_left(Intf,b) by A3,Def3;
set Intfg = r(#)Intf;
A8: Intfg is_left_convergent_in b by A6,LIMFUNC2:43;
A9: dom Intfg = [.a,b.[ &
for x be Real st x in dom Intfg holds Intfg.x =
integral(r(#)f,a,x)
proof
A10: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
thus
A11: dom Intfg = [.a,b.[ by A4,VALUED_1:def 5;
let x be Real;
assume
A12: x in dom Intfg;
then
A13: a <= x by A11,XXREAL_1:3;
then
A14: [' a,x '] = [.a,x.] by INTEGRA5:def 3;
A15: x < b by A11,A12,XXREAL_1:3;
then
A16: [.a,x.] c= [.a,b.] by XXREAL_1:34;
A17: f is_integrable_on [' a,x '] & f|[' a,x '] is bounded by A3,A13,A15;
thus Intfg.x = r*Intf.x by A12,VALUED_1:def 5
.= r*integral(f,a,x) by A4,A5,A11,A12
.= integral(r(#)f,a,x) by A2,A13,A14,A10,A16,A17,INTEGRA6:10,XBOOLE_1:1
;
end;
for d be Real
st a<= d & d < b holds r(#)f is_integrable_on [' a,d '] &
(r(#)f)|[' a,d '] is bounded
proof
let d be Real;
assume
A18: a <= d & d < b;
then
A19: [' a,d '] = [.a,d.] & [.a,d.] c= [.a,b.] by INTEGRA5:def 3,XXREAL_1:34;
A20: f is_integrable_on [' a,d '] & f|[' a,d '] is bounded by A3,A18;
[' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then [' a,d '] c= dom f by A2,A19;
hence thesis by A20,INTEGRA6:9,RFUNCT_1:80;
end;
hence
A21: r(#)f is_right_ext_Riemann_integrable_on a,b by A9,A8;
lim_left (Intfg,b) = r*ext_right_integral(f,a,b) by A6,A7,LIMFUNC2:43;
hence thesis by A9,A8,A21,Def3;
end;
hence thesis;
end;
theorem
for f,g be PartFunc of REAL,REAL, a,b be Real st a < b & [' a,b '] c=
dom f & [' a,b '] c= dom g & f is_left_ext_Riemann_integrable_on a,b & g
is_left_ext_Riemann_integrable_on a,b holds f + g
is_left_ext_Riemann_integrable_on a,b & ext_left_integral(f + g,a,b) =
ext_left_integral(f,a,b) + ext_left_integral(g,a,b)
proof
let f,g be PartFunc of REAL,REAL, a,b be Real such that
A1: a < b and
A2: [' a,b '] c= dom f & [' a,b '] c= dom g and
A3: f is_left_ext_Riemann_integrable_on a,b and
A4: g is_left_ext_Riemann_integrable_on a,b;
consider Intg be PartFunc of REAL,REAL such that
A5: dom Intg = ].a,b.] and
A6: for x be Real st x in dom Intg holds Intg.x = integral(g,x,b) and
A7: Intg is_right_convergent_in a and
A8: ext_left_integral(g,a,b) = lim_right(Intg,a) by A4,Def4;
consider Intf be PartFunc of REAL,REAL such that
A9: dom Intf = ].a,b.] and
A10: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
A11: Intf is_right_convergent_in a and
A12: ext_left_integral(f,a,b) = lim_right(Intf,a) by A3,Def4;
set Intfg = Intf + Intg;
A13: dom Intfg = ].a,b.] &
for x be Real st x in dom Intfg holds Intfg.x =
integral(f + g,x,b)
proof
A14: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
thus
A15: dom Intfg = dom Intf /\ dom Intg by VALUED_1:def 1
.= ].a,b.] by A9,A5;
let x be Real;
assume
A16: x in dom Intfg;
then
A17: a < x by A15,XXREAL_1:2;
then
A18: [.x,b.] c= [.a,b.] by XXREAL_1:34;
A19: x <= b by A15,A16,XXREAL_1:2;
then
A20: f is_integrable_on [' x,b '] & f|[' x,b '] is bounded by A3,A17;
[' x,b '] = [.x,b.] by A19,INTEGRA5:def 3;
then
A21: [' x,b '] c= dom f & [' x,b '] c= dom g by A2,A14,A18;
A22: g is_integrable_on [' x,b '] & g|[' x,b '] is bounded by A4,A17,A19;
thus Intfg.x = Intf.x + Intg.x by A16,VALUED_1:def 1
.= integral(f,x,b) + Intg.x by A9,A10,A15,A16
.= integral(f,x,b) + integral(g,x,b) by A5,A6,A15,A16
.= integral(f + g,x,b) by A19,A21,A20,A22,INTEGRA6:12;
end;
A23: for r st a < r ex g st g < r & a < g & g in dom(Intf + Intg)
proof
let r be Real such that
A24: a < r;
per cases;
suppose
A25: b < r;
reconsider g = b as Real;
take g;
thus thesis by A1,A13,A25,XXREAL_1:2;
end;
suppose
A26: not b < r;
reconsider g = r - (r - a)/2 as Real;
take g;
A27: 0 < r - a by A24,XREAL_1:50;
then (r - a)/2 < r - a by XREAL_1:216;
then
A28: (r - a)/2 + (a - (r - a)/2) < r - a + (a - (r - a)/2) by XREAL_1:8;
A29: 0 < (r - a)/2 by A27,XREAL_1:215;
then r - (r - a)/2 < b - 0 by A26,XREAL_1:15;
hence thesis by A13,A29,A28,XREAL_1:44,XXREAL_1:2;
end;
end;
then
A30: Intfg is_right_convergent_in a by A11,A7,LIMFUNC2:54;
for d be Real st a < d & d <= b holds f + g is_integrable_on [' d,b ']
& (f+g)|[' d,b '] is bounded
proof
let d be Real;
assume
A31: a < d & d <= b;
then
A32: [' d,b '] = [.d,b.] & [.d,b.] c= [.a,b.] by INTEGRA5:def 3,XXREAL_1:34;
[' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A33: [' d,b '] c= dom f & [' d,b '] c= dom g by A2,A32;
A34: f is_integrable_on [' d,b '] & g is_integrable_on [' d,b '] by A3,A4,A31;
A35: f|[' d,b '] is bounded & g|[' d,b '] is bounded by A3,A4,A31;
then (f + g)|([' d,b '] /\ [' d,b ']) is bounded by RFUNCT_1:83;
hence thesis by A33,A34,A35,INTEGRA6:11;
end;
hence
A36: f + g is_left_ext_Riemann_integrable_on a,b by A13,A30;
lim_right(Intfg,a) = ext_left_integral(f, a,b) + ext_left_integral(g,a,
b) by A11,A12,A7,A8,A23,LIMFUNC2:54;
hence thesis by A13,A30,A36,Def4;
end;
theorem
for f be PartFunc of REAL,REAL, a,b be Real st a < b & [' a,b '] c=
dom f & f is_left_ext_Riemann_integrable_on a,b holds for r be Real holds r(#)f
is_left_ext_Riemann_integrable_on a,b & ext_left_integral(r(#)f,a,b) = r*
ext_left_integral(f,a,b)
proof
let f be PartFunc of REAL,REAL, a,b be Real such that
A1: a < b and
A2: [' a,b '] c= dom f and
A3: f is_left_ext_Riemann_integrable_on a,b;
for r be Real holds r(#)f is_left_ext_Riemann_integrable_on a,b &
ext_left_integral(r(#)f,a,b) = r*ext_left_integral(f,a,b)
proof
let r be Real;
consider Intf be PartFunc of REAL,REAL such that
A4: dom Intf = ].a,b.] and
A5: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
A6: Intf is_right_convergent_in a and
A7: ext_left_integral(f,a,b) = lim_right(Intf,a) by A3,Def4;
set Intfg = r(#)Intf;
A8: Intfg is_right_convergent_in a by A6,LIMFUNC2:52;
A9: dom Intfg = ].a,b.] &
for x be Real st x in dom Intfg holds Intfg.x =
integral(r(#)f,x,b)
proof
A10: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
thus
A11: dom Intfg = ].a,b.] by A4,VALUED_1:def 5;
let x be Real;
assume
A12: x in dom Intfg;
then
A13: a < x by A11,XXREAL_1:2;
then
A14: [.x,b.] c= [.a,b.] by XXREAL_1:34;
A15: x <= b by A11,A12,XXREAL_1:2;
then
A16: [' x,b '] = [.x,b.] by INTEGRA5:def 3;
A17: f is_integrable_on [' x,b '] & f|[' x,b '] is bounded by A3,A13,A15;
thus Intfg.x = r*Intf.x by A12,VALUED_1:def 5
.= r*integral(f,x,b) by A4,A5,A11,A12
.= integral(r(#)f,x,b) by A2,A15,A16,A10,A14,A17,INTEGRA6:10,XBOOLE_1:1
;
end;
for d be Real st a < d & d <= b
holds r(#)f is_integrable_on [' d,b ']
& (r(#)f)|[' d,b '] is bounded
proof
let d be Real;
assume
A18: a < d & d <= b;
then
A19: [' d,b '] = [.d,b.] & [.d,b.] c= [.a,b.] by INTEGRA5:def 3,XXREAL_1:34;
A20: f is_integrable_on [' d,b '] & f|[' d,b '] is bounded by A3,A18;
[' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then [' d,b '] c= dom f by A2,A19;
hence thesis by A20,INTEGRA6:9,RFUNCT_1:80;
end;
hence
A21: r(#)f is_left_ext_Riemann_integrable_on a,b by A9,A8;
lim_right (Intfg,a) = r*ext_left_integral(f,a,b) by A6,A7,LIMFUNC2:52;
hence thesis by A9,A8,A21,Def4;
end;
hence thesis;
end;
theorem Th8:
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_ext_Riemann_integrable_on a & g is_+infty_ext_Riemann_integrable_on a
holds 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)
proof
let f,g be PartFunc of REAL,REAL, a be Real;
assume that
A1: right_closed_halfline(a) c= dom f & right_closed_halfline(a) c= dom g and
A2: f is_+infty_ext_Riemann_integrable_on a and
A3: g is_+infty_ext_Riemann_integrable_on a;
consider Intg be PartFunc of REAL,REAL such that
A4: dom Intg = right_closed_halfline(a) and
A5: for x be Real st x in dom Intg holds Intg.x = integral(g,a,x) and
A6: Intg is convergent_in+infty and
A7: infty_ext_right_integral(g,a) = lim_in+infty Intg by A3,Def7;
consider Intf be PartFunc of REAL,REAL such that
A8: dom Intf = right_closed_halfline(a) and
A9: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x) and
A10: Intf is convergent_in+infty and
A11: infty_ext_right_integral(f,a) = lim_in+infty Intf by A2,Def7;
set Intfg = Intf + Intg;
A12: dom Intfg = right_closed_halfline(a) & for x be Real st x in dom Intfg
holds Intfg.x = integral(f + g,a,x)
proof
thus
A13: dom Intfg = dom Intf /\ dom Intg by VALUED_1:def 1
.= right_closed_halfline(a) by A8,A4;
let x be Real;
assume
A14: x in dom Intfg;
then
A15: a <= x by A13,XXREAL_1:236;
then
A16: f is_integrable_on [' a,x '] & f|[' a,x '] is bounded by A2;
A17: [.a,x.] c= right_closed_halfline(a) by XXREAL_1:251;
[' a,x '] = [.a,x.] by A15,INTEGRA5:def 3;
then
A18: [' a,x '] c= dom f & [' a,x '] c= dom g by A1,A17;
A19: g is_integrable_on [' a,x '] & g|[' a,x '] is bounded by A3,A15;
thus Intfg.x = Intf.x + Intg.x by A14,VALUED_1:def 1
.= integral(f,a,x) + Intg.x by A8,A9,A13,A14
.= integral(f,a,x) + integral(g,a,x) by A4,A5,A13,A14
.= integral(f + g,a,x) by A15,A18,A16,A19,INTEGRA6:12;
end;
A20: for r ex g st r < g & g in dom(Intf + Intg)
proof
let r be Real;
per cases;
suppose
A21: r < a;
reconsider g = a as Real;
take g;
thus thesis by A12,A21,XXREAL_1:236;
end;
suppose
A22: not r < a;
reconsider g = r + 1 as Real;
take g;
A23: r + 0 < r + 1 by XREAL_1:8;
then a <= g by A22,XXREAL_0:2;
hence thesis by A12,A23,XXREAL_1:236;
end;
end;
then
A24: Intfg is convergent_in+infty by A10,A6,LIMFUNC1:82;
for b be Real st a <= b holds f + g is_integrable_on [' a,b '] & (f+g)|
[' a,b '] is bounded
proof
let b be Real;
A25: [.a,b.] c= right_closed_halfline(a) by XXREAL_1:251;
assume
A26: a <= b;
then
A27: f is_integrable_on [' a,b '] & g is_integrable_on [' a,b '] by A2,A3;
[' a,b '] = [.a,b.] by A26,INTEGRA5:def 3;
then
A28: [' a,b '] c= dom f & [' a,b '] c= dom g by A1,A25;
A29: f|[' a,b '] is bounded & g|[' a,b '] is bounded by A2,A3,A26;
then (f + g)|([' a,b '] /\ [' a,b ']) is bounded by RFUNCT_1:83;
hence thesis by A28,A27,A29,INTEGRA6:11;
end;
hence
A30: (f + g) is_+infty_ext_Riemann_integrable_on a by A12,A24;
lim_in+infty (Intfg) = infty_ext_right_integral(f,a) +
infty_ext_right_integral(g,a) by A10,A11,A6,A7,A20,LIMFUNC1:82;
hence thesis by A12,A24,A30,Def7;
end;
theorem Th9:
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 r be Real holds r(#)f is_+infty_ext_Riemann_integrable_on a &
infty_ext_right_integral(r(#)f,a) = r*infty_ext_right_integral(f,a)
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;
for r be Real holds r(#)f is_+infty_ext_Riemann_integrable_on a &
infty_ext_right_integral(r(#)f,a) = r*infty_ext_right_integral(f,a)
proof
let r be Real;
consider Intf be PartFunc of REAL,REAL such 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) and
A5: Intf is convergent_in+infty and
A6: infty_ext_right_integral(f,a) = lim_in+infty Intf by A2,Def7;
set Intfg = r(#)Intf;
A7: Intfg is convergent_in+infty by A5,LIMFUNC1:80;
A8: dom Intfg = right_closed_halfline(a) & for x be Real st x in dom
Intfg holds Intfg.x = integral(r(#)f,a,x)
proof
thus
A9: dom Intfg = right_closed_halfline(a) by A3,VALUED_1:def 5;
let x be Real;
assume
A10: x in dom Intfg;
then
A11: a <= x by A9,XXREAL_1:236;
then
A12: [' a,x '] = [.a,x.] & f is_integrable_on [' a,x '] by A2,
INTEGRA5:def 3;
A13: [.a,x.] c= right_closed_halfline(a) & f|[' a,x '] is bounded by A2,A11
,XXREAL_1:251;
thus Intfg.x = r*Intf.x by A10,VALUED_1:def 5
.= r*integral(f,a,x) by A3,A4,A9,A10
.=integral(r(#)f,a,x) by A1,A11,A12,A13,INTEGRA6:10,XBOOLE_1:1;
end;
for b be Real st a <= b holds r(#)f is_integrable_on [' a,b '] & (r(#)
f)|[' a,b '] is bounded
proof
let b be Real;
A14: [.a,b.] c= right_closed_halfline(a) by XXREAL_1:251;
assume
A15: a <= b;
then
A16: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded by A2;
[' a,b '] = [.a,b.] by A15,INTEGRA5:def 3;
then [' a,b '] c= dom f by A1,A14;
hence thesis by A16,INTEGRA6:9,RFUNCT_1:80;
end;
hence
A17: r(#)f is_+infty_ext_Riemann_integrable_on a by A8,A7;
lim_in+infty (Intfg) = r*infty_ext_right_integral(f,a) by A5,A6,LIMFUNC1:80
;
hence thesis by A8,A7,A17,Def7;
end;
hence thesis;
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_ext_Riemann_integrable_on b & g is_-infty_ext_Riemann_integrable_on b
holds 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)
proof
let f,g be PartFunc of REAL,REAL, b be Real;
assume that
A1: left_closed_halfline(b) c= dom f & left_closed_halfline(b) c= dom g and
A2: f is_-infty_ext_Riemann_integrable_on b and
A3: g is_-infty_ext_Riemann_integrable_on b;
consider Intg be PartFunc of REAL,REAL such that
A4: dom Intg = left_closed_halfline(b) and
A5: for x be Real st x in dom Intg holds Intg.x = integral(g,x,b) and
A6: Intg is convergent_in-infty and
A7: infty_ext_left_integral(g,b) = lim_in-infty Intg by A3,Def8;
consider Intf be PartFunc of REAL,REAL such that
A8: dom Intf = left_closed_halfline(b) and
A9: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b) and
A10: Intf is convergent_in-infty and
A11: infty_ext_left_integral(f,b) = lim_in-infty Intf by A2,Def8;
set Intfg = Intf + Intg;
A12: dom Intfg = left_closed_halfline(b) & for x be Real st x in dom Intfg
holds Intfg.x = integral(f + g,x,b)
proof
thus
A13: dom Intfg = dom Intf /\ dom Intg by VALUED_1:def 1
.= left_closed_halfline(b) by A8,A4;
let x be Real;
assume
A14: x in dom Intfg;
then
A15: x <= b by A13,XXREAL_1:234;
then
A16: f is_integrable_on [' x,b '] & f|[' x,b '] is bounded by A2;
A17: [.x,b.] c= left_closed_halfline(b) by XXREAL_1:265;
[' x,b '] = [.x,b.] by A15,INTEGRA5:def 3;
then
A18: [' x,b '] c= dom f & [' x,b '] c= dom g by A1,A17;
A19: g is_integrable_on [' x,b '] & g|[' x,b '] is bounded by A3,A15;
thus Intfg.x = Intf.x + Intg.x by A14,VALUED_1:def 1
.= integral(f,x,b) + Intg.x by A8,A9,A13,A14
.= integral(f,x,b) + integral(g,x,b) by A4,A5,A13,A14
.= integral(f + g,x,b) by A15,A18,A16,A19,INTEGRA6:12;
end;
A20: for r ex g st g < r & g in dom(Intf + Intg)
proof
let r be Real;
per cases;
suppose
A21: b < r;
reconsider g = b as Real;
take g;
thus thesis by A12,A21,XXREAL_1:234;
end;
suppose
A22: not b < r;
reconsider g = r - 1 as Real;
take g;
A23: r - 1 < r - 0 by XREAL_1:15;
then g <= b by A22,XXREAL_0:2;
hence thesis by A12,A23,XXREAL_1:234;
end;
end;
then
A24: Intfg is convergent_in-infty by A10,A6,LIMFUNC1:91;
for a be Real st a <= b holds f + g is_integrable_on [' a,b '] & (f+g)|
[' a,b '] is bounded
proof
let a be Real;
A25: [.a,b.] c= left_closed_halfline(b) by XXREAL_1:265;
assume
A26: a <= b;
then
A27: f is_integrable_on [' a,b '] & g is_integrable_on [' a,b '] by A2,A3;
[' a,b '] = [.a,b.] by A26,INTEGRA5:def 3;
then
A28: [' a,b '] c= dom f & [' a,b '] c= dom g by A1,A25;
A29: f|[' a,b '] is bounded & g|[' a,b '] is bounded by A2,A3,A26;
then (f + g)|([' a,b '] /\ [' a,b ']) is bounded by RFUNCT_1:83;
hence thesis by A28,A27,A29,INTEGRA6:11;
end;
hence
A30: (f + g) is_-infty_ext_Riemann_integrable_on b by A12,A24;
lim_in-infty (Intfg) = infty_ext_left_integral(f,b) +
infty_ext_left_integral(g,b) by A10,A11,A6,A7,A20,LIMFUNC1:91;
hence thesis by A12,A24,A30,Def8;
end;
theorem
for f be PartFunc of REAL,REAL, b be Real st
left_closed_halfline(b) c= dom f & f is_-infty_ext_Riemann_integrable_on b
holds for r be Real holds r(#)f is_-infty_ext_Riemann_integrable_on b &
infty_ext_left_integral(r(#)f,b) = r*infty_ext_left_integral(f,b)
proof
let f be PartFunc of REAL,REAL, b be Real;
assume that
A1: left_closed_halfline(b) c= dom f and
A2: f is_-infty_ext_Riemann_integrable_on b;
for r be Real holds r(#)f is_-infty_ext_Riemann_integrable_on b &
infty_ext_left_integral(r(#)f,b) = r*infty_ext_left_integral(f,b)
proof
let r be Real;
consider Intf be PartFunc of REAL,REAL such 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) and
A5: Intf is convergent_in-infty and
A6: infty_ext_left_integral(f,b) = lim_in-infty Intf by A2,Def8;
set Intfg = r(#)Intf;
A7: Intfg is convergent_in-infty by A5,LIMFUNC1:89;
A8: dom Intfg = left_closed_halfline(b) & for x be Real st x in dom Intfg
holds Intfg.x = integral(r(#)f,x,b)
proof
thus
A9: dom Intfg = left_closed_halfline(b) by A3,VALUED_1:def 5;
let x be Real;
assume
A10: x in dom Intfg;
then
A11: x <= b by A9,XXREAL_1:234;
then
A12: [' x,b '] = [.x,b.] & f is_integrable_on [' x,b '] by A2,
INTEGRA5:def 3;
A13: [.x,b.] c= left_closed_halfline(b) & f|[' x,b '] is bounded by A2,A11
,XXREAL_1:265;
thus Intfg.x = r*Intf.x by A10,VALUED_1:def 5
.= r*integral(f,x,b) by A3,A4,A9,A10
.= integral(r(#)f,x,b) by A1,A11,A12,A13,INTEGRA6:10,XBOOLE_1:1;
end;
for a be Real st a <= b holds r(#)f is_integrable_on [' a,b '] & (r(#)
f)|[' a,b '] is bounded
proof
let a be Real;
A14: [.a,b.] c= left_closed_halfline(b) by XXREAL_1:265;
assume
A15: a <= b;
then
A16: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded by A2;
[' a,b '] = [.a,b.] by A15,INTEGRA5:def 3;
then [' a,b '] c= dom f by A1,A14;
hence thesis by A16,INTEGRA6:9,RFUNCT_1:80;
end;
hence
A17: r(#)f is_-infty_ext_Riemann_integrable_on b by A8,A7;
lim_in-infty (Intfg) = r*infty_ext_left_integral(f,b) by A5,A6,LIMFUNC1:89;
hence thesis by A8,A7,A17,Def8;
end;
hence thesis;
end;
theorem
for f be PartFunc of REAL,REAL, a,b be Real st a < b & [' a,b '] c=
dom f & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded holds
ext_right_integral(f,a,b) = integral(f,a,b)
proof
let f be PartFunc of REAL,REAL, a,b be Real such that
A1: a < b and
A2: [' a,b '] c= dom f and
A3: f is_integrable_on [' a,b '] and
A4: f|[' a,b '] is bounded;
reconsider AB = [.a,b.[ as non empty Subset of REAL by A1,XXREAL_1:3;
deffunc F(Element of AB) = In(integral(f,a,$1),REAL);
consider Intf be Function of AB, REAL such that
A5: for x being Element of AB holds Intf.x = F(x) from FUNCT_2:sch 4;
A6: dom Intf = AB by FUNCT_2:def 1;
then reconsider Intf as PartFunc of REAL, REAL by RELSET_1:5;
consider M0 be Real such that
A7: for x being object st x in [' a,b '] /\ dom f holds |.f.x.| <= M0 by A4,
RFUNCT_1:73;
reconsider M = M0 + 1 as Real;
A8: for x be Real st x in [' a,b '] holds |.f.x.| < M
proof
A9: [' a,b '] /\ dom f = [' a,b '] by A2,XBOOLE_1:28;
let x be Real;
assume x in [' a,b '];
hence thesis by A7,A9,XREAL_1:39;
end;
a in {r where r is Real: a <= r & r <= b } by A1;
then a in [.a,b.] by RCOMP_1:def 1;
then a in [' a,b '] by A1,INTEGRA5:def 3;
then |.f.a.| < M by A8;
then
A10: 0 < M by COMPLEX1:46;
A11: for g1 be Real st 0 < g1
ex r be Real st r < b &
for r1 be Real st r <
r1 & r1 < b & r1 in dom Intf holds |.Intf.r1 - integral(f,a,b).| < g1
proof
let g1 be Real;
assume 0 < g1;
then consider r be Real such that
A12: a < r and
A13: r < b and
A14: (b - r)*M < g1 by A1,A10,Th1;
reconsider r as Real;
take r;
thus r < b by A13;
now
let r1 be Real;
assume that
A15: r < r1 and
A16: r1 < b and
r1 in dom Intf;
A17: a <= r1 by A12,A15,XXREAL_0:2;
then reconsider rr=r1 as Element of AB by A16,XXREAL_1:3;
A18: Intf.r1 = F(rr) by A5;
r1 in [. a,b .] by A16,XXREAL_1:1,A17;
then
A19: r1 in [' a,b '] by A1,INTEGRA5:def 3;
b - r1 < b - r by A15,XREAL_1:15;
then
A20: M * (b - r1) < M * (b - r) by A10,XREAL_1:68;
A21: [' a,b '] = [. a,b .] by A1,INTEGRA5:def 3;
[. r1,b .] = [' r1,b '] by A16,INTEGRA5:def 3;
then [' r1,b '] c= [' a,b '] by A21,A17,XXREAL_1:34;
then
A22: for x be Real st x in [' r1,b '] holds |.f.x.| <= M by A8;
b in [' a,b '] by A1,A21,XXREAL_1:1;
then |.integral(f,r1,b).| <= M * (b - r1) by A1,A2,A3,A4,A16,A19,A22,
INTEGRA6:23;
then
A23: |.integral(f,r1,b).| < M * (b - r) by A20,XXREAL_0:2;
|.Intf.r1 - integral(f,a,b).| = |.integral(f,a,b) - Intf.r1 .| by
COMPLEX1:60
.= |.integral(f,a,r1) + integral(f,r1,b) - integral(f,a,r1).|
by A1,A2
,A3,A4,A18,A19,INTEGRA6:17
.= |.integral(f,r1,b).|;
hence |.Intf.r1 - integral(f,a,b).| < g1 by A14,A23,XXREAL_0:2;
end;
hence thesis;
end;
A24: for x be Real st x in dom Intf holds Intf.x = integral(f,a,x)
proof let x be Real such that
A25: x in dom Intf;
dom Intf = AB by FUNCT_2:def 1;
then reconsider x as Element of AB by A25;
Intf.x = F(x) by A5;
hence thesis;
end;
for r st r < b ex g be Real st r < g & g < b & g in dom Intf
proof
let r such that
A26: r < b;
per cases;
suppose
A27: r < a;
reconsider g = a as Real;
take g;
thus thesis by A1,A6,A27,XXREAL_1:3;
end;
suppose
not r < a;
then
A28: a - a <= r - a by XREAL_1:9;
reconsider g = r + (b - r)/2 as Real;
take g;
A29: 0 < b - r by A26,XREAL_1:50;
then (b - r)/2 < b - r by XREAL_1:216;
then
A30: (b - r)/2 + r < b - r + r by XREAL_1:8;
r < g by A29,XREAL_1:29,215;
then
A31: r - (r - a) < g - 0 by A28,XREAL_1:14;
0 < (b - r)/2 by A29,XREAL_1:215;
hence thesis by A6,A31,A30,XREAL_1:8,XXREAL_1:3;
end;
end;
then
A32: Intf is_left_convergent_in b by A11,LIMFUNC2:7;
then
A33: integral(f,a,b) = lim_left(Intf,b) by A11,LIMFUNC2:41;
for d be Real st a <= d & d < b
holds f is_integrable_on [' a,d '] & f|
[' a,d '] is bounded by A2,A3,A4,INTEGRA6:18;
then f is_right_ext_Riemann_integrable_on a,b by A6,A24,A32;
hence thesis by A6,A24,A32,A33,Def3;
end;
theorem
for f be PartFunc of REAL,REAL, a,b be Real st a < b & [' a,b '] c=
dom f & f is_integrable_on [' a,b '] & f|[' a,b '] is bounded holds
ext_left_integral(f,a,b) = integral(f,a,b)
proof
let f be PartFunc of REAL,REAL, a,b be Real such that
A1: a < b and
A2: [' a,b '] c= dom f and
A3: f is_integrable_on [' a,b '] and
A4: f|[' a,b '] is bounded;
reconsider AB = ].a,b.] as non empty Subset of REAL by A1,XXREAL_1:2;
deffunc F(Element of AB) = In(integral(f,$1,b),REAL);
consider Intf be Function of AB, REAL such that
A5: for x being Element of AB holds Intf.x = F(x) from FUNCT_2:sch 4;
A6: dom Intf = AB by FUNCT_2:def 1;
then reconsider Intf as PartFunc of REAL, REAL by RELSET_1:5;
consider M0 be Real such that
A7: for x being object st x in [' a,b '] /\ dom f holds |.f.x.| <= M0 by A4,
RFUNCT_1:73;
reconsider M = M0 + 1 as Real;
A8: for x be Real st x in [' a,b '] holds |.f.x.| < M
proof
A9: [' a,b '] /\ dom f = [' a,b '] by A2,XBOOLE_1:28;
let x be Real;
assume x in [' a,b '];
hence thesis by A7,A9,XREAL_1:39;
end;
a in {r where r is Real: a <= r & r <= b } by A1;
then a in [.a,b.] by RCOMP_1:def 1;
then a in [' a,b '] by A1,INTEGRA5:def 3;
then |.f.a.| < M by A8;
then
A10: 0 < M by COMPLEX1:46;
A11: for g1 be Real st 0 < g1 ex r be Real st a < r &
for r1 be Real st r1 <
r & a < r1 & r1 in dom Intf holds |.Intf.r1 - integral(f,a,b).| < g1
proof
let g1 be Real;
assume 0 < g1;
then consider r be Real such that
A12: a < r and
A13: r < b and
A14: (r - a)*M < g1 by A1,A10,Th2;
take r;
thus a < r by A12;
now
let r1 be Real;
assume that
A15: a < r1 and
A16: r1 < r and
r1 in dom Intf;
r1 < b by A16,A13,XXREAL_0:2;
then reconsider rr=r1 as Element of AB by A15,XXREAL_1:2;
A17: Intf.r1 = F(rr) by A5;
r1 - a < r - a by A16,XREAL_1:14;
then
A18: M * (r1 - a) < M * (r - a) by A10,XREAL_1:68;
A19: [' a,b '] = [. a,b .] by A1,INTEGRA5:def 3;
A20: r1 <= b by A13,A16,XXREAL_0:2;
then
A21: r1 in [' a,b '] by A15,A19,XXREAL_1:1;
[. a,r1 .] = [' a,r1 '] by A15,INTEGRA5:def 3;
then [' a,r1 '] c= [' a,b '] by A19,A20,XXREAL_1:34;
then
A22: for x be Real st x in [' a,r1 '] holds |.f.x.| <= M by A8;
a in [' a,b '] by A1,A19,XXREAL_1:1;
then |.integral(f,a,r1).| <= M * (r1 - a) by A1,A2,A3,A4,A15,A21,A22,
INTEGRA6:23;
then
A23: |.integral(f,a,r1).| < M * (r - a) by A18,XXREAL_0:2;
|.Intf.r1 - integral(f,a,b).| = |.integral(f,a,b) - Intf.r1.| by
COMPLEX1:60
.= |.integral(f,a,r1) + integral(f,r1,b) - integral(f,r1,b).|
by A1,A2
,A3,A4,A17,A21,INTEGRA6:17
.= |.integral(f,a,r1).|;
hence |.Intf.r1 - integral(f,a,b).| < g1 by A14,A23,XXREAL_0:2;
end;
hence thesis;
end;
A24: for x be Real st x in dom Intf holds Intf.x = integral(f,x,b)
proof let x be Real such that
A25: x in dom Intf;
dom Intf = AB by FUNCT_2:def 1;
then reconsider x as Element of AB by A25;
Intf.x = F(x) by A5;
hence thesis;
end;
for r st a < r ex g be Real st g < r & a < g & g in dom Intf
proof
let r such that
A26: a < r;
per cases;
suppose
A27: b < r;
reconsider g = b as Real;
take g;
g in ].a,b.] by A1,XXREAL_1:2;
hence thesis by A1,A27,FUNCT_2:def 1;
end;
suppose
A28: not b < r;
reconsider g = a + (r - a)/2 as Real;
take g;
A29: 0 < r - a by A26,XREAL_1:50;
then
A30: a < g by XREAL_1:29,215;
(r - a)/2 < r - a by A29,XREAL_1:216;
then
A31: (r - a)/2 + a < r - a + a by XREAL_1:8;
then g < b by A28,XXREAL_0:2;
hence thesis by A6,A30,A31,XXREAL_1:2;
end;
end;
then
A32: Intf is_right_convergent_in a by A11,LIMFUNC2:10;
then
A33: integral(f,a,b) = lim_right(Intf,a) by A11,LIMFUNC2:42;
for d be Real st a < d & d <= b
holds f is_integrable_on [' d,b '] & f|
[' d,b '] is bounded by A2,A3,A4,INTEGRA6:18;
then f is_left_ext_Riemann_integrable_on a,b by A6,A24,A32;
hence thesis by A6,A24,A32,A33,Def4;
end;
begin :: The Definition of One-Sided Laplace Transform
definition
let s be Real;
func exp*- s -> Function of REAL,REAL means
for t be Real holds it.t = exp_R .(-s*t);
existence
proof
deffunc F(Real) = In(exp_R.(-s*$1),REAL);
consider g being Function of REAL,REAL such that
A1: for x be Element of REAL holds g.x = F(x) from FUNCT_2:sch 4;
take g;
let x be Real;
x in REAL by XREAL_0:def 1;
then g.x = F(x) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of REAL, REAL;
assume that
A2: for d be Real holds f1.d = exp_R.(-s*d) and
A3: for d be Real holds f2.d = exp_R.(-s*d);
for d being Element of REAL holds f1.d = f2.d
proof
let d be Element of REAL;
thus f1.d = exp_R.(-s*d) by A2
.=f2.d by A3;
end;
hence f1 = f2 by FUNCT_2:63;
end;
end;
definition
let f be PartFunc of REAL,REAL;
func One-sided_Laplace_transform(f) -> PartFunc of REAL,REAL means
:Def12:
dom it = right_open_halfline(0) & for s be Real st s in dom it holds it.s =
infty_ext_right_integral(f(#)(exp*-s),0);
existence
proof
defpred P[Real,Real] means $1 in right_open_halfline
(0) & $2 = infty_ext_right_integral(f(#)(exp*-$1),0);
consider g being PartFunc of REAL,REAL such that
A1: (for d be Element of REAL holds d in dom g iff (ex c be Element of
REAL st P[d,c])) & for d be Element of REAL st d in dom g holds P[d,g/.d] from
PARTFUN2:sch 1;
A2: for d be Real holds d in dom g iff
ex c be Real st P[d,c]
proof let d be Real;
reconsider dd=d as Element of REAL by XREAL_0:def 1;
thus d in dom g implies ex c being Real st P[d,c] by A1;
given c being Real such that
A3: P[d,c];
reconsider c as Element of REAL by XREAL_0:def 1;
P[dd,c] by A3;
then dd in dom g by A1;
hence thesis;
end;
A4: for d be Real st d in dom g holds P[d,g/.d]
by A1;
A5: dom g = right_open_halfline(0)
proof
let s1 be Real;
reconsider s = s1 as Real;
s in right_open_halfline(0) implies s in dom g
proof
assume s in right_open_halfline(0);
then ex y be Real st s in right_open_halfline(0) & y =
infty_ext_right_integral(f(#)(exp*-s),0);
hence thesis by A2;
end;
hence thesis by A4;
end;
take g;
for s be Real st s in dom g holds g.s = infty_ext_right_integral(f(#)(
exp*-s),0)
proof
let s be Real;
assume
A6: s in dom g;
then g/.s = infty_ext_right_integral(f(#)(exp*-s),0) by A4;
hence thesis by A6,PARTFUN1:def 6;
end;
hence thesis by A5;
end;
uniqueness
proof
let f1,f2 be PartFunc of REAL, REAL;
assume that
A7: dom f1 = right_open_halfline(0) and
A8: for s be Real st s in dom f1 holds f1.s =
infty_ext_right_integral( f(#)(exp*-s),0);
assume that
A9: dom f2 = right_open_halfline(0) and
A10: for s be Real st s in dom f2 holds f2.s =
infty_ext_right_integral( f(#)(exp*-s),0);
for s being Element of REAL st s in dom f1 holds f1.s = f2.s
proof
let s be Element of REAL such that
A11: s in dom f1;
f1.s = infty_ext_right_integral(f(#)(exp*-s),0) by A8,A11;
hence thesis by A7,A9,A10,A11;
end;
hence f1 = f2 by A7,A9,PARTFUN1:5;
end;
end;
begin :: Linearity of One-Sided Laplace Transform
theorem
for f, g be PartFunc of REAL,REAL st dom f = right_closed_halfline(0)
& dom g = right_closed_halfline(0) & (for s be Real st s in right_open_halfline
(0) holds f(#)(exp*-s) is_+infty_ext_Riemann_integrable_on 0) & (for s be Real
st s in right_open_halfline(0) holds g(#)(exp*-s)
is_+infty_ext_Riemann_integrable_on 0) holds (for s be Real st s in
right_open_halfline(0) holds (f + g)(#)(exp*-s)
is_+infty_ext_Riemann_integrable_on 0) & One-sided_Laplace_transform(f + g) =
One-sided_Laplace_transform(f) + One-sided_Laplace_transform(g)
proof
let f, g be PartFunc of REAL,REAL such that
A1: dom f = right_closed_halfline(0) and
A2: dom g = right_closed_halfline(0) and
A3: ( for s be Real st s in right_open_halfline(0) holds f(#)(exp*-s)
is_+infty_ext_Riemann_integrable_on 0)& for s be Real st s in
right_open_halfline(0) holds g(#)(exp*-s) is_+infty_ext_Riemann_integrable_on 0
;
set Intg = One-sided_Laplace_transform(g);
set Intf = One-sided_Laplace_transform(f);
set F = One-sided_Laplace_transform(f) + One-sided_Laplace_transform(g);
A4: dom F = dom Intf /\ dom Intg by VALUED_1:def 1
.= right_open_halfline(0) /\ dom Intg by Def12
.= right_open_halfline(0) /\ right_open_halfline(0) by Def12
.= right_open_halfline(0);
A5: for s be Real st s in right_open_halfline(0) holds (f + g)(#)(exp*-s)
is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral((f + g)(#)(
exp*-s),0) = infty_ext_right_integral(f(#)(exp*-s),0) +
infty_ext_right_integral(g(#)(exp*-s),0)
proof
let s be Real;
A6: (f + g)(#)(exp*-s) = f(#)(exp*-s) + g(#)(exp*-s) by RFUNCT_1:10;
A7: dom (g(#)(exp*-s)) = dom g /\ dom (exp*-s) by VALUED_1:def 4
.= right_closed_halfline(0) /\ REAL by A2,FUNCT_2:def 1
.= right_closed_halfline(0) by XBOOLE_1:28;
assume s in right_open_halfline(0);
then
A8: f(#)(exp*-s) is_+infty_ext_Riemann_integrable_on 0 & g(#)(exp*-s)
is_+infty_ext_Riemann_integrable_on 0 by A3;
dom (f(#)(exp*-s)) = dom f /\ dom (exp*-s) by VALUED_1:def 4
.= right_closed_halfline(0) /\ REAL by A1,FUNCT_2:def 1
.= right_closed_halfline(0) by XBOOLE_1:28;
hence thesis by A8,A6,A7,Th8;
end;
for s be Real st s in dom F holds F.s = infty_ext_right_integral((f + g
)(#)(exp*-s),0)
proof
let s be Real;
assume
A9: s in dom F;
then
A10: s in dom Intf by A4,Def12;
A11: s in dom Intg by A4,A9,Def12;
thus infty_ext_right_integral((f + g)(#)(exp*-s),0) =
infty_ext_right_integral(f(#)(exp*-s),0) + infty_ext_right_integral(g(#)(exp*-s
),0) by A5,A4,A9
.= Intf.s + infty_ext_right_integral(g(#)(exp*-s),0) by A10,Def12
.= Intf.s + Intg.s by A11,Def12
.= F.s by A9,VALUED_1:def 1;
end;
hence thesis by A5,A4,Def12;
end;
theorem
for f be PartFunc of REAL,REAL, a be Real st dom f =
right_closed_halfline(0) & (for s be Real st s in right_open_halfline(0) holds
f(#)(exp*-s) is_+infty_ext_Riemann_integrable_on 0) holds (for s be Real st s
in right_open_halfline(0) holds (a(#)f)(#)(exp*-s)
is_+infty_ext_Riemann_integrable_on 0) & One-sided_Laplace_transform(a(#)f) = a
(#)One-sided_Laplace_transform(f)
proof
let f be PartFunc of REAL,REAL, a be Real such that
A1: dom f = right_closed_halfline(0) and
A2: for s be Real st s in right_open_halfline(0) holds f(#)(exp*-s)
is_+infty_ext_Riemann_integrable_on 0;
set Intf = One-sided_Laplace_transform(f);
set F = a(#)One-sided_Laplace_transform(f);
A3: dom F = dom Intf by VALUED_1:def 5
.= right_open_halfline(0) by Def12;
A4: for s be Real st s in right_open_halfline(0) holds (a(#)f)(#)(exp*-s)
is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral((a(#)f)(#)(
exp*-s),0) = a*infty_ext_right_integral(f(#)(exp*-s),0)
proof
let s be Real;
A5: (a(#)f)(#)(exp*-s) = a(#)(f(#)(exp*-s)) by RFUNCT_1:12;
assume s in right_open_halfline(0);
then
A6: f(#)(exp*-s) is_+infty_ext_Riemann_integrable_on 0 by A2;
dom (f(#)(exp*-s)) = dom f /\ dom (exp*-s) by VALUED_1:def 4
.= right_closed_halfline(0) /\ REAL by A1,FUNCT_2:def 1
.= right_closed_halfline(0) by XBOOLE_1:28;
hence thesis by A6,A5,Th9;
end;
for s be Real st s in dom F holds F.s = infty_ext_right_integral((a(#)f)
(#)(exp*-s),0)
proof
let s be Real;
assume
A7: s in dom F;
then
A8: s in dom Intf by A3,Def12;
thus infty_ext_right_integral((a(#)f)(#)(exp*-s),0) = a*
infty_ext_right_integral(f(#)(exp*-s),0) by A4,A3,A7
.= a*Intf.s by A8,Def12
.= F.s by VALUED_1:6;
end;
hence thesis by A4,A3,Def12;
end;