:: 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-2016 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,
MEASURE5, SQUARE_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions FDIFF_1;
equalities XCMPLX_0, SUBSET_1, INTEGRA1, INTEGRA5, VALUED_1, SQUARE_1;
expansions INTEGRA1, INTEGRA5, FDIFF_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;
then rng g is non empty Subset of REAL by RELAT_1:42;
then
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;
rng f is non empty Subset of REAL by A4,RELAT_1:42;
then 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;
then rng g is non empty Subset of REAL by RELAT_1:42;
then
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;
rng f is non empty Subset of REAL by A4,RELAT_1:42;
then 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 by RELAT_1:72;
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 implies f is_differentiable_on X
proof
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 by Th4;
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 thesis by A2;
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,XBOOLE_1:1;
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,FCONT_1:def 2;
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.|~~= 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 by INTEGRA5:7;
A20: H0|AB is bounded_below by A18,INTEGRA5:8;
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.|=N & x in AB
holds |.(H.n).x-(lim(H,AB)).x.|~~