:: Differential Equations on Functions from $\mathbbR$ into Real {B}anach
:: Space
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-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 PRE_TOPC, NORMSP_1, FUNCT_1, ARYTM_1, NAT_1, SUBSET_1, NUMBERS,
CARD_1, XXREAL_0, FUNCT_7, REAL_1, ARYTM_3, RELAT_1, ORDINAL2, SEQ_1,
SEQ_2, POWER, LOPBAN_1, ORDEQ_01, STRUCT_0, COMPLEX1, VALUED_1, ALI2,
SUPINF_2, XBOOLE_0, ABIAN, INTEGRA1, FINSEQ_1, TARSKI, INTEGRA5,
MEASURE7, CARD_3, XXREAL_1, PARTFUN1, RLVECT_1, SEQ_4, FUNCT_2, RCOMP_1,
VALUED_0, XXREAL_2, FCONT_1, CFCONT_1, MEASURE5, NFCONT_1, FUNCOP_1,
REALSET1, FDIFF_1, INTEGRA7, SERIES_1, SIN_COS, REAL_NS1, NEWTON,
XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1,
COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, VALUED_1, SEQ_1, SEQ_2, RVSUM_1,
NEWTON, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1, ABIAN, POWER, SERIES_1,
MEASURE5, SIN_COS, INTEGRA1, INTEGRA5, STRUCT_0, PRE_TOPC, RLVECT_1,
VFUNCT_1, NORMSP_0, NORMSP_1, EUCLID, LOPBAN_1, NFCONT_1, NFCONT_2,
NDIFF_1, REAL_NS1, INTEGRA7, PDIFF_1, INTEGR18, NFCONT_3, NDIFF_3,
NDIFF_5, INTEGR19, ORDEQ_01;
constructors ABIAN, SEQ_2, RELSET_1, SEQ_4, VFUNCT_1, PDIFF_1, RLSUB_1,
FCONT_1, NFCONT_1, INTEGRA3, INTEGRA4, NDIFF_1, NDIFF_3, INTEGR18,
RVSUM_1, INTEGR19, INTEGR15, COMSEQ_2, VALUED_2, FDIFF_1, INTEGRA7,
COMSEQ_3, SIN_COS, NFCONT_2, C0SP2, ORDEQ_01, RFUNCT_1, RFINSEQ2,
SQUARE_1, PDIFF_7, NDIFF_5, INTEGR20;
registrations STRUCT_0, NAT_1, VALUED_1, NORMSP_0, XXREAL_0, NUMBERS,
XBOOLE_0, FUNCT_1, FUNCT_2, XREAL_0, MEMBERED, NORMSP_1, RELAT_1,
FINSEQ_2, RELSET_1, ORDINAL1, FUNCOP_1, NEWTON, NFCONT_3, XXREAL_2,
RCOMP_1, RLVECT_1, REAL_NS1, VALUED_0, FDIFF_1, FCONT_1, MEASURE5, POWER,
PREPOWER, LOPBAN_1, ORDEQ_01, NDIFF_1, INT_1, PDIFF_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities RCOMP_1, ORDEQ_01, SUBSET_1, STRUCT_0, ALGSTR_0, NORMSP_0, EUCLID,
INTEGRA5, XCMPLX_0, NDIFF_5, LOPBAN_1;
expansions ORDEQ_01, ABIAN, FDIFF_1, INTEGRA5, NFCONT_2, NFCONT_3, NDIFF_1,
NDIFF_3, NORMSP_1, TARSKI, NFCONT_1;
theorems TARSKI, ABSVALUE, RLVECT_1, NORMSP_0, XCMPLX_1, SEQ_1, SEQ_2,
SERIES_1, PARTFUN1, PARTFUN2, INTEGRA7, FUNCT_1, POWER, FUNCT_2,
NORMSP_1, XREAL_1, LOPBAN_1, FUNCT_7, XXREAL_0, XREAL_0, ORDINAL1,
RELAT_1, NFCONT_1, NFCONT_3, FCONT_1, SEQ_4, VFUNCT_1, NEWTON, XBOOLE_0,
RCOMP_1, FUNCOP_1, FINSEQ_1, NDIFF_3, SIN_COS, COMSEQ_2, INTEGRA2,
XXREAL_1, RVSUM_1, COMPLEX1, NDIFF_4, PDIFF_1, FDIFF_1, VALUED_1,
XBOOLE_1, INTEGR19, REAL_NS1, INTEGRA4, INTEGRA5, HOLDER_1, INT_1,
RELSET_1, ORDEQ_01, NDIFF_1, INTEGRA6, FINSEQ_2, XXREAL_2, FRECHET,
RLTOPSP1, NDIFF_5, ZFMISC_1, VECTSP_1, INTEGR18, INTEGR21;
schemes SEQ_1, NAT_1, FUNCT_2, PARTFUN1;
begin :: Some Properties of Differentiable Functions on Real normed space
reserve Y for RealNormSpace;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
Lm1: the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
Lm2:
dom proj(1,1) = REAL 1 & rng proj(1,1) = REAL &
for x be Element of REAL holds proj(1,1).<*x*> = x
& proj(1,1) qua Function".x = <*x*>
proof
set f=proj(1,1);
for y be object st y in REAL ex x be object st x in REAL 1 & y = f.x
proof
let y be object;
assume y in REAL;
then reconsider y1=y as Element of REAL;
reconsider x=<*y1*> as Element of REAL 1 by FINSEQ_2:98;
f.x = x.1 by PDIFF_1:def 1;
then f.x = y by FINSEQ_1:40;
hence thesis;
end;
hence thesis by FUNCT_2:10,def 1,PDIFF_1:1;
end;
theorem NDIFF435:
for Y be RealNormSpace, J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y
st J=proj(1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g*J holds
f is_continuous_in x0 iff g is_continuous_in y0
proof
let Y be RealNormSpace, J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y;
assume A1: J=proj(1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g*J;
thus f is_continuous_in x0 implies g is_continuous_in y0
proof
reconsider I= proj(1,1) qua Function" as Function of REAL,REAL-NS 1
by PDIFF_1:2,REAL_NS1:def 4;
A2: J*I = id REAL by A1,Lm2,FUNCT_1:39;
f*I = g*(id REAL) by A1,A2,RELAT_1:36; then
A3: f*I = g by FUNCT_2:17;
I/.y0 = x0 by A1,PDIFF_1:1;
hence thesis by A3,NDIFF_4:33,A1,NFCONT_3:15;
end;
J/.x0 = y0 by A1,PDIFF_1:1;
hence thesis by A1,NDIFF_4:32,NDIFF_4:34;
end;
theorem
for Y be RealNormSpace, I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y
st I=proj(1,1) qua Function"
& x0 in dom f & y0 in dom g & x0=<*y0*> & f*I = g holds
f is_continuous_in x0 iff g is_continuous_in y0
proof
let Y be RealNormSpace, I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y;
assume A1: I=proj(1,1) qua Function"
& x0 in dom f & y0 in dom g & x0=<*y0*> & f*I = g;
reconsider J= proj(1,1) as Function of REAL-NS 1,REAL by Lm1;
thus f is_continuous_in x0 implies g is_continuous_in y0
proof
I/.y0 = x0 by A1,PDIFF_1:1;
hence thesis by A1,NDIFF_4:33,NFCONT_3:15;
end;
A2: I*J = id REAL-NS 1 by A1,Lm2,Lm1,FUNCT_1:39;
A3: g*J = f*(id REAL-NS 1) by A2,A1,RELAT_1:36
.= f by FUNCT_2:17;
J/.x0 = y0 by A1,PDIFF_1:1;
hence thesis by A3,NDIFF_4:32,A1,NDIFF_4:34;
end;
theorem FTh40:
for I be Function of REAL,REAL-NS 1 st I=proj(1,1) qua Function" holds
(for R being RestFunc of REAL-NS 1,Y holds R*I is RestFunc of Y)
& for L being LinearOperator of REAL-NS 1,Y holds L*I is LinearFunc of Y
proof
let I be Function of REAL,REAL-NS 1;
assume A1: I=proj(1,1) qua Function";
A0:dom I = REAL by FUNCT_2:def 1;
thus for R being RestFunc of REAL-NS 1,Y holds R*I is RestFunc of Y
proof
let R be RestFunc of REAL-NS 1,Y;
A2: R is total by NDIFF_1:def 5; then
reconsider R0=R as Function of REAL 1,Y by Lm1;
reconsider R1=R*I as PartFunc of REAL,Y;
A3: R0*I is Function of REAL,Y by Lm1; then
A4: dom R1 = REAL by FUNCT_2:def 1;
A5: for r be Real st r > 0
ex d be Real st d > 0 & for z1 be Real st
z1 <> 0 & |. z1 .| < d holds |. z1 .|"*||. R1/.z1 .|| < r
proof
let r be Real;
assume r > 0;
then consider d be Real such that
A6: d > 0 and
A7: for z be Point of REAL-NS 1 st z <> 0.(REAL-NS 1) & ||.z.|| < d
holds ||.z.||"*||. R/.z .|| < r by A2,NDIFF_1:23;
take d;
for z1 be Real st z1 <> 0 & |.z1.| < d holds |.z1.|" * ||. R1/.z1 .|| < r
proof
let z1 be Real such that
A8: z1 <> 0 and
A9: |.z1.| < d;
reconsider zz=z1 as Element of REAL by XREAL_0:def 1;
reconsider z = I.zz as Point of REAL-NS 1;
|.zz.| > 0 by A8,COMPLEX1:47;
then ||.z.|| <> 0 by A1,Lm1,PDIFF_1:3;
then
A10: z <> 0.(REAL-NS 1);
R is total by NDIFF_1:def 5;
then dom R = the carrier of REAL-NS 1 by PARTFUN1:def 2;
then R/.z = R.(I.z1) by PARTFUN1:def 6;
then R/.z = R1.zz by A0,FUNCT_1:13;
then
A12: ||. R/.z .|| =||. R1/.zz .|| by A4,PARTFUN1:def 6;
A13: ||.z.||" = |.z1.|" by A1,Lm1,PDIFF_1:3;
||.z.|| < d by A1,A9,Lm1,PDIFF_1:3;
hence thesis by A7,A10,A13,A12;
end;
hence thesis by A6;
end;
for h be 0-convergent non-zero Real_Sequence
holds h"(#)(R1/*h) is convergent & lim(h"(#)(R1/*h)) = 0.Y
proof
let h be 0-convergent non-zero Real_Sequence;
A14: now let r be Real;
A15: lim h = 0;
assume r > 0;
then consider d be Real such that
A16: d > 0 and
A17: for z1 be Real st z1 <> 0 & |. z1 .| < d holds
|. z1 .|" * ||. R1/.z1 .|| < r by A5;
reconsider d1 =d as Real;
consider n0 be Nat such that
A18: for m be Nat st n0 <= m holds |.h.m-0 .| < d1 by A16,A15,SEQ_2:def 7;
take n0;
hereby let m be Nat;
A19: m in NAT by ORDINAL1:def 12;
rng h c= dom R1 by A4; then
A21: |.h.m.|" * ||. R1/.(h.m) .||
= |.h.m.|" * ||. (R1/*h).m .|| by A19,FUNCT_2:109
.= ((abs h).m)" * ||. (R1/*h).m .|| by SEQ_1:12
.= (abs h)".m * ||. (R1/*h).m .|| by VALUED_1:10
.= |.h".|.m * ||. (R1/*h).m .|| by SEQ_1:54
.= |.h".m.| * ||. (R1/*h).m .|| by SEQ_1:12
.= ||. h".m * (R1/*h).m .|| by NORMSP_1:def 1
.= ||. (h"(#)(R1/*h)).m - 0.Y .|| by NDIFF_1:def 2;
assume n0 <= m;
then |.h.m - 0 .| < d by A18;
hence ||. (h"(#)(R1/*h)).m - 0.Y .|| < r by A17,SEQ_1:5,A21;
end;
end;
hence (h")(#)(R1/*h) is convergent;
hence thesis by A14,NORMSP_1:def 7;
end;
hence thesis by A3,NDIFF_3:def 1;
end;
let L be LinearOperator of REAL-NS 1,Y;
reconsider L0=L as Function of REAL 1, Y by Lm1;
reconsider L1=L0*I as PartFunc of REAL,Y;
reconsider r = L1.jj as Point of Y by FUNCT_2:5;
A22: dom(L0*I) = REAL & dom L1 = REAL by FUNCT_2:def 1;
for p be Real holds L1/.p = p*r
proof
reconsider 1p = I.jj as VECTOR of REAL-NS 1;
let p be Real;
L1.p = L0.(I.(p*1)) by A0,XREAL_0:def 1,FUNCT_1:13;
then L1.p = L.(p*1p) by A1,Lm1,PDIFF_1:3;
then L1.p = p*(L/.1p) by LOPBAN_1:def 5;
then L1/.p = p*(L/.1p) by XREAL_0:def 1,A22,PARTFUN1:def 6;
hence thesis by A22,FUNCT_1:12;
end;
hence thesis by NDIFF_3:def 2;
end;
theorem FTh41:
for J be Function of REAL-NS 1,REAL st J = proj(1,1) holds
(for R being RestFunc of Y holds R*J is RestFunc of REAL-NS 1,Y)
& for L being LinearFunc of Y holds
L*J is Lipschitzian LinearOperator of REAL-NS 1,Y
proof
let J be Function of REAL-NS 1,REAL;
assume A1: J=proj(1,1);
thus for R being RestFunc of Y holds R*J is RestFunc of REAL-NS 1,Y
proof
let R be RestFunc of Y;
A2: R is total by NDIFF_3:def 1;
reconsider R0=R as Function of REAL,Y by A2;
reconsider R1 = R0*J as PartFunc of REAL-NS 1,Y;
for h be (0.(REAL-NS 1))-convergent sequence of REAL-NS 1
st h is non-zero
holds ||.h.||"(#)(R1/*h) is convergent & lim(||.h.||"(#)(R1/*h)) = 0.Y
proof
let h be (0.(REAL-NS 1))-convergent sequence of REAL-NS 1;
assume A3: h is non-zero;
A4: lim h = 0.(REAL-NS 1) by NDIFF_1:def 4;
deffunc F(Nat)=J.(h.$1);
consider s be Real_Sequence such that
A5: for n be Nat holds s.n = F(n) from SEQ_1:sch 1;
A6: h is convergent by NDIFF_1:def 4;
A7: now let p be Real;
assume 0 < p;
then consider m be Nat such that
A8: for n be Nat st m <= n holds ||. h.n - 0.(REAL-NS 1).|| < p
by A6,A4,NORMSP_1:def 7;
take m;
now let n be Nat;
assume m <= n; then
A91: ||. h.n - 0.(REAL-NS 1).|| < p by A8;
s.n = J.(h.n) by A5;
hence |.s.n-0 .| < p by A1,A91,PDIFF_1:4;
end;
hence for n be Nat st m <= n holds |.s.n-0 .|< p;
end; then
s is convergent by SEQ_2:def 6; then
A11: lim s = 0 by A7,SEQ_2:def 7;
now let x be object;
assume x in NAT;
then reconsider n=x as Element of NAT;
A13: ||. h.n .|| <> 0 by NORMSP_0:def 5,A3,NDIFF_1:6;
s.n = J.(h.n) by A5;
then |.s.n.| <> 0 by A1,A13,PDIFF_1:4;
hence s.x <> 0 by COMPLEX1:47;
end;
then reconsider s as 0-convergent non-zero Real_Sequence
by A7,SEQ_2:def 6,A11,FDIFF_1:def 1,SEQ_1:4;
now
reconsider f1=R1 as Function;
let n be Element of NAT;
rng h c= the carrier of REAL-NS 1; then
A14: rng h c= dom R1 by FUNCT_2:def 1;
(R/*s).n =R.(s.n) by NDIFF_3:def 1,FUNCT_2:115; then
A15: (R/*s).n =R.(J.(h.n)) by A5;
NAT = dom h by FUNCT_2:def 1; then
R1.(h.n) =(f1*h).n by FUNCT_1:13; then
A17: R1.(h.n) =(R1/*h).n by A14,FUNCT_2:def 11;
A18: s.n = J.(h.n) by A5;
||. ||.h.||"(#)(R1/*h).|| .n
= ||.(||.h.||"(#)(R1/*h)).n .|| by NORMSP_0:def 4
.= ||.(||.h.||").n * (R1/*h).n .|| by NDIFF_1:def 2
.= |.(||.h.||").n.| * ||.(R1/*h).n .|| by NORMSP_1:def 1
.= |.(||.h.||.n)".| * ||.(R1/*h).n .|| by VALUED_1:10
.= |.||.h.n.||".| * ||.(R1/*h).n .|| by NORMSP_0:def 4
.= ||.h.n .||" *||.(R1/*h).n .|| by ABSVALUE:def 1
.= (|.s.n.|)" *||.(R1/*h).n .|| by A1,A18,PDIFF_1:4
.= (|.s.n.|)" *||.(R/*s).n .|| by A17,A15,FUNCT_2:15
.= ((abs s).n)"*||.(R/*s).n .|| by SEQ_1:12
.= ((abs s)".n)*||.(R/*s).n .|| by VALUED_1:10
.=(|.s".|.n)*||.(R/*s).n .|| by SEQ_1:54
.=|.s".n.|*||.(R/*s).n .|| by SEQ_1:12
.= ||. (s".n)*(R/*s).n .|| by NORMSP_1:def 1
.= ||. (s"(#)(R/*s)).n .|| by NDIFF_1:def 2
.= ||. (s"(#)(R/*s)) .||.n by NORMSP_0:def 4;
hence ||. ||.h.||"(#)(R1/*h) .|| .n = ||. (s"(#)(R/*s)) .||.n;
end;
then
A19: ||. ||.h.||"(#)(R1/*h) .|| = ||. s"(#)(R/*s) .|| by FUNCT_2:63;
s"(#)(R/*s) is convergent & lim(s"(#)(R/*s))=0.Y by NDIFF_3:def 1; then
A22: lim ||. s"(#)(R/*s) .|| = ||. 0.Y .|| by LOPBAN_1:20;
A23: ||. s"(#)(R/*s) .|| is convergent by NDIFF_3:def 1,NORMSP_1:23;
A24: now let p be Real;
assume 0 < p;
then consider n0 be Nat such that
A25: for m be Nat st n0 <= m holds |.||. ||.h.||"(#)(R1/*h).||.m - 0 .| < p
by A19,A23,A22,SEQ_2:def 7;
take n0;
hereby let m be Nat;
assume n0 <= m; then
|. ||. ||.h.||"(#)(R1/*h).|| .m - 0 .| < p by A25; then
|. ||.( ||.h.||"(#)(R1/*h)).m.|| .| < p by NORMSP_0:def 4;
hence ||.(||.h.||"(#)(R1/*h)).m -0.(Y) .|| < p by ABSVALUE:def 1;
end;
end;
then ||.h.||"(#)(R1/*h) is convergent;
hence thesis by A24,NORMSP_1:def 7;
end;
hence thesis by NDIFF_1:def 5;
end;
let L be LinearFunc of Y;
consider r be Point of Y such that
A27:for p be Real holds L/.p = p*r by NDIFF_3:def 2;
reconsider L0 = L as Function of REAL,Y;
set K = ||.r.||;
reconsider L1 = L*J as Function of REAL-NS 1,Y;
A28: dom L1 = REAL 1 by Lm1,FUNCT_2:def 1;
A29:
now let x,y be Point of REAL-NS 1;
L1.(x+y) =L/.(J.(x+y)) by Lm1,A28,FUNCT_1:12;
then L1.(x+y) = L/.((J.x+J.y)) by A1,PDIFF_1:4;
then L1.(x+y) = (J.x+J.y)*r by A27;
then L1.(x+y) = (J.x)*r+(J.y)*r by RLVECT_1:def 6;
then L1.(x+y) = L/.(J.x)+(J.y)*r by A27;
then
A30:L1.(x+y) = L/.(J.x)+L/.(J.y) by A27;
L/.(J.x) = L1.x by Lm1,A28,FUNCT_1:12;
hence L1.(x+y) =L1.x + L1.y by Lm1,A28,A30,FUNCT_1:12;
end;
now let x be Point of REAL-NS 1, a be Real;
L1.(a*x) = L/.(J.(a*x)) by Lm1,A28,FUNCT_1:12;
then L1.(a*x) = L/.(a*(J.x)) by A1,PDIFF_1:4;
then L1.(a*x) = (a*(J.x))*r by A27;
then
A31:L1.(a*x) = a*((J.x)*r) by RLVECT_1:def 7;
L/.(J.x) = L1.x by Lm1,A28,FUNCT_1:12;
hence L1.(a*x) =a*(L1.x) by A31,A27;
end;
then reconsider L1 as LinearOperator of REAL-NS 1,Y
by A29,LOPBAN_1:def 5,VECTSP_1:def 20;
now let x be Point of REAL-NS 1;
||. L1.x .|| =||. L/.(J.x) .|| by Lm1,A28,FUNCT_1:12;
then ||. L1.x .|| =||. (J.x)*r .|| by A27;
then ||. L1.x .|| =||.r.||*|.J.x .| by NORMSP_1:def 1;
hence ||. L1.x .|| <= K* ||.x.|| by A1,PDIFF_1:4;
end;
hence thesis by LOPBAN_1:def 8;
end;
theorem FTh42:
for I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y
st I=proj(1,1) qua Function" & x0 in dom f & y0 in dom g
& x0=<*y0*> & f*I = g & f is_differentiable_in x0 holds
g is_differentiable_in y0 & diff(g,y0)=diff(f,x0).<*1*> &
for r be Element of REAL holds diff(f,x0).<*r*> = r*diff(g,y0)
proof
let I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y;
assume that
A1: I=proj(1,1) qua Function" and
A2: x0 in dom f and
A3: y0 in dom g and
A4: x0=<*y0*> and
A5: f*I = g and
A6: f is_differentiable_in x0;
reconsider J= proj(1,1) as Function of REAL-NS 1, REAL by Lm1;
consider NN being Neighbourhood of x0 such that
A7: NN c= dom f and
A8: ex L be Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS 1,Y),
R be RestFunc of REAL-NS 1,Y
st for x be Point of REAL-NS 1 st x in NN
holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0) by A6;
A9:I*J = id REAL-NS 1 by Lm1,A1,Lm2,FUNCT_1:39;
A10:
g*J = f*(id REAL-NS 1) by A9,A5,RELAT_1:36
.= f by FUNCT_2:17;
consider e be Real such that
A11:0 < e and
A12:{z where z is Point of REAL-NS 1 : ||.z-x0.|| < e} c= NN by NFCONT_1:def 1;
consider L be Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS 1,Y),
R being RestFunc of REAL-NS 1,Y such that
A13:for x9 be Point of REAL-NS 1 st x9 in NN holds
f/.x9 - f/.x0 = L.(x9-x0) + R/.(x9-x0) by A8;
reconsider R0=R*I as RestFunc of Y by A1,FTh40;
L is LinearOperator of REAL-NS 1,Y by LOPBAN_1:def 9;
then reconsider L0=L*I as LinearFunc of Y by A1,FTh40;
set N={z where z is Point of REAL-NS 1 : ||.z-x0.|| < e};
A14:N c= the carrier of REAL-NS 1
proof
let y be object;
assume y in N;
then ex z be Point of REAL-NS 1 st y=z & ||.z-x0.|| < e;
hence thesis;
end;
then reconsider N as Neighbourhood of x0 by A11,NFCONT_1:def 1;
set N0={z where z is Element of REAL: |.z-y0.| < e};
now let z be object;
hereby assume z in N0;
then consider y9 be Element of REAL such that
A16: z=y9 and
A17: |.y9-y0.| < e;
reconsider w=I.y9 as Point of REAL-NS 1;
x0=I.y0 by A1,A4,Lm2;
then w-x0=I.(y9-y0) by A1,Lm1,PDIFF_1:3;
then ||.w-x0.||=|.y9-y0.| by A1,Lm1,PDIFF_1:3;
then
A18: w in {z0 where z0 is Point of REAL-NS 1 : ||.z0 - x0.|| < e} by A17;
J.(I.y9) = y9 by A1,Lm2,FUNCT_1:35;
hence z in J.:N by A18,A16,FUNCT_2:35;
end;
assume z in J.:N;
then consider ww be object such that
A19: ww in REAL 1 & ww in N & z=J.ww by FUNCT_2:64;
consider w be Point of REAL-NS 1 such that
A21: ww=w & ||.w-x0.|| < e by A19;
reconsider y9=J.w as Element of REAL;
J.x0=y0 by A4,Lm2;
then J.(w-x0) =y9-y0 by PDIFF_1:4;
then |.y9-y0.| < e by A21,PDIFF_1:4;
hence z in N0 by A19,A21;
end;
then
A23: N0=J.:N by TARSKI:2;
J.:(dom f) = J.:(J"(dom g)) by A10,RELAT_1:147;
then
A24: J.:(dom f) = dom(f*I) by A5,Lm2,FUNCT_1:77;
A25: I*J =id (REAL 1) by A1,Lm2,FUNCT_1:39;
A261: N c= dom f by A7,A12; then
A26: N0 c= dom(f*I) by A24,A23,RELAT_1:123;
A27: ].y0-e,y0+e.[ c= N0
proof
now let d be object;
assume A28: d in ].y0-e,y0+e.[; then
reconsider y1=d as Element of REAL;
|.y1-y0.| < e by A28,RCOMP_1:1;
hence d in N0;
end;
hence thesis;
end;
N0 c= ].y0-e,y0+e.[
proof
let d be object;
assume d in N0;
then ex r be Element of REAL st d=r & |.r-y0.| < e;
hence thesis by RCOMP_1:1;
end; then
N0 = ].y0-e,y0+e.[ by A27,XBOOLE_0:def 10; then
A29: N0 is Neighbourhood of y0 by A11,RCOMP_1:def 6;
N c= REAL 1 by A14,REAL_NS1:def 4;
then (I*J).:N = N by A25,FRECHET:13;
then
A30: I.:N0 = N by A23,RELAT_1:126;
A31:for y1 be Real st y1 in N0 holds
(f*I)/.y1 - (f*I)/.y0 = L0/.(y1-y0) + R0/.(y1-y0)
proof
let y1 be Real;
reconsider yy=y1 as Element of REAL by XREAL_0:def 1;
reconsider y9 = I.yy as Point of REAL-NS 1;
R is total by NDIFF_1:def 5; then
A32:dom R = the carrier of REAL-NS 1 by PARTFUN1:def 2;
R0 is total by NDIFF_3:def 1; then
A33: dom(R*I) = REAL by PARTFUN1:def 2;
reconsider dy1y0 = y1 - y0 as Element of REAL by XREAL_0:def 1;
I.(dy1y0) in dom R by A32;
then R/.(I.(y1-y0)) =R.(I.(y1-y0)) by PARTFUN1:def 6;
then R/.(I.(dy1y0)) =R0.(dy1y0) by A33,FUNCT_1:12;
then
A34:R/.(I.(y1-y0)) =R0/.(dy1y0) by A33,PARTFUN1:def 6;
L0 is total; then
A35:dom(L*I) = REAL by PARTFUN1:def 2;
assume
A36: y1 in N0; then
A37:I.yy in N by A30,FUNCT_2:35; then
f/.(I.y1) =f.(I.y1) by A7,A12,PARTFUN1:def 6; then
f/.(I.y1) =(f*I).y1 by A26,A36,FUNCT_1:12; then
A39:f/.(I.y1) =(f*I)/.y1 by A26,A36,PARTFUN1:def 6;
A40:x0=I.y0 by A4,A1,Lm2;
then f/.(I.y0) =f.(I.y0) by A2,PARTFUN1:def 6;
then f/.(I.y0) =(f*I).y0 by A3,A5,FUNCT_1:12;
then
A41:f/.(I.y0) =(f*I)/.y0 by A3,A5,PARTFUN1:def 6;
reconsider d = y1 - y0 as Element of REAL by XREAL_0:def 1;
f/.y9 - f/.x0=L.(y9-x0) + R/.(y9-x0) by A13,A12,A37;
then
A42:f/.(I.y1) - f/.(I.y0)=L.(I.d) + R/.(y9-x0) by A1,A40,Lm1,PDIFF_1:3;
L.(I.d) =L0/.(dy1y0) by A35,FUNCT_1:12;
hence thesis by A40,A42,A34,A39,A41,A1,Lm1,PDIFF_1:3;
end;
hence g is_differentiable_in y0 by A5,A29,A261,A24,A23,RELAT_1:123;
then diff(f*I,y0)=L0/.jj by A5,A31,A29,A26,NDIFF_3:def 4;
hence
A45:diff(g,y0)=(diff(f,x0)*I).1 by A5,A6,A13,A7,NDIFF_1:def 7
.=diff(f,x0).(I.jj) by A1,FUNCT_1:13,PDIFF_1:2
.=diff(f,x0).<*1*> by A1,Lm2;
let r be Element of REAL;
A46: <*jj*> is Element of REAL 1 by FINSEQ_2:98;
then reconsider x = <*1*> as Point of REAL-NS 1 by REAL_NS1:def 4;
A47: diff(f,x0) is LinearOperator of REAL-NS 1,Y by LOPBAN_1:def 9;
thus diff(f,x0).<*r*> = diff(f,x0).<*r*1*>
.= diff(f,x0).(r*<*1*>) by RVSUM_1:47
.= diff(f,x0).(r*x) by A46,REAL_NS1:3
.= r*diff(g,y0) by A45,A47,LOPBAN_1:def 5;
end;
theorem FTh43:
for I be Function of REAL,REAL-NS 1, x0 be Point of REAL-NS 1, y0 be Real,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y
st I=proj(1,1) qua Function" & x0 in dom f & y0 in dom g
& x0=<*y0*> & f*I = g holds
f is_differentiable_in x0 iff g is_differentiable_in y0
proof
let I be Function of REAL,REAL-NS 1, x0 be Point of REAL-NS 1, y0 be Real,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y;
assume that
A1: I=proj(1,1) qua Function" and
A2: x0 in dom f and
A3: y0 in dom g and
A4: x0=<*y0*> and
A5: f*I = g;
reconsider J = proj(1,1) as Function of REAL-NS 1, REAL by Lm1;
thus f is_differentiable_in x0 implies g is_differentiable_in y0
by A2,A3,A4,A5,FTh42,A1;
assume g is_differentiable_in y0; then
consider N0 being Neighbourhood of y0 such that
A6: N0 c= dom (f*I) and
A7: ex L be LinearFunc of Y,R be RestFunc of Y st
for y be Real st y in N0 holds
(f*I)/.y - (f*I)/.y0 = L/.(y-y0) + R/.(y-y0) by A5;
reconsider y0 as Element of REAL by XREAL_0:def 1;
A8:I*J = id REAL-NS 1 by Lm1,A1,Lm2,FUNCT_1:39;
A9:g*J = f*(id REAL-NS 1) by A5,A8,RELAT_1:36
.= f by FUNCT_2:17;
consider e0 be Real such that
A10:0 < e0 and
A11:N0 = ].y0 - e0,y0 + e0.[ by RCOMP_1:def 6;
reconsider e = e0 as Element of REAL by XREAL_0:def 1;
set N = {z where z is Point of REAL-NS 1 : ||.z-x0.|| < e};
consider L be LinearFunc of Y, R be RestFunc of Y such that
A12: for y1 be Real st y1 in N0 holds
(f*I)/.y1 - (f*I)/.y0 = L/.(y1-y0) + R/.(y1-y0) by A7;
reconsider R0=R*J as RestFunc of REAL-NS 1,Y by FTh41;
reconsider L0=L*J as Lipschitzian LinearOperator of REAL-NS 1,Y by FTh41;
now let z be object;
hereby assume z in N;
then consider w be Point of REAL-NS 1 such that
A13: z=w and
A14: ||.w-x0.|| < e;
reconsider y2=J.w as Element of REAL;
J.x0=y0 by A4,Lm2;
then J.(w-x0) =y2-y0 by PDIFF_1:4;
then |.y2-y0.| < e by A14,PDIFF_1:4;
then
A15: y2 in N0 by A11,RCOMP_1:1;
w in the carrier of REAL-NS 1;
then w in dom J by Lm2,REAL_NS1:def 4;
then w=I.y2 by A1,FUNCT_1:34;
hence z in I.:N0 by A13,A15,FUNCT_2:35;
end;
assume z in I.:N0;
then consider yy be object such that
A16: yy in REAL and
A17: yy in N0 and
A18: z=I.yy by FUNCT_2:64;
reconsider y3=yy as Element of REAL by A16;
set w = I.y3;
I.y0=x0 by A4,A1,Lm2;
then
A19:w-x0 =I.(y3-y0) by A1,Lm1,PDIFF_1:3;
|.y3-y0.| < e by A11,A17,RCOMP_1:1;
then ||.w-x0.|| < e by A19,A1,Lm1,PDIFF_1:3;
hence z in N by A18;
end;
then
A20: N=I.:N0 by TARSKI:2;
I.:(dom g) = I.:(I"(dom f)) by A5,RELAT_1:147;
then
A211: I.:(dom g) = dom f by A1,Lm1,FUNCT_1:77,PDIFF_1:2;
then
A21: N c= dom f by A5,A6,A20,RELAT_1:123;
N c= the carrier of REAL-NS 1
proof
let y be object;
assume y in N;
then ex z be Point of REAL-NS 1 st y=z & ||.z-x0.|| < e;
hence thesis;
end;
then
A22: N is Neighbourhood of x0 by A10,NFCONT_1:def 1;
J*I=id REAL by A1,Lm2,FUNCT_1:39;
then (J*I).:N0 = N0 by FRECHET:13;
then
A23: J.:N = N0 by A20,RELAT_1:126;
A24: for y be Point of REAL-NS 1 st y in N holds
f/.y - f/.x0 = L0.(y-x0) + R0/.(y-x0)
proof
x0 in the carrier of REAL-NS 1;
then x0 in dom J by Lm2,REAL_NS1:def 4;
then g.(J.x0) =f.x0 by A9,FUNCT_1:13;
then
A25:g.(J.x0) =f/.x0 by A2,PARTFUN1:def 6;
A26:J.x0 = y0 by A4,Lm2;
let y be Point of REAL-NS 1;
assume
A27: y in N;
set y3 = J.y;
reconsider p1=g/.y3,p2=g/.y0, q1=L/.(y3-y0), q2=R/.(y3-y0)
as VECTOR of Y;
A28: J.x0=y0 by A4,Lm2;
g/.y3 - g/.y0=q1+q2 by A5,A12,A23,A27,FUNCT_2:35;
then g/.(J.y) - g/.(J.x0)=L/.(J.(y-x0)) + R/.(y3-y0) by A28,PDIFF_1:4;
then
A29: g/.(J.y) - g/.(J.x0)= L/.(J.(y-x0)) + R/.(J.(y-x0)) by A28,PDIFF_1:4;
A30: dom L0 = the carrier of REAL-NS 1 by FUNCT_2:def 1;
y-x0 in the carrier of REAL-NS 1;
then y-x0 in dom J by Lm2,REAL_NS1:def 4;
then
A31: R.(J.(y-x0)) =(R*J).(y-x0) by FUNCT_1:13;
R0 is total by NDIFF_1:def 5;
then
A32: dom(R*J) = the carrier of REAL-NS 1 by PARTFUN1:def 2;
A33: R.(J.(y-x0)) =R0/.(y-x0) by A31,A32,PARTFUN1:def 6;
J.(y-x0) in dom R by A32,FUNCT_1:11;
then
A34: R/.(J.(y-x0)) =R0/.(y-x0) by A33,PARTFUN1:def 6;
y in the carrier of REAL-NS 1;
then
A35: y in dom J by Lm2,REAL_NS1:def 4;
g.(J.y) =f.y by A9,A35,FUNCT_1:13;
then
A36: g.(J.y) =f/.y by A21,A27,PARTFUN1:def 6;
J.y in dom g by A21,A27,A9,FUNCT_1:11;
then g/.(J.y) =f/.y by A36,PARTFUN1:def 6;
then g/.(J.y) - g/.(J.x0) = f/.y -f/.x0 by A3,A26,A25,PARTFUN1:def 6;
hence thesis by A29,A34,A30,FUNCT_1:12;
end;
reconsider L0 as Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS 1,Y) by LOPBAN_1:def 9;
for x be Point of REAL-NS 1 st x in N
holds f/.x - f/.x0 = L0.(x-x0) + R0/.(x-x0) by A24;
hence f is_differentiable_in x0 by A22,A211,A5,A6,A20,RELAT_1:123;
end;
theorem FTh44:
for J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y
st J=proj(1,1) & x0 in dom f & y0 in dom g & x0=<*y0*> & f = g*J holds
f is_differentiable_in x0 iff g is_differentiable_in y0
proof
let J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y;
assume A1: J=proj(1,1) & x0 in dom f & y0 in dom g & x0=<*y0*> & f = g*J;
reconsider I= (proj(1,1) qua Function") as Function of REAL,REAL-NS 1
by PDIFF_1:2,REAL_NS1:def 4;
J*I = id REAL by A1,Lm2,FUNCT_1:39; then
f*I = g*(id REAL) by A1,RELAT_1:36
.= g by FUNCT_2:17;
hence thesis by A1,FTh43;
end;
LM519A:
for x be Point of REAL-NS 1 ex z be Real st x=<*z*>
proof
let x be Point of REAL-NS 1;
x is Element of REAL 1 by REAL_NS1:def 4;
then ex z be Element of REAL st x = <*z*> by FINSEQ_2:97;
hence thesis;
end;
theorem FTh42A:
for I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y
st I=proj(1,1) qua Function" & x0 in dom f & y0 in dom g
& x0=<*y0*> & f*I = g & f is_differentiable_in x0 holds
||.diff(g,y0).|| = ||.diff(f,x0).||
proof
let I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1, y0 be Element of REAL,
g be PartFunc of REAL,Y, f be PartFunc of REAL-NS 1,Y;
assume A1:I=proj(1,1) qua Function" & x0 in dom f & y0 in dom g
& x0=<*y0*> & f*I = g & f is_differentiable_in x0;
reconsider J= proj(1,1) as Function of REAL-NS 1,REAL by Lm1;
reconsider j1=1 as Real;
<*jj*> in REAL 1 by FINSEQ_2:98; then
reconsider t=<*jj*> as Point of REAL-NS 1 by REAL_NS1:def 4;
J.t = jj by Lm2; then
||.t.|| = |.j1.| by PDIFF_1:4; then
A3: ||.t.|| = 1 by ABSVALUE:def 1;
reconsider dfx0 = diff(f,x0) as Lipschitzian LinearOperator of REAL-NS 1,Y
by LOPBAN_1:def 9;
set A = PreNorms(dfx0);
||.diff(g,y0).|| = ||.diff(f,x0).t .|| by A1,FTh42; then
A5:||.diff(g,y0).|| in A by A3;
A6:||.diff(f,x0).||
= upper_bound PreNorms(modetrans(diff(f,x0),REAL-NS 1,Y))
by LOPBAN_1:def 13
.= upper_bound A by LOPBAN_1:29;
A is bounded_above by LOPBAN_1:27; then
A7:||.diff(g,y0).|| <= ||.diff(f,x0).|| by A6,A5,SEQ_4:def 1;
for r be Real st r in A holds r <= ||.diff(g,y0).||
proof
let r be Real;
assume r in A; then
consider v be VECTOR of REAL-NS 1 such that
A8: r = ||. dfx0.v .|| & ||.v.|| <= 1;
consider s be Real such that
X12: v = <*s*> by LM519A;
reconsider J= proj(1,1) as Function of REAL 1,REAL;
J.v = s by X12,PDIFF_1:1; then
X13:||.v.|| = |.s.| by PDIFF_1:4;
reconsider s1=s as Element of REAL by XREAL_0:def 1;
A9: diff(f,x0).<*s1*> = s1 * diff(g,y0) by A1,FTh42;
|.s.|*||.diff(g,y0).|| <= 1 * ||.diff(g,y0).|| by A8,X13,XREAL_1:64;
hence thesis by A8,A9,X12,NORMSP_1:def 1;
end; then
||.diff(f,x0).|| <= ||.diff(g,y0).|| by A6,SEQ_4:45;
hence ||.diff(g,y0).|| = ||.diff(f,x0).|| by A7,XXREAL_0:1;
end;
theorem LM519B1:
for a,b,z be Real, p,q,x be Point of REAL-NS 1
st p= <*a*> & q= <*b*> & x = <*z*> holds
( z in ].a,b.[ implies x in ].p,q.[ )
& ( x in ].p,q.[ implies
a <> b
& (a < b implies z in ].a,b.[)
& (a > b implies z in ].b,a.[) )
proof
let a,b,z be Real,p,q,x be Point of REAL-NS 1;
reconsider I= proj(1,1) qua Function" as Function of REAL,REAL 1
by PDIFF_1:2;
reconsider J= proj(1,1) as Function of REAL-NS 1,REAL by Lm1;
assume
P2: p = <*a*> & q = <*b*> & x = <*z*>;
A2:I.a = p & I.b = q & I.z = x & J.p = a & J.q = b & J.x = z by P2,PDIFF_1:1;
hereby assume z in ].a,b.[; then
A4: a < z & z < b by XXREAL_1:4; then
A5: a < b by XXREAL_0:2;
reconsider r=(z-a)/(b-a) as Real;
A6: 0 < z-a & 0 < b-a & z-a < b-a by A4,A5,XREAL_1:14,50; then
C1: 0 < r & r < 1 by XREAL_1:139,191;
C3: (1-r)*a + r*b = a + (z-a)/(b-a)*(b-a)
.= a + (z-a) by A6,XCMPLX_1:87;
q-p = I.(b-a) by A2,PDIFF_1:3; then
r*(q-p) = I.(r*(b-a)) by PDIFF_1:3; then
p + r*(q-p) = x by A2,C3,PDIFF_1:3; then
x in { p+t*(q-p) where t is Real : 0 < t & t < 1} by C1;
hence x in ].p,q.[ by A4,P2,FINSEQ_1:76,NDIFF_5:16;
end;
assume x in ].p,q.[; then
X1:x in [.p,q.] & not x in {p,q} by XBOOLE_0:def 5; then
x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1}
by RLTOPSP1:def 2; then
consider r be Real such that
B1: x = (1-r)*p+r*q & 0 <= r & r <= 1;
B2:J.x = J.((1-r)*p) + J.(r*q) by B1,PDIFF_1:4
.= (1-r)*J.p + J.(r*q) by PDIFF_1:4
.=(1-r)*J.p + r*J.q by PDIFF_1:4;
hence a <> b by A2,X1,TARSKI:def 2;
X3:now assume r=0; then
x = p + (0 qua Real)*q by B1,RLVECT_1:def 8
.= p + 0.(REAL-NS 1) by RLVECT_1:10;
hence contradiction by X1,TARSKI:def 2;
end;
now assume r=1; then
x = (0 qua Real)*p + q by B1,RLVECT_1:def 8
.= 0.(REAL-NS 1) + q by RLVECT_1:10;
hence contradiction by X1,TARSKI:def 2;
end; then
X4:r < 1 by B1,XXREAL_0:1;
set s = 1-r;
X5:r = 1-s & 0<s & s<1 by X3,B1,X4,XREAL_1:44,50;
hereby assume a < b; then
a < z & z < b by A2,X3,B1,X4,XREAL_1:177,178,B2;
hence z in ].a,b.[;
end;
assume a > b; then
b < z & z < a by A2,X5,XREAL_1:177,178,B2;
hence z in ].b,a.[;
end;
theorem LM519C1:
for a,b,z be Real,p,q,x be Point of REAL-NS 1
st p= <*a*> & q= <*b*> & x = <*z*> holds
( z in [.a,b.] implies x in [.p,q.] )
& ( x in [.p,q.] implies
(a <= b implies z in [.a,b.])
& (a >= b implies z in [.b,a.]) )
proof
let a,b,z be Real,p,q,x be Point of REAL-NS 1;
reconsider I= proj(1,1) qua Function" as Function of REAL,REAL 1
by PDIFF_1:2;
reconsider J= proj(1,1) as Function of REAL-NS 1, REAL by Lm1;
assume A1: p= <*a*> & q= <*b*> & x = <*z*>; then
A2:p = I.a & q = I.b & x = I.z & J.p = a & J.q = b & J.x = z by PDIFF_1:1;
thus z in [.a,b.] implies x in [.p,q.]
proof
assume z in [.a,b.]; then
A5: a <= z & z <= b by XXREAL_1:1; then
A6: a <= b by XXREAL_0:2;
per cases;
suppose Z1: a = b;
reconsider r = 0 as Real;
Z2: z = (1-r)*a + r*b by Z1,A5,XXREAL_0:1;
(1-r)*p = I.((1-r)*a) & r*q = I.(r*b) by A2,PDIFF_1:3; then
I.z = (1-r)*p + r*q by Z2,PDIFF_1:3; then
x = (1-r)*p + r*q by A1,PDIFF_1:1; then
x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1 };
hence thesis by RLTOPSP1:def 2;
end;
suppose a <> b; then
X2: a < b by A6,XXREAL_0:1;
reconsider r=(z-a)/(b-a) as Real;
A7: 0 <= z-a & 0 <= b-a by A5,A6,XREAL_1:48;
z-a <= b-a by A5,XREAL_1:13; then
C2: r <= 1 by A7,XREAL_1:185;
A8: 0 < b-a by X2,XREAL_1:50;
C3: (1-r)*a + r*b = a + (z-a)/(b-a)*(b-a)
.= a + (z-a) by A8,XCMPLX_1:87;
(1-r)*p = I.((1-r)*a) & r*q = I.(r*b) by A2,PDIFF_1:3; then
(1-r)*p + r*q = I.z by C3,PDIFF_1:3
.= x by A1,PDIFF_1:1; then
x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1 } by A7,C2;
hence thesis by RLTOPSP1:def 2;
end;
end;
assume x in [.p,q.]; then
x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1 }
by RLTOPSP1:def 2; then
consider r be Real such that
B2: x = (1-r)*p+r*q & 0 <= r & r <= 1;
B4:J.x = J.((1-r)*p)+J.(r*q) by B2,PDIFF_1:4
.= (1-r)*J.p + J.(r*q) by PDIFF_1:4
.= (1-r)*J.p + r*J.q by PDIFF_1:4;
B5:now assume a <= b; then
a <= z & z <= b by A2,XREAL_1:171,172,B2,B4;
hence z in [.a,b.];
end;
now assume B6: a >= b;
set s = 1-r;
0 <= s & s <= 1 & J.x = s*J.p + (1-s)*J.q by B2,B4,XREAL_1:43,48; then
b <= z & z <= a by A2,XREAL_1:171,172,B6;
hence z in [.b,a.];
end;
hence thesis by B5;
end;
theorem LM519D:
for a,b be Real,p,q be Point of REAL-NS 1,
I be Function of REAL,REAL-NS 1
st p= <*a*> & q= <*b*> & I = proj(1,1) qua Function" holds
(a<=b implies I.:([.a,b.]) = [.p,q.])
& ( a<b implies I.:(].a,b.[) = ].p,q.[)
proof
let a,b be Real,p,q be Point of REAL-NS 1,
I be Function of REAL,REAL-NS 1;
assume that
A1: p= <*a*> & q= <*b*> and
A2: I = proj(1,1) qua Function";
hereby assume X1: a<=b;
now let y be object;
assume y in I.:([.a,b.]); then
consider x be object such that
A3: x in dom I & [x,y] in I & x in [.a,b.] by RELAT_1:110;
reconsider x as Element of REAL by A3;
I.x = <*x*> by A2,PDIFF_1:1; then
I.x in [.p,q.] by A1,A3,LM519C1;
hence y in [.p,q.] by A3,FUNCT_1:1;
end; then
A6: I.:([.a,b.]) c= [.p,q.];
reconsider J= proj(1,1) as Function of REAL-NS 1, REAL by Lm1;
A7: J.p = a & J.q = b by A1,PDIFF_1:1;
now let x be object;
assume B0: x in [.p,q.]; then
x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1 }
by RLTOPSP1:def 2; then
consider r be Real such that
B2: x = (1-r)*p+r*q & 0 <= r & r <= 1;
J.x = J.((1-r)*p)+J.(r*q) by B2,PDIFF_1:4
.= (1-r)*J.p + J.(r*q) by PDIFF_1:4
.= (1-r)*J.p + r*J.q by PDIFF_1:4; then
a <= J.x & J.x <= b by A7,X1,XREAL_1:171,172,B2; then
B5: J.x in [.a,b.]; then
reconsider z=J.x as Element of REAL;
set z1=I.z;
[z,I.z] in I by A2,PDIFF_1:2,FUNCT_1:1; then
B9: I.z in I.:([.a,b.]) by B5,A2,PDIFF_1:2,RELAT_1:110;
I*J = id rng I by PDIFF_1:2,A2,Lm2,FUNCT_1:39; then
J = I" by A2,PDIFF_1:2,Lm2,FUNCT_1:42;
hence x in I.:([.a,b.]) by B9,FUNCT_1:35,Lm1,A2,PDIFF_1:2,B0;
end; then
[.p,q.] c= I.:([.a,b.]);
hence I.:([.a,b.]) = [.p,q.] by A6,XBOOLE_0:def 10;
end;
assume X2: a<b;
now let y be object;
assume y in I.:(].a,b.[); then
consider x be object such that
B3: x in dom I & [x,y] in I & x in ].a,b.[ by RELAT_1:110;
reconsider x as Element of REAL by B3;
I.x = <*x*> by A2,PDIFF_1:1; then
I.x in ].p,q.[ by A1,B3,LM519B1;
hence y in ].p,q.[ by B3,FUNCT_1:1;
end; then
B6:I.:(].a,b.[) c= ].p,q.[;
reconsider J= proj(1,1) as Function of REAL-NS 1, REAL by Lm1;
A7:J.p = a & J.q = b by A1,PDIFF_1:1;
now let x be object;
assume B0: x in ].p,q.[; then
B0c: x in [.p,q.] & not x in {p,q} by XBOOLE_0:def 5; then
B0b:x <> p & x <> q by TARSKI:def 2;
x in {(1-r)*p + r*q where r is Real: 0 <= r & r <= 1}
by B0c,RLTOPSP1:def 2; then
consider r be Real such that
B1: x = (1-r)*p+r*q & 0 <= r & r <= 1;
now assume r = 1; then
x = 0.(REAL-NS 1) + (1 qua Real)*q by B1,RLVECT_1:10;
hence contradiction by B0b,RLVECT_1:def 8;
end; then
B1a:r < 1 by B1,XXREAL_0:1;
B1b:now assume r = 0; then
x = (1 qua Real)*p + 0.(REAL-NS 1) by B1,RLVECT_1:10;
hence contradiction by B0b,RLVECT_1:def 8;
end;
J.x = J.((1-r)*p) + J.(r*q) by B1,PDIFF_1:4
.= (1-r)*J.p + J.(r*q) by PDIFF_1:4
.= (1-r)*J.p + r*J.q by PDIFF_1:4; then
a < J.x & J.x < b by A7,X2,XREAL_1:177,178,B1a,B1,B1b; then
B5: J.x in ].a,b.[; then
reconsider z=J.x as Element of REAL;
set z1=I.z;
B91:[z,I.z] in I by A2,PDIFF_1:2,FUNCT_1:1;
B11:rng I = the carrier of REAL-NS 1 by A2,REAL_NS1:def 4,PDIFF_1:2;
I*J = id rng I by PDIFF_1:2,A2,Lm2,FUNCT_1:39; then
B14:J = I" by A2,PDIFF_1:2,Lm2,FUNCT_1:42;
x = I.(J.x) by A2,B14,FUNCT_1:35,B11,B0;
hence x in I.:(].a,b.[) by B91,B5,A2,PDIFF_1:2,RELAT_1:110;
end; then
].p,q.[ c= I.:(].a,b.[);
hence I.:(].a,b.[) = ].p,q.[ by B6,XBOOLE_0:def 10;
end;
theorem Th519:
for Y be RealNormSpace, g be PartFunc of REAL,the carrier of Y,
a,b,M be Real
st a <= b &
[.a,b.] c= dom g
& (for x be Real st x in [.a,b.] holds g is_continuous_in x)
& (for x be Real st x in ].a,b.[ holds g is_differentiable_in x)
& (for x be Real st x in ].a,b.[ holds ||.diff(g,x).|| <= M) holds
||. g/.b - g/.a .|| <= M*|.b-a.|
proof
let Y be RealNormSpace, g be PartFunc of REAL,the carrier of Y,
a,b,M be Real;
assume AS0: a <= b;
assume AS1: [.a,b.] c= dom g;
assume AS2: for x be Real st x in [.a,b.] holds g is_continuous_in x;
assume AS3: for x be Real st x in ].a,b.[ holds g is_differentiable_in x;
assume AS4: for x be Real st x in ].a,b.[ holds ||. diff(g,x) .|| <= M;
the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4; then
reconsider J=proj(1,1) as Function of REAL-NS 1,REAL;
reconsider f = g*J as PartFunc of REAL-NS 1,Y;
reconsider I= (proj(1,1) qua Function") as Function of REAL,REAL-NS 1
by PDIFF_1:2,REAL_NS1:def 4;
now let r be Real;
r is Element of REAL by XREAL_0:def 1; then
<*r*> in REAL 1 by FINSEQ_2:98;
hence <*r*> is Point of REAL-NS 1 by REAL_NS1:def 4;
end; then
reconsider p = <*a*>, q=<*b*> as Point of REAL-NS 1;
Y0:].a,b.[ c= [.a,b.] by XXREAL_1:25;
DX1: J*I = id REAL by Lm2,FUNCT_1:39;
DX2: f*I = g*(id REAL) by DX1,RELAT_1:36
.= g by FUNCT_2:17;
dom f = J"(dom g) by RELAT_1:147
.= I.:(dom g) by FUNCT_1:85; then
I.:([.a,b.]) c= dom f by AS1,RELAT_1:123; then
X0:[.p,q.] c= dom f by AS0,LM519D;
X1:for x be Point of REAL-NS 1 st x in [.p,q.] holds f is_continuous_in x
proof
let x be Point of REAL-NS 1;
assume X11: x in [.p,q.];
consider z be Real such that
X12: x=<*z*> by LM519A;
z in [.a,b.] by AS0,LM519C1,X11,X12; then
g is_continuous_in z by AS2;
hence f is_continuous_in x by NDIFF435,X12,X0,X11;
end;
X2:for x be Point of REAL-NS 1 st x in ].p,q.[
holds f is_differentiable_in x
proof
let x be Point of REAL-NS 1;
assume X11: x in ].p,q.[; then
X15:x in [.p,q.] by XBOOLE_0:def 5;
consider z be Real such that
X12: x=<*z*> by LM519A;
per cases;
suppose a = b;
hence f is_differentiable_in x by X11,X12,LM519B1;
end;
suppose a <> b; then
a < b by AS0,XXREAL_0:1; then
z in ].a,b.[ by LM519B1,X11,X12; then
z in dom g & g is_differentiable_in z by AS1,Y0,AS3;
hence f is_differentiable_in x by FTh44,X12,X0,X15;
end;
end;
X3:for x be Point of REAL-NS 1 st x in ].p,q.[ holds ||.diff(f,x).|| <= M
proof
let x be Point of REAL-NS 1;
assume X11: x in ].p,q.[; then
B11:x in [.p,q.] by XBOOLE_0:def 5;
consider z be Real such that
X12: x=<*z*> by LM519A;
per cases;
suppose a=b;
hence ||.diff(f,x).|| <= M by X11,X12,LM519B1;
end;
suppose a<>b; then
a<b by AS0,XXREAL_0:1; then
X13: z in ].a,b.[ by LM519B1,X11,X12; then
X14: ||.diff(g,z).|| <= M by AS4;
f is_differentiable_in x by X2,X11;
hence ||.diff(f,x).|| <= M by B11,Y0,X0,X12,DX2,X14,FTh42A,AS1,X13;
end;
end;
S0:dom I = REAL by FUNCT_2:def 1;
S1:p = I.a & q=I.b by PDIFF_1:1;
S2:p in dom f & q in dom f by X0,RLTOPSP1:68;
a in [.a,b.] & b in [.a,b.] by AS0; then
g/.a = g.a & g/.b = g.b by PARTFUN1:def 6,AS1; then
g/.a = f.(I.a) & g/.b = f.(I.b) by DX2,FUNCT_1:13,S0,XREAL_0:def 1; then
S3:g/.a = f/.p & g/.b = f/.q by S1,S2,PARTFUN1:def 6;
q-p = I.(b-a) by S1,Lm1,PDIFF_1:3; then
||.q-p.|| = |.b-a.| by Lm1,PDIFF_1:3;
hence thesis by NDIFF_5:19,X0,X1,X2,X3,S3;
end;
begin :: Differential Equations
reserve X,Y for RealBanachSpace;
reserve Z for open Subset of REAL;
reserve a,b,c,d,e,r,x0 for Real;
reserve y0 for VECTOR of X;
reserve G for Function of X,X;
Lm13a:
for f be continuous PartFunc of REAL,the carrier of Y
st ( [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.]
& for x be Real st x in [.min(c,d),max(c,d).] holds ||. f/.x .|| <= e)
holds ||.integral(f,c,d).||<= e * |.d-c.|
proof
let f be continuous PartFunc of REAL,the carrier of Y;
set A = ['min(c,d),max(c,d)'];
assume that
A1: [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.] and
A2: for x be Real st x in [.min(c,d),max(c,d).] holds ||. f/.x .|| <= e;
X0:a <= c & c <= b by A1,XXREAL_1:1; then
X3:a <= b by XXREAL_0:2;
X1:[.a,b.] = ['a,b'] by X0,XXREAL_0:2,INTEGRA5:def 3;
rng ||.f.|| c= REAL; then
A3:||.f.|| is Function of dom ||.f.||,REAL by FUNCT_2:2;
min(c,d) <= c & c <= max(c,d) by XXREAL_0:17,25; then
X2:['min(c,d),max(c,d)'] = [.min(c,d),max(c,d).]
by XXREAL_0:2,INTEGRA5:def 3;
dom ||.f.|| = dom f by NORMSP_0:def 2; then
A4:['min(c,d),max(c,d)'] c= dom ||.f.||
by A1,X0,XXREAL_0:2,X1,INTEGR19:3; then
reconsider g =||.f.|| |A as Function of A,REAL by A3,FUNCT_2:32;
A5:vol A = |.d-c.| by INTEGRA6:6;
A6: ||.f.|| is_integrable_on A by A1,X3,X1,INTEGR21:22;
consider h be Function of A,REAL such that
A7: rng h = {e} and
A8: h|A is bounded by INTEGRA4:5;
A9:now let x be Real;
assume
A10: x in A; then
g.x = ||.f.||.x by FUNCT_1:49; then
A11:g.x = ||.f/.x .|| by A10,A4,NORMSP_0:def 3;
h.x in {e} by A7,A10,FUNCT_2:4; then
h.x =e by TARSKI:def 1;
hence g.x <= h.x by A11,A2,A10,X2;
end;
A12: ||.integral(f,c,d).|| <= integral(||.f.||,min(c,d),max(c,d))
by A1,X1,X3,INTEGR21:22;
min(c,d) <= c & c <= max(c,d) by XXREAL_0:17,25; then
A13: integral(||.f.||,min(c,d),max(c,d)) = integral(||.f.||,A)
by INTEGRA5:def 4,XXREAL_0:2;
A14: g|A is bounded by A1,X1,X3,INTEGR21:22;
h is integrable & integral h = e*vol A by A7,INTEGRA4:4; then
integral(||.f.||,min(c,d),max(c,d)) <= e * |.d-c.|
by A13,A8,A9,A6,A14,A5,INTEGRA2:34;
hence thesis by A12,XXREAL_0:2;
end;
Lm14a:
for f be continuous PartFunc of REAL,the carrier of Y
st ( c <= d & [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.]
& for x be Real st x in [.c,d.] holds ||.f/.x .|| <= e )
holds ||.integral(f,c,d).|| <= e * (d-c)
proof
let f be continuous PartFunc of REAL,the carrier of Y;
assume that
A2: c <= d and
A3: [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.]
& for x be Real st x in [.c,d.] holds ||.f/.x .|| <= e;
A4:|.d-c.| = d-c by ABSVALUE:def 1,A2,XREAL_1:48;
min(c,d) = c & max(c,d) = d by A2,XXREAL_0:def 9,def 10;
hence thesis by A3,A4,Lm13a;
end;
Lm17:
for X be RealNormSpace, x be Point of X holds ||.a"*x.|| = ||.x.||/|.a.|
proof
let X be RealNormSpace, x be Point of X;
||.a"*x.|| = |.a".|*||.x.|| by NORMSP_1:def 1;
hence ||.a"*x.|| =||.x.||/|.a.| by COMPLEX1:66;
end;
theorem Th1955:
for X be RealBanachSpace, F be PartFunc of REAL,the carrier of X,
f be continuous PartFunc of REAL,the carrier of X
st [.a,b.] c= dom f & ].a,b.[ c= dom F
& (for x be Real st x in ].a,b.[ holds F/.x = integral(f,a,x))
& x0 in ].a,b.[ & f is_continuous_in x0 holds
F is_differentiable_in x0 & diff(F,x0)=f/.x0
proof
let X be RealBanachSpace,
F be PartFunc of REAL,the carrier of X,
f be continuous PartFunc of REAL,the carrier of X;
deffunc F2(object) = 0.X;
assume that
A4: [.a,b.] c= dom f and
A5: ].a,b.[ c= dom F and
A6: for x be Real st x in ].a,b.[ holds F/.x = integral(f,a,x) and
A7: x0 in ].a,b.[ and
A8: f is_continuous_in x0;
per cases;
suppose A1: a <= b; then
X5: ['a,b'] = [.a,b.] by INTEGRA5:def 3;
defpred C1[object] means x0+In($1,REAL) in ].a,b.[;
deffunc F0(Real)=$1*(f/.x0);
consider L be Function of REAL,the carrier of X such that
B9: for h be Element of REAL holds L.h=F0(h) from FUNCT_2:sch 4;
A9: for h be Real holds L.h=F0(h)
proof
let h be Real;
h is Element of REAL by XREAL_0:def 1;
hence thesis by B9;
end;
C9: for h be Real holds L/.h=F0(h)
proof
let h be Real;
reconsider h as Element of REAL by XREAL_0:def 1;
L/.h = F0(h) by B9;
hence thesis;
end;
then reconsider L as LinearFunc of X by NDIFF_3:def 2;
deffunc F1(object) = F/.(x0+In($1,REAL))-F/.x0-L.(In($1,REAL));
consider R be Function such that
A10: dom R=REAL
& for x be object st x in REAL holds
( C1[x] implies R.x = F1(x) )
& ( not C1[x] implies R.x = F2(x) ) from PARTFUN1:sch 1;
rng R c= the carrier of X
proof
let y be object;
assume y in rng R;
then consider x be object such that
A11: x in dom R & y=R.x by FUNCT_1:def 3;
(C1[x] implies R.x = F1(x)) & (not C1[x] implies R.x = F2(x)) by A10,A11;
hence thesis by A11;
end;
then reconsider R as PartFunc of REAL,the carrier of X by A10,RELSET_1:4;
A14:R is total by A10,PARTFUN1:def 2;
A15:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
X1: ].a,b.[ c= ['a,b'] by XXREAL_1:25;
A16:for h be 0-convergent non-zero Real_Sequence holds
(h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0.X
proof
let h be 0-convergent non-zero Real_Sequence;
set Z0 = 0.X;
A17: for e be Real st 0<e
ex n be Nat st
for m be Nat st n <= m holds ||.((h")(#)(R/*h)).m - Z0 .|| < e
proof
set g = REAL --> (f/.x0);
let e0 be Real;
set e = e0/2;
A18: h is convergent & lim h = 0;
assume
A19: 0 < e0;
then consider p be Real such that
A20: 0 < p and
A21: for t be Real st t in dom f & |.t - x0.| < p holds
||.f/.t - f/.x0.|| < e by A8,NFCONT_3:8,XREAL_1:215;
A22: e0/2 < e0 & 0 < p/2 & p/2 < p by A19,A20,XREAL_1:215,216;
consider N be Neighbourhood of x0 such that
A24: N c= ].a,b.[ by A7,RCOMP_1:18;
consider q be Real such that
A25: 0<q and
A26: N = ].x0-q,x0+q.[ by RCOMP_1:def 6;
set r=min(p/2,q/2);
A27: 0 < q/2 & q/2 < q by A25,XREAL_1:215,216;
then 0 < r by A22,XXREAL_0:15;
then consider n0 be Nat such that
A28: for m be Nat st n0 <= m holds |.h.m - 0 .|<r by A18,SEQ_2:def 7;
reconsider n0 as Element of NAT by ORDINAL1:def 12;
take n0;
let m be Nat;
A40: r <= p/2 & r <= q/2 by XXREAL_0:17;
then
A29: ].x0-r,x0+r.[ c= ].x0-q,x0+q.[ by A27,INTEGRA6:2,XXREAL_0:2;
assume n0 <= m; then
A30: |.h.m - 0 .| < r by A28;
then |.(x0 + h.m)-x0.| < r; then
A31: x0 + h.m in ].x0-q,x0+q.[ by A29,RCOMP_1:1; then
X2: x0+h.m in ].a,b.[ by A24,A26;
A32: R.(h.m)=F/.(x0+h.m)-F/.x0-L.In(h.m,REAL) by A10,A24,A26,A31;
F/.x0 =integral(f,a,x0) & F/.(x0+h.m) =integral(f,a,x0+h.m)
by A6,A7,A24,A26,A31; then
A35: R.(h.m) =integral(f,a,x0+h.m) -integral(f,a,x0) -h.m*(f/.x0) by A9,A32;
A36: dom g = REAL;
['a,b'] /\ ['a,b'] c= dom f /\ dom g by A4,X5,XBOOLE_1:27;
then
A37: ['a,b'] c= dom (f-g) by VFUNCT_1:def 2;
A39: integral(f,a,x0+h.m) = integral(f,a,x0) +integral(f,x0,x0+h.m)
by A1,X5,A4,A7,X1,X2,INTEGR21:29;
A41: for x be Real st x in ['min(x0,x0+h.m),max(x0,x0+h.m)']
holds ||.(f-g)/.x .|| <= e
proof
let x be Real;
A42: min(x0,x0+h.m) <= x0 & x0 <= max(x0,x0+h.m) by XXREAL_0:17,25;
assume x in ['min(x0,x0+h.m),max(x0,x0+h.m)']; then
A43: x in [. min(x0,x0+h.m),max(x0,x0+h.m) .]
by A42,INTEGRA5:def 3,XXREAL_0:2;
|.x-x0.| <=|.h.m.|
proof
per cases;
suppose x0<= x0+h.m;
then x0 = min(x0,x0+h.m) & x0+h.m = max(x0,x0+h.m)
by XXREAL_0:def 9,def 10; then
A44: ex z be Real st x=z & x0<=z & z<=x0+h.m by A43;
then
A45: |.x-x0.| = x-x0 by ABSVALUE:def 1,XREAL_1:48;
A46: x-x0 <= x0+h.m - x0 by A44,XREAL_1:9;
then 0 <= h.m by A44,XREAL_1:48;
hence thesis by A46,A45,ABSVALUE:def 1;
end;
suppose
A47: not x0<=x0 +h.m;
then x0 = max(x0,x0+h.m) & x0+h.m = min(x0,x0+h.m)
by XXREAL_0:def 9,def 10;
then
A48: ex z be Real st x=z & x0+h.m<=z & z<=x0 by A43;
then
A49: x0 +h.m -x0 <= x-x0 by XREAL_1:9;
per cases;
suppose x-x0 <> 0; then
x-x0 < 0 by A48,XREAL_1:47; then
A50: |.x-x0.| = -(x-x0) by ABSVALUE:def 1;
|.h.m.| = -(h.m) by A47,XREAL_1:31,ABSVALUE:def 1;
hence thesis by A49,A50,XREAL_1:24;
end;
suppose x-x0 = 0;
then |.x-x0.| = 0 by ABSVALUE:def 1;
hence thesis by COMPLEX1:46;
end;
end;
end; then
A52: |.x-x0.| < r by A30,XXREAL_0:2; then
x in ].x0-q,x0+q.[ by A29,RCOMP_1:1; then
A53: x in [.a,b.] by X1,A15,A24,A26;
reconsider xx = x as Element of REAL by XREAL_0:def 1;
|.x-x0.| < p/2 by A40,A52,XXREAL_0:2;
then |.x-x0.| < p by A22,XXREAL_0:2;
then ||. f/.x- f/.x0 .|| <= e by A4,A21,A53;
then ||. f/.x- g/.xx .|| <= e;
hence thesis by A15,A37,A53,VFUNCT_1:def 2;
end;
B54: now let x be Real;
assume B1:x in ['a,b'];
thus g/.x = g.x by A36,XREAL_0:def 1,PARTFUN1:def 6
.= f/.x0 by B1,FUNCOP_1:7;
end;
XX: m in NAT by ORDINAL1:def 12;
rng h c= dom R by A10;
then (h.m)"*(R/.(h.m)) =(h.m)"*(R/*h).m by FUNCT_2:109,XX;
then (h.m)"*(R/.(h.m)) =((h").m)*((R/*h).m) by VALUED_1:10;
then
A57: (h.m)"*(R/.(h.m)) = ((h")(#)(R/*h)).m by NDIFF_1:def 2;
A58: 0 < |.h.m.| by COMPLEX1:47,SEQ_1:5;
A60: ||. integral(f-g,x0,x0+h.m) .|| <= e*|.x0+h.m-x0.|
by A1,A7,X1,X2,A37,A41,INTEGR21:25;
A61: integral(g,x0,x0+h.m)=((x0+h.m)-x0)*(f/.x0)
by A1,A7,X1,X2,A36,B54,INTEGR21:28
.= (h.m)*(f/.x0);
A62: integral(f-g,x0,x0+h.m) = integral(f,x0,x0+h.m)
- integral(g,x0,x0+h.m) by A1,X5,A4,A7,X1,X2,A36,INTEGR21:30;
R.(h.m) = integral(f,x0,x0+h.m)
+ (integral(f,a,x0)-integral(f,a,x0)) -h.m*(f/.x0)
by A35,A39,RLVECT_1:28
.= integral(f,x0,x0+h.m) + Z0 -(h.m)*(f/.x0) by RLVECT_1:15
.= integral(f,x0,x0+h.m) - integral(g,x0,x0+h.m) by A61;
then R/.(h.m) =integral(f-g,x0,x0+h.m) by A62,A10,PARTFUN1:def 6;
then ||.(h.m)"*(R/.(h.m)) .|| = ||.(R/.(h.m)).|| /|.h.m.| &
||.(R/.(h.m)).|| /|.h.m.|
<= e*|.h.m.|/|.h.m.| by A60,A58,Lm17,XREAL_1:72;
then ||.(h.m)"*(R/.(h.m)).|| <= e0/2 by A58,XCMPLX_1:89;
hence thesis by A22,A57,XXREAL_0:2;
end;
hence (h")(#)(R/*h) is convergent;
hence thesis by A17,NORMSP_1:def 7;
end;
consider N be Neighbourhood of x0 such that
A64: N c= ].a,b.[ by A7,RCOMP_1:18;
reconsider R as RestFunc of X by A14,A16,NDIFF_3:def 1;
A65:for x be Real st x in N holds F/.x-F/.x0 = L/.(x-x0) + R/.(x-x0)
proof
let x be Real;
assume x in N; then
x0+In(x-x0,REAL) = x0 + (x-x0) & R.(x-x0) = F1(x-x0) by A10,A64; then
R/.(x-x0) = F/.(x0+In(x-x0,REAL))-F/.x0-L/.(In(x-x0,REAL))
by A10,PARTFUN1:def 6;
then R/.(x-x0) + L/.(x-x0) = F/.x-F/.x0 - (L/.(x-x0) - L/.(x-x0))
by RLVECT_1:29; then
R/.(x-x0) + L/.(x-x0) = F/.x-F/.x0 - 0.X by RLVECT_1:15;
hence thesis;
end;
A66:N c= dom F by A5,A64;
hence A67: F is_differentiable_in x0 by A65;
reconsider N1=1 as Real;
L/.1 = N1*(f/.x0) by C9; then
L/.1 = f/.x0 by RLVECT_1:def 8;
hence thesis by A66,A65,A67,NDIFF_3:def 4;
end;
suppose a > b;
hence thesis by A7,XXREAL_1:28;
end;
end;
theorem Th35:
for F be PartFunc of REAL,the carrier of X,
f be continuous PartFunc of REAL,the carrier of X
st dom f =[.a,b.] & dom F =[.a,b.]
& for t be Real st t in [.a,b.] holds F/.t = integral(f,a,t) holds
for x be Real st x in [.a,b.] holds F is_continuous_in x
proof
let F be PartFunc of REAL,the carrier of X;
let f be continuous PartFunc of REAL,the carrier of X;
set f1 = ||.f.||;
assume A1: dom f =[.a,b.] & dom F =[.a,b.]
& for t be Real st t in [.a,b.] holds F/.t = integral(f,a,t);
let x0 be Real;
assume A12: x0 in [.a,b.];
per cases;
suppose a > b;
hence thesis by A12,XXREAL_1:29;
end;
suppose X1: a<=b;
reconsider AB = ['a,b'] as non empty closed_interval Subset of REAL;
X2:AB = [.a,b.] by X1,INTEGRA5:def 3; then
A2:f|AB is bounded by A1,X1,INTEGR21:11;
B1:dom f = dom f1 by NORMSP_0:def 2; then
f1|AB = f1 by A1,X2; then
f1 is bounded by A1,A2,X2,INTEGR21:9; then
consider K be Real such that
A3: for y be set st y in dom f1 holds |. f1.y .| < K by COMSEQ_2:def 3;
B2:[.a,b.] = AB by X1,INTEGRA5:def 3; then
a in AB by X1; then
|. f1.a .| < K by A1,X2,B1,A3; then
A5:0 < K by COMPLEX1:46;
A6:now let c,d be Real;
assume A11: c in ['a,b'] & d in ['a,b']; then
A7: ['min(c,d),max(c,d)'] c= ['a,b'] by X1,INTEGR19:3;
now let y be Real;
assume y in ['min(c,d),max(c,d)']; then
y in ['a,b'] by A7; then
A9: y in dom f1 by X2,NORMSP_0:def 2,A1; then
|. f1.y .|< K by A3; then
|. ||.f/.y .|| .| < K by A9,NORMSP_0:def 2;
hence ||. f/.y .|| <= K by ABSVALUE:def 1;
end;
hence ||. integral(f,c,d) .|| <= K * |.d-c.| by A1,X1,X2,A11,INTEGR21:25;
end;
for r be Real st 0<r
ex s be Real st 0<s
& for x1 be Real st x1 in dom F & |.(x1-x0).|<s
holds ||. F/.x1 - F/.x0 .||<r
proof
let r be Real;
assume 0 < r; then
consider s be Real such that
A16: 0 < s & s < r/K by A5,XREAL_1:5,139;
s*K < (r/K)*K by A5,A16,XREAL_1:68; then
A17:K*s < r by A5,XCMPLX_1:87;
take s;
thus 0 < s by A16;
let x1 be Real;
assume A18: x1 in dom F & |.x1-x0.|<s; then
A20: ||.integral(f,x0,x1).|| <= K*|.x1-x0.| by A1,A12,B2,A6;
K * |.x1-x0.| <= K *s by A5,A18,XREAL_1:64; then
A21:K * |.x1-x0.| < r by A17,XXREAL_0:2;
A23:F/.x0 = integral(f,a,x0) & F/.x1 =integral(f,a,x1) by A1,A12,A18;
reconsider R1= F/.x0 as VECTOR of X;
reconsider R2= integral(f,x0,x1) as VECTOR of X;
(F/.x0 + integral(f,x0,x1)) - F/.x0
= (F/.x0 + (- F/.x0)) + integral(f,x0,x1) by RLVECT_1:def 3
.= 0.X + integral(f,x0,x1) by RLVECT_1:5
.= integral(f,x0,x1);
then ||. F/.x1 - F/.x0 .|| <= K * |.x1-x0.|
by A23,A1,X1,A12,B2,A18,INTEGR21:29,A20;
hence thesis by A21,XXREAL_0:2;
end;
hence F is_continuous_in x0 by A1,A12,NFCONT_3:8;
end;
end;
theorem Lm00:
for f be continuous PartFunc of REAL,the carrier of X
st a in dom f holds integral(f,a,a) = 0.X
proof
let f be continuous PartFunc of REAL,the carrier of X;
assume A1: a in dom f;
[.a,a.] = {a} by XXREAL_1:17; then
A2:[.a,a.] c= dom f by A1,ZFMISC_1:31;
A3:['a,a'] = [.a,a.] by INTEGRA5:def 3; then
A4:integral(f,['a,a']) = integral(f,a,a) by INTEGR18:16;
vol ['a,a'] = a-a by INTEGRA6:5;
hence thesis by A4,A2,A3,INTEGR18:17;
end;
theorem Th40a:
for f be continuous PartFunc of REAL,the carrier of X,
g be PartFunc of REAL,the carrier of X
st a <= b & dom f = [.a,b.]
& for t be Real st t in [.a,b.] holds g/.t = y0 + integral(f,a,t) holds
g/.a = y0
proof
let f be continuous PartFunc of REAL,the carrier of X,
g be PartFunc of REAL,the carrier of X;
assume that
A1:a <= b and
A2:dom f = [.a,b.] and
A6:for t be Real st t in [.a,b.] holds g/.t = y0+ integral(f,a,t);
A4:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
a in ['a,b'] by A1; then
integral(f,a,a) = 0.X & g/.a = y0 + integral(f,a,a) by A2,A6,A4,Lm00;
hence g/.a = y0;
end;
theorem Th40:
for f be continuous PartFunc of REAL,the carrier of X,
g be PartFunc of REAL,the carrier of X
st dom f = [.a,b.] & dom g = [.a,b.] & Z = ].a,b.[
& for t be Real st t in [.a,b.] holds g/.t = y0 + integral(f,a,t) holds
g is continuous & g is_differentiable_on Z
& for t be Real st t in Z holds diff(g,t) = f/.t
proof
let f be continuous PartFunc of REAL,the carrier of X,
g be PartFunc of REAL,the carrier of X;
assume that
A2: dom f = [.a,b.] and
A3: dom g = [.a,b.] and
D1: Z = ].a,b.[ and
D2: for t be Real st t in [.a,b.] holds g/.t = y0+ integral(f,a,t);
deffunc FX(Element of REAL) = integral(f,a,$1);
consider F0 be Function of REAL,the carrier of X such that
A5: for x be Element of REAL holds F0.x = FX(x) from FUNCT_2:sch 4;
set G0 = REAL --> y0;
set F = F0|[.a,b.], G = G0|[.a,b.];
dom F = dom F0 /\ [.a,b.] & dom G = dom G0 /\ [.a,b.] by RELAT_1:61; then
dom F = REAL /\ [.a,b.] & dom G = REAL /\ [.a,b.] by FUNCT_2:def 1; then
A6:dom F = [.a,b.] & dom G = [.a,b.] & dom g = dom F /\ dom G
by A3,XBOOLE_1:28;
A10:].a,b.[ c= [.a,b.] by XXREAL_1:25;
A7:for x be Real st x in [.a,b.] holds F/.x = integral(f,a,x)
proof
let x be Real;
assume x in [.a,b.]; then
A8: F/.x = F.x & F.x = F0.x by A6,PARTFUN1:def 6,FUNCT_1:47;
x in REAL by XREAL_0:def 1;
hence F/.x = integral(f,a,x) by A5,A8;
end; then
A12:for x be Real st
x in ].a,b.[ holds F/.x = integral(f,a,x) by A10;
A14:now let x be Real;
assume A15: x in Z;
then f is_continuous_in x by A10,A2,D1,NFCONT_3:def 2;
hence F is_differentiable_in x & diff(F,x)=f/.x
by A15,A2,D1,A12,A10,A6,Th1955;
end;
then for x be Real st x in Z holds F is_differentiable_in x;
then
A16:F is_differentiable_on Z by D1,A6,XXREAL_1:25,NDIFF_3:10;
A18:now let x be Real;
assume A19: x in [.a,b.]; then
G/.x = G.x by A6,PARTFUN1:def 6; then
G/.x = G0.x by A19,A6,FUNCT_1:47;
hence G/.x = y0 by XREAL_0:def 1,FUNCOP_1:7;
end;
G|Z is constant; then
A23: G is_differentiable_on Z & for x be Real st x in Z holds (G`|Z).x = 0.X
by A6,D1,A10,NDIFF_3:20;
now let x be Element of REAL;
assume A25: x in dom g; then
G/.x = y0 & F/.x = integral(f,a,x) by A3,A7,A18;
hence g/.x = G/.x + F/.x by A3,D2,A25;
end; then
A29: g = G + F by A6,VFUNCT_1:def 1;
F is continuous by A6,A7,Th35,A2;
hence g is continuous by A29;
thus B1: g is_differentiable_on Z
by A29,A16,A23,A3,D1,A10,NDIFF_3:17;
thus for t be Real st t in Z holds diff(g,t) = f/.t
proof
let t be Real;
assume A33: t in Z; then
diff(g,t) = (g`|Z).t & (g`|Z).t = diff(G,t) + diff(F,t)
& diff(G,t) = (G`|Z).t & (G`|Z).t = 0.X by A23,B1,A29,A16,NDIFF_3:17,def 6;
hence diff(g,t) = f/.t by A14,A33;
end;
end;
theorem Th45a:
for f be PartFunc of REAL,the carrier of X
st a <= b & [.a,b.] c= dom f
& (for x be Real st x in [.a,b.] holds f is_continuous_in x)
& f is_differentiable_on ].a,b.[
& for x be Real st x in ].a,b.[ holds diff(f,x) = 0.X holds
f/.b = f/.a
proof
let f be PartFunc of REAL,the carrier of X;
assume that
A1: a <= b & [.a,b.] c= dom f
& for x be Real st x in [.a,b.] holds f is_continuous_in x and
A2: f is_differentiable_on ].a,b.[ and
A3: for x be Real st x in ].a,b.[ holds diff(f,x) = 0.X;
A5:for x be Real st x in ].a,b.[ holds f is_differentiable_in x
by A2,NDIFF_3:10;
now let x be Real;
assume x in ].a,b.[; then
||.diff(f,x).|| = ||. 0.X .|| by A3;
hence ||.diff(f,x).|| <= 0;
end; then
||. f/.b - f/.a .|| <= 0*|.b-a.| by A5,Th519,A1; then
||. f/.b - f/.a .|| = 0;
hence f/.b = f/.a by NORMSP_1:6;
end;
theorem Th45:
for f be PartFunc of REAL,the carrier of X
st [.a,b.] c= dom f
& (for x be Real st x in [.a,b.] holds f is_continuous_in x)
& f is_differentiable_on ].a,b.[
& for x be Real st x in ].a,b.[ holds diff(f,x) = 0.X holds
f|(].a,b.[) is constant
proof
let f be PartFunc of REAL,the carrier of X;
assume that
A1: [.a,b.] c= dom f
& for x be Real st x in [.a,b.] holds f is_continuous_in x and
A2: f is_differentiable_on ].a,b.[
& for x be Real st x in ].a,b.[ holds diff(f,x) = 0.X;
now let x1,x2 be Element of REAL;
assume x1 in ].a,b.[ /\ dom f & x2 in ].a,b.[ /\ dom f; then
A4: x1 in ].a,b.[ & x2 in ].a,b.[ by XBOOLE_0:def 4;
reconsider Z1=].x1,x2.[, Z2=].x2,x1.[ as open Subset of REAL;
A7: ].a,b.[ c= [.a,b.] & Z1 c= [.x1,x2.] & Z2 c= [.x2,x1.] by XXREAL_1:25; then
[.x1,x2.] c= [.a,b.] & [.x2,x1.] c= [.a,b.] by A4,XXREAL_2:def 12; then
C1: [.x1,x2.] c= dom f & [.x2,x1.] c= dom f
& (for x be Real st x in [.x1,x2.] holds f is_continuous_in x)
& (for x be Real st x in [.x2,x1.] holds f is_continuous_in x) by A1;
[.x1,x2.] c= ].a,b.[ & [.x2,x1.] c= ].a,b.[ by A4,XXREAL_2:def 12; then
(f is_differentiable_on Z1 &
for x be Real st x in Z1 holds diff(f,x) = 0.X)
& (f is_differentiable_on Z2 &
for x be Real st x in Z2 holds diff(f,x) = 0.X)
by A2,A7,NDIFF_3:24,XBOOLE_1:1; then
(x1 < x2 implies f/.x1 = f/.x2) & (x2 < x1 implies f/.x1 = f/.x2)
by C1,Th45a;
hence f/.x1 = f/.x2 by XXREAL_0:1;
end;
hence f| (].a,b.[) is constant by PARTFUN2:36;
end;
theorem Th46:
for f be continuous PartFunc of REAL,the carrier of X
st [.a,b.] = dom f & f | ].a,b.[ is constant holds
for x be Real st x in [.a,b.] holds f/.x = f/.a
proof
let f be continuous PartFunc of REAL,the carrier of X;
assume A1: [.a,b.] = dom f & f| (].a,b.[) is constant;
A2:].a,b.[ c= [.a,b.] by XXREAL_1:25;
per cases;
suppose X0: a >= b;
hereby let x be Real;
assume x in [.a,b.]; then
a <= x & x <= b by XXREAL_1:1; then
a <= x & x <= a by X0,XXREAL_0:2;
hence f/.x = f/.a by XXREAL_0:1;
end;
end;
suppose A0: a < b;
reconsider d = (b-a)/2 as Real;
A3: 0 < b-a by A0,XREAL_1:50; then
A4: 0 < d by XREAL_1:215;
a+(b-a)/2 = (a+b) / 2; then
A5: a < a+d & a+d < b by A0,XREAL_1:226; then
a+d in ].a,b.[; then
f.(a+d) in rng f by A2,A1,FUNCT_1:3; then
reconsider f0=f.(a+d) as Point of X;
dom (f| (].a,b.[) ) = dom f /\ (].a,b.[) by RELAT_1:61; then
A6: dom (f| (].a,b.[) ) = ].a,b.[ by A1,XXREAL_1:25,XBOOLE_1:28;
A7: now let x be Real;
assume A8: x in ].a,b.[;
A9: a+d in dom (f| (].a,b.[) ) by A5,A6;
thus f/.x = f.x by A8,A2,A1,PARTFUN1:def 6
.= (f| (].a,b.[) ).x by A6,A8,FUNCT_1:47
.= (f| (].a,b.[) ).(a+d) by A1,A6,A8,A9,FUNCT_1:def 10
.=f0 by A9,FUNCT_1:47;
end;
a in dom f & b in dom f by A1,A0; then
A14:f is_continuous_in a & f is_continuous_in b by NFCONT_3:def 2;
deffunc F1(Nat) = a+d/($1+1);
A12:for x being Element of NAT holds F1(x) is Element of REAL by XREAL_0:def 1;
consider s1 be Real_Sequence such that
A13: for x being Element of NAT holds s1.x = F1(x) from FUNCT_2:sch 9(A12);
A15:now let y be object;
assume y in rng s1; then
consider x be object such that
A16: x in dom s1 & y=s1.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A16;
A17: y = a+d/(x+1) by A13,A16;
0 < d/(x+1) by A4,XREAL_1:139; then
A20: a + (0 qua Real) < a + d/(x+1) by XREAL_1:8;
1 + (0 qua Real) <= 1 + x by XREAL_1:7; then
d/(x+1) <= d / 1 by XREAL_1:118,A3; then
a + d/(x+1) <= a + d by XREAL_1:7; then
a + d/(x+1) < b by A5,XXREAL_0:2;
hence y in ].a,b.[ by A17,A20;
end; then
A21:rng s1 c= ].a,b.[ & rng s1 c= dom f by A2,A1;
A23:now let p be Real;
assume A24: 0<p;
consider n be Nat such that
A25: d/p < n by SEQ_4:3;
n + (0 qua Real) < n + 1 by XREAL_1:8; then
d/p < n + 1 by XXREAL_0:2,A25; then
(d/p)*p < (n + 1)*p by A24,XREAL_1:68; then
d < (n + 1)*p by A24,XCMPLX_1:87; then
d/(n+1) < p by XREAL_1:83; then
A29: |.(d/(n+1)).| < p by A3,ABSVALUE:def 1;
A28: |.(d/(n+1)).| = d/(n+1) by A3,ABSVALUE:def 1;
take n;
thus for m be Nat st n<=m holds |.(s1.m-a).| < p
proof
let m be Nat;
K: m in NAT by ORDINAL1:def 12;
assume n<=m; then
n+1 <= m+1 by XREAL_1:7; then
d/(m+1) <= d/(n+1) by A3,XREAL_1:118; then
A31: |.(d/(m+1)).| <= |.(d/(n+1)).| by A28,A3,ABSVALUE:def 1;
|.(s1.m-a).| = |.(a+d/(m+1) -a ).| by A13,K;
hence |.(s1.m-a).| < p by A31,A29,XXREAL_0:2;
end;
end; then
A32:s1 is convergent by SEQ_2:def 6; then
lim s1 = a by A23,SEQ_2:def 7; then
A34:f/*s1 is convergent & f/.a = lim (f/*s1) by A14,A21,A32;
A35:for i be Nat holds (f/*s1).i = f0
proof
let i be Nat;
S: i in NAT by ORDINAL1:def 12;
A36: s1.i in rng s1 by FUNCT_2:4,ORDINAL1:def 12;
thus (f/*s1).i = f/.(s1.i) by A21,FUNCT_2:109,S
.= f0 by A7,A36,A15;
end;
now let r be Real;
assume A37: 0 < r;
reconsider m = the Element of NAT as Nat;
take m;
thus for k be Nat st m <= k holds ||.(f/*s1).k - f0.|| < r
proof
let k be Nat;
assume m <= k;
||.(f/*s1).k - f0.|| = ||.f0 - f0.|| by A35
.= ||. 0.X .|| by RLVECT_1:15;
hence thesis by A37;
end;
end; then
A38:f/.a = f0 by A34,NORMSP_1:def 7;
deffunc F2(Nat) = b-d/($1+1);
A39:for x being Element of NAT holds F2(x) is Element of REAL by XREAL_0:def 1;
consider s2 be Real_Sequence such that
A40: for x being Element of NAT holds s2.x = F2(x) from FUNCT_2:sch 9(A39);
A42:now let y be object;
assume y in rng s2; then
consider x be object such that
A43: x in dom s2 & y=s2.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A43;
A44: y = b-d/(x+1) by A40,A43;
0 < d/(x+1) by A4,XREAL_1:139; then
A47: b - d/(x+1) < b - (0 qua Real) by XREAL_1:15;
1 + (0 qua Real) <= 1 + x by XREAL_1:7; then
d/(x+1) <= d / 1 by XREAL_1:118,A3; then
b - d <= b - d/(x+1) by XREAL_1:13; then
a < b - d/(x+1) by A5,XXREAL_0:2;
hence y in ].a,b.[ by A44,A47;
end; then
A48:rng s2 c= ].a,b.[ & rng s2 c= dom f by A2,A1;
A50:now let p be Real;
assume A51: 0<p;
consider n be Nat such that
A52: d/p < n by SEQ_4:3;
n + (0 qua Real) < n + 1 by XREAL_1:8; then
d/p < n + 1 by XXREAL_0:2,A52; then
(d/p)*p < (n + 1)*p by A51,XREAL_1:68; then
d < (n + 1)*p by A51,XCMPLX_1:87; then
A54: d/(n+1) < p by XREAL_1:83;
take n;
thus for m be Nat st n<=m holds |.(s2.m-b).| < p
proof
let m be Nat;
K: m in NAT by ORDINAL1:def 12;
assume n<=m; then
n+1 <= m+1 by XREAL_1:7; then
d/(m+1) <= d/(n+1) by A3,XREAL_1:118; then
A57: |.d/(m+1).|<= d/(n+1) by A3,ABSVALUE:def 1;
|.(s2.m-b).| = |.(b-d/(m+1) -b ).| by A40,K
.= |.(d/(m+1)).| by COMPLEX1:52;
hence |.(s2.m-b).| < p by A57,XXREAL_0:2,A54;
end;
end; then
A58:s2 is convergent by SEQ_2:def 6; then
lim s2 = b by A50,SEQ_2:def 7; then
A60:f/*s2 is convergent & f/.b = lim (f/*s2) by A14,A48,A58;
A61:for i be Element of NAT holds (f/*s2).i = f0
proof
let i be Element of NAT;
s2.i in rng s2 by FUNCT_2:4; then
f/.(s2.i) = f0 by A7,A42;
hence (f/*s2).i = f0 by A48,FUNCT_2:109;
end;
now let r be Real;
assume A63: 0 < r;
reconsider m = the Element of NAT as Nat;
take m;
thus for k be Nat st m <= k holds ||.(f/*s2).k - f0.|| < r
proof
let k be Nat;
assume m <= k;
k in NAT by ORDINAL1:def 12; then
||.(f/*s2).k - f0.|| = ||.f0 - f0.|| by A61
.= ||. 0.X .|| by RLVECT_1:15
.= 0;
hence thesis by A63;
end;
end; then
A64:f/.b = f0 by A60,NORMSP_1:def 7;
let x be Real;
assume x in [.a,b.]; then
A65:ex r be Real st x=r & a <=r & r <= b;
per cases;
suppose x in ].a,b.[;
hence f/.x = f/.a by A38,A7;
end;
suppose not x in ].a,b.[; then
x <=a or b <= x;
hence f/.x =f/.a by A38,A64,A65,XXREAL_0:1;
end;
end;
end;
theorem Th47:
for y,Gf be continuous PartFunc of REAL,the carrier of X,
g be PartFunc of REAL,the carrier of X
st a <= b & Z = ].a,b.[
& dom y = [.a,b.] & dom g = [.a,b.] & dom Gf = [.a,b.]
& y is_differentiable_on Z
& y/.a = y0
& (for t be Real st t in Z holds diff(y,t) = Gf/.t)
& (for t be Real st t in [.a,b.] holds g/.t = y0 + integral(Gf,a,t) )
holds y=g
proof
let y,Gf be continuous PartFunc of REAL,the carrier of X,
g be PartFunc of REAL,the carrier of X;
assume A1: a <= b & Z = ].a,b.[
& dom y = [.a,b.] & dom g =[.a,b.] & dom Gf =[.a,b.]
& y is_differentiable_on Z
& y/.a = y0
& (for t be Real st t in Z holds diff(y,t) = Gf/.t)
& (for t be Real st t in [.a,b.] holds g/.t = y0+ integral(Gf,a,t));
then
A2:g is continuous & g/.a=y0 &
g is_differentiable_on Z
& for t be Real st t in Z holds diff(g,t) = Gf/.t by Th40,Th40a;
reconsider h=y-g as continuous PartFunc of REAL,the carrier of X by A2;
A5:dom h = [.a,b.] /\ [.a,b.] by A1,VFUNCT_1:def 2; then
A7:h is_differentiable_on ].a,b.[ by A1,A2,NDIFF_3:18;
A8:now let x be Real;
assume A9: x in ].a,b.[; then
A10:diff(y,x) = Gf/.x & diff(g,x) = Gf/.x by A1,Th40;
thus diff(h,x) = ((y-g)`|(].a,b.[)).x by A9,A7,NDIFF_3:def 6
.= Gf/.x - Gf/.x by A10,A1,A2,A5,A9,NDIFF_3:18
.= 0.X by RLVECT_1:15;
end;
for x be Real st x in [.a,b.] holds h is_continuous_in x
by A5,NFCONT_3:def 2; then
A12:
h|(].a,b.[) is constant by A1,Th45,A5,A2,NDIFF_3:18,A8;
A13:for x being Real st x in dom h holds h/.x = 0.X
proof
let x be Real;
assume A14: x in dom h;
A15:a in dom h by A5,A1;
thus h/.x = h/.a by A14,Th46,A12,A5
.= y0-y0 by A2,A1,A15,VFUNCT_1:def 2
.= 0.X by RLVECT_1:15;
end;
for x being Element of REAL st x in dom y holds y.x = g.x
proof
let x be Element of REAL;
assume A16: x in dom y; then
0.X = h/.x by A13,A1,A5
.= y/.x -g/.x by A16,A1,A5,VFUNCT_1:def 2; then
A17:y/.x = g/.x by RLVECT_1:21;
thus y.x = y/.x by A16,PARTFUN1:def 6
.= g.x by A17,A16,A1,PARTFUN1:def 6;
end;
hence thesis by A1,PARTFUN1:5;
end;
Lm4:
for n be Nat for a,r,L be Real, g be Function of REAL,REAL
st for x be Real holds
g.x = ( (r*(x-a))|^(n+1) )/ ((n+1)!) * L holds
for x be Real holds
g is_differentiable_in x
& diff(g,x) = r*(((r*(x-a))|^n)/(n!) * L)
proof
let n be Nat, a,r,L be Real, g be Function of REAL,REAL;
assume A1: for x be Real holds g.x = ( (r*(x-a))|^(n+1) )/((n+1)!) * L;
A2:dom g = REAL by FUNCT_2:def 1;
deffunc F(Real) = In((($1-a)|^(n+1)) / ((n+1) !),REAL);
consider f be Function of REAL,REAL such that
A3: for x be Element of REAL holds f.x = F(x) from FUNCT_2:sch 4;
a3:for x be Real holds f.x = ((x-a) |^ (n+1)) / ((n+1) !)
proof
let x be Real; x in REAL by XREAL_0:def 1; then
f.x = F(x) by A3;
hence thesis;
end;
A5:dom ((r|^(n+1)*L)(#)f) = REAL by FUNCT_2:def 1;
now let x be Element of REAL;
assume x in dom ((r|^(n+1)*L)(#)f);
hence ((r|^(n+1)*L)(#)f).x = ((r|^(n+1)*L))* f.x by VALUED_1:def 5
.= (r|^(n+1)*L)*(((x-a)|^(n+1))/((n+1)!)) by a3
.= (((r|^(n+1))*((x-a)|^(n+1)))/((n+1)!)) *L
.= (((r*(x-a))|^(n+1))/((n+1)!)) * L by NEWTON:7
.= g.x by A1;
end; then
A6:(r|^(n+1) * L)(#)f = g by PARTFUN1:5,A2,A5;
for x be Real holds (r|^(n+1)*L)(#)f is_differentiable_in x
& diff((r|^(n+1)*L)(#)f,x) = r*(((r*(x-a))|^n)/(n!) * L)
proof
let x be Real;
A8: f is_differentiable_in x & diff(f,x) = ((x-a)|^n)/(n!)
by ORDEQ_01:47,a3;
hence (r|^(n+1) * L)(#)f is_differentiable_in x by FDIFF_1:15;
thus diff((r|^(n+1) * L)(#)f,x) = (r|^(n+1) * L) * diff(f,x)
by A8,FDIFF_1:15
.= ((r|^(n+1)) * ((x-a)|^n)) / (n!) * L by A8
.= ((r * r|^n) * ((x-a)|^n)) / (n!) * L by NEWTON:6
.= (r * ((r|^n) * ((x-a)|^n))) / (n!) * L
.= ( r * ( (r*(x-a))|^n ) ) / (n!) * L by NEWTON:7
.= r*( ( (r*(x-a))|^n )/ (n!) * L );
end;
hence thesis by A6;
end;
Lm5:
for m be non zero Element of NAT, a,r,L be Real,
g be Function of REAL,REAL
st ( for x be Real holds g.x = r*(((r*(x-a))|^m)/(m!)*L) )
holds for x be Real holds g is_differentiable_in x
proof
let m be non zero Element of NAT,
a,r,L be Real, g be Function of REAL,REAL;
assume A1: for x be Real holds g.x = r*( ( (r*(x-a))|^m)/ (m!) * L );
A2:dom g = REAL by FUNCT_2:def 1;
reconsider n = m-1 as Element of NAT by ORDINAL1:def 12;
deffunc F(Real) = In((($1-a)|^(n+1))/((n+1)!),REAL);
consider f be Function of REAL,REAL such that
A3: for x be Element of REAL holds f.x = F(x) from FUNCT_2:sch 4;
a3:for x be Real holds f.x = ((x-a)|^(n+1))/((n+1)!)
proof
let x be Real;
x in REAL by XREAL_0:def 1; then
f.x = F(x) by A3;
hence thesis;
end;
A5:dom ((r|^(n+2) * L)(#)f) = REAL by FUNCT_2:def 1;
A6:now let x be Element of REAL;
assume x in dom ((r|^(n+2) * L)(#)f);
hence ((r|^(n+2) * L)(#)f).x = ((r|^(n+2) * L))* f.x by VALUED_1:def 5
.= (r|^(n+2) * L)*( ((x-a)|^(n+1)) / ((n+1)!) ) by a3
.= (r|^(n+1+1))*( ((x-a)|^(n+1)) / ((n+1) !) ) *L
.= (r * r|^(n+1))*( ((x-a)|^(n+1)) / ((n+1)!) ) *L by NEWTON:6
.= r * ( ((r|^(n+1)) * ((x-a)|^(n+1)) ) / ((n+1)!) ) *L
.= r * ( ((r*(x-a))|^(n+1)) / ((n+1)!) ) * L by NEWTON:7
.= r * ( ((r*(x-a))|^m)/ (m!) * L )
.= g.x by A1;
end;
A7:for x be Real holds (r|^(n+2) * L)(#)f is_differentiable_in x
proof
let x be Real;
f is_differentiable_in x by ORDEQ_01:47,a3;
hence (r|^(n+2) * L)(#)f is_differentiable_in x by FDIFF_1:15;
end;
(r|^(n+2) * L)(#)f = g by A6,A2,A5,PARTFUN1:5;
hence thesis by A7;
end;
Lm6:
for n be non zero Element of NAT, a,r,t,L be Real,
f0 be Function of REAL,REAL
st a <= t
& for x be Real holds f0.x = r*(((r*(x-a))|^n)/(n!) * L)
holds f0|[.a,t.] is continuous & f0|[.a,t.] is bounded
& f0 is_integrable_on ['a,t']
& integral(f0,a,t) = ( (r*(t-a))|^(n+1) ) / ((n+1)!) * L
proof
let n be non zero Element of NAT;
let a,r,t,L be Real, f0 be Function of REAL,REAL;
S: a in REAL by XREAL_0:def 1;
assume A1: a <= t;
assume A2: for x be Real holds f0.x = r*(((r*(x-a))|^n)/(n!) * L);
A5:dom f0 = REAL by FUNCT_2:def 1;
for x be Real st x in dom f0
holds f0 is_continuous_in x by A2,Lm5,FDIFF_1:24; then
reconsider f0 as continuous PartFunc of REAL,REAL by FCONT_1:def 2;
deffunc F(Real) = In(( (r*($1-a))|^(n+1))/ ((n+1)!) * L,REAL);
consider g be Function of REAL,REAL such that
A6: for x be Element of REAL holds g.x = F(x) from FUNCT_2:sch 4;
a6:for x be Real holds g.x = ((r*(x-a))|^(n+1)) / ((n+1)!) * L
proof
let x be Real;
x in REAL by XREAL_0:def 1; then
g.x = In(((r*(x-a))|^(n+1)) / ((n+1)!) * L,REAL) by A6;
hence thesis;
end; then
A8:g is_differentiable_on REAL by Lm4,FUNCT_2:def 1;
A9:now let x be Element of REAL;
assume x in dom (g`| [#]REAL);
thus (g`| [#]REAL).x = diff(g,x) by A8,FDIFF_1:def 7
.= r*(((r*(x-a))|^n)/(n!) * L) by Lm4,a6
.= (f0 | [#]REAL).x by A2;
end;
dom (g`|[#]REAL) = [#]REAL by A8,FDIFF_1:def 7
.= dom (f0 | [#]REAL) by FUNCT_2:def 1; then
g`| [#]REAL = f0 | [#]REAL by A9,PARTFUN1:5; then
g in IntegralFuncs(f0,[#]REAL) by A8,INTEGRA7:def 1; then
A10: g is_integral_of f0,[#]REAL by INTEGRA7:def 2;
A11: f0|['a,t'] is bounded by INTEGRA5:10,A5;
A12: g.t = integral(f0,a,t) + g.a by A1,INTEGRA7:18,A5,INTEGRA5:11,A11,A10;
A13: (0 qua Real) + 1 <= n +1 by XREAL_1:6;
g.a = In(( (r*(a-a))|^(n+1))/((n+1)!) * L,REAL) by A6,S
.= (0 qua Real)/ ((n+1)!) * L by A13,NEWTON:11
.= (0 qua Real);
hence thesis by A11,A12,A5,INTEGRA5:11,a6,A1,INTEGRA5:def 3;
end;
Lm7:
for a,t,L,r be Real, k be non zero Element of NAT
st a <= t
ex rg be PartFunc of REAL,REAL
st dom rg = [.a,t.]
& (for x be Real st x in [.a,t.] holds
rg.x =r*( ( (r*(x-a))|^k)/ (k!) * L) )
& rg is continuous & rg is_integrable_on ['a,t']
& rg|[.a,t.] is bounded
& integral(rg,a,t) = ( (r*(t-a))|^(k+1) ) /((k+1)!) * L
proof
let a,t,L,r be Real, k be non zero Element of NAT;
assume A1: a <= t; then
X1:['a,t'] = [.a,t.] by INTEGRA5:def 3;
deffunc F(Real) = In(r*(((r*($1-a))|^k)/(k!) * L),REAL);
consider f0 be Function of REAL,REAL such that
A2: for x be Element of REAL holds f0.x = F(x) from FUNCT_2:sch 4;
a2:for x be Real holds f0.x = r*( ((r*(x-a))|^k)/(k!)*L )
proof
let x be Real; x in REAL by XREAL_0:def 1; then
f0.x = In(r*( ( (r*(x-a))|^k )/ (k!) * L ),REAL) by A2;
hence thesis;
end;
A3:dom f0 = REAL by FUNCT_2:def 1;
A4:f0|[.a,t.] is continuous & f0|[.a,t.] is bounded
& f0 is_integrable_on ['a,t']
& integral(f0,a,t) = ((r*(t-a))|^(k+1)) / ((k+1)!) * L by Lm6,A1,a2;
set f = f0|[.a,t.];
reconsider f as continuous PartFunc of REAL,REAL by Lm6,A1,a2;
A7:now let x be Real;
assume A8: x in [.a,t.];
A9: x in REAL by XREAL_0:def 1;
thus f.x = f0.x by A8,FUNCT_1:49
.= In(r*( ( (r*(x-a))|^k )/ (k!) * L ),REAL) by A2,A9
.= r*( ( (r*(x-a))|^k )/ (k!) * L );
end;
A10:
integral(f0,a,t) = integral(f0,['a,t'])
& integral(f,a,t) = integral(f,['a,t']) by INTEGRA5:def 4,A1;
take f;
thus thesis by A7,A10,A4,A3,X1,RELAT_1:62;
end;
definition
let X be RealBanachSpace;
let y0 be VECTOR of X,
G be Function of X,X,
a,b be Real;
assume A1: a<=b & G is_continuous_on dom G;
func Fredholm(G,a,b,y0) -> Function of
R_NormSpace_of_ContinuousFunctions(['a,b'],X),
R_NormSpace_of_ContinuousFunctions(['a,b'],X) means
:Def8:
for x be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X)
ex f,g,Gf be continuous PartFunc of REAL,the carrier of X
st x=f & it.x = g & dom f =['a,b'] & dom g =['a,b'] & Gf = G*f
& for t be Real st t in ['a,b'] holds g/.t = y0 + integral(Gf,a,t);
existence
proof
defpred P[set,set] means
ex f,g,Gf be continuous PartFunc of REAL,the carrier of X
st $1=f & $2=g & dom f =['a,b'] & dom g =['a,b'] & Gf=G*f
& for t be Real st t in ['a,b'] holds g/.t = y0+ integral(Gf,a,t);
set D = the carrier of R_NormSpace_of_ContinuousFunctions(['a,b'],X);
X1:the carrier of X = dom G by FUNCT_2:def 1;
A2:for x being Element of D ex y being Element of D st P[x,y]
proof
let x be Element of D;
consider f0 be continuous PartFunc of REAL,the carrier of X such that
A3: x=f0 & dom f0 = ['a,b'] by ORDEQ_01:def 2;
now let x0 be Real;
assume A4: x0 in dom(G*f0); then
f0 is_continuous_in x0 by NFCONT_3:def 2,FUNCT_1:11;
hence G*f0 is_continuous_in x0 by A4,X1,NFCONT_3:15,A1;
end; then
reconsider Gf = G*f0 as continuous PartFunc of REAL,the carrier of X
by NFCONT_3:def 2;
rng f0 c= dom G by X1; then
A6: dom Gf = ['a,b'] by A3,RELAT_1:27;
A7: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
deffunc FX(Element of REAL) = integral(Gf,a,$1);
consider F0 be Function of REAL,the carrier of X such that
A8: for x be Element of REAL holds F0.x = FX(x) from FUNCT_2:sch 4;
set F = F0|['a,b'];
dom F0 = REAL by FUNCT_2:def 1; then
A9: dom F = ['a,b'] by RELAT_1:62;
A10:now let t be Real;
assume A11: t in [.a,b.];
A12: t in REAL by XREAL_0:def 1;
thus F/.t = F.t by A7,A9,A11,PARTFUN1:def 6
.= F0.t by A11,A9,A7,FUNCT_1:47
.= integral(Gf,a,t) by A8,A12;
end;
set G0 = REAL --> y0;
set G1 = G0| ['a,b'];
dom G0 = REAL; then
A14:dom G1 = ['a,b'] by RELAT_1:62;
A15:now let t be Real;
assume A16: t in [.a,b.];
hence G1/.t = G1.t by A7,A14,PARTFUN1:def 6
.= G0.t by A16,A14,A7,FUNCT_1:47
.= y0 by XREAL_0:def 1,FUNCOP_1:7;
end;
set g=G1+F;
A19:dom g = dom F /\ dom G1 by VFUNCT_1:def 1
.= ['a,b'] by A9,A14;
F is continuous by A7,A9,Th35,A6,A10; then
reconsider g as continuous PartFunc of REAL,the carrier of X;
reconsider y=g as Element of D by A19,ORDEQ_01:def 2;
take y;
now let t be Real;
assume A20:t in ['a,b']; then
G1/.t = y0 & F/.t = integral(Gf,a,t) by A7,A10,A15;
hence g/.t = y0 + integral(Gf,a,t) by A19,A20,VFUNCT_1:def 1;
end;
hence thesis by A19,A3;
end;
consider F being Function of D,D such that
A23:for x being Element of D holds P[x,F.x] from FUNCT_2:sch 3 (A2);
take F;
thus thesis by A23;
end;
uniqueness
proof
let F1,F2 be Function of
R_NormSpace_of_ContinuousFunctions(['a,b'],X),
R_NormSpace_of_ContinuousFunctions(['a,b'],X);
assume
A24:for x be VECTOR of
R_NormSpace_of_ContinuousFunctions(['a,b'],X) holds
ex f,g,Gf be continuous PartFunc of REAL,the carrier of X
st x=f & F1.x = g & dom f =['a,b'] & dom g =['a,b'] & Gf = G*f
& for t be Real st t in ['a,b']
holds g/.t = y0+ integral(Gf,a,t);
assume
A25:for x be VECTOR of
R_NormSpace_of_ContinuousFunctions(['a,b'],X) holds
ex f,g,Gf be continuous PartFunc of REAL,the carrier of X
st x=f & F2.x = g & dom f =['a,b'] & dom g =['a,b'] & Gf = G*f
& for t be Real st t in ['a,b']
holds g/.t = y0+ integral(Gf,a,t);
now let x be Element of
R_NormSpace_of_ContinuousFunctions(['a,b'],X);
consider f1,g1,Gf1 be continuous PartFunc of REAL,the carrier of X
such that
A26: x=f1 & F1.x = g1 & dom f1 =['a,b'] & dom g1 =['a,b'] & Gf1 = G*f1
& for t be Real st t in ['a,b']
holds g1/.t = y0+ integral(Gf1,a,t) by A24;
consider f2,g2,Gf2 be continuous PartFunc of REAL,the carrier of X
such that
A27: x=f2 & F2.x = g2 & dom f2 =['a,b'] & dom g2 =['a,b'] & Gf2 = G*f2
& for t be Real st t in ['a,b']
holds g2/.t = y0+ integral(Gf2,a,t) by A25;
now let t be object;
assume A28: t in dom g1; then
reconsider t0=t as Real;
A29: g1/.t = y0+ integral(Gf2,a,t0) by A27,A28,A26
.= g2/.t by A28,A27,A26;
thus g1.t = g1/.t by A28,PARTFUN1:def 6
.= g2.t by A26,A27,A28,A29,PARTFUN1:def 6;
end;
hence F1.x = F2.x by A26,A27,FUNCT_1:2;
end;
hence F1=F2 by FUNCT_2:def 8;
end;
end;
theorem Th53:
a <= b & 0 < r &
(for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
implies
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X),
g,h be continuous PartFunc of REAL,the carrier of X
st g= Fredholm(G,a,b,y0).u & h= Fredholm(G,a,b,y0).v holds
for t be Real st t in ['a,b'] holds
||. g/.t - h/.t .|| <= r*(t-a)*||.u-v.||
proof
assume A1: a<=b & 0 < r
& for y1, y2 be VECTOR of X holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||;
A2:dom G = the carrier of X by FUNCT_2:def 1;
for x1,x2 be Point of X
st x1 in (the carrier of X) & x2 in (the carrier of X)
holds ||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A1; then
G is_Lipschitzian_on the carrier of X by A1,FUNCT_2:def 1; then
A3:G is_continuous_on dom G by A2,NFCONT_1:45;
let u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X),
g,h be continuous PartFunc of REAL,the carrier of X;
assume A4: g= Fredholm(G,a,b,y0).u & h= Fredholm(G,a,b,y0).v;
set F= Fredholm(G,a,b,y0);
consider f1,g1,Gf1 be continuous PartFunc of REAL,the carrier of X
such that
A5: u=f1 & F.u = g1 & dom f1 =['a,b'] & dom g1 =['a,b'] & Gf1 = G*f1
& for t be Real st t in ['a,b']
holds g1/.t = y0+ integral(Gf1,a,t) by Def8,A1,A3;
consider f2,g2,Gf2 be continuous PartFunc of REAL,the carrier of X
such that
A6: v=f2 & F.v = g2 & dom f2 =['a,b'] & dom g2 =['a,b'] & Gf2 = G*f2
& for t be Real st t in ['a,b']
holds g2/.t = y0+ integral(Gf2,a,t) by Def8,A1,A3;
set Gf12= Gf1 - Gf2;
dom G = the carrier of X by FUNCT_2:def 1; then
rng f1 c= dom G & rng f2 c= dom G; then
A8:dom Gf1 =['a,b'] & dom Gf2 =['a,b'] by A5,A6,RELAT_1:27;
reconsider Gf12 as continuous PartFunc of REAL,the carrier of X;
A10:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
A18:a in ['a,b'] by A1;
let t be Real;
assume A11: t in ['a,b']; then
A12:ex g be Real st t=g & a<=g & g <= b by A10; then
A20:['a,t'] c= ['a,b'] by INTEGR19:1;
X1:['a,t'] = [.a,t.] by A12,INTEGRA5:def 3;
A13:dom Gf12 = dom Gf1 /\ dom Gf2 by VFUNCT_1:def 2;
for x be Real st x in ['a,t'] holds ||. Gf12/.x .|| <= r*||.u-v.||
proof
let x be Real;
assume A19: x in ['a,t']; then
A21:Gf12/.x =Gf1/.x -Gf2/.x by A8,A13,A20,VFUNCT_1:def 2;
A24:r*||.(f1/.x)-(f2/.x).|| <=r*||.u-v.||
by A1,XREAL_1:64,A19,A20,A5,A6,ORDEQ_01:26;
A22:Gf1/.x = (Gf1).x by A8,A20,A19,PARTFUN1:def 6
.= G.(f1.x) by A20,A19,A8,A5,FUNCT_1:12
.= G/.(f1/.x) by A20,A19,A5,PARTFUN1:def 6;
Gf2/.x = (Gf2).x by A8,A20,A19,PARTFUN1:def 6
.= G.(f2.x) by A20,A19,A8,A6,FUNCT_1:12
.= G/.(f2/.x) by A20,A19,A6,PARTFUN1:def 6; then
||. Gf1/.x -Gf2/.x .||<=r*||.(f1/.x)-(f2/.x).|| by A22,A1;
hence thesis by A21,A24,XXREAL_0:2;
end; then
A25: ||. integral(Gf12,a,t) .||<= r*||.u-v.||*(t-a)
by Lm14a,X1,A8,A13,A18,A10,A11,A12;
g/.t = y0 + integral(Gf1,a,t) & h/.t = y0 + integral(Gf2,a,t)
by A4,A5,A6,A11; then
g/.t - h/.t
= (y0+ integral(Gf1,a,t) - y0 ) -integral(Gf2,a,t) by RLVECT_1:27
.= integral(Gf1,a,t) + (y0 - y0) -integral(Gf2,a,t) by RLVECT_1:28
.= integral(Gf1,a,t) + 0.X -integral(Gf2,a,t) by RLVECT_1:15
.= integral(Gf12,a,t) by A8,A18,A11,A1,INTEGR21:30;
hence thesis by A25;
end;
theorem Th54:
a <= b & 0 < r
& (for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
implies
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X),
m be Element of NAT,
g,h be continuous PartFunc of REAL,the carrier of X
st g = iter(Fredholm(G,a,b,y0),(m+1)).u
& h = iter(Fredholm(G,a,b,y0),(m+1)).v holds
for t be Real st t in ['a,b']
holds ||. g/.t - h/.t .|| <= ((r*(t-a))|^(m+1))/((m+1)!) * ||.u-v.||
proof
assume A1: a<=b & 0 < r
& for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||;
set F = Fredholm(G,a,b,y0);
A2:dom G = the carrier of X by FUNCT_2:def 1;
for x1,x2 be Point of X
st x1 in the carrier of X & x2 in the carrier of X holds
||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A1; then
G is_Lipschitzian_on the carrier of X by A1,FUNCT_2:def 1; then
A3:G is_continuous_on dom G by A2,NFCONT_1:45;
let u1,v1 be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X);
defpred P[Nat] means
for g,h be continuous PartFunc of REAL,the carrier of X
st g = iter(F,($1+1)).u1 & h = iter(F,($1+1)).v1
holds for t be Real st t in ['a,b']
holds ||. g/.t - h/.t .||
<= ((r*(t-a))|^($1+1))/(($1+1)!) * ||.u1-v1.||;
reconsider Z0 = 0 as Element of NAT;
A4:P[0]
proof
let g,h be continuous PartFunc of REAL,the carrier of X;
assume g = iter(F,( (0 qua Element of NAT ) + 1)).u1
& h = iter(F,( (0 qua Element of NAT ) + 1)).v1; then
A6: g= F.u1 & h= F.v1 by FUNCT_7:70;
for t be Real st t in ['a,b'] holds
||. g/.t - h/.t .|| <= ((r*(t-a))|^(Z0 + 1) )
/((Z0 + 1)!) * ||.u1-v1.|| by NEWTON:13,Th53,A1,A6;
hence thesis;
end;
A8:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A9: P[k];
let g,h be continuous PartFunc of REAL,the carrier of X;
assume A10: g = iter(F,((k+1)+1)).u1 & h = iter(F,((k+1)+1)).v1;
reconsider u=iter(F,(k+1)).u1, v=iter(F,(k+1)).v1 as
VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X);
A11:dom iter(F,k+1) = the carrier of
R_NormSpace_of_ContinuousFunctions(['a,b'],X) by FUNCT_2:def 1;
A12:iter(F,((k+1)+1)).u1 = (F*iter(F,k+1)).u1 by FUNCT_7:71
.= F.u by A11,FUNCT_1:13;
A13:iter(F,((k+1)+1)).v1 = (F*iter(F,k+1)).v1 by FUNCT_7:71
.= F.v by A11,FUNCT_1:13;
consider f1,g1,Gf1 be continuous PartFunc of REAL,the carrier of X
such that
A14: u=f1 & F.u = g1 & dom f1 =['a,b'] & dom g1 =['a,b'] & Gf1 = G*f1
& for t be Real st t in ['a,b']
holds g1/.t = y0+ integral(Gf1,a,t) by Def8,A1,A3;
consider f2,g2,Gf2 be continuous PartFunc of REAL,the carrier of X
such that
A15: v=f2 & F.v = g2 & dom f2 =['a,b'] & dom g2 =['a,b'] & Gf2 = G*f2
& for t be Real st t in ['a,b']
holds g2/.t = y0+ integral(Gf2,a,t) by Def8,A1,A3;
set Gf12= Gf1 - Gf2;
dom G = the carrier of X by FUNCT_2:def 1; then
rng f1 c= dom G & rng f2 c= dom G; then
A18:dom Gf1 =['a,b'] & dom Gf2 =['a,b'] by A14,A15,RELAT_1:27;
reconsider Gf12 as continuous PartFunc of REAL,the carrier of X;
A20:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
let t be Real;
assume A21: t in ['a,b']; then
A22:ex g be Real st t=g & a<=g & g <= b by A20;
a22:ex g be Element of REAL st t=g & a<=g & g <= b
proof
consider g be Real such that H1: t=g & a<=g & g <= b by A21,A20;
reconsider g as Element of REAL by XREAL_0:def 1;
take g;
thus thesis by H1;
end;
A23:dom Gf12 = dom Gf1 /\ dom Gf2 by VFUNCT_1:def 2
.= ['a,b'] by A18; then
A24:dom ||.Gf12.|| = ['a,b'] by NORMSP_0:def 2;
A27:a in ['a,b'] by A20,A1;
min(a,t) = a & max(a,t) = t by A22,XXREAL_0:def 9,def 10; then
A30:||.Gf12.|| is_integrable_on ['a,t'] &
(||.Gf12.||) | ['a,t'] is bounded &
||.integral(Gf12,a,t).|| <= integral(||.Gf12.||,a,t)
by A1,A23,A27,A21,INTEGR21:22;
['a,t'] = [.a,t.] by A22,INTEGRA5:def 3; then
consider rg be PartFunc of REAL,REAL such that
A31: dom rg = ['a,t']
& (for x be Real st x in ['a,t']
holds rg.x = r*(( (r*(x-a))|^(k+1) )/((k+1)!) * ||.u1-v1.|| ))
& rg is continuous
& rg is_integrable_on ['a,t'] & rg| ['a,t'] is bounded
& integral(rg,a,t) = ((r*(t-a))|^((k+1)+1))
/ (((k+1)+1)!) * ||.u1-v1.|| by Lm7,a22;
A32:['a,t'] c= ['a,b'] by A22,INTEGR19:1;
for x be Real st x in ['a,t'] holds ||.Gf12.||.x <= rg.x
proof
let x be Real;
assume A33: x in ['a,t']; then
A34: Gf12/.x =Gf1/.x -Gf2/.x by A23,A32,VFUNCT_1:def 2;
A35: Gf1/.x = (Gf1).x by A18,A32,A33,PARTFUN1:def 6
.= G.(f1.x) by A32,A33,A18,A14,FUNCT_1:12
.= G/.(f1/.x) by A32,A33,A14,PARTFUN1:def 6;
Gf2/.x = (Gf2).x by A18,A32,A33,PARTFUN1:def 6
.= G.(f2.x) by A32,A33,A18,A15,FUNCT_1:12
.= G/.(f2/.x) by A32,A33,A15,PARTFUN1:def 6; then
A37: ||. Gf1/.x -Gf2/.x .|| <= r*||.(f1/.x)-(f2/.x).|| by A35,A1;
r*||.(f1/.x)-(f2/.x).||
<=r*(( (r*(x-a))|^(k+1) )/((k+1)!) * ||.u1-v1.||)
by A1,XREAL_1:64,A9,A14,A15,A32,A33; then
r*||.(f1/.x)-(f2/.x).|| <=rg.x by A33,A31; then
||. Gf1/.x -Gf2/.x .|| <=rg.x by A37,XXREAL_0:2;
hence thesis by A24,A32,A33,NORMSP_0:def 2,A34;
end; then
A38:integral(||.Gf12.||,a,t) <= integral(rg,a,t)
by A30,A22,A24,A32,A31,ORDEQ_01:48;
g/.t = y0+ integral(Gf1,a,t) & h/.t = y0+ integral(Gf2,a,t)
by A14,A15,A21,A12,A10,A13; then
g/.t - h/.t
= (y0+ integral(Gf1,a,t) - y0 ) -integral(Gf2,a,t) by RLVECT_1:27
.= integral(Gf1,a,t) + (y0 - y0) -integral(Gf2,a,t) by RLVECT_1:28
.= integral(Gf1,a,t) + 0.X -integral(Gf2,a,t) by RLVECT_1:15
.= integral(Gf12,a,t) by A18,A27,A21,A1,INTEGR21:30;
hence thesis by A38,A30,XXREAL_0:2,A31;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A8);
hence thesis;
end;
Lm8:
for r,L,a,b,t be Real,m be Nat
st a<=t & t <= b & 0 <= L & 0<=r holds
((r*(t-a))|^(m+1))/((m+1)!) * L <= ((r*(b-a))|^(m+1))/((m+1)!) * L
proof
let r,L,a,b,t be Real, m be Nat;
assume A1: a<=t & t <= b & 0 <= L & 0<=r; then
t-a <= b-a by XREAL_1:13; then
A2:r*(t-a) <= r*(b-a) by A1,XREAL_1:64;
0 <= t-a by A1,XREAL_1:48; then
A3:(r*(t-a)) to_power (m+1) <= (r*(b-a)) to_power (m+1) by A1,HOLDER_1:3,A2;
((r*(t-a))|^(m+1))/((m+1)!) <= ((r*(b-a))|^(m+1))/((m+1)!) by A3,XREAL_1:72;
hence thesis by A1,XREAL_1:64;
end;
Lm9:
a < b & 0 < r implies
ex m be Element of NAT st ((r*(b-a))|^(m+1))/((m+1)!) < 1
& 0 < ((r*(b-a))|^(m+1))/((m+1)!)
proof
assume A1: a < b & 0 < r;
set z=r*(b-a);
set s = z rExpSeq;
s is summable by SIN_COS:45; then
s is convergent & lim s = 0 by SERIES_1:4; then
consider n be Nat such that
A3: for m be Nat st n<=m holds |.s.m- 0 .| < 1 by SEQ_2:def 7;
reconsider m0 = max(n,1) as Element of NAT by ORDINAL1:def 12;
reconsider m = m0 - 1 as Element of NAT by INT_1:5,XXREAL_0:25;
take m;
|.s.(m+1) - 0 .| < 1 by A3,XXREAL_0:25; then
A4:|. ((r*(b-a))|^(m+1))/((m+1)!) .| < 1 by SIN_COS:def 5;
0 < b - a by A1,XREAL_1:50; then
(0 qua Real) *r < r*(b-a) by A1,XREAL_1:68; then
0 < (r*(b-a)) to_power (m+1) by POWER:34;
hence thesis by A4,ABSVALUE:def 1,XREAL_1:139;
end;
theorem Th55:
for m be Nat st a <= b & 0 < r
& (for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||) holds
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X)
holds ||. iter(Fredholm(G,a,b,y0),(m+1)).u
- iter(Fredholm(G,a,b,y0),(m+1)).v .||
<= ((r*(b-a))|^(m+1))/((m+1)!) * ||.u-v.||
proof
let m be Nat;
assume A1: a<=b & 0 < r
& for y1,y2 be VECTOR of X holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||;
let u,v be VECTOR of
R_NormSpace_of_ContinuousFunctions(['a,b'],X);
reconsider u1=iter(Fredholm(G,a,b,y0),(m+1)).u as VECTOR of
R_NormSpace_of_ContinuousFunctions(['a,b'],X);
reconsider v1=iter(Fredholm(G,a,b,y0),(m+1)).v as VECTOR of
R_NormSpace_of_ContinuousFunctions(['a,b'],X);
consider g be continuous PartFunc of REAL,the carrier of X such that
A2: u1=g & dom g = ['a,b'] by ORDEQ_01:def 2;
consider h be continuous PartFunc of REAL,the carrier of X such that
A3: v1=h & dom h = ['a,b'] by ORDEQ_01:def 2;
now let t be Real;
A4: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
assume A5: t in ['a,b']; then
A6: ex g be Real st t=g & a<=g & g <= b by A4;
m in NAT by ORDINAL1:def 12; then
A7: ||. g/.t - h/.t .||
<= ((r*(t-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by A5,Th54,A1,A2,A3;
((r*(t-a))|^(m+1) )/((m+1)!) * ||.u-v.||
<= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by A6,A1,Lm8;
hence ||. g/.t - h/.t .|| <= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.||
by A7,XXREAL_0:2;
end;
hence thesis by ORDEQ_01:27,A2,A3;
end;
theorem Th56:
a < b & G is_Lipschitzian_on the carrier of X implies
ex m be Nat st iter(Fredholm(G,a,b,y0),(m+1)) is contraction
proof
assume A1: a<b & G is_Lipschitzian_on the carrier of X; then
consider r be Real such that
A2: 0<r & for x1,x2 be Point of X
st x1 in the carrier of X & x2 in the carrier of X holds
||.G/.x1-G/.x2.||<=r*||.x1-x2.||;
A3:for x1,x2 be Point of X holds ||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A2;
consider m be Element of NAT such that
A4: ((r*(b-a))|^(m+1))/((m+1)!) < 1
& 0 < ((r*(b-a))|^(m+1))/((m+1)!) by Lm9,A1,A2;
take m;
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions(['a,b'],X)
holds ||. iter(Fredholm(G,a,b,y0),(m+1)).u
- iter(Fredholm(G,a,b,y0),(m+1)).v .||
<= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by Th55,A3,A2,A1;
hence thesis by A4;
end;
theorem Th57:
a < b & G is_Lipschitzian_on the carrier of X implies
Fredholm(G,a,b,y0) is with_unique_fixpoint
proof
assume a<b & G is_Lipschitzian_on the carrier of X; then
ex m be Nat st iter(Fredholm(G,a,b,y0),m+1) is contraction by Th56;
hence thesis by ORDEQ_01:7;
end;
theorem Th58:
for f,g be continuous PartFunc of REAL,the carrier of X
st dom f =['a,b'] & dom g =['a,b'] & Z = ].a,b.[
& a<b & G is_Lipschitzian_on the carrier of X
& g=Fredholm(G,a,b,y0).f holds
g/.a=y0
& g is_differentiable_on Z
& for t be Real st t in Z holds diff(g,t) = (G*f)/.t
proof
let f,g be continuous PartFunc of REAL,the carrier of X;
assume A1: dom f =['a,b'] & dom g =['a,b'] & Z = ].a,b.[
& a<b & G is_Lipschitzian_on the carrier of X
& g=Fredholm(G,a,b,y0).f;
X1:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
set D = R_NormSpace_of_ContinuousFunctions(['a,b'],X);
X2:dom G = the carrier of X by FUNCT_2:def 1; then
A2:G is_continuous_on dom G by A1,NFCONT_1:45;
f is Element of D by ORDEQ_01:def 2,A1; then
consider f0,g0,Gf0 be continuous PartFunc of REAL,the carrier of X
such that
A3: f=f0 & Fredholm(G,a,b,y0).f = g0
& dom f0 = ['a,b'] & dom g0 =['a,b'] & Gf0 = G*f0
& for t be Real st t in ['a,b']
holds g0/.t = y0+ integral(Gf0,a,t) by A1,A2,Def8;
reconsider Gf=G*f as continuous PartFunc of REAL,the carrier of X by A3;
rng f c= dom G by X2; then
dom Gf =['a,b'] by A1,RELAT_1:27;
hence thesis by A1,X1,Th40,Th40a,A3;
end;
theorem Th59:
for y be continuous PartFunc of REAL,the carrier of X
st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X
& dom y = ['a,b'] & y is_differentiable_on Z & y/.a = y0
& (for t be Real st t in Z holds diff(y,t) = G.(y/.t)) holds
y is_a_fixpoint_of Fredholm(G,a,b,y0)
proof
let y be continuous PartFunc of REAL,the carrier of X;
assume A1: a<b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X
& dom y = ['a,b'] & y is_differentiable_on Z & y/.a = y0
& (for t be Real st t in Z holds diff(y,t) = G.(y/.t));
X1:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
A2:dom (Fredholm(G,a,b,y0))
= the carrier of R_NormSpace_of_ContinuousFunctions(['a,b'],X)
by FUNCT_2:def 1;
A3:y is Element of the carrier of
R_NormSpace_of_ContinuousFunctions(['a,b'],X) by ORDEQ_01:def 2,A1;
X2:dom G = the carrier of X by FUNCT_2:def 1; then
G is_continuous_on dom G by A1,NFCONT_1:45; then
consider f,g,Gf be continuous PartFunc of REAL,the carrier of X
such that
A5: y=f & (Fredholm(G,a,b,y0)).y = g
& dom f =['a,b'] & dom g =['a,b'] & Gf = G*f
& for t be Real st t in ['a,b']
holds g/.t = y0+ integral(Gf,a,t) by Def8,A1,A3;
rng f c= dom G by X2; then
A6:dom (G*f) = ['a,b'] by A5,RELAT_1:27;
for t be Real st t in Z holds diff(y,t) = (Gf)/.t
proof
let t be Real;
assume A7:t in Z;
hence diff(y,t) = G.(y/.t) by A1
.= G.(y.t) by A1,A7,PARTFUN1:def 6
.= (Gf).t by A5,A1,A7,FUNCT_1:13
.= (Gf)/.t by A5,A1,A7,A6,PARTFUN1:def 6;
end;
hence thesis by A1,X1,A2,A5,Th47,A6,ORDEQ_01:def 2;
end;
theorem
for y1,y2 be continuous PartFunc of REAL,the carrier of X
st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X
& dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1/.a = y0
& (for t be Real st t in Z holds diff(y1,t) = G.(y1/.t))
& dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2/.a = y0
& (for t be Real st t in Z holds diff(y2,t) = G.(y2/.t))
holds y1=y2
proof
let y1,y2 be continuous PartFunc of REAL,the carrier of X;
assume
A1:a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X
& dom y1 = ['a,b'] & y1 is_differentiable_on Z & y1/.a = y0
& (for t be Real st t in Z holds diff(y1,t) = G.(y1/.t))
& dom y2 = ['a,b'] & y2 is_differentiable_on Z & y2/.a = y0
& (for t be Real st t in Z holds diff(y2,t) = G.(y2/.t)); then
Fredholm(G,a,b,y0) is with_unique_fixpoint by Th57; then
consider y being set such that
SS: y is_a_fixpoint_of Fredholm(G,a,b,y0)
& for z being set st z is_a_fixpoint_of Fredholm(G,a,b,y0) holds y = z;
y1 = y by Th59,A1,SS .= y2 by Th59,A1,SS;
hence thesis;
end;
theorem
a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X implies
ex y be continuous PartFunc of REAL,the carrier of X st
dom y = ['a,b'] & y is_differentiable_on Z & y/.a = y0
& for t be Real st t in Z holds diff(y,t) = G.(y/.t)
proof
assume A1: a<b & Z = ].a,b.[
& G is_Lipschitzian_on the carrier of X; then
Fredholm(G,a,b,y0) is with_unique_fixpoint by Th57; then
consider x be set such that
A2: x is_a_fixpoint_of Fredholm(G,a,b,y0)
& for y being set st y is_a_fixpoint_of Fredholm(G,a,b,y0) holds x = y;
x in dom Fredholm(G,a,b,y0) & x = (Fredholm(G,a,b,y0)).x by A2; then
reconsider x as Element of the carrier of
R_NormSpace_of_ContinuousFunctions(['a,b'],X);
consider f be continuous PartFunc of REAL,the carrier of X such that
A4: x=f & dom f = ['a,b'] by ORDEQ_01:def 2;
take f;
thus dom f = ['a,b'] & f is_differentiable_on Z & f/.a = y0
by Th58,A4,A1,A2;
A5:].a,b.[ c= [.a,b.] by XXREAL_1:25;
A6:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
let t be Real;
assume A7:t in Z;
dom G = the carrier of X by FUNCT_2:def 1; then
rng f c= dom G; then
A8:dom (G*f) = ['a,b'] by A4,RELAT_1:27;
thus diff(f,t) = (G*f)/.t by A7,Th58,A4,A1,A2
.= (G*f).t by A8,A5,A1,A7,A6,PARTFUN1:def 6
.= G.(f.t) by A8,A5,A1,A7,A6,FUNCT_1:12
.= G.(f/.t) by A5,A1,A7,A6,A4,PARTFUN1:def 6;
end;