:: Contracting Mapping on Normed Linear Space
:: by Keiichi Miyajima , Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received August 19, 2012
:: Copyright (c) 2012-2017 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, RSSPACE3, LOPBAN_1, ORDEQ_01, STRUCT_0, COMPLEX1, VALUED_1,
ALI2, SUPINF_2, XBOOLE_0, ABIAN, INTEGRA1, FINSEQ_1, TARSKI, INTEGRA5,
CARD_3, XXREAL_1, PARTFUN1, RLVECT_1, SEQ_4, FUNCT_2, RCOMP_1, VALUED_0,
XXREAL_2, FCONT_1, ALGSTR_0, CFCONT_1, MEASURE5, RLSUB_1, RELAT_2,
REWRITE1, NFCONT_1, C0SP2, RSSPACE, RSSPACE4, FUNCOP_1, REALSET1,
FDIFF_1, PREPOWER, INTEGRA7, METRIC_1, SERIES_1, SIN_COS, SEQFUNC,
REAL_NS1, FINSEQ_2, EUCLID, NEWTON, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, PARTFUN2, NUMBERS, XXREAL_0, XREAL_0, REAL_1, NAT_1,
VALUED_0, COMPLEX1, XCMPLX_0, XXREAL_2, FUNCOP_1, FINSEQ_1, VALUED_1,
FINSEQ_2, SEQ_1, SEQ_2, NEWTON, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1,
FUNCT_7, ABIAN, PREPOWER, POWER, SERIES_1, SEQFUNC, MEASURE5, SIN_COS,
TAYLOR_1, INTEGRA1, INTEGRA5, INTEGRA7, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, VFUNCT_1, RSSPACE, EUCLID,
RSSPACE3, LOPBAN_1, NFCONT_1, INTEGR19, RSSPACE4, REAL_NS1, PDIFF_1,
INTEGR15, INTEGR18, NFCONT_3, NDIFF_3, NFCONT_2, NFCONT_4;
constructors REAL_1, ABIAN, SEQ_1, SEQ_2, RSSPACE3, RELSET_1, SEQ_4, VFUNCT_1,
PDIFF_1, INTEGRA5, NFCONT_3, RLSUB_1, PARTFUN2, FCONT_1, NFCONT_1,
NDIFF_1, NDIFF_3, RSSPACE4, SEQFUNC, INTEGR18, RVSUM_1, BINOP_2,
INTEGR19, INTEGR15, NFCONT_4, FDIFF_1, VALUED_2, PREPOWER, INTEGRA7,
COMSEQ_2, COMSEQ_3, SIN_COS, TAYLOR_1, NFCONT_2, C0SP2;
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, INTEGRA1, ORDINAL1, FUNCOP_1, NEWTON, NFCONT_3,
XXREAL_2, RSSPACE4, RCOMP_1, RLVECT_1, REAL_NS1, VALUED_0, FINSEQ_1,
FDIFF_1, FCONT_1, EUCLID, MEASURE5, VALUED_2, FCONT_3, POWER, NFCONT_4,
PREPOWER;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
begin :: The Principle of Contracting Mapping on Normed Linear Space
reserve n for non zero Element of NAT;
reserve a,b,r,t for Real;
definition
let f be Function;
attr f is with_unique_fixpoint means
:: ORDEQ_01:def 1
ex x being set st x is_a_fixpoint_of f &
for y being set st y is_a_fixpoint_of f holds x = y;
end;
theorem :: ORDEQ_01:1
for x being set holds x is_a_fixpoint_of {[x,x]};
theorem :: ORDEQ_01:2
for x,y,z being set st x is_a_fixpoint_of {[y,z]} holds x = y;
registration
let x be set;
cluster {[x,x]} -> with_unique_fixpoint;
end;
theorem :: ORDEQ_01:3
for X being RealNormSpace, x being Point of X holds
(for e being Real st e > 0 holds ||.x.|| < e) implies x = 0.X;
theorem :: ORDEQ_01:4
for X being RealNormSpace, x,y being Point of X holds
(for e being Real st e > 0 holds ||.x-y.|| < e) implies x = y;
theorem :: ORDEQ_01:5
for K, L, e being Real st 0 < K & K < 1 & 0 < e
ex n being Nat st |. L*(K to_power n) .| < e;
registration
let X be RealNormSpace;
cluster constant -> contraction for Function of X,X;
end;
registration
let X be RealBanachSpace;
cluster contraction -> with_unique_fixpoint for Function of X,X;
end;
::$CT
theorem :: ORDEQ_01:7
for X being RealBanachSpace, f being Function of X,X st
ex n0 being Nat st iter(f,n0) is contraction holds
f is with_unique_fixpoint;
theorem :: ORDEQ_01:8
for X being RealBanachSpace, f being Function of X,X st
ex n0 being Element of NAT st iter(f,n0) is contraction holds
ex xp being Point of X st f.xp = xp &
for x being Point of X st f.x = x holds xp = x;
begin :: The Real Banach Space C([a,b],X)
theorem :: ORDEQ_01:9
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
f be continuous PartFunc of REAL,Y
st dom f = X holds
f is bounded Function of X,Y;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func ContinuousFunctions(X,Y)
-> Subset of R_VectorSpace_of_BoundedFunctions(X,Y) means
:: ORDEQ_01:def 2
for x being set holds x in it iff
ex f be continuous PartFunc of REAL,Y st x = f & dom f = X;
end;
registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
cluster ContinuousFunctions(X,Y) -> non empty;
end;
registration
let X be non empty closed_interval Subset of REAL, Y be RealNormSpace;
cluster ContinuousFunctions(X,Y) -> linearly-closed;
end;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func R_VectorSpace_of_ContinuousFunctions(X,Y) -> strict RealLinearSpace
equals
:: ORDEQ_01:def 3
RLSStruct (# ContinuousFunctions(X,Y), Zero_(ContinuousFunctions(X,Y),
R_VectorSpace_of_BoundedFunctions (X,Y)), Add_(ContinuousFunctions(X,Y),
R_VectorSpace_of_BoundedFunctions (X,Y)), Mult_(ContinuousFunctions(X,Y),
R_VectorSpace_of_BoundedFunctions(X,Y)) #);
end;
registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
cluster R_VectorSpace_of_ContinuousFunctions(X,Y) ->
Abelian add-associative
right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
end;
theorem :: ORDEQ_01:10
for X be non empty closed_interval Subset of REAL, Y be RealNormSpace,
f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(X,Y),
f9,g9,h9 be continuous PartFunc of REAL,Y
st f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X
holds (h = f+g iff for x
be Element of X holds h9/.x = f9/.x + g9/.x );
theorem :: ORDEQ_01:11
for X be non empty closed_interval Subset of REAL, Y be RealNormSpace,
f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(X,Y),
f9,h9 be continuous PartFunc of REAL,Y
st f9=f & h9=h & dom f9=X & dom h9=X
holds h = a*f iff for x be Element of X holds h9/.x = a*f9/.x;
theorem :: ORDEQ_01:12
for X be non empty closed_interval Subset of REAL, Y be RealNormSpace holds
0. R_VectorSpace_of_ContinuousFunctions(X,Y) = X -->0.Y;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func ContinuousFunctionsNorm(X,Y) ->
Function of ContinuousFunctions(X,Y),REAL equals
:: ORDEQ_01:def 4
(BoundedFunctionsNorm(X,Y)) | (ContinuousFunctions(X,Y));
end;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let f be set such that
f in ContinuousFunctions(X,Y);
func modetrans(f,X,Y) -> continuous PartFunc of REAL,Y means
:: ORDEQ_01:def 5
it = f & dom it = X;
end;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func R_NormSpace_of_ContinuousFunctions(X,Y) -> strict non empty NORMSTR
equals
:: ORDEQ_01:def 6
NORMSTR (# ContinuousFunctions(X,Y),
Zero_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
Add_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
Mult_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
ContinuousFunctionsNorm(X,Y) #);
end;
theorem :: ORDEQ_01:13
for X be non empty closed_interval Subset of REAL,Y be RealNormSpace,
f be continuous PartFunc of REAL,Y
st dom f=X holds modetrans(f,X,Y)=f;
theorem :: ORDEQ_01:14
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace holds (X --> 0.Y)
= 0.R_NormSpace_of_ContinuousFunctions(X,Y);
theorem :: ORDEQ_01:15
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace, f,g,h be Point of
R_NormSpace_of_ContinuousFunctions(X,Y),
f9,g9,h9 be continuous PartFunc of REAL,Y
st f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X
holds (h = f+g iff for x be Element of X
holds h9/.x = f9/.x + g9/.x);
theorem :: ORDEQ_01:16
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
f,h be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f9,h9 be continuous PartFunc of REAL,Y
st f9=f & h9=h & dom f9=X & dom h9=X
holds (h = a*f iff for x be Element of X
holds h9/.x = a*f9/.x);
theorem :: ORDEQ_01:17
for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
f be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g be Point of R_NormSpace_of_BoundedFunctions(X,Y)
st f=g holds ||.f.|| = ||.g.||;
theorem :: ORDEQ_01:18
for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
f,g be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f1,g1 be Point of R_NormSpace_of_BoundedFunctions(X,Y)
st f1=f & g1=g holds f+g = f1+g1;
theorem :: ORDEQ_01:19
for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
f be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f1 be Point of R_NormSpace_of_BoundedFunctions(X,Y) st f1=f
holds a*f = a*f1;
registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
cluster R_NormSpace_of_ContinuousFunctions(X,Y) ->
reflexive discerning RealNormSpace-like vector-distributive
scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
end;
theorem :: ORDEQ_01:20
for X be non empty closed_interval Subset of REAL
for Y be RealNormSpace
for f,g,h be Point of R_NormSpace_of_ContinuousFunctions(X,Y)
for f9,g9,h9 be continuous PartFunc of REAL,Y
st f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X
holds (h = f-g iff for x be Element of X holds h9/.x = f9/.x - g9/.x );
theorem :: ORDEQ_01:21
for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
f,g be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f1,g1 be Point of R_NormSpace_of_BoundedFunctions(X,Y)
st f1=f & g1=g
holds f-g = f1-g1;
registration
let X be non empty closed_interval Subset of REAL,
Y be RealNormSpace;
cluster closed for Subset of R_NormSpace_of_BoundedFunctions(X,Y);
end;
theorem :: ORDEQ_01:22
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace holds
ContinuousFunctions(X,Y)
is closed Subset of R_NormSpace_of_BoundedFunctions(X,Y);
theorem :: ORDEQ_01:23
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
seq be sequence of R_NormSpace_of_ContinuousFunctions(X,Y)
st Y is complete &
seq is Cauchy_sequence_by_Norm holds seq is convergent;
registration
let X be non empty closed_interval Subset of REAL;
let Y be RealBanachSpace;
cluster R_NormSpace_of_ContinuousFunctions(X,Y) -> complete;
end;
theorem :: ORDEQ_01:24
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
v be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g be PartFunc of REAL,Y st g=v
holds for t be Real st t in X holds ||.g/.t.|| <= ||.v.||;
theorem :: ORDEQ_01:25
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
K be Real,
v being Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g be PartFunc of REAL,Y st g=v &
for t be Real st t in X holds ||.g/.t.|| <= K
holds ||.v.|| <= K;
theorem :: ORDEQ_01:26
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
v1,v2 be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g1,g2 be PartFunc of REAL,Y
st g1=v1 & g2=v2
holds for t be Real st t in X holds
||.g1/.t - g2/.t .|| <= ||.v1-v2.||;
theorem :: ORDEQ_01:27
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
K be Real,
v1,v2 being Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g1,g2 be PartFunc of REAL,Y
st g1=v1 & g2=v2 &
for t be Real st t in X holds
||.g1/.t - g2/.t .|| <= K
holds ||.v1-v2.|| <= K;
begin :: Differential Equations
theorem :: ORDEQ_01:28
for n,i be Nat, f be PartFunc of REAL,REAL n,
A be Subset of REAL holds proj(i,n)*(f|A) = (proj(i,n)*f)|A;
theorem :: ORDEQ_01:29
for g be continuous PartFunc of REAL, REAL n st dom g = [' a,b ']
holds g | [' a,b '] is bounded;
theorem :: ORDEQ_01:30
for g be continuous PartFunc of REAL,REAL n
st dom g =[' a,b ']
holds g is_integrable_on [' a,b '];
theorem :: ORDEQ_01:31
for f,F be PartFunc of REAL,REAL n
st a <= b
& dom f =[' a,b '] & dom F =[' a,b ']
& f is continuous
& 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;
theorem :: ORDEQ_01:32
for f be continuous PartFunc of REAL,REAL-NS n st dom f = [' a,b ']
holds f|([' a,b ']) is bounded;
theorem :: ORDEQ_01:33
for f be continuous PartFunc of REAL,REAL-NS n st dom f = [' a,b ']
holds f is_integrable_on [' a,b '];
theorem :: ORDEQ_01:34
for f be continuous PartFunc of REAL,REAL-NS n,
F be PartFunc of REAL,REAL-NS n
st a <= b
& 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;
theorem :: ORDEQ_01:35
for R be PartFunc of REAL, REAL
st R is total holds R is RestFunc-like iff
for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
st z <> 0 & |. z .| < d holds |.z.|"* |. R/.z .| < r;
reserve
Z for open Subset of REAL,
y0 for VECTOR of REAL-NS n,
G for Function of REAL-NS n,REAL-NS n;
theorem :: ORDEQ_01:36
for f be continuous PartFunc of REAL,REAL-NS n,
g be PartFunc of REAL,REAL-NS n st a <= b
& 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/.a=y0 &
g is_differentiable_on Z
& for t be Real st t in Z holds diff(g,t) = f/.t;
theorem :: ORDEQ_01:37
for i be Nat,
y1,y2 be Point of REAL-NS n holds
proj(i,n).(y1 + y2) = proj(i,n).y1 + proj(i,n).y2;
theorem :: ORDEQ_01:38
for i be Nat,
y1 be Point of REAL-NS n, r being Real holds
proj(i,n).(r*y1) = r*(proj(i,n).y1);
theorem :: ORDEQ_01:39
for g be PartFunc of REAL,REAL-NS n,
x0 be Real,
i be Nat st
1 <= i & i <= n & g is_differentiable_in x0 holds
(proj(i,n)*g) is_differentiable_in x0 &
proj(i,n).(diff(g,x0)) = diff((proj(i,n)*g),x0);
theorem :: ORDEQ_01:40
for f be PartFunc of REAL,REAL-NS n,
X be set st
for i be Nat st 1 <= i & i <= n
holds (proj(i,n)*f) | X is constant
holds
f| X is constant;
theorem :: ORDEQ_01:41
for f be PartFunc of REAL,REAL-NS n
st ].a,b.[ c= dom f
& f is_differentiable_on ].a,b.[
& for x be Real
st x in ].a,b.[ holds diff(f,x) = 0.(REAL-NS n)
holds f| (].a,b.[) is constant;
theorem :: ORDEQ_01:42
for f be continuous PartFunc of REAL,REAL-NS n st a < b
& [.a,b.] = dom f & f | ].a,b.[ is constant holds
for x be Real st x in [.a,b.] holds f.x = f.a;
theorem :: ORDEQ_01:43
for y,Gf be continuous PartFunc of REAL,REAL-NS n,
g be PartFunc of REAL,REAL-NS n st a** Function of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) means
:: ORDEQ_01:def 7
for x be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n)
ex f,g,Gf be continuous PartFunc of REAL,REAL-NS n
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);
end;
theorem :: ORDEQ_01:49
a <= b & 0 < r &
(for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
implies
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
g,h be continuous PartFunc of REAL,REAL-NS n
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.||;
theorem :: ORDEQ_01:50
a <= b & 0 < r &
(for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
implies
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
m be Element of NAT,
g,h be continuous PartFunc of REAL,REAL-NS n
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.||
;
theorem :: ORDEQ_01:51
for m be Nat st a <= b & 0 < r &
(for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
holds
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n)
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.||;
theorem :: ORDEQ_01:52
a**