:: Riemann Indefinite Integral of Functions of Real Variable
:: by Yasunari Shidama , Noboru Endou , Katsumi Wasaki and Katuhiko Kanazashi
::
:: Received June 6, 2007
:: Copyright (c) 2007-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, XBOOLE_0, PARTFUN1, SUBSET_1, FUNCT_1, RELAT_1,
XXREAL_2, COMPLEX1, ARYTM_1, XXREAL_0, SEQ_4, ARYTM_3, REAL_1, FDIFF_1,
RCOMP_1, TARSKI, VALUED_1, CARD_1, ORDINAL4, INTEGRA5, INTEGRA1,
XXREAL_1, SQUARE_1, ORDINAL2, FUNCOP_1, FCONT_1, REALSET1, SIN_COS,
PREPOWER, SEQFUNC, SEQ_1, SEQ_2, INTEGRA2, FUNCT_3, FINSEQ_1, FINSEQ_2,
CARD_3, MEASURE7, NAT_1, INTEGRA7, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
XXREAL_0, XXREAL_2, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCOP_1, RELSET_1,
FUNCT_2, RCOMP_1, PARTFUN1, PARTFUN2, FINSEQ_1, VALUED_1, SEQ_1,
RFUNCT_1, SEQ_2, SEQ_4, SQUARE_1, PREPOWER, FCONT_1, FDIFF_1, FINSEQ_2,
RVSUM_1, INTEGRA1, INTEGRA2, SEQFUNC, SIN_COS, TAYLOR_1, INTEGRA3,
INTEGRA5;
constructors REAL_1, FDIFF_1, PARTFUN2, RFUNCT_1, INTEGRA2, LIMFUNC1, FCONT_1,
BINOP_2, INTEGRA5, SIN_COS, PREPOWER, TAYLOR_1, SQUARE_1, SEQFUNC,
RVSUM_1, SEQ_4, RELSET_1, SEQ_2, COMPLEX1, INTEGRA3, COMSEQ_2;
registrations XREAL_0, RELSET_1, INTEGRA1, RCOMP_1, INT_1, MEMBERED, PREPOWER,
XBOOLE_0, NUMBERS, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, SEQ_2, FCONT_3,
SQUARE_1, FINSEQ_2, RELAT_1, FCONT_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions FDIFF_1, RCOMP_1, FCONT_1;
equalities XCMPLX_0, SUBSET_1, INTEGRA1, INTEGRA5, VALUED_1, SQUARE_1,
RCOMP_1;
expansions INTEGRA1, INTEGRA5, FDIFF_1, TARSKI, FCONT_1;
theorems TARSKI, PARTFUN1, RVSUM_1, ZFMISC_1, PREPOWER, INTEGRA1, INTEGRA2,
RFUNCT_1, FUNCT_1, SEQ_1, SEQ_2, FDIFF_1, SEQFUNC, ABSVALUE, XCMPLX_1,
FINSEQ_1, FINSEQ_2, RCOMP_1, FCONT_1, FDIFF_2, RELAT_1, XREAL_0,
XXREAL_0, PARTFUN2, FUNCT_2, XBOOLE_0, XBOOLE_1, SEQ_4, XREAL_1,
COMPLEX1, INTEGRA4, INTEGRA5, SIN_COS, INTEGRA6, TAYLOR_1, VALUED_1,
XXREAL_1, XXREAL_2, FUNCOP_1, ORDINAL1;
schemes FUNCT_2, XBOOLE_0;
begin :: Preliminaries
reserve a,b,r for Real;
reserve A for non empty set;
reserve X,x for set;
reserve f,g,F,G for PartFunc of REAL,REAL;
reserve n for Element of NAT;
theorem Th1:
for f,g being Function of A,REAL st
rng f is bounded_above & rng g is bounded_above &
(for x be set st x in A holds |.f.x-g.x.|<=a) holds
upper_bound rng f - upper_bound rng g <= a &
upper_bound rng g - upper_bound rng f <= a
proof
let f,g be Function of A,REAL;
assume that
A1: rng f is bounded_above and
A2: rng g is bounded_above and
A3: for x be set st x in A holds |.f.x-g.x.|<=a;
A4: dom f = A by FUNCT_2:def 1;
A5: for b st b in rng g holds b <= upper_bound rng f + a
proof
let b;
assume b in rng g;
then consider x being Element of A such that
x in dom g and
A6: b=g.x by PARTFUN1:3;
|.f.x-g.x.|<=a by A3;
then |.g.x-f.x.|<=a by COMPLEX1:60;
then g.x-f.x <= a by ABSVALUE:5;
then
A7: b <= a + f.x by A6,XREAL_1:20;
f.x in rng f by A4,FUNCT_1:3;
then f.x <= upper_bound rng f by A1,SEQ_4:def 1;
then a + f.x <= a + upper_bound rng f by XREAL_1:6;
hence thesis by A7,XXREAL_0:2;
end;
A8: dom g = A by FUNCT_2:def 1;
A9: upper_bound rng g <= upper_bound rng f + a by A5,SEQ_4:45;
A10: for b st b in rng f holds b <= upper_bound rng g + a
proof
let b;
assume b in rng f;
then consider x being Element of A such that
x in dom f and
A11: b=f.x by PARTFUN1:3;
g.x in rng g by A8,FUNCT_1:3;
then g.x <= upper_bound rng g by A2,SEQ_4:def 1;
then
A12: a + g.x <= a + upper_bound rng g by XREAL_1:6;
|.f.x-g.x.|<=a by A3;
then f.x-g.x <= a by ABSVALUE:5;
then b <= a + g.x by A11,XREAL_1:20;
hence thesis by A12,XXREAL_0:2;
end;
upper_bound rng f <= upper_bound rng g + a by A10,SEQ_4:45;
hence thesis by A9,XREAL_1:20;
end;
theorem Th2:
for f,g being Function of A,REAL st
rng f is bounded_below & rng g is bounded_below &
(for x be set st x in A holds |.f.x-g.x.|<=a) holds
lower_bound rng f - lower_bound rng g <= a &
lower_bound rng g - lower_bound rng f <= a
proof
let f,g be Function of A,REAL;
assume that
A1: rng f is bounded_below and
A2: rng g is bounded_below and
A3: for x be set st x in A holds |.f.x-g.x.|<=a;
A4: dom f = A by FUNCT_2:def 1;
A5: for b st b in rng g holds lower_bound rng f -a <= b
proof
let b;
assume b in rng g;
then consider x being Element of A such that
x in dom g and
A6: b=g.x by PARTFUN1:3;
f.x in rng f by A4,FUNCT_1:3;
then lower_bound rng f <= f.x by A1,SEQ_4:def 2;
then
A7: lower_bound rng f - a <= f.x -a by XREAL_1:9;
|.f.x-g.x.|<=a by A3;
then f.x-g.x <= a by ABSVALUE:5;
then f.x - a <= b by A6,XREAL_1:12;
hence thesis by A7,XXREAL_0:2;
end;
A8: dom g = A by FUNCT_2:def 1;
A9: lower_bound rng f -a <= lower_bound rng g by A5,SEQ_4:43;
A10: for b st b in rng f holds lower_bound rng g -a <=b
proof
let b;
assume b in rng f;
then consider x being Element of A such that
x in dom f and
A11: b=f.x by PARTFUN1:3;
|.f.x-g.x.|<=a by A3;
then |.g.x-f.x.|<=a by COMPLEX1:60;
then g.x-f.x <= a by ABSVALUE:5;
then
A12: g.x - a <=b by A11,XREAL_1:12;
g.x in rng g by A8,FUNCT_1:3;
then lower_bound rng g <=g.x by A2,SEQ_4:def 2;
then lower_bound rng g - a <= g.x-a by XREAL_1:9;
hence thesis by A12,XXREAL_0:2;
end;
lower_bound rng g-a <= lower_bound rng f by A10,SEQ_4:43;
hence thesis by A9,XREAL_1:12;
end;
theorem
f|X|X is bounded implies f|X is bounded;
theorem Th4:
for x be Real st x in X & f|X is_differentiable_in x holds
f is_differentiable_in x
proof
let x be Real;
assume that
A1: x in X and
A2: f|X is_differentiable_in x;
consider N be Neighbourhood of x such that
A3: N c= dom(f|X) and
A4: ex L be LinearFunc, R be RestFunc st
for x1 be Real st x1 in N holds (f|X).
x1 - (f|X).x = L.(x1-x) + R.(x1-x) by A2;
A5: (f|X).x = f.x by A1,FUNCT_1:49;
take N;
N c= dom f /\ X by A3,RELAT_1:61;
hence N c= dom f by XBOOLE_1:18;
consider L be LinearFunc, R be RestFunc such that
A6: for x1 be Real st x1 in N holds (f|X).x1 - (f|X).x = L.(x1-x) + R.(
x1-x) by A4;
take L,R;
let x1 be Real;
assume
A7: x1 in N;
then (f|X).x1 = f.x1 by A3,FUNCT_1:47;
hence thesis by A6,A7,A5;
end;
theorem
f|X is_differentiable_on X iff f is_differentiable_on X
proof
hereby assume
A1: f|X is_differentiable_on X; then
A2: for x being Real st x in X holds f|X is_differentiable_in x;
X c= dom(f|X) by A1;
then X c= dom f /\ X by RELAT_1:61;
then X c= dom f by XBOOLE_1:18;
hence f is_differentiable_on X by A2;
end;
thus thesis by RELAT_1:62;
end;
theorem Th6:
f is_differentiable_on X & g is_differentiable_on X implies
f+g is_differentiable_on X & f-g is_differentiable_on X &
f(#)g is_differentiable_on X
proof
assume that
A1: f is_differentiable_on X and
A2: g is_differentiable_on X;
reconsider Z = X as Subset of REAL by A1,FDIFF_1:8;
reconsider Z as open Subset of REAL by A1,FDIFF_1:10;
X c= dom f & X c= dom g by A1,A2;
then
A3: Z c= dom f /\ dom g by XBOOLE_1:19;
then
A4: Z c= dom(f(#)g) by VALUED_1:def 4;
Z c= dom(f+g) & Z c= dom(f-g) by A3,VALUED_1:12,def 1;
hence thesis by A1,A2,A4,FDIFF_1:18,19,21;
end;
theorem Th7:
f is_differentiable_on X implies r(#)f is_differentiable_on X
proof
reconsider r1 = r as Real;
assume
A1: f is_differentiable_on X;
then reconsider Z = X as Subset of REAL by FDIFF_1:8;
reconsider Z as open Subset of REAL by A1,FDIFF_1:10;
X c= dom f by A1;
then Z c= dom(r(#)f) by VALUED_1:def 5;
then (r1(#)f) is_differentiable_on X by A1,FDIFF_1:20;
hence thesis;
end;
theorem Th8:
(for x be set st x in X holds g.x <> 0) &
f is_differentiable_on X & g is_differentiable_on X implies
f/g is_differentiable_on X
proof
assume that
A1: for x be set st x in X holds g.x <> 0 and
A2: f is_differentiable_on X and
A3: g is_differentiable_on X;
reconsider Z = X as Subset of REAL by A2,FDIFF_1:8;
reconsider Z as open Subset of REAL by A2,FDIFF_1:10;
for x be Real st x in Z holds g.x <> 0 by A1;
hence thesis by A2,A3,FDIFF_2:21;
end;
theorem
(for x be set st x in X holds f.x <> 0) & f is_differentiable_on X
implies f^ is_differentiable_on X
proof
assume that
A1: for x be set st x in X holds f.x <> 0 and
A2: f is_differentiable_on X;
reconsider Z = X as Subset of REAL by A2,FDIFF_1:8;
reconsider Z as open Subset of REAL by A2,FDIFF_1:10;
for x be Real st x in Z holds f.x <> 0 by A1;
hence thesis by A2,FDIFF_2:22;
end;
theorem Th10:
a <= b & [' a,b '] c= X & F is_differentiable_on X &
F`|X is_integrable_on [' a,b '] & (F`|X)|[' a,b '] is bounded
implies F.b = integral (F`|X,a,b) + F.a
proof
assume that
A1: a <= b and
A2: [' a,b '] c= X & F is_differentiable_on X & F`|X is_integrable_on ['
a,b '] & (F`|X)|[' a,b '] is bounded;
integral(F`|X,a,b) = integral(F`|X,[' a,b ']) by A1,INTEGRA5:def 4;
then
A3: integral(F`|X,a,b) = F.(upper_bound [' a,b ']) - F.(lower_bound [' a,b
']) by A2,INTEGRA5:13;
A4: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A5: [.a,b.] = [.lower_bound [.a,b.], upper_bound [.a,b.].] by INTEGRA1:4;
then a=lower_bound [.a,b.] by A4,INTEGRA1:5;
hence thesis by A4,A5,A3,INTEGRA1:5;
end;
begin :: The Definition of Indefinite Integral
definition
let X be set, f be PartFunc of REAL,REAL;
func IntegralFuncs(f,X) -> set means
:Def1:
x in it iff ex F be PartFunc of REAL,REAL st
x = F & F is_differentiable_on X & F`|X = f|X;
existence
proof
defpred P[object] means ex F be PartFunc of REAL,REAL st $1 = F & F
is_differentiable_on X & F`|X = f|X;
consider Z being set such that
A1: for x being object holds x in Z iff x in PFuncs(REAL,REAL) & P[x]
from XBOOLE_0:sch 1;
take Z;
let x;
thus x in Z implies ex F being PartFunc of REAL,REAL st x = F & F
is_differentiable_on X & F`|X = f|X by A1;
given F being PartFunc of REAL,REAL such that
A2: x = F & F is_differentiable_on X & F`|X = f|X;
F in PFuncs(REAL,REAL) by PARTFUN1:45;
hence thesis by A1,A2;
end;
uniqueness
proof
let Z1,Z2 be set such that
A3: x in Z1 iff ex F be PartFunc of REAL,REAL st x = F & F
is_differentiable_on X & F`|X = f|X and
A4: x in Z2 iff ex F be PartFunc of REAL,REAL st x = F & F
is_differentiable_on X & F`|X = f|X;
for x being object holds x in Z1 iff x in Z2
proof let x be object;
x in Z1 iff ex F be PartFunc of REAL,REAL st x = F & F
is_differentiable_on X & F`|X = f|X by A3;
hence thesis by A4;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let X be set, F,f be PartFunc of REAL,REAL;
pred F is_integral_of f,X means
F in IntegralFuncs(f,X);
end;
Lm1: F is_integral_of f,X iff F is_differentiable_on X & F`|X = f|X
proof
hereby
assume F is_integral_of f,X;
then F in IntegralFuncs(f,X);
then
ex F9 be PartFunc of REAL,REAL st F = F9 & F9 is_differentiable_on X &
F9`|X = f|X by Def1;
hence F is_differentiable_on X & F`|X = f|X;
end;
assume F is_differentiable_on X & F`|X = f|X;
then F in IntegralFuncs(f,X) by Def1;
hence thesis;
end;
theorem Th11:
F is_integral_of f,X implies X c= dom F
proof
assume F is_integral_of f,X;
then F in IntegralFuncs(f,X); then
ex G be PartFunc of REAL,REAL st F = G & G is_differentiable_on X & G`|X
= f|X by Def1;
hence thesis;
end;
theorem
F is_integral_of f,X & G is_integral_of g,X implies
F+G is_integral_of f+g,X & F-G is_integral_of f-g,X
proof
assume that
A1: F is_integral_of f,X and
A2: G is_integral_of g,X;
A3: G is_differentiable_on X by A2,Lm1;
A4: G`|X = g|X by A2,Lm1;
then dom(g|X) = X by A3,FDIFF_1:def 7;
then dom g /\ X = X by RELAT_1:61;
then
A5: X c= dom g by XBOOLE_1:18;
A6: F is_differentiable_on X by A1,Lm1;
then
A7: F+G is_differentiable_on X by A3,Th6;
A8: F`|X = f|X by A1,Lm1;
then dom(f|X) = X by A6,FDIFF_1:def 7;
then dom f /\ X = X by RELAT_1:61;
then X c= dom f by XBOOLE_1:18;
then
A9: X c= dom f /\ dom g by A5,XBOOLE_1:19;
then
A10: X c= dom(f+g) by VALUED_1:def 1;
A11: now
let x be Element of REAL;
assume x in dom((F+G)`|X);
then
A12: x in X by A7,FDIFF_1:def 7;
then F|X is_differentiable_in x by A6;
then
A13: F is_differentiable_in x by A12,Th4;
(G`|X).x = diff(G,x) by A3,A12,FDIFF_1:def 7;
then
A14: g.x = diff(G,x) by A4,A12,FUNCT_1:49;
(F`|X).x = diff(F,x) by A6,A12,FDIFF_1:def 7;
then
A15: f.x = diff(F,x) by A8,A12,FUNCT_1:49;
G|X is_differentiable_in x by A3,A12;
then
A16: G is_differentiable_in x by A12,Th4;
((F+G)`|X).x = diff(F+G,x) by A7,A12,FDIFF_1:def 7;
then ((F+G)`|X).x = diff(F,x) + diff(G,x) by A13,A16,FDIFF_1:13;
then ((F+G)`|X).x = (f+g).x by A10,A12,A15,A14,VALUED_1:def 1;
hence ((F+G)`|X).x = ((f+g)|X).x by A12,FUNCT_1:49;
end;
A17: F-G is_differentiable_on X by A6,A3,Th6;
A18: X c= dom(f-g) by A9,VALUED_1:12;
A19: now
let x be Element of REAL;
assume x in dom((F-G)`|X);
then
A20: x in X by A17,FDIFF_1:def 7;
then F|X is_differentiable_in x by A6;
then
A21: F is_differentiable_in x by A20,Th4;
(G`|X).x = diff(G,x) by A3,A20,FDIFF_1:def 7;
then
A22: g.x = diff(G,x) by A4,A20,FUNCT_1:49;
(F`|X).x = diff(F,x) by A6,A20,FDIFF_1:def 7;
then
A23: f.x = diff(F,x) by A8,A20,FUNCT_1:49;
G|X is_differentiable_in x by A3,A20;
then
A24: G is_differentiable_in x by A20,Th4;
((F-G)`|X).x = diff(F-G,x) by A17,A20,FDIFF_1:def 7;
then ((F-G)`|X).x = diff(F,x) - diff(G,x) by A21,A24,FDIFF_1:14;
then ((F-G)`|X).x = (f-g).x by A18,A20,A23,A22,VALUED_1:13;
hence ((F-G)`|X).x = ((f-g)|X).x by A20,FUNCT_1:49;
end;
X = dom((f+g)|X) by A10,RELAT_1:62;
then dom((F+G)`|X) = dom((f+g)|X) by A7,FDIFF_1:def 7;
then (F+G)`|X = (f+g)|X by A11,PARTFUN1:5;
hence F+G is_integral_of f+g,X by A7,Lm1;
X = dom((f-g)|X) by A18,RELAT_1:62;
then dom((F-G)`|X) = dom((f-g)|X) by A17,FDIFF_1:def 7;
then (F-G)`|X = (f-g)|X by A19,PARTFUN1:5;
hence thesis by A17,Lm1;
end;
theorem
F is_integral_of f,X implies r(#)F is_integral_of r(#)f,X
proof
assume
A1: F is_integral_of f,X;
then
A2: F is_differentiable_on X by Lm1;
then
A3: r(#)F is_differentiable_on X by Th7;
A4: F`|X = f|X by A1,Lm1;
then dom(f|X) = X by A2,FDIFF_1:def 7;
then dom f /\ X = X by RELAT_1:61;
then X c= dom f by XBOOLE_1:18;
then
A5: X c= dom(r(#)f) by VALUED_1:def 5;
A6: now
reconsider r1 = r as Real;
let x be Element of REAL;
assume x in dom((r(#)F)`|X);
then
A7: x in X by A3,FDIFF_1:def 7;
then F|X is_differentiable_in x by A2;
then
A8: F is_differentiable_in x by A7,Th4;
((r(#)F)`|X).x = diff(r(#)F,x) by A3,A7,FDIFF_1:def 7;
then
A9: ((r1(#)F)`|X).x = r1*diff(F,x) by A8,FDIFF_1:15;
(F`|X).x = diff(F,x) by A2,A7,FDIFF_1:def 7;
then f.x = diff(F,x) by A4,A7,FUNCT_1:49;
then ((r(#)F)`|X).x = (r(#)f).x by A5,A7,A9,VALUED_1:def 5;
hence ((r(#)F)`|X).x = ((r(#)f)|X).x by A7,FUNCT_1:49;
end;
X = dom((r(#)f)|X) by A5,RELAT_1:62;
then dom((r(#)F)`|X) = dom((r(#)f)|X) by A3,FDIFF_1:def 7;
then (r(#)F)`|X = (r(#)f)|X by A6,PARTFUN1:5;
hence thesis by A3,Lm1;
end;
theorem
F is_integral_of f,X & G is_integral_of g,X implies
F(#)G is_integral_of f(#)G+F(#)g,X
proof
assume that
A1: F is_integral_of f,X and
A2: G is_integral_of g,X;
A3: G is_differentiable_on X by A2,Lm1;
A4: X c= dom F by A1,Th11;
A5: G`|X = g|X by A2,Lm1;
then dom(g|X) = X by A3,FDIFF_1:def 7;
then dom g /\ X = X by RELAT_1:61;
then X c= dom g by XBOOLE_1:18;
then X c= dom F /\ dom g by A4,XBOOLE_1:19;
then
A6: X c= dom(F(#)g) by VALUED_1:def 4;
A7: X c= dom G by A2,Th11;
A8: F is_differentiable_on X by A1,Lm1;
then
A9: F(#)G is_differentiable_on X by A3,Th6;
A10: F`|X = f|X by A1,Lm1;
then dom(f|X) = X by A8,FDIFF_1:def 7;
then dom f /\ X = X by RELAT_1:61;
then X c= dom f by XBOOLE_1:18;
then X c= dom f /\ dom G by A7,XBOOLE_1:19;
then X c= dom(f(#)G) by VALUED_1:def 4;
then X c= dom(f(#)G) /\ dom(F(#)g) by A6,XBOOLE_1:19;
then
A11: X c= dom(f(#)G+F(#)g) by VALUED_1:def 1;
A12: now
let x be Element of REAL;
assume x in dom((F(#)G)`|X);
then
A13: x in X by A9,FDIFF_1:def 7;
then F|X is_differentiable_in x by A8;
then
A14: F is_differentiable_in x by A13,Th4;
(G`|X).x = diff(G,x) by A3,A13,FDIFF_1:def 7;
then g.x = diff(G,x) by A5,A13,FUNCT_1:49;
then
A15: (F(#)g).x = (F.x)*diff(G,x) by VALUED_1:5;
(F`|X).x = diff(F,x) by A8,A13,FDIFF_1:def 7;
then f.x = diff(F,x) by A10,A13,FUNCT_1:49;
then
A16: (f(#)G).x = (G.x)*diff(F,x) by VALUED_1:5;
G|X is_differentiable_in x by A3,A13;
then
A17: G is_differentiable_in x by A13,Th4;
((F(#)G)`|X).x = diff(F(#)G,x) by A9,A13,FDIFF_1:def 7;
then ((F(#)G)`|X).x = (G.x)*diff(F,x) + (F.x)*diff(G,x) by A14,A17,
FDIFF_1:16;
then ((F(#)G)`|X).x = (F(#)g+f(#)G).x by A11,A13,A15,A16,VALUED_1:def 1;
hence ((F(#)G)`|X).x = ((F(#)g+f(#)G)|X).x by A13,FUNCT_1:49;
end;
X = dom((f(#)G+F(#)g)|X) by A11,RELAT_1:62;
then dom((F(#)G)`|X) = dom((f(#)G+F(#)g)|X) by A9,FDIFF_1:def 7;
then (F(#)G)`|X = (F(#)g+f(#)G)|X by A12,PARTFUN1:5;
hence thesis by A9,Lm1;
end;
theorem
(for x be set st x in X holds G.x <> 0) &
F is_integral_of f,X & G is_integral_of g,X implies
F/G is_integral_of (f(#)G-F(#)g)/(G(#)G),X
proof
assume that
A1: for x be set st x in X holds G.x <> 0 and
A2: F is_integral_of f,X and
A3: G is_integral_of g,X;
A4: G is_differentiable_on X by A3,Lm1;
A5: X c= dom F by A2,Th11;
A6: G`|X = g|X by A3,Lm1;
then dom(g|X) = X by A4,FDIFF_1:def 7;
then dom g /\ X = X by RELAT_1:61;
then X c= dom g by XBOOLE_1:18;
then X c= dom F /\ dom g by A5,XBOOLE_1:19;
then
A7: X c= dom(F(#)g) by VALUED_1:def 4;
A8: X c= dom G by A3,Th11;
A9: F is_differentiable_on X by A2,Lm1;
then
A10: F/G is_differentiable_on X by A1,A4,Th8;
A11: F`|X = f|X by A2,Lm1;
then dom(f|X) = X by A9,FDIFF_1:def 7;
then dom f /\ X = X by RELAT_1:61;
then X c= dom f by XBOOLE_1:18;
then X c= dom f /\ dom G by A8,XBOOLE_1:19;
then X c= dom(f(#)G) by VALUED_1:def 4;
then X c= dom(f(#)G) /\ dom(F(#)g) by A7,XBOOLE_1:19;
then
A12: X c= dom(f(#)G-F(#)g) by VALUED_1:12;
A13: now
let x be Element of REAL;
X = dom G /\ X by A3,Th11,XBOOLE_1:28;
then
A14: X = dom(G|X) by RELAT_1:61;
assume x in dom((F/G)`|X);
then
A15: x in X by A10,FDIFF_1:def 7;
then F|X is_differentiable_in x by A9;
then
A16: F is_differentiable_in x by A15,Th4;
G|X is_differentiable_in x by A4,A15;
then
A17: G is_differentiable_in x by A15,Th4;
G.x = (G|X).x by A15,FUNCT_1:49;
then
A18: (G.x)^2 = ((G|X)(#)(G|X)).x by VALUED_1:5;
now
let y be set;
assume
A19: y in dom(G|X);
then y in dom G /\ X by RELAT_1:61;
then y in X by XBOOLE_0:def 4;
then
A20: G.y <> 0 by A1;
(G|X).y = G.y by A19,FUNCT_1:47;
then not (G|X).y in {0} by A20,TARSKI:def 1;
hence not y in (G|X)"{0} by FUNCT_1:def 7;
end;
then not x in (G|X)"{0} by A15,A14;
then x in (dom(G|X)\(G|X)"{0}) /\ (dom(G|X)\(G|X)"{0}) by A15,A14,
XBOOLE_0:def 5;
then x in dom((G|X)(#)(G|X)) \ ((G|X)(#)(G|X))"{0} by RFUNCT_1:2;
then
x in dom((f(#)G-F(#)g)) /\ (dom((G|X)(#)(G|X)) \ ((G|X)(#)(G|X))"{0})
by A12,A15,XBOOLE_0:def 4;
then
A21: x in dom((f(#)G-F(#)g)/((G|X)(#)(G|X))) by RFUNCT_1:def 1;
(G`|X).x = diff(G,x) by A4,A15,FDIFF_1:def 7;
then g.x = diff(G,x) by A6,A15,FUNCT_1:49;
then
A22: (F(#)g).x = (F.x)*diff(G,x) by VALUED_1:5;
(F`|X).x = diff(F,x) by A9,A15,FDIFF_1:def 7;
then f.x = diff(F,x) by A11,A15,FUNCT_1:49;
then (f(#)G).x = (G.x)*diff(F,x) by VALUED_1:5;
then
A23: (f(#)G-F(#)g).x = diff(F,x)*G.x - diff(G,x)*F.x by A12,A15,A22,VALUED_1:13
;
((F/G)`|X).x = diff(F/G,x) & G.x <> 0 by A1,A10,A15,FDIFF_1:def 7;
then ((F/G)`|X).x = (diff(F,x)*G.x - diff(G,x)*F.x)/((G.x)^2) by A16,A17,
FDIFF_2:14;
then ((F/G)`|X).x = ((f(#)G-F(#)g)/((G|X)(#)(G|X))).x by A21,A23,A18,
RFUNCT_1:def 1;
then ((F/G)`|X).x = ((f(#)G-F(#)g)/(G(#)G)|X).x by RFUNCT_1:45;
hence ((F/G)`|X).x = (((f(#)G-F(#)g)/(G(#)G))|X).x by RFUNCT_1:48;
end;
now
assume (G|X)"{0} <> {};
then consider y be object such that
A24: y in (G|X)"{0} by XBOOLE_0:def 1;
A25: y in dom(G|X) by A24,FUNCT_1:def 7;
then
A26: (G|X).y = G.y by FUNCT_1:47;
y in dom G /\ X by A25,RELAT_1:61;
then y in X by XBOOLE_0:def 4;
then
A27: G.y <> 0 by A1;
(G|X).y in {0} by A24,FUNCT_1:def 7;
hence contradiction by A27,A26,TARSKI:def 1;
end;
then (dom(G|X) \ (G|X)"{0}) /\ (dom(G|X) \ (G|X)"{0}) = dom(G|X);
then dom((G|X)(#)(G|X)) \ ((G|X)(#)(G|X))"{0} = dom(G|X) by RFUNCT_1:2;
then dom((G|X)(#)(G|X)) \ ((G|X)(#)(G|X))"{0} = dom G /\ X by RELAT_1:61;
then
A28: dom((G|X)(#)(G|X)) \ ((G|X)(#)(G|X))"{0} = X by A3,Th11,XBOOLE_1:28;
X = dom((f(#)G-F(#)g)|X) by A12,RELAT_1:62;
then dom((f(#)G-F(#)g)|X) /\ (dom((G|X)(#)(G|X)) \ ((G|X)(#)(G|X))"{0}) = X
by A28;
then dom(((f(#)G-F(#)g)|X)/((G|X)(#)(G|X))) = X by RFUNCT_1:def 1;
then dom(((f(#)G-F(#)g)|X)/((G(#)G)|X)) = X by RFUNCT_1:45;
then dom(((f(#)G-F(#)g)/(G(#)G))|X) = X by RFUNCT_1:48;
then dom((F/G)`|X) = dom(((f(#)G-F(#)g)/(G(#)G))|X) by A10,FDIFF_1:def 7;
then (F/G)`|X = ((f(#)G-F(#)g)/(G(#)G))|X by A13,PARTFUN1:5;
hence thesis by A10,Lm1;
end;
theorem
a <= b & [' a,b '] c= dom f & f|[' a,b '] is continuous &
]. a,b .[ c= dom F &
(for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x) + F.a)
implies F is_integral_of f,]. a,b .[
proof
set O = ].a,b.[;
assume that
A1: a <= b and
A2: [' a,b '] c= dom f and
A3: f|[' a,b '] is continuous and
A4: ]. a,b .[ c= dom F and
A5: for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x) +F. a;
dom(F|O) = dom F /\ O by PARTFUN2:15;
then
A6: dom(F|O) = O by A4,XBOOLE_1:28;
reconsider Fa = F.a as Element of REAL by XREAL_0:def 1;
set H1 = REAL --> Fa;
deffunc G0(Real) = In(integral(f,a,$1),REAL);
consider G1 be Function of REAL,REAL such that
A7: for h be Element of REAL holds G1.h=G0(h) from FUNCT_2:sch 4;
reconsider H=H1|O as PartFunc of REAL,REAL;
reconsider G=G1|O as PartFunc of REAL,REAL;
dom H = dom H1 /\ O by RELAT_1:61;
then
A8: dom H = REAL /\ O by FUNCT_2:def 1;
then
A9: dom H = O by XBOOLE_1:28;
now
let x be Element of REAL;
reconsider z=x as Real;
assume
A10: x in O /\ dom H;
then H.x = H1.z by A9,FUNCT_1:47;
then H.x = F.a by FUNCOP_1:7;
hence H/.x = F.a by A9,A10,PARTFUN1:def 6;
end;
then
A11: H|O is constant by PARTFUN2:35;
then
A12: H is_differentiable_on O by A9,FDIFF_1:22;
dom G = dom G1 /\ O by RELAT_1:61;
then
A13: dom G = REAL /\ O by FUNCT_2:def 1;
then
A14: O = dom G by XBOOLE_1:28;
A15: now
let x be Real;
reconsider z = x as Element of REAL by XREAL_0:def 1;
assume x in ].a,b.[;
then G.x = G1.x by A14,FUNCT_1:47;
then G.x = G0(z) by A7;
hence G.x = integral(f,a,x);
end;
A16: now
let x be object;
assume
A17: x in dom(F|O);
then reconsider z=x as Real;
reconsider z1=z as Element of REAL by XREAL_0:def 1;
H.x = H1.z1 by A9,A6,A17,FUNCT_1:47;
then
A18: H.x = F.a by FUNCOP_1:7;
(F|O).x = F.z by A17,FUNCT_1:47;
then (F|O).x = integral(f,a,z) + F.a by A5,A6,A17;
hence (F|O).x = G.x + H.x by A15,A6,A17,A18;
end;
A19: [' a,b '] = [.a,b.] by A1,INTEGRA5:def 3;
then
A20: O c= [' a,b '] by XXREAL_1:25; then
A21: O c= dom f by A2;
A22: for x be Real st x in O holds G is_differentiable_in x & diff(G,x)=f.x
proof
let x be Real;
reconsider z = x as Real;
A23: f|O is continuous by A3,A19,FCONT_1:16,XXREAL_1:25;
assume
A24: x in ]. a,b .[;
then x in dom(f|O) by A21,RELAT_1:57;
then
A25: f|O is_continuous_in z by A23;
for r be Real st 0 < r ex s be Real st 0 < s & for x1
be Real st x1 in dom f & |.x1-z.| < s holds |.f.x1 - f.z.| < r
proof
let r be Real;
consider ss1 be Real such that
A26: 0 < ss1 and
A27: ].z-ss1,z+ss1.[ c= O by A24,RCOMP_1:19;
assume 0 < r;
then consider s be Real such that
A28: 0 < s and
A29: for x1 be Real st x1 in dom(f|O) & |.x1-z.|<s holds
|.(f| O).x1 - (f|O).z.| < r by A25,FCONT_1:3;
set s1=min(ss1,s);
take s1;
now
let x1 be Real;
assume that
x1 in dom f and
A30: |.x1-z.|<s1;
s1 <= s by XXREAL_0:17; then
A31: |.x1-z.| < s by A30,XXREAL_0:2;
O = O /\ dom f by A2,A20,XBOOLE_1:1,28; then
A32: O = dom(f|O) by PARTFUN2:15;
s1 <= ss1 by XXREAL_0:17;
then |.x1-z.| < ss1 by A30,XXREAL_0:2;
then
A33: x1 in ].z-ss1,z+ss1.[ by RCOMP_1:1;
then |.f.x1-f.z.| = |.(f|O).x1 - f.z.| by A27,A32,FUNCT_1:47;
then |.f.x1-f.z.| = |.(f|O).x1 - (f|O).z.| by A24,A32,FUNCT_1:47;
hence |.f.x1-f.z.|<r by A29,A27,A31,A33,A32;
end;
hence thesis by A28,A26,XXREAL_0:15;
end;
then
A34: f is_continuous_in z by FCONT_1:3;
f|[' a,b '] is bounded & f is_integrable_on [' a,b '] by A2,A3,INTEGRA5:10
,11;
hence thesis by A1,A2,A14,A15,A24,A34,INTEGRA6:28;
end;
then for x be Real st x in O holds G is_differentiable_in x;
then
A35: G is_differentiable_on O by A14;
dom(F|O)= dom G /\ dom H by A13,A8,A6,XBOOLE_1:28;
then
A36: F|O = G+H by A16,VALUED_1:def 1;
then F|O is_differentiable_on O by A35,A12,A6,FDIFF_1:18;
then for x be Real st x in O holds F|O is_differentiable_in x;
then
A37: F is_differentiable_on O by A4;
A38: now
let x be Element of REAL;
assume x in dom (F`|O);
then
A39: x in O by A37,FDIFF_1:def 7;
then x in dom f /\ O by A21,XBOOLE_0:def 4;
then
A40: x in dom (f|O) by PARTFUN2:15;
(F`|O).x = ((F|O)`|O).x by A37,FDIFF_2:16;
then (F`|O).x = diff(G,x) + diff(H,x) by A35,A12,A6,A36,A39,FDIFF_1:18;
then
A41: (F`|O).x = f.x + diff(H,x) by A22,A39;
(H`|O).x = 0 by A9,A11,A39,FDIFF_1:22;
then diff(H,x) = 0 by A12,A39,FDIFF_1:def 7;
hence (F`|O).x = (f|O).x by A40,A41,FUNCT_1:47;
end;
dom(F`|O) = O by A37,FDIFF_1:def 7;
then dom(F`|O) = O /\ dom f by A2,A20,XBOOLE_1:1,28;
then dom(F`|O) = dom(f|O) by PARTFUN2:15;
then F`|O = f|O by A38,PARTFUN1:5;
hence thesis by A37,Lm1;
end;
theorem
for x,x0 be Real st f| [. a,b .] is continuous &
[.a,b.] c= dom f & x in ].a,b.[ & x0 in ].a,b.[ &
F is_integral_of f,].a,b.[ holds
F.x = integral(f,x0,x) + F.x0
proof
let x,x0 be Real;
set O = ].a,b.[;
assume that
A1: f| [. a,b .] is continuous and
A2: [. a,b .] c= dom f and
A3: x in ].a,b.[ & x0 in ].a,b.[ and
A4: F is_integral_of f,].a,b.[;
A5: F is_differentiable_on O & F`|O = f|O by A4,Lm1;
A6: O c= [.a,b.] by XXREAL_1:25;
A7: [.x,x0.] c=].a,b.[ by A3,XXREAL_2:def 12;
A8: now
assume
A9: x < x0;
then
A10: [' x,x0 '] c= ].a,b.[ by A7,INTEGRA5:def 3;
then
A11: f| [' x,x0 '] is continuous by A1,A6,FCONT_1:16,XBOOLE_1:1;
(F`|]. a,b .[)|| [' x,x0 '] =(f|].a,b.[)|[' x,x0 '] by A4,Lm1;
then
A12: (F`|]. a,b .[)|| [' x,x0 '] = f|| [' x,x0 '] by A10,FUNCT_1:51;
A13: [' x,x0 '] c= [.a,b.] by A6,A10;
then [' x,x0 '] c= dom f by A2;
then f is_integrable_on [' x,x0 '] by A11,INTEGRA5:17;
then f||[' x,x0 '] is integrable; then
A14: F`|].a,b.[ is_integrable_on [' x,x0 '] by A12;
(F`|].a,b.[)|[' x,x0 '] is bounded by A2,A12,A13,A11,INTEGRA5:10,XBOOLE_1:1
;
then F.x0 = integral(f|]. a,b .[,x,x0) +F.x by A5,A9,A10,A14,Th10;
then F.x0 = integral(f|]. a,b .[,[' x,x0 ']) +F.x by A9,INTEGRA5:def 4;
then F.x0 = integral(f,[' x,x0 ']) +F.x by A10,FUNCT_1:51;
then
A15: F.x0 = integral(f,x,x0) +F.x by A9,INTEGRA5:def 4;
integral(f,x0,x) = -integral(f,[' x,x0 ']) by A9,INTEGRA5:def 4;
then integral(f,x0,x) = -integral(f,x,x0) by A9,INTEGRA5:def 4;
hence thesis by A15;
end;
A16: [.x0,x.] c=].a,b.[ by A3,XXREAL_2:def 12;
now
assume
A17: x0 <= x;
then
A18: [' x0,x '] c= ].a,b.[ by A16,INTEGRA5:def 3;
then
A19: f| [' x0,x '] is continuous by A1,A6,FCONT_1:16,XBOOLE_1:1;
(F`|].a,b.[)||[' x0,x '] = (f|].a,b.[)|[' x0,x '] by A4,Lm1;
then
A20: (F`|].a,b.[)||[' x0,x '] = f||[' x0,x '] by A18,FUNCT_1:51;
[' x0,x '] c= [.a,b.] by A6,A18; then
A21: [' x0,x '] c= dom f by A2;
f|[' x0,x '] is continuous by A1,A6,A18,FCONT_1:16,XBOOLE_1:1;
then f is_integrable_on [' x0,x '] by A21,INTEGRA5:17;
then f||[' x0,x '] is integrable;
then F`|].a,b.[ is_integrable_on [' x0,x '] by A20;
then F.x = integral(f|].a,b.[,x0,x) +F.x0 by A5,A17,A18,A20,A21,A19,Th10,
INTEGRA5:10;
then F.x = integral(f|].a,b.[,[' x0,x ']) + F.x0 by A17,INTEGRA5:def 4;
then F.x = integral(f,[' x0,x ']) + F.x0 by A18,FUNCT_1:51;
hence thesis by A17,INTEGRA5:def 4;
end;
hence thesis by A8;
end;
theorem Th18:
a <= b & [' a,b '] c= X & F is_integral_of f,X &
f is_integrable_on [' a,b '] & f|[' a,b '] is bounded implies
F.b = integral(f,a,b) + F.a
proof
assume that
A1: a <= b and
A2: [' a,b '] c= X;
assume
A3: F is_integral_of f,X;
then
A4: F is_differentiable_on X & F`|X=f|X by Lm1;
assume f is_integrable_on [' a,b '];
then
A5: f||[' a,b '] is integrable;
assume
A6: f|[' a,b '] is bounded;
(F`|X)||[' a,b '] =(f|X )|[' a,b '] by A3,Lm1;
then
A7: (F`|X)||[' a,b '] = f||[' a,b '] by A2,FUNCT_1:51;
then F`|X is_integrable_on [' a,b '] by A5;
then F.b = integral(f|X,a,b) +F.a by A1,A2,A4,A7,A6,Th10;
then F.b = integral(f|X,[' a,b ']) +F.a by A1,INTEGRA5:def 4;
then F.b =integral(f,[' a,b ']) +F.a by A2,FUNCT_1:51;
hence thesis by A1,INTEGRA5:def 4;
end;
theorem Th19:
a <= b & [. a,b .] c= X & X c= dom f & f|X is continuous implies
f|[' a,b '] is continuous & f is_integrable_on [' a,b '] &
f|[' a,b '] is bounded
proof
assume a <= b; then
A1: [. a,b .] = [' a,b '] by INTEGRA5:def 3;
assume that
A2: [. a,b .] c= X and
A3: X c= dom f and
A4: f|X is continuous;
thus
A5: f|[' a,b '] is continuous by A1,A2,A4,FCONT_1:16;
[. a,b .] c= dom f by A2,A3;
hence thesis by A1,A5,INTEGRA5:10,17;
end;
theorem Th20:
a <= b & [. a,b .] c= X & X c= dom f & f|X is continuous &
F is_integral_of f,X implies F.b = integral(f,a,b) + F.a
proof
assume that
A1: a <= b and
A2: [. a,b .] c= X and
A3: X c= dom f;
assume f|X is continuous;
then
A4: f is_integrable_on [' a,b '] & f|[' a,b '] is bounded by A1,A2,A3,Th19;
A5: [. a,b .] =[' a,b '] by A1,INTEGRA5:def 3;
assume F is_integral_of f,X;
hence thesis by A1,A2,A5,A4,Th18;
end;
theorem Th21:
b <= a & [' b,a '] c= X & f is_integrable_on [' b,a '] &
g is_integrable_on [' b,a '] & f|[' b,a '] is bounded &
g|[' b,a '] is bounded & X c= dom f & X c= dom g &
F is_integral_of f,X & G is_integral_of g,X implies
(F.a)*(G.a) - (F.b)*(G.b) = integral(f(#)G,b,a) + integral(F(#)g,b,a)
proof
assume that
A1: b <= a and
A2: [' b,a '] c= X and
A3: f is_integrable_on [' b,a '] and
A4: g is_integrable_on [' b,a '] and
A5: f|[' b,a '] is bounded and
A6: g|[' b,a '] is bounded;
set I = [' b,a '];
assume that
A7: X c= dom f and
A8: X c= dom g and
A9: F is_integral_of f,X and
A10: G is_integral_of g,X;
A11: X c= dom G by A10,Th11;
then
A12: I c= dom G by A2;
A13: G is_differentiable_on X by A10,Lm1;
then
A14: G|X is continuous by FDIFF_1:25;
then
A15: G|I is bounded by A2,A12,FCONT_1:16,INTEGRA5:10;
then
A16: (f(#)G)|(I /\ I) is bounded by A5,RFUNCT_1:84;
A17: X c= dom F by A9,Th11;
then
A18: I c= dom F by A2;
A19: F is_differentiable_on X by A9,Lm1;
then
A20: X is open Subset of REAL by FDIFF_1:8,10;
A21: F|X is continuous by A19,FDIFF_1:25;
then
A22: F|I is bounded by A2,A18,FCONT_1:16,INTEGRA5:10;
then
A23: (F(#)g)|(I /\ I) is bounded by A6,RFUNCT_1:84;
then
A24: (f(#)G + F(#)g)|(I /\ I) is bounded by A16,RFUNCT_1:83;
F|I is continuous by A2,A21,FCONT_1:16;
then
A25: F is_integrable_on I by A18,INTEGRA5:17;
I c= dom g by A2,A8;
then
A26: F(#)g is_integrable_on I by A4,A6,A18,A25,A22,INTEGRA6:14;
F`|X=f|X & G`|X=g|X by A9,A10,Lm1;
then (F(#)G)`|X = (f|X)(#)G +F(#)(g|X) by A19,A13,A20,FDIFF_2:20;
then (F(#)G)`|X =(f(#)G)|X +F(#)(g|X) by RFUNCT_1:45;
then (F(#)G)`|X =(f(#)G)|X +(F(#)g)|X by RFUNCT_1:45;
then
A27: (F(#)G)`|X =(f(#)G+F(#)g)|X by RFUNCT_1:44;
F(#)G is_differentiable_on X by A19,A13,A20,FDIFF_2:20;
then
A28: F(#)G is_integral_of (f(#)G+F(#)g),X by A27,Lm1;
min(b,a) = b by A1,XXREAL_0:def 9;
then
A29: max(b,a) = a by XXREAL_0:36;
b <= max(b,a) & [. b,a .] = I by A1,INTEGRA5:def 3,XXREAL_0:25;
then
A30: b in I & a in I by A29;
X c= dom F /\ dom g by A8,A17,XBOOLE_1:19;
then X c=dom (F(#)g) by VALUED_1:def 4;
then
A31: I c= dom(F(#)g) by A2;
G|I is continuous by A2,A14,FCONT_1:16;
then
A32: G is_integrable_on I by A12,INTEGRA5:17;
X c= dom f /\ dom G by A7,A11,XBOOLE_1:19;
then X c=dom (f(#)G) by VALUED_1:def 4;
then
A33: I c= dom(f(#)G) by A2;
I c= dom f by A2,A7;
then
A34: f(#)G is_integrable_on I by A3,A5,A12,A32,A15,INTEGRA6:14;
then f(#)G + F(#)g is_integrable_on I by A33,A31,A26,A16,A23,INTEGRA6:11;
then (F(#)G).a = integral(f(#)G+F(#)g,b,a) +(F(#)G).b by A1,A2,A24,A28,Th18;
then (F(#)G).b=(F.b)*(G.b) & (F(#)G).a-(F(#)G).b = integral(f(#)G,b,a) +
integral (F(#)g,b,a) by A1,A33,A31,A34,A26,A16,A23,A30,INTEGRA6:24,VALUED_1:5
;
hence thesis by VALUED_1:5;
end;
theorem
b <= a & [. b,a .] c= X & X c= dom f & X c= dom g & f|X is continuous &
g|X is continuous & F is_integral_of f,X & G is_integral_of g,X implies
(F.a)*(G.a) - (F.b)*(G.b) = integral(f(#)G,b,a)+ integral(F(#)g,b,a)
proof
assume that
A1: b <= a and
A2: [. b,a .] c= X;
assume that
A3: X c= dom f and
A4: X c= dom g and
A5: f|X is continuous and
A6: g|X is continuous and
A7: F is_integral_of f,X & G is_integral_of g,X;
A8: [. b,a .] c= dom f by A2,A3;
A9: [. b,a .] =[' b,a '] by A1,INTEGRA5:def 3;
then f|[' b,a '] is continuous by A2,A5,FCONT_1:16;
then
A10: f is_integrable_on [' b,a '] by A8,A9,INTEGRA5:17;
A11: [. b,a .] c= dom g by A2,A4;
then
A12: g|[' b,a '] is bounded by A2,A6,A9,FCONT_1:16,INTEGRA5:10;
g|[' b,a '] is continuous by A2,A6,A9,FCONT_1:16;
then
A13: g is_integrable_on [' b,a '] by A11,A9,INTEGRA5:17;
f|[' b,a '] is bounded by A2,A5,A8,A9,FCONT_1:16,INTEGRA5:10;
hence thesis by A1,A2,A3,A4,A7,A9,A10,A13,A12,Th21;
end;
begin :: Examples of Indefinite Integral
theorem Th23:
sin is_integral_of cos,REAL
proof
A1: dom(cos|REAL) = REAL /\ REAL by SIN_COS:24;
A2: now
let x be object;
assume
A3: x in dom(sin`|REAL);
then reconsider z=x as Real;
(sin`|REAL).x = diff(sin,z) by A3,FDIFF_1:def 7,SIN_COS:68;
then (sin`|REAL).x = cos.z by SIN_COS:64;
hence (sin`|REAL).x = (cos|REAL).x;
end;
dom(sin`|REAL) = REAL by FDIFF_1:def 7,SIN_COS:68;
then sin`|REAL=cos|REAL by A1,A2,FUNCT_1:2;
hence thesis by Lm1,SIN_COS:68;
end;
theorem
sin.b-sin.a = integral(cos,a,b)
proof
A1: min(a,b) <= a by XXREAL_0:17;
A2: REAL = dom cos & [. min(a,b),max(a,b) .] c= REAL by FUNCT_2:def 1;
cos|REAL is continuous & a <= max(a,b) by FDIFF_1:25,SIN_COS:67,XXREAL_0:25;
then
A3: sin.max(a,b) = integral(cos,min(a,b),max(a,b)) + sin.min(a,b) by A1,A2,Th20
,Th23,XXREAL_0:2;
A4: now
assume
A5: min(a,b) = a;
then max(a,b) = b by XXREAL_0:36;
hence thesis by A3,A5;
end;
now
assume
A6: min(a,b) = b;
then
A7: max(a,b) = a by XXREAL_0:36;
now
assume b < a;
then integral(cos,a,b) = -integral(cos,[' b,a ']) by INTEGRA5:def 4;
then sin.a = -integral(cos,a,b) + sin.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;
theorem Th25:
(-1)(#)cos is_integral_of sin,REAL
proof
A1: dom(sin|REAL) = REAL /\ REAL by SIN_COS:24;
A2: dom((-1)(#)cos) =[#]REAL by SIN_COS:24,VALUED_1:def 5;
A3: now
let x be object;
assume
A4: x in dom(((-1)(#)cos)`|REAL);
then reconsider z=x as Real;
(((-1)(#)cos)`|REAL).x=(-1)*diff(cos,z) by A2,A4,FDIFF_1:20,SIN_COS:67;
then (((-1)(#)cos)`|REAL).x=(-1)*(-sin.z) by SIN_COS:63;
hence (((-1)(#)cos)`|REAL).x=(sin|REAL).x;
end;
A5: (-1)(#)cos is_differentiable_on REAL by A2,FDIFF_1:20,SIN_COS:67;
then dom (((-1)(#)cos)`|REAL) = REAL by FDIFF_1:def 7;
then ((-1)(#)cos)`|REAL=sin|REAL by A1,A3,FUNCT_1:2;
hence thesis by A5,Lm1;
end;
theorem
cos.a - cos.b = integral(sin,a,b)
proof
A1: min(a,b) <= a by XXREAL_0:17;
max(a,b) in REAL by XREAL_0:def 1;
then
A2: max(a,b) in dom((-1)(#)cos) by SIN_COS:24,VALUED_1:def 5;
min(a,b) in REAL by XREAL_0:def 1;
then
A3: min(a,b) in dom((-1)(#)cos) by SIN_COS:24,VALUED_1:def 5;
A4: a <= max(a,b) & [. min(a,b),max(a,b) .] c= REAL by XXREAL_0:25;
sin|REAL is continuous & REAL c= dom sin by FDIFF_1:25,FUNCT_2:def 1
,SIN_COS:68;
then
((-1)(#)cos).max(a,b) = integral(sin,min(a,b),max(a,b)) + ((-1)(#)cos).
min(a,b) by A1,A4,Th20,Th25,XXREAL_0:2;
then
(-1)*cos.max(a,b) = integral(sin,min(a,b),max(a,b)) + ((-1)(#)cos).min (
a,b) by A2,VALUED_1:def 5;
then (-1)*cos.max(a,b) = integral(sin,min(a,b),max(a,b)) + (-1)*cos.min(a,b
) by A3,VALUED_1:def 5;
then
A5: cos.min(a,b) - cos.max(a,b) = integral(sin,min(a,b),max(a,b));
A6: now
assume
A7: min(a,b) = a;
then max(a,b) = b by XXREAL_0:36;
hence thesis by A5,A7;
end;
now
assume
A8: min(a,b) = b;
then
A9: max(a,b) = a by XXREAL_0:36;
b < a implies cos.a - cos.b= integral(sin,a,b)
proof
assume
A10: b < a;
then integral(sin,a,b) = -integral(sin,[' b,a ']) by INTEGRA5:def 4;
then integral(sin,a,b) = -integral(sin,b,a) by A10,INTEGRA5:def 4;
hence thesis by A5,A8,A9;
end;
hence thesis by A1,A6,A8,XXREAL_0:1;
end;
hence thesis by A6,XXREAL_0:15;
end;
theorem Th27:
exp_R is_integral_of exp_R,REAL
proof
A1: dom(exp_R|REAL) = REAL /\ REAL by TAYLOR_1:16;
A2: now
let x be object;
assume
A3: x in dom(exp_R`|REAL);
then reconsider z=x as Real;
reconsider z1=z as Element of REAL by XREAL_0:def 1;
(exp_R`|REAL).x = diff(exp_R,z) by A3,FDIFF_1:def 7,TAYLOR_1:16;
then (exp_R`|REAL).x = exp_R.z1 by TAYLOR_1:16;
hence (exp_R`|REAL).x = (exp_R|REAL).x;
end;
dom(exp_R`|REAL) = REAL by FDIFF_1:def 7,TAYLOR_1:16;
then exp_R`|REAL=exp_R|REAL by A1,A2,FUNCT_1:2;
hence thesis by Lm1,TAYLOR_1:16;
end;
theorem
integral(exp_R,a,b) = exp_R.b-exp_R.a
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 FDIFF_1:25,TAYLOR_1:16
,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,Th20,Th27,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;
theorem Th29:
#Z (n+1) is_integral_of (n+1)(#)( #Z n),REAL
proof
reconsider m = n+1 as Nat;
A1: dom(((n+1)(#)( #Z n))|REAL) = REAL /\ REAL by FUNCT_2:def 1;
A2: dom( #Z (n+1)) = REAL by FUNCT_2:def 1;
for x be Real
st x in REAL holds ( #Z (n+1))|REAL is_differentiable_in x by TAYLOR_1:2;
then
A3: #Z (n+1) is_differentiable_on REAL by A2;
A4: dom( #Z n) = REAL by FUNCT_2:def 1;
A5: now
let x be object;
assume
A6: x in dom(( #Z (n+1))`|REAL);
then reconsider z=x as Real;
(( #Z (n+1))`|REAL).x = diff(( #Z (n+1)),z) by A3,A6,FDIFF_1:def 7;
then (( #Z (n+1))`|REAL).x = m * z #Z (m-1) by TAYLOR_1:2;
then
A7: (( #Z (n+1))`|REAL).x = (n+1) * ( #Z n).x by TAYLOR_1:def 1;
x in dom( #Z n) by A4,A6;
then x in dom((n+1)(#)( #Z n)) by VALUED_1:def 5;
then (( #Z (n+1))`|REAL).x = ((n+1)(#)( #Z n)).x by A7,VALUED_1:def 5;
hence (( #Z (n+1))`|REAL).x = (((n+1)(#)( #Z n))|REAL).x;
end;
dom(( #Z (n+1))`|REAL) = REAL by A3,FDIFF_1:def 7;
then (( #Z (n+1))`|REAL) = (((n+1)(#)( #Z n))|REAL) by A1,A5,FUNCT_1:2;
hence thesis by A3,Lm1;
end;
theorem
( #Z (n+1)).b - ( #Z (n+1)).a = integral((n+1)(#)( #Z n),a,b)
proof
A1: [#]REAL c= dom((n+1)(#)( #Z n)) by FUNCT_2:def 1;
A2: dom( #Z n) = REAL by FUNCT_2:def 1;
for x be Real st
x in REAL holds ( #Z n)|REAL is_differentiable_in x by TAYLOR_1:2;
then #Z n is_differentiable_on REAL by A2;
then
A3: ((n+1)(#)( #Z n))|REAL is continuous by A1,FDIFF_1:20,25;
A4: min(a,b) <= a by XXREAL_0:17;
A5: [. min(a,b),max(a,b) .] c= REAL;
a <= max(a,b) by XXREAL_0:25;
then min(a,b) <= max(a,b) by A4,XXREAL_0:2;
then
A6: ( #Z (n+1)).max(a,b) = integral((n+1)(#)( #Z n),min(a,b),max(a,b)) + (
#Z (n+1)).min(a,b) by A1,A3,A5,Th20,Th29;
A7: min(a,b) = a implies ( #Z (n+1)).b - ( #Z (n+1)).a= integral((n+1)(#)(
#Z n),a,b)
proof
assume
A8: min(a,b) = a;
then max(a,b) = b by XXREAL_0:36;
hence thesis by A6,A8;
end;
min(a,b) = b implies ( #Z (n+1)).b - ( #Z (n+1)).a= integral((n+1)(#)(
#Z n),a,b)
proof
assume
A9: min(a,b) = b;
then
A10: max(a,b) = a by XXREAL_0:36;
b < a implies ( #Z (n+1)).b - ( #Z (n+1)).a= integral((n+1)(#)( #Z n) ,a,b)
proof
assume b < a;
then
integral((n+1)(#)( #Z n),a,b) = -integral((n+1)(#)( #Z n),[' b,a ']
) by INTEGRA5:def 4;
then ( #Z (n+1)).a = -integral((n+1)(#)( #Z n),a,b) + ( #Z (n+1)).b by A4
,A6,A9,A10,INTEGRA5:def 4;
hence thesis;
end;
hence thesis by A4,A7,A9,XXREAL_0:1;
end;
hence thesis by A7,XXREAL_0:15;
end;
begin :: Uniform Convergent Functional Sequence
theorem
for H be Functional_Sequence of REAL,REAL, rseq be Real_Sequence st
a < b & (for n be Element of NAT holds H.n is_integrable_on [' a,b '] &
(H.n)|['a,b '] is bounded & rseq.n = integral(H.n,a,b)) &
H is_unif_conv_on [' a,b '] holds
lim(H,[' a,b '])|[' a,b '] is bounded &
lim(H,[' a,b ']) is_integrable_on [' a,b '] & rseq is convergent &
lim rseq = integral(lim(H,[' a,b ']),a,b)
proof
let H be Functional_Sequence of REAL,REAL, rseq be Real_Sequence;
set AB = [' a,b '];
assume that
A1: a < b and
A2: for n be Element of NAT holds H.n is_integrable_on AB & (H.n)|AB is
bounded & rseq.n =integral(H.n,a,b) and
A3: H is_unif_conv_on AB;
consider T being DivSequence of AB such that
A4: delta T is convergent & lim delta T = 0 by INTEGRA4:11;
A5: for n be Nat holds H.n is_integrable_on AB & (H.n)|AB is
bounded & rseq.n =integral(H.n,a,b)
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
A6: AB common_on_dom H by A3,SEQFUNC:43;
A7: for n be Element of NAT holds (H.n)||AB is Function of AB,REAL & (H.n)
||AB|AB is bounded & lower_sum((H.n)||AB,T) is convergent & lim lower_sum((H.n)
||AB,T) = lower_integral((H.n)||AB) & upper_sum((H.n)||AB,T) is convergent &
lim upper_sum((H.n)||AB,T) = upper_integral((H.n)||AB) & lower_integral((H.n)||
AB) = upper_integral((H.n)||AB) & rseq.n =integral((H.n)||AB)
proof
let n be Element of NAT;
AB c= dom (H.n) by A6,SEQFUNC:def 9;
hence
A8: (H.n)||AB is Function of AB,REAL by FUNCT_2:68,INTEGRA5:6;
thus (H.n)||AB|AB is bounded by A2;
hence lower_sum((H.n)||AB,T) is convergent & lim lower_sum((H.n)||AB,T) =
lower_integral((H.n)||AB) & upper_sum((H.n)||AB,T) is convergent & lim
upper_sum((H.n)||AB,T) = upper_integral((H.n)||AB) by A4,A8,INTEGRA4:8,9;
(H.n) is_integrable_on AB by A2;
then (H.n)||AB is integrable;
hence lower_integral((H.n)||AB) = upper_integral((H.n)||AB);
rseq.n = integral(H.n,a,b) by A2;
then rseq.n = integral(H.n,AB) by A1,INTEGRA5:def 4;
hence thesis;
end;
set L1 = lower_integral(lim(H,AB)||AB);
set K1 = upper_integral(lim(H,AB)||AB);
A9: 0 < b-a by A1,XREAL_1:50;
reconsider jj=1 as Real;
consider K be Nat such that
A10: for n be Nat,x be Element of REAL st n >= K & x in AB
holds |.(H.n).x-(lim(H,AB)).x.| < jj by A3,SEQFUNC:43;
(H.K)|AB is bounded by A5;
then consider r be Real such that
A11: for c be object st c in AB /\ dom(H.K) holds |.(H.K).c.| <= r
by RFUNCT_1:73;
set H0 = lim(H,AB)||AB;
H is_point_conv_on AB by A3,SEQFUNC:22;
then
A12: dom lim(H,AB) = AB by SEQFUNC:21;
then
A13: H0 is Function of AB,REAL by FUNCT_2:68,INTEGRA5:6;
dom lim(H,AB) c= dom(H.K) by A6,A12,SEQFUNC:def 9;
then
A14: AB /\ dom lim(H,AB) c= AB /\ dom(H.K) by XBOOLE_1:26;
now
let c be object;
(lim(H,AB)).c = (H.K).c - ((H.K).c - (lim(H,AB)).c);
then
A15: |.(lim(H,AB)).c.| <= |.(H.K).c.| + |.(H.K).c-(lim(H,AB)).c.| by
COMPLEX1:57;
assume
A16: c in AB /\ dom lim(H,AB);
then c in AB by XBOOLE_0:def 4;
then
A17: |.(H.K).c - (lim(H,AB)).c.| < 1 by A10;
|.(H.K).c.| <= r by A11,A14,A16;
then |.(H.K).c.| + |.(H.K).c-(lim(H,AB)).c.| <= r+1 by A17,XREAL_1:7;
hence |.(lim(H,AB)).c.| <= r+1 by A15,XXREAL_0:2;
end;
hence
A18: lim(H,AB)|AB is bounded by RFUNCT_1:73;
then
A19: H0|AB is bounded_above;
A20: H0|AB is bounded_below by A18;
then
A21: upper_sum(H0,T) is convergent by A4,A19,A13,INTEGRA4:9;
A22: for e be Real st 0 < e ex N be Element of NAT st for n,k be
Element of NAT st N<=n holds |.upper_sum((H.n)||AB,T).k-upper_sum(H0,T).k.| <=
e*(b-a)
proof
let e be Real;
assume 0 < e;
then consider N be Nat such that
A23: for n be Nat,x be Element of REAL st n>=N & x in AB
holds |.(H.n).x-(lim(H,AB)).x.|<e by A3,SEQFUNC:43;
reconsider N as Element of NAT by ORDINAL1:def 12;
take N;
let n,k be Element of NAT;
reconsider Tk=T.k as Division of AB;
set l0 = len Tk;
A24: dom Tk = Seg l0 by FINSEQ_1:def 3;
set Hn = (H.n)||AB;
len upper_volume(Hn,T.k) = l0 by INTEGRA1:def 6;
then reconsider
R1=upper_volume(Hn,T.k) as Element of l0-tuples_on REAL by FINSEQ_2:92;
len upper_volume(H0,T.k) = l0 by INTEGRA1:def 6;
then reconsider
R2=upper_volume(H0,T.k) as Element of l0-tuples_on REAL by FINSEQ_2:92;
upper_sum(H0,T).k-upper_sum(Hn,T).k = upper_sum(H0,T.k)-upper_sum(
Hn,T).k by INTEGRA2:def 2;
then upper_sum(H0,T).k-upper_sum(Hn,T).k = upper_sum(H0,T.k)-upper_sum(
Hn,T.k) by INTEGRA2:def 2;
then
A25: upper_sum(H0,T).k-upper_sum(Hn,T).k = Sum(R2-R1) by RVSUM_1:90;
consider H1 be Function of AB,REAL such that
A26: rng H1 = {e} and
A27: H1|AB is bounded by INTEGRA4:5;
len upper_volume(H1,T.k) = l0 by INTEGRA1:def 6;
then reconsider
R3=upper_volume(H1,T.k) as Element of l0-tuples_on REAL by FINSEQ_2:92;
A28: vol AB = b-a by A1,INTEGRA6:5;
upper_bound rng H1 = e by A26,SEQ_4:9;
then
A29: upper_sum(H1,T.k) <= e*(b-a) by A27,A28,INTEGRA1:27;
assume
A30: N<= n;
A31: for i be Element of NAT st i in dom Tk holds (R1-R2).i <= R3.i & (
R2-R1).i <= R3.i
proof
let i be Element of NAT;
A32: 0 <= vol divset(T.k,i) by INTEGRA1:9;
assume
A33: i in dom Tk;
A34: upper_bound rng(Hn|divset(T.k,i)) - upper_bound rng(H0|divset(T.k
,i)) <= upper_bound rng(H1|divset(T.k,i)) & upper_bound rng(H0|divset(T.k,i)) -
upper_bound rng(Hn|divset(T.k,i)) <= upper_bound rng(H1|divset(T.k,i))
proof
A35: divset(T.k,i) c= AB by A33,INTEGRA1:8;
then reconsider
g = H0|divset(T.k,i) as Function of divset(T.k,i),REAL by A13,
FUNCT_2:32;
consider x0 be object such that
A36: x0 in divset(T.k,i) by XBOOLE_0:def 1;
Hn is Function of AB, REAL by A7;
then reconsider
f = Hn|divset(T.k,i) as Function of divset(T.k,i),REAL by A35,
FUNCT_2:32;
A37: for x be set st x in divset(T.k,i) holds |.f.x-g.x.| <=e
proof
let x be set;
assume
A38: x in divset(T.k,i);
then |.f.x-g.x.| = |.Hn.x-g.x.| by FUNCT_1:49;
then |.f.x-g.x.| = |.Hn.x-H0.x.| by A38,FUNCT_1:49;
then |.f.x-g.x.| = |.(H.n).x-H0.x.| by A35,A38,FUNCT_1:49;
then |.f.x-g.x.| = |.(H.n).x-(lim(H,AB)).x.| by A35,A38,
FUNCT_1:49;
hence thesis by A23,A30,A35,A38;
end;
Hn|AB is bounded by A7;
then f|divset(T.k,i) is bounded_above by A33,INTEGRA1:8,INTEGRA2:5;
then
A39: rng f is bounded_above by INTEGRA1:13;
H1.x0 in {e} by A26,A35,A36,FUNCT_2:4;
then H1.x0 = e by TARSKI:def 1;
then
A40: (H1|divset(T.k,i)).x0 = e by A36,FUNCT_1:49;
H1|divset(T.k,i) is Function of divset(T.k,i),REAL by A35,FUNCT_2:32;
then e in rng(H1|divset(T.k,i)) by A36,A40,FUNCT_2:4;
then
A41: {e} c= rng(H1|divset(T.k,i)) by ZFMISC_1:31;
rng (H1|divset(T.k,i)) c= {e} by A26,RELAT_1:70;
then rng(H1|divset(T.k,i)) = {e} by A41,XBOOLE_0:def 10;
then
A42: e=upper_bound rng(H1|divset(T.k,i)) by SEQ_4:9;
g|divset(T.k,i) is bounded_above by A19,A33,INTEGRA1:8,INTEGRA2:5;
then
A43: rng g is bounded_above by INTEGRA1:13;
hence
upper_bound rng(Hn|divset(T.k,i)) - upper_bound rng(H0|divset(T
.k,i)) <= upper_bound rng(H1|divset(T.k,i)) by A39,A42,A37,Th1;
for x be set st x in divset(T.k,i) holds |.g.x-f.x.| <=
upper_bound rng(H1|divset(T.k,i))
proof
let x be set;
assume x in divset(T.k,i);
then |.f.x-g.x.| <= upper_bound rng(H1|divset(T.k,i)) by A42,A37;
hence thesis by COMPLEX1:60;
end;
hence thesis by A39,A43,Th1;
end;
(R1-R2).i = R1.i-R2.i by RVSUM_1:27; then
(R1-R2).i = upper_bound rng(Hn|divset(T.k,i)) * vol divset(T.k,i)
- (upper_volume(H0,T.k)).i by A33,INTEGRA1:def 6;
then
(R1-R2).i = upper_bound rng(Hn|divset(T.k,i)) * vol divset(T.k,i)
- upper_bound rng(H0|divset(T.k,i)) * vol divset(T.k,i) by A33,INTEGRA1:def 6;
then
(R1-R2).i = (upper_bound rng (Hn|divset(T.k,i)) - upper_bound rng
(H0| divset(T.k,i))) * vol divset(T.k,i);
then
(R1-R2).i <= upper_bound rng(H1|divset(T.k,i)) * vol divset(T.k,i
) by A34,A32,XREAL_1:64;
hence (R1-R2).i <= R3.i by A33,INTEGRA1:def 6;
(R2-R1).i = R2.i-R1.i by RVSUM_1:27; then
(R2-R1).i = upper_bound rng(H0|divset(T.k,i)) * vol divset(T.k,i)
- (upper_volume(Hn,T.k)).i by A33,INTEGRA1:def 6;
then
(R2-R1).i = upper_bound rng(H0|divset(T.k,i)) * vol divset(T.k,i)
- upper_bound rng (Hn|divset(T.k,i)) * vol divset(T.k,i) by A33,INTEGRA1:def 6;
then
(R2-R1).i = (upper_bound rng(H0|divset(T.k,i)) - upper_bound rng(
Hn|divset (T.k,i))) * vol divset(T.k,i);
then
(R2-R1).i <= upper_bound rng(H1|divset(T.k,i)) * vol divset(T.k,i
) by A34,A32,XREAL_1:64;
hence thesis by A33,INTEGRA1:def 6;
end;
then for i be Nat st i in dom Tk holds (R2-R1).i <= R3.i;
then upper_sum(H0,T).k-upper_sum(Hn,T).k <= Sum R3 by A24,A25,RVSUM_1:82;
then upper_sum(H0,T).k-upper_sum(Hn,T).k <= e*(b-a) by A29,XXREAL_0:2;
then
A44: -
e*(b-a) <= -(upper_sum(H0,T).k - upper_sum((H.n)||AB,T).k) by XREAL_1:24;
upper_sum(Hn,T).k-upper_sum(H0,T).k = upper_sum(Hn,T.k)-upper_sum(
H0,T).k by INTEGRA2:def 2;
then
upper_sum(Hn,T).k-upper_sum(H0,T).k =upper_sum(Hn,T.k)-upper_sum(H0
,T.k) by INTEGRA2:def 2;
then
A45: upper_sum(Hn,T).k-upper_sum(H0,T).k = Sum(R1-R2) by RVSUM_1:90;
for i be Nat st i in Seg l0 holds (R1-R2).i <= R3.i by A24,A31;
then upper_sum(Hn,T).k-upper_sum(H0,T).k <= Sum R3 by A45,RVSUM_1:82;
then upper_sum((H.n)||AB,T).k-upper_sum(H0,T).k <= e*(b-a) by A29,
XXREAL_0:2;
hence |.upper_sum((H.n)||AB,T).k-upper_sum(H0,T).k.| <=e*(b-a) by A44,
ABSVALUE:5;
end;
A46: for e be Real st 0 < e ex N be Element of NAT st for n be
Element of NAT st N<=n holds |.upper_integral((H.n)||AB) -upper_integral(lim(
H,AB)||AB ).| <=e
proof
let e be Real;
reconsider ee=e as Real;
assume 0 < e;
then consider N be Element of NAT such that
A47: for n,k be Element of NAT st N<=n holds |.upper_sum((H.n)||AB,
T).k-upper_sum(H0,T).k.| <= (ee/(b-a)) * (b-a) by A22,A9,XREAL_1:139;
take N;
A48: now
let n,k be Element of NAT;
assume N<=n;
then |.upper_sum((H.n)||AB,T).k-upper_sum(H0,T).k.| <=(e/(b-a)) * (b-a
) by A47;
hence |.upper_sum((H.n)||AB,T).k-upper_sum(H0,T).k.| <= e by A9,
XCMPLX_1:87;
end;
hereby
let n be Element of NAT;
assume
A49: N<=n;
A50: now
let k be Nat;
k in NAT by ORDINAL1:def 12;
then |.upper_sum((H.n)||AB,T).k-upper_sum(H0,T).k.| <=e by A48,A49;
then |.upper_sum((H.n)||AB,T).k+(-upper_sum(H0,T)).k.| <= e by
SEQ_1:10;
then |.(upper_sum((H.n)||AB,T)+-upper_sum(H0,T)).k.| <= e by SEQ_1:7;
hence |.upper_sum((H.n)||AB,T)-upper_sum(H0,T).|.k <= e by SEQ_1:12;
end;
A51: upper_sum((H.n)||AB,T) is convergent by A7;
then lim(upper_sum((H.n)||AB,T)-upper_sum(H0,T)) = lim upper_sum((H.n)
||AB,T) -lim upper_sum(H0,T) by A21,SEQ_2:12;
then lim(upper_sum((H.n)||AB,T)-upper_sum(H0,T)) = upper_integral((H.n)
||AB) -lim upper_sum(H0,T) by A7;
then
A52: lim(upper_sum((H.n)||AB,T)-upper_sum(H0,T)) = upper_integral((H.n)
||AB) - upper_integral(lim(H,AB)||AB) by A4,A19,A20,A13,INTEGRA4:9;
A53: upper_sum((H.n)||AB,T)-upper_sum(H0,T) is convergent by A21,A51;
then abs(upper_sum((H.n)||AB,T)-upper_sum(H0,T)) is convergent by
SEQ_4:13;
then lim |.upper_sum((H.n)||AB,T)-upper_sum(H0,T).| <= e by A50,
PREPOWER:2;
hence |.upper_integral((H.n)||AB) - upper_integral(lim(H,AB)||AB).| <=e
by A53,A52,SEQ_4:14;
end;
end;
A54: lower_sum (H0,T) is convergent by A4,A19,A20,A13,INTEGRA4:8;
A55: for e be Real st 0 < e ex N be Element of NAT st for n,k be
Element of NAT st N<=n holds |.lower_sum((H.n)||AB,T).k-lower_sum(H0,T).k.| <=
e*(b-a)
proof
let e be Real;
assume 0 < e;
then consider N be Nat such that
A56: for n be Nat,x be Element of REAL st n>=N & x in AB
holds |.(H.n).x-(lim(H,AB)).x.|<e by A3,SEQFUNC:43;
reconsider N as Element of NAT by ORDINAL1:def 12;
take N;
hereby
let n,k be Element of NAT;
set Hn=(H.n)||AB;
reconsider Tk=T.k as Division of AB;
set l0 = len Tk;
consider H1 be Function of AB,REAL such that
A57: rng H1 = {e} and
A58: H1|AB is bounded by INTEGRA4:5;
A59: lower_sum(H1,T.k) <= upper_sum(H1,T.k) by A58,INTEGRA1:28;
len lower_volume(H0,T.k) = l0 by INTEGRA1:def 7;
then reconsider
R2=lower_volume(H0,T.k) as Element of l0-tuples_on REAL by FINSEQ_2:92;
len lower_volume(Hn,T.k) = l0 by INTEGRA1:def 7;
then reconsider
R1=lower_volume(Hn,T.k) as Element of l0-tuples_on REAL by FINSEQ_2:92;
len lower_volume(H1,T.k) = l0 by INTEGRA1:def 7;
then reconsider
R3=lower_volume(H1,T.k) as Element of l0-tuples_on REAL by FINSEQ_2:92;
assume
A60: N<= n;
A61: for i be Element of NAT st i in dom Tk holds (R1-R2).i <= R3.i & (
R2-R1).i <= R3.i
proof
let i be Element of NAT;
consider x0 be object such that
A62: x0 in divset(T.k,i) by XBOOLE_0:def 1;
A63: rng(H1|divset(T.k,i)) c= {e} by A57,RELAT_1:70;
assume
A64: i in dom Tk;
then
A65: divset(T.k,i) c= AB by INTEGRA1:8;
then reconsider
g = H0|divset(T.k,i) as Function of divset(T.k,i),REAL by A13,
FUNCT_2:32;
Hn is Function of AB,REAL by A7;
then reconsider
f = Hn|divset(T.k,i) as Function of divset(T.k,i),REAL by A65,
FUNCT_2:32;
A66: 0 <= vol divset(T.k,i) by INTEGRA1:9;
H1.x0 in {e} by A57,A65,A62,FUNCT_2:4;
then H1.x0 = e by TARSKI:def 1;
then
A67: (H1|divset(T.k,i)).x0 = e by A62,FUNCT_1:49;
H1|divset(T.k,i) is Function of divset(T.k,i),REAL by A65,FUNCT_2:32;
then e in rng(H1|divset(T.k,i)) by A62,A67,FUNCT_2:4;
then {e} c= rng(H1|divset(T.k,i)) by ZFMISC_1:31;
then rng(H1|divset(T.k,i)) = {e} by A63,XBOOLE_0:def 10;
then
A68: e=lower_bound rng(H1|divset(T.k,i)) by SEQ_4:9;
A69: now
let x be set;
assume
A70: x in divset(T.k,i);
then |.f.x-g.x.| = |.Hn.x-g.x.| by FUNCT_1:49;
then |.f.x-g.x.| = |.Hn.x-H0.x.| by A70,FUNCT_1:49;
then |.f.x-g.x.| = |.(H.n).x-H0.x.| by A65,A70,FUNCT_1:49;
then |.f.x-g.x.| = |.(H.n).x-(lim(H,AB)).x.| by A65,A70,FUNCT_1:49;
hence |.f.x - g.x.| <= e by A56,A60,A65,A70;
end;
(R2-R1).i = R2.i-R1.i by RVSUM_1:27;
then (R2-R1).i = lower_bound rng(H0|divset(T.k,i)) * vol divset(T.k,i
) - (lower_volume(Hn,T.k)).i by A64,INTEGRA1:def 7;
then (R2-R1).i = lower_bound rng(H0|divset(T.k,i)) * vol divset(T.k,i
) - lower_bound rng(Hn|divset(T.k,i)) * vol divset(T.k,i) by A64,INTEGRA1:def 7
;
then
A71: (R2-R1).i = (lower_bound rng(H0|divset(T.k,i)) - lower_bound rng
(Hn|divset (T.k,i))) * vol divset(T.k,i);
(R1-R2).i = R1.i-R2.i by RVSUM_1:27;
then (R1-R2).i = lower_bound rng(Hn|divset(T.k,i)) * vol divset(T.k,i
) - (lower_volume(H0,T.k)).i by A64,INTEGRA1:def 7;
then (R1-R2).i = lower_bound rng(Hn|divset(T.k,i)) * vol divset(T.k,i
) - lower_bound rng(H0|divset(T.k,i)) * vol divset(T.k,i) by A64,INTEGRA1:def 7
;
then
A72: (R1-R2).i = (lower_bound rng(Hn|divset(T.k,i)) - lower_bound rng
(H0|divset (T.k,i)) ) * vol divset(T.k,i);
Hn|AB is bounded by A7;
then f|divset(T.k,i) is bounded_below by A64,INTEGRA1:8,INTEGRA2:6;
then
A73: rng f is bounded_below by INTEGRA1:11;
g|divset(T.k,i) is bounded_below by A20,A64,INTEGRA1:8,INTEGRA2:6;
then
A74: rng g is bounded_below by INTEGRA1:11;
then lower_bound rng(Hn|divset(T.k,i)) - lower_bound rng(H0|divset(T.
k,i)) <= lower_bound rng(H1|divset(T.k,i)) by A73,A68,A69,Th2;
then (R1-R2).i <= lower_bound rng(H1|divset(T.k,i)) * vol divset(T.k,
i) by A72,A66,XREAL_1:64;
hence (R1-R2).i <= R3.i by A64,INTEGRA1:def 7;
now
let x be set;
assume x in divset(T.k,i);
then |.f.x-g.x.| <= lower_bound (rng (H1|divset(T.k,i))) by A68,A69;
hence |.g.x-f.x.| <= lower_bound rng(H1|divset(T.k,i)) by
COMPLEX1:60;
end;
then lower_bound rng(H0|divset(T.k,i)) - lower_bound rng(Hn|divset(T.
k,i)) <= lower_bound rng(H1|divset(T.k,i)) by A73,A74,Th2;
then (R2-R1).i <= lower_bound rng(H1|divset(T.k,i)) * vol divset(T.k,
i) by A71,A66,XREAL_1:64;
hence thesis by A64,INTEGRA1:def 7;
end;
lower_sum(Hn,T).k-lower_sum(H0,T).k = lower_sum(Hn,T.k)-lower_sum(
H0,T).k by INTEGRA2:def 3;
then lower_sum(Hn,T).k-lower_sum(H0,T).k =lower_sum(Hn,T.k)-lower_sum(
H0,T.k) by INTEGRA2:def 3;
then
A75: lower_sum(Hn,T).k-lower_sum(H0,T).k = Sum(R1-R2) by RVSUM_1:90;
A76: vol AB = b-a by A1,INTEGRA6:5;
upper_bound rng H1 = e by A57,SEQ_4:9;
then upper_sum(H1,T.k) <= e*(b-a) by A58,A76,INTEGRA1:27;
then
A77: lower_sum(H1,T.k) <= e*(b-a) by A59,XXREAL_0:2;
lower_sum(H0,T).k-lower_sum(Hn,T).k =lower_sum(H0,T.k)-lower_sum(
Hn,T).k by INTEGRA2:def 3;
then lower_sum(H0,T).k-lower_sum(Hn,T).k =lower_sum(H0,T.k)-lower_sum(
Hn,T.k) by INTEGRA2:def 3;
then
A78: lower_sum(H0,T).k-lower_sum(Hn,T).k =Sum(R2-R1) by RVSUM_1:90;
A79: Seg l0 = dom Tk by FINSEQ_1:def 3;
then for i be Nat st i in Seg l0 holds (R2-R1).i <= R3.i by A61;
then lower_sum(H0,T).k-lower_sum(Hn,T).k <= Sum R3 by A78,RVSUM_1:82;
then lower_sum(H0,T).k-lower_sum(Hn,T).k <= e*(b-a) by A77,XXREAL_0:2;
then
A80: -e*(b-a) <= -(lower_sum(H0,T).k - lower_sum((H.n)||AB,T).k) by XREAL_1:24
;
for i be Nat st i in Seg l0 holds (R1-R2).i <= R3.i by A79,A61;
then lower_sum(Hn,T).k-lower_sum(H0,T).k <=lower_sum(H1,T.k) by A75,
RVSUM_1:82;
then lower_sum((H.n)||AB,T).k-lower_sum(H0,T).k <= e*(b-a) by A77,
XXREAL_0:2;
hence |.lower_sum((H.n)||AB,T).k-lower_sum(H0,T).k.| <=e*(b-a) by A80,
ABSVALUE:5;
end;
end;
A81: for e be Real st 0 < e ex N be Element of NAT st for n,k be
Element of NAT st N<=n holds |.lower_sum((H.n)||AB,T).k-lower_sum(H0,T).k.| <=
e
proof
let e be Real;
assume 0 < e;
then consider N be Element of NAT such that
A82: for n,k be Element of NAT st N <= n holds |.lower_sum((H.n)||
AB,T).k-lower_sum(H0,T).k.| <=(e/(b-a)) * (b-a) by A55,A9,XREAL_1:139;
take N;
hereby
let n,k be Element of NAT;
assume N<=n;
then |.lower_sum((H.n)||AB,T).k-lower_sum(H0,T).k.| <=(e/(b-a)) * (b-a
) by A82;
hence |.lower_sum((H.n)||AB,T).k-lower_sum(H0,T).k.| <= e by A9,
XCMPLX_1:87;
end;
end;
A83: for e be Real st 0 < e ex N be Element of NAT st for n be
Element of NAT st N<=n holds |.lower_integral((H.n)||AB) -lower_integral(lim(
H,AB)||AB ).| <=e
proof
let e be Real;
assume 0 < e;
then consider N be Element of NAT such that
A84: for n,k be Element of NAT st N<=n holds |.lower_sum((H.n)||AB,
T).k-lower_sum(H0,T).k.| <=e by A81;
take N;
hereby
let n be Element of NAT;
set LHT = lower_sum((H.n)||AB,T);
assume
A85: N<=n;
A86: now
let k be Nat;
k in NAT by ORDINAL1:def 12;
then |.LHT.k - lower_sum(H0,T).k.| <=e by A84,A85;
then |.LHT.k + (-lower_sum(H0,T)).k.| <= e by SEQ_1:10;
then |.(LHT + -lower_sum(H0,T)).k.| <= e by SEQ_1:7;
hence abs(LHT - lower_sum(H0,T)).k <= e by SEQ_1:12;
end;
A87: LHT is convergent by A7;
then lim(LHT - lower_sum(H0,T)) = lim LHT -lim lower_sum(H0,T) by A54,
SEQ_2:12;
then lim(LHT - lower_sum(H0,T)) = lower_integral((H.n)||AB) -lim
lower_sum(H0,T) by A7;
then
A88: lim(LHT - lower_sum(H0,T)) = lower_integral((H.n)||AB) -
lower_integral(lim(H,AB)||AB) by A4,A19,A20,A13,INTEGRA4:8;
A89: LHT - lower_sum(H0,T) is convergent by A54,A87;
then |.LHT - lower_sum(H0,T).| is convergent by SEQ_4:13;
then lim |.LHT - lower_sum(H0,T).| <= e by A86,PREPOWER:2;
hence
|.lower_integral((H.n)||AB) - lower_integral(lim(H,AB)||AB ).| <=e
by A88,A89,SEQ_4:14;
end;
end;
A90: now
let e1 be Real;
set e=e1/2;
assume
A91: 0 < e1;
then
A92: 0 < e1/2 by XREAL_1:215;
then consider N1 be Element of NAT such that
A93: for n be Element of NAT st N1<=n holds |.upper_integral((H.n)
||AB) -upper_integral(lim(H,AB)||AB ).| <=e/2 by A46,XREAL_1:215;
consider N2 be Element of NAT such that
A94: for n be Element of NAT st N2<=n holds |.lower_integral((H.n)
||AB) -lower_integral(lim(H,AB)||AB ).| <=e/2 by A83,A92,XREAL_1:215;
reconsider n=max(N1,N2) as Element of NAT;
set K = upper_integral((H.n)||AB);
set L = lower_integral((H.n)||AB);
|.L - L1.| <=e/2 by A94,XXREAL_0:25; then
A95: |.K - L1.| <= e/2 by A7;
(K - K1) - (K - L1) = L1 - K1;
then
A96: |.L1 - K1.| <= |.K - K1.| + |.K - L1.| by COMPLEX1:57;
|.K - K1.| <=e/2 by A93,XXREAL_0:25;
then |.K - K1.| + |.K-L1.| <= e/2+e/2 by A95,XREAL_1:7;
then
A97: |.L1 - K1.| <= e by A96,XXREAL_0:2;
e1/2 < e1 by A91,XREAL_1:216;
hence |.L1 - K1.| < e1 by A97,XXREAL_0:2;
end;
A98: K1 = L1 by COMPLEX1:62,A90;
H0 is upper_integrable & H0 is lower_integrable by A19,A20,A13,INTEGRA4:10;
then lim(H,AB)||AB is integrable by A98;
hence lim(H,AB) is_integrable_on AB;
A99: for p be Real st 0<p ex n be Nat st
for m be Nat st n<=m holds |.rseq.m-integral(lim(H,AB),a,b).|<p
proof
let p be Real;
set e=p/2;
assume
A100: 0<p;
then consider N be Element of NAT such that
A101: for n be Element of NAT st N<=n holds |.upper_integral((H.n)||
AB) -upper_integral(lim(H,AB)||AB ).| <=e by A46,XREAL_1:215;
take N;
A102: p/2 < p by A100,XREAL_1:216;
hereby
let n be Nat;
A103: n in NAT by ORDINAL1:def 12;
upper_integral((H.n)||AB) = integral((H.n)||AB);
then
A104: upper_integral((H.n)||AB) = rseq.n by A7,A103;
upper_integral(lim(H,AB)||AB) = integral(lim(H,AB),AB);
then
A105: upper_integral
(lim(H,AB)||AB) = integral(lim(H,AB),a,b) by A1,INTEGRA5:def 4;
assume N<=n;
then |.upper_integral((H.n)||AB) - upper_integral(lim(H,AB)||AB).| <=e
by A101,A103;
hence |.rseq.n - integral(lim(H,AB),a,b).| < p by A102,A104,A105,
XXREAL_0:2;
end;
end;
hence rseq is convergent by SEQ_2:def 6;
hence thesis by A99,SEQ_2:def 7;
end;
:: Added by YS, 2023.03.12 Integration by substitution
theorem Th32:
for a,b be Real,
f be PartFunc of REAL,REAL st a<=b
& ['a,b'] c= dom f
& f is continuous
holds
ex F being PartFunc of REAL,REAL
st ].a,b.[ c= dom F
& (for t being Real st t in ].a,b.[ holds
F.t = integral (f,a,t))
& for t being Real st t in ].a,b.[ holds
F is_differentiable_in t
& diff (F,t) = f . t
proof
let a,b be Real,
f be PartFunc of REAL,REAL;
assume A1: a<=b & ['a,b'] c= dom f & f is continuous; then
f| ['a,b'] is continuous; then
A2: f | ['a,b'] is bounded & f is_integrable_on ['a,b ']
by A1,INTEGRA5:10,INTEGRA5:11;
deffunc FX(Real) = In(integral(f,a,$1),REAL);
consider F0 be Function of REAL,REAL such that
A3: for t being Element of REAL holds F0.t = FX(t)
from FUNCT_2:sch 4;
A4: for t being Real holds F0.t = integral(f,a,t)
proof
let t be Real;
t in REAL by XREAL_0:def 1; then
F0.t = In(integral(f,a,t),REAL) by A3;
hence thesis;
end;
set F = F0 | [.a,b.];
dom F0 = REAL by FUNCT_2:def 1; then
A5: dom F = [.a,b.] by RELAT_1:62;
reconsider F as PartFunc of REAL,REAL;
take F;
thus
A6: ].a,b.[ c= dom F by A5,XXREAL_1:25;
thus
A7: for t be Real st t in ].a,b.[ holds F.t = integral(f,a,t)
proof
let t be Real;
assume A8: t in ].a,b.[;
].a,b.[ c= [.a,b.] by XXREAL_1:25;
hence F.t = F0.t by FUNCT_1:49,A8
.= integral(f,a,t) by A4;
end;
let t be Real;
assume A9: t in ].a,b.[;
].a,b.[ c= [.a,b.] by XXREAL_1:25; then
t in [.a,b.] by A9; then
t in ['a,b'] by A1,INTEGRA5:def 3; then
f is_continuous_in t by A1;
hence F is_differentiable_in t
& diff (F,t) = f . t by A1,A2,A7,A6,A9,INTEGRA6:28;
end;
theorem
for f,P be PartFunc of REAL,REAL,
x,y,a,b,s,t be Real
st x <= y & s <= t & ['s,t'] c= ].a,b.[
& ['x,y'] c= dom f
& f is continuous
& P is_differentiable_on ].a,b.[
& P .: ].a,b.[ is open Subset of REAL
& (P `| ].a,b.[) is continuous
& P .: ].a,b.[ c= ].x,y.[
& [' s,t '] c= dom (f*P)
holds
f | ['x,y'] is bounded & f is_integrable_on [' x,y '] &
((f*P) (#) (P `| ].a,b.[)) | [' s,t '] is continuous
& [' s,t '] c= dom ( ((f*P) (#) (P `| ].a,b.[)))
& ((f*P) (#) (P `| ].a,b.[ )) | [' s,t '] is bounded
& ((f*P) (#) (P `| ].a,b.[ )) is_integrable_on [' s,t ']
&
integral((f* P) (#) (P `| ].a,b.[),s,t)
= integral(f,P.s,P.t)
proof
let f,P be PartFunc of REAL,REAL;
let x,y,a,b,s,t be Real;
assume
A1: x <= y & s <= t & ['s,t'] c= ].a,b.[;
assume that
A2: ['x,y'] c= dom f and
A3: f is continuous and
A4: P is_differentiable_on ].a,b.[ and
A5: P .: ].a,b.[ is open Subset of REAL and
A6: (P `| ].a,b.[) is continuous and
A7: P .: ].a,b.[ c= ].x,y.[ and
A8:[' s,t '] c= dom (f*P);
A9: ['x,y'] = [.x,y.] by A1,INTEGRA5:def 3;
A10: ].x,y.[ c= [.x,y.] by XXREAL_1:25; then
A11: P .: ].a,b.[ c= dom f by A7,A2,A9;
A12: ].a,b.[ c= dom P by A4;
A13: ['s,t'] = [.s,t.] by A1,INTEGRA5:def 3;
s in [.s,t.] & t in [.s,t.] by A1; then
A14: s in ].a,b.[ & t in ].a,b.[ by A1,A13; then
A15: s in dom P & t in dom P by A12; then
P.s in P .: ].a,b.[ & P.t in P .: ].a,b.[ by A14,FUNCT_1:def 6; then
A16: P.s in ].x,y.[ & P.t in ].x,y.[ by A7;
f | ['x,y'] is continuous by A3;
hence f | ['x,y'] is bounded & f is_integrable_on [' x,y ']
by A2,INTEGRA5:10,INTEGRA5:11;
consider F being PartFunc of REAL,REAL such that
A17: ].x,y.[ c= dom F & ( for t being Real st t in ].x,y.[
holds F . t = integral (f,x,t) ) &
for t being Real st t in ].x,y.[ holds
F is_differentiable_in t & diff (F,t) = f . t
by A1,A2,A3,Th32;
for t being Real st t in ].x,y.[ holds
F is_differentiable_in t by A17; then
F is_differentiable_on ].x,y.[ by FDIFF_1:9,A17; then
A18: F is_differentiable_on P .: ].a,b.[ by A7,A5,FDIFF_1:26;
set G = F*P;
A19: P | ].a,b.[ is continuous by A4,FDIFF_1:25;
A20: dom (F `| (P .: ].a,b.[)) = P .: ].a,b.[ by A18,FDIFF_1:def 7;
A21: dom ( f| (P .: ].a,b.[)) = P .: ].a,b.[ by RELAT_1:62,A11;
now let t be object;
assume t in dom (F `| (P .: ].a,b.[)); then
A22: t in P .: ].a,b.[ by A20; then
reconsider s=t as Real;
A23: s in ].x,y.[ by A22,A7;
thus (F `| (P .: ].a,b.[)).t =diff(F,s) by A22,A18,FDIFF_1:def 7
.= f.t by A17,A23
.= ( f| (P .: ].a,b.[) ).t by A22,FUNCT_1:49;
end; then
A24:F `| (P .: ].a,b.[) = f| (P .: ].a,b.[) by A20,A21,FUNCT_1:2; then
A25: F `| (P .: ].a,b.[) is continuous by A3;
A26: dom (P|].a,b.[) = ].a,b.[ by A4,RELAT_1:62;
A27: rng (P|(].a,b.[) ) = P .: ].a,b.[ by RELAT_1:115; then
A28: dom ( ( F `| ( P .: ].a,b.[) ) * (P| ].a,b.[))
= ].a,b.[ by A26,A20,RELAT_1:27;
now let t be Real;
assume A29: t in dom (( F `| (P .: ].a,b.[) ) * (P|].a,b.[) );
then
A30: t in dom (P|].a,b.[) by A26,A28; then
A31: ( P | ].a,b.[) is_continuous_in t by A19;
F `| (P .: ].a,b.[) is_continuous_in (P|].a,b.[).t
by A20,A25,A27,A30,FUNCT_1:3;
hence ( F `| (P .: ].a,b.[)) * (P|].a,b.[)
is_continuous_in t by A29,A31,FCONT_1:12;
end; then
A32: ( F `| (P .: ].a,b.[)) * (P|].a,b.[) is continuous;
A33: (F `| (P .: ].a,b.[)) * (P|].a,b.[)
= ( f| (P .: ].a,b.[)) * (P|].a,b.[) by A24;
A34: G is_differentiable_on ].a,b.[
& G `| ].a,b.[ = (( F `| (P .: ].a,b.[)) * P) (#) (P `| ].a,b.[)
by FDIFF_2:23,A4,A5,A18; then
dom ( G `| ].a,b.[ ) = ].a,b.[ by FDIFF_1:def 7; then
G `| ].a,b.[ = (G `| ].a,b.[) | ].a,b.[
.=( (( F `| (P .: ].a,b.[ ) ) * P) | ].a,b.[ )
(#) (P `| ].a,b.[ ) by A34,RFUNCT_1:45
.= ( ( F `| (P .: ].a,b.[ ))
* (P|].a,b.[)) (#) (P `| ].a,b.[ ) by RELAT_1:83; then
A35: (( F `| (P .: ].a,b.[ ) ) * P) (#) (P `| ].a,b.[ )
= (( F `| (P .: ].a,b.[ )) * (P|].a,b.[)) (#) (P `| ].a,b.[ )
by A34;
A36: dom ( G`| ].a,b.[) = ].a,b.[ by A34,FDIFF_1:def 7;
A37: ( G`| ].a,b.[ ) | ['s,t'] is continuous by A6,A32,A34,A35; then
( G`| ].a,b.[ ) | [' s,t'] is bounded &
G`| ].a,b.[ is_integrable_on [' s,t ']
by A1,A36,INTEGRA5:10,INTEGRA5:11; then
A38: G.t = integral(G`|].a,b.[,s,t) + G.s by A1,A34,Th10;
A39: integral(G`|].a,b.[,s,t)
= integral((( f| (P .: ].a,b.[ ))*(P|].a,b.[))
(#) (P `| ].a,b.[ ),s,t) by A33,A35,A34;
A40: F.(P.t) = integral (f,x,P.t) by A17,A16;
A41: F.(P.s) = integral (f,x,P.s) by A17,A16;
A42: F.(P.t) - F.(P.s) = integral(f,P.s,P.t)
proof
A43: P.t in [.x,y.] & P.s in [.x,y.] by A10,A16; then
A44: ex r be Real st P.t =r & x<=r & r <= y;
A45: ex r be Real st P.s =r & x<=r & r <= y by A43;
per cases;
suppose A46: P.t <= P.s; then
A49: x <= P.s by A44,XXREAL_0:2; then
A50: ['x,P.s'] = [.x,P.s.] by INTEGRA5:def 3;
['P.t,P.s'] = [.P.t,P.s.] by A46,INTEGRA5:def 3; then
- integral(f,['P.t,P.s']) = integral(f,P.s,P.t) by INTEGRA5:20; then
A51: integral(f,['P.t,P.s']) = -integral(f,P.s,P.t);
[.x,P.s.] c= [.x,y.] by A45,XXREAL_1:34; then
A52: ['x,P.s'] c= dom f by A2,A9,A50;
f | ['x,P.s'] is continuous by A3; then
A53: f| ['x,P.s'] is bounded & f is_integrable_on ['x,P.s']
by A52,INTEGRA5:10,11;
P.t in ['x,P.s'] & P.s in ['x,P.s'] by A44,A45,A46,A50; then
integral(f,x,P.s) = integral(f,x,P.t) + integral(f,P.t,P.s)
by A49,A52,A53,INTEGRA6:20; then
integral(f,x,P.s) - integral(f,x,P.t)
= -integral(f,P.s,P.t) by A51,A46,INTEGRA5:def 4;
hence F.(P.t) - F.(P.s) = integral(f,P.s,P.t) by A40,A41;
end;
suppose A54: P.s <= P.t; then
A57: x <= P.t by A45,XXREAL_0:2; then
A58: ['x,P.t'] = [.x,P.t.] by INTEGRA5:def 3;
[.x,P.t.] c= [.x,y.] by A44,XXREAL_1:34; then
A59: ['x,P.t'] c= dom f by A2,A9,A58;
f | ['x,P.t'] is continuous by A3; then
A60: f| ['x,P.t'] is bounded & f is_integrable_on ['x,P.t']
by A59,INTEGRA5:10,11;
P.s in [.x,P.t.] & P.t in [.x,P.t.] by A44,A45,A54; then
integral(f,x,P.t) = integral(f,x,P.s) + integral(f,P.s,P.t)
by A58,A57,A59,A60,INTEGRA6:20;
hence F.(P.t) - F.(P.s) = integral(f,P.s,P.t) by A40,A41;
end;
end;
A61:G.s = F.(P.s) by FUNCT_1:13,A15;
A62: G.t = F.(P.t) by FUNCT_1:13,A15;
A63:integral((( f| (P .: ].a,b.[ ))*(P|].a,b.[))
(#) (P `| ].a,b.[ ),s,t)
= integral(f,P.s,P.t) by A38,A39,A42,A61,A62;
set K = f| (P .: ].a,b.[ );
set W = (( f| (P .: ].a,b.[ ) )*(P|].a,b.[));
set R = (( f| (P .: ].a,b.[ ) )*(P|].a,b.[))(#) (P `| ].a,b.[ );
A64: integral(R,s,t) = integral(R,[' s,t ']) by A1,INTEGRA5:def 4
.=integral(R||[' s,t ']);
A65: (K*P) | [' s,t '] = K*(P| [' s,t ']) by RELAT_1:83;
A66: (f*P) | [' s,t '] = f*(P| [' s,t ']) by RELAT_1:83;
rng ((P| [' s,t '])) = P .: [' s,t '] by RELAT_1:115; then
A67: rng ((P| [' s,t '])) c= P .: ].a,b.[ by A1,RELAT_1:123; then
A68: rng ((P| [' s,t '])) c= dom f by A11;
A69: [' s,t '] c= dom P by A1,A12;
A70: dom ((f*P) | [' s,t '] ) = dom (P| [' s,t ']) by A66,A68,RELAT_1:27
.= [' s,t '] by RELAT_1:62,A69;
dom K = P .: ].a,b.[ by RELAT_1:62,A11; then
A71: dom ((K*P) | [' s,t '] ) = dom (P| [' s,t ']) by A65,A67,RELAT_1:27
.= [' s,t '] by RELAT_1:62,A69;
now let v be object;
assume v in dom ((f*P) | [' s,t '] ); then
A72: v in [' s,t '] by A70; then
reconsider r=v as Real;
A73: r in dom P by A69,A72; then
A74: P.r in (P .: ].a,b.[ ) by A1,A72,FUNCT_1:def 6;
thus ((f*P) | [' s,t '] ).v = (f*P).r by FUNCT_1:49,A72
.= f.(P.r) by A73,FUNCT_1:13
.= K. (P.v) by FUNCT_1:49,A74
.= (K*P).r by FUNCT_1:13,A73
.= ((K*P) | [' s,t '] ).v by FUNCT_1:49,A72;
end; then
A75: (f*P) | [' s,t '] = (K*P) | [' s,t '] by A70,A71,FUNCT_1:2;
A76: (P|].a,b.[)| [' s,t '] = P | [' s,t '] by A1,RELAT_1:74;
A77: R||[' s,t ']
= ( W| [' s,t ']) (#) ( (P `| ].a,b.[ ) | [' s,t ']) by RFUNCT_1:45
.= (K* ((P|].a,b.[)| [' s,t '])(#) ( (P `| ].a,b.[ ) | [' s,t ']) )
by RELAT_1:83
.= ((K*P) | [' s,t '] )(#) ( (P `| ].a,b.[ ) | [' s,t '])
by A76,RELAT_1:83
.= ((f*P) (#) (P `| ].a,b.[ )) || [' s,t '] by A75,RFUNCT_1:45;
hence
A78:((f*P) (#) (P `| ].a,b.[ )) | [' s,t '] is continuous
by A37,A35,A24,A34;
dom (P `| ].a,b.[ ) = ].a,b.[ by A4,FDIFF_1:def 7; then
A79: dom ( ((f*P) (#) (P `| ].a,b.[ )) )
= dom (f*P) /\ ].a,b.[ by VALUED_1:def 4;
[' s,t '] /\ ].a,b.[ c= dom (f*P) /\ ].a,b.[ by XBOOLE_1:26,A8;
hence [' s,t '] c= dom ( ((f*P) (#) (P `| ].a,b.[ )))
by A1,A79,XBOOLE_1:28;
hence ((f*P) (#) (P `| ].a,b.[ )) | [' s,t '] is bounded
& ((f*P) (#) (P `| ].a,b.[ )) is_integrable_on [' s,t ']
by A78,INTEGRA5:10,INTEGRA5:11;
integral(R||[' s,t ']) = integral((f*P) (#) (P `| ].a,b.[ ),[' s,t '])
by A77
.= integral((f*P) (#) (P `| ].a,b.[ ),s,t) by A1,INTEGRA5:def 4;
hence integral((f* P) (#) (P `| ].a,b.[ ),s,t) = integral(f,P.s,P.t)
by A63,A64;
end;