:: The Uniform Continuity of Functions on Normed Linear Spaces
:: by Takaya Nishiyama , Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received April 6, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, NORMSP_1, PARTFUN1, NAT_1, PRE_TOPC,
TARSKI, RELAT_1, CARD_1, ARYTM_3, ARYTM_1, STRUCT_0, COMPLEX1, XBOOLE_0,
XXREAL_0, VALUED_1, SUPINF_2, FUNCT_1, CFCONT_1, NFCONT_1, RCOMP_1,
VALUED_0, SEQ_2, ORDINAL2, FCONT_1, FUNCT_2, SEQ_4, LOPBAN_1, ALI2,
FUNCOP_1, POWER, SEQ_1, RSSPACE3, FUNCT_7, NFCONT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FUNCOP_1, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, NUMBERS,
COMPLEX1, REAL_1, NAT_1, RLVECT_1, STRUCT_0, PRE_TOPC, VALUED_1, SEQ_1,
SEQ_2, VALUED_0, SEQ_4, ABIAN, POWER, VFUNCT_1, NORMSP_0, NORMSP_1,
LOPBAN_1, RSSPACE3, NFCONT_1, RECDEF_1;
constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_2, SEQ_4, POWER, ABIAN, VFUNCT_1,
RSSPACE3, LOPBAN_3, NFCONT_1, RECDEF_1, RELSET_1, COMSEQ_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, NORMSP_1,
NAT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1;
theorems TARSKI, ABSVALUE, XBOOLE_1, RLVECT_1, XCMPLX_1, FUNCOP_1, SEQ_1,
SEQ_2, SERIES_1, NAT_1, POWER, RELAT_1, VFUNCT_1, LOPBAN_1, NORMSP_1,
SEQ_4, FUNCT_2, RSSPACE3, FUNCT_7, LOPBAN_3, PARTFUN2, NFCONT_1, XREAL_1,
COMPLEX1, XXREAL_0, ORDINAL1, PARTFUN1, VALUED_0, NORMSP_0;
schemes SEQ_1, NAT_1, FUNCT_2;
begin :: Uniform Continuity of Functions on Normed Linear Spaces
reserve n,m for Nat,
x,X,X1 for set,
s,g,r,p for Real,
S,T for RealNormSpace,
f,f1,f2 for PartFunc of S, T,
s1,s2,q1 for sequence of S,
x0,x1, x2 for Point of S,
Y for Subset of S;
definition
let X,S,T;
let f;
pred f is_uniformly_continuous_on X means
X c= dom f & for r st 0<r
ex s st 0<s & for x1,x2 st x1 in X & x2 in X & ||.x1 - x2.|| < s holds ||. f/.
x1 - f/.x2 .|| < r;
end;
definition
let X,S;
let f be PartFunc of the carrier of S,REAL;
pred f is_uniformly_continuous_on X means
X c= dom f & for r st 0<r
ex s st 0<s & for x1,x2 st x1 in X & x2 in X & ||.x1 - x2.|| < s holds |.f/.
x1 - f/.x2.| < r;
end;
theorem Th1:
f is_uniformly_continuous_on X & X1 c= X implies f
is_uniformly_continuous_on X1
proof
assume that
A1: f is_uniformly_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence X1 c= dom f by A2,XBOOLE_1:1;
let r;
assume 0<r;
then consider s such that
A3: 0<s and
A4: for x1,x2 st x1 in X & x2 in X & ||.x1-x2.||<s holds ||.f/.x1-f/.x2
.||<r by A1;
take s;
thus 0<s by A3;
let x1,x2;
assume x1 in X1 & x2 in X1 & ||.x1-x2.||<s;
hence thesis by A2,A4;
end;
theorem
f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1
implies f1+f2 is_uniformly_continuous_on X/\X1
proof
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1;
A3: f2 is_uniformly_continuous_on X /\ X1 by A2,Th1,XBOOLE_1:17;
then
A4: X /\ X1 c= dom f2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1,Th1,XBOOLE_1:17;
then X /\ X1 c= dom f1;
then X /\ X1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:19;
hence
A6: X /\ X1 c= dom (f1+f2) by VFUNCT_1:def 1;
let r;
assume 0<r;
then
A7: 0<r/2 by XREAL_1:215;
then consider s such that
A8: 0<s and
A9: for x1,x2 st x1 in X /\ X1 & x2 in X /\X1 & ||.x1-x2.||<s holds ||.
f1/.x1-f1/.x2.||<r/2 by A5;
consider g such that
A10: 0<g and
A11: for x1,x2 st x1 in X /\ X1 & x2 in X /\ X1 & ||.x1-x2.||<g holds
||.f2/.x1-f2/.x2.||<r/2 by A3,A7;
take p=min(s,g);
thus 0<p by A8,A10,XXREAL_0:15;
let x1,x2;
assume that
A12: x1 in X/\X1 and
A13: x2 in X/\X1 and
A14: ||.x1-x2.||<p;
p <= g by XXREAL_0:17;
then ||.x1-x2.||<g by A14,XXREAL_0:2;
then
A15: ||.f2/.x1-f2/.x2.||<r/2 by A11,A12,A13;
p <= s by XXREAL_0:17;
then ||.x1-x2.||<s by A14,XXREAL_0:2;
then ||.f1/.x1-f1/.x2.||<r/2 by A9,A12,A13;
then
A16: ||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||<r/2+r/2 by A15,XREAL_1:8;
A17: ||.f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| <= ||.f1/.x1-f1/.x2.|| + ||.f2
/.x1-f2/.x2.|| by NORMSP_1:def 1;
||.(f1+f2)/.x1-(f1+f2)/.x2.|| = ||.f1/.x1 + f2/.x1-(f1+f2)/.x2.|| by A6,A12,
VFUNCT_1:def 1
.= ||.f1/.x1 + f2/.x1 - (f1/.x2+f2/.x2).|| by A6,A13,VFUNCT_1:def 1
.= ||.f1/.x1 + (f2/.x1 - (f1/.x2+f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 + (f2/.x1 - f1/.x2-f2/.x2).|| by RLVECT_1:27
.= ||.f1/.x1 + (-f1/.x2 + f2/.x1-f2/.x2).||
.= ||.f1/.x1 + (-f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 3;
hence thesis by A16,A17,XXREAL_0:2;
end;
theorem
f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1
implies f1-f2 is_uniformly_continuous_on X/\X1
proof
assume that
A1: f1 is_uniformly_continuous_on X and
A2: f2 is_uniformly_continuous_on X1;
A3: f2 is_uniformly_continuous_on X /\ X1 by A2,Th1,XBOOLE_1:17;
then
A4: X /\ X1 c= dom f2;
A5: f1 is_uniformly_continuous_on X /\ X1 by A1,Th1,XBOOLE_1:17;
then X /\ X1 c= dom f1;
then X /\ X1 c= dom f1 /\ dom f2 by A4,XBOOLE_1:19;
hence
A6: X /\ X1 c= dom (f1-f2) by VFUNCT_1:def 2;
let r;
assume 0<r;
then
A7: 0<r/2 by XREAL_1:215;
then consider s such that
A8: 0<s and
A9: for x1,x2 st x1 in X /\ X1 & x2 in X /\X1 & ||.x1-x2.||<s holds ||.
f1/.x1-f1/.x2.||<r/2 by A5;
consider g such that
A10: 0<g and
A11: for x1,x2 st x1 in X /\ X1 & x2 in X /\ X1 & ||.x1-x2.||<g holds
||.f2/.x1-f2/.x2.||<r/2 by A3,A7;
take p=min(s,g);
thus 0<p by A8,A10,XXREAL_0:15;
let x1,x2;
assume that
A12: x1 in X/\X1 and
A13: x2 in X/\X1 and
A14: ||.x1-x2.||<p;
p <= g by XXREAL_0:17;
then ||.x1-x2.||<g by A14,XXREAL_0:2;
then
A15: ||.f2/.x1-f2/.x2.||<r/2 by A11,A12,A13;
p <= s by XXREAL_0:17;
then ||.x1-x2.||<s by A14,XXREAL_0:2;
then ||.f1/.x1-f1/.x2.||<r/2 by A9,A12,A13;
then
A16: ||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||<r/2+r/2 by A15,XREAL_1:8;
A17: ||.f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| <= ||.f1/.x1-f1/.x2.|| + ||.f2
/.x1-f2/.x2.|| by NORMSP_1:3;
||.(f1-f2)/.x1-(f1-f2)/.x2.|| = ||.f1/.x1 - f2/.x1-(f1-f2)/.x2.|| by A6,A12,
VFUNCT_1:def 2
.= ||.f1/.x1 - f2/.x1 - (f1/.x2-f2/.x2).|| by A6,A13,VFUNCT_1:def 2
.= ||.f1/.x1 - (f2/.x1 + (f1/.x2-f2/.x2)).|| by RLVECT_1:27
.= ||.f1/.x1 - (f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:def 3
.= ||.f1/.x1 - (f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:def 3
.= ||.f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| by RLVECT_1:27;
hence thesis by A16,A17,XXREAL_0:2;
end;
theorem Th4:
f is_uniformly_continuous_on X implies p(#)f is_uniformly_continuous_on X
proof
assume
A1: f is_uniformly_continuous_on X;
then X c= dom f;
hence
A2: X c= dom (p(#)f) by VFUNCT_1:def 4;
now
per cases;
suppose
A3: p=0;
let r;
assume
A4: 0<r;
then consider s such that
A5: 0<s and
for x1,x2 st x1 in X & x2 in X & ||.x1-x2.||<s holds ||.f/.x1-f/.x2
.||<r by A1;
take s;
thus 0<s by A5;
let x1,x2;
assume that
A6: x1 in X and
A7: x2 in X and
||.x1-x2.||<s;
||.(p(#)f)/.x1-(p(#)f)/.x2.|| = ||.p*(f/.x1)-(p(#)f)/.x2.|| by A2,A6,
VFUNCT_1:def 4
.= ||.0.T -(p(#)f)/.x2.|| by A3,RLVECT_1:10
.= ||.0.T - p*(f/.x2).|| by A2,A7,VFUNCT_1:def 4
.= ||.0.T - 0.T.|| by A3,RLVECT_1:10
.= ||.0.T .|| by RLVECT_1:13
.= 0 by NORMSP_0:def 6;
hence ||.(p(#)f)/.x1-(p(#)f)/.x2.|| <r by A4;
end;
suppose
A8: p<>0;
then
A9: 0 <> |.p.| by COMPLEX1:47;
let r;
A10: 0<|.p.| by A8,COMPLEX1:47;
assume 0<r;
then 0 < r/|.p.| by A10,XREAL_1:139;
then consider s such that
A11: 0<s and
A12: for x1,x2 st x1 in X & x2 in X & ||.x1-x2.||<s holds ||.f/.x1-f
/.x2 .||<r/|.p.| by A1;
take s;
thus 0<s by A11;
let x1,x2;
assume that
A13: x1 in X and
A14: x2 in X and
A15: ||.x1-x2.||<s;
A16: ||.(p(#)f)/.x1-(p(#)f)/.x2.|| = ||.p*(f/.x1)-(p(#)f)/.x2.|| by A2,A13,
VFUNCT_1:def 4
.= ||.p*(f/.x1) - p*(f/.x2).|| by A2,A14,VFUNCT_1:def 4
.= ||.p*(f/.x1 - f/.x2).|| by RLVECT_1:34
.= |.p.|*||.f/.x1 - f/.x2.|| by NORMSP_1:def 1;
|.p.|*||.f/.x1-f/.x2.||<r/|.p.|*|.p.| by A10,A12,A13,A14,A15,
XREAL_1:68;
hence ||.(p(#)f)/.x1-(p(#)f)/.x2.|| <r by A9,A16,XCMPLX_1:87;
end;
end;
hence thesis;
end;
theorem
f is_uniformly_continuous_on X implies -f is_uniformly_continuous_on X
proof
A1: -f = (-1)(#)f by VFUNCT_1:23;
assume f is_uniformly_continuous_on X;
hence thesis by A1,Th4;
end;
theorem
f is_uniformly_continuous_on X implies ||.f .|| is_uniformly_continuous_on X
proof
assume
A1: f is_uniformly_continuous_on X;
then X c= dom f;
hence
A2: X c= dom (||.f.||) by NORMSP_0:def 3;
let r;
assume 0<r;
then consider s such that
A3: 0<s and
A4: for x1,x2 st x1 in X & x2 in X & ||.x1-x2.||<s holds ||.f/.x1-f/.x2
.||<r by A1;
take s;
thus 0<s by A3;
let x1,x2;
assume that
A5: x1 in X and
A6: x2 in X and
A7: ||.x1-x2.||<s;
|.(||.f.||)/.x1-(||.f.||)/.x2.| =|.(||.f.||).x1-(||.f.||)/.x2.| by A2,A5,
PARTFUN1:def 6
.=|.(||.f.||).x1-(||.f.||).x2.| by A2,A6,PARTFUN1:def 6
.= |.||.f/.x1.||-(||.f.||).x2.| by A2,A5,NORMSP_0:def 3
.= |.||.f/.x1.|| - ||.f/.x2.||.| by A2,A6,NORMSP_0:def 3;
then
A8: |.(||.f.||)/.x1-(||.f.||)/.x2.| <= ||.f/.x1-f/.x2.|| by NORMSP_1:9;
||.f/.x1-f/.x2.||<r by A4,A5,A6,A7;
hence thesis by A8,XXREAL_0:2;
end;
theorem Th7:
f is_uniformly_continuous_on X implies f is_continuous_on X
proof
assume
A1: f is_uniformly_continuous_on X;
A2: now
let x0;
let r be Real;
assume that
A3: x0 in X and
A4: 0<r;
consider s be Real such that
A5: 0<s and
A6: for x1,x2 st x1 in X & x2 in X & ||.x1 -x2.|| < s holds ||.f/.x1 -
f /.x2.||< r by A1,A4;
take s;
thus 0<s by A5;
let x1;
assume x1 in X & ||.x1-x0.|| < s;
hence ||.f/.x1 - f/.x0.|| < r by A3,A6;
end;
X c= dom f by A1;
hence thesis by A2,NFCONT_1:19;
end;
theorem Th8:
for f be PartFunc of the carrier of S, REAL st f
is_uniformly_continuous_on X holds f is_continuous_on X
proof
let f be PartFunc of the carrier of S, REAL;
assume
A1: f is_uniformly_continuous_on X;
A2: now
let x0;
let r be Real;
assume that
A3: x0 in X and
A4: 0<r;
consider s be Real such that
A5: 0<s and
A6: for x1,x2 st x1 in X & x2 in X & ||.x1 -x2.|| < s holds |.f/.x1
- f/.x2.|< r by A1,A4;
take s;
thus 0<s by A5;
let x1;
assume x1 in X & ||.x1-x0.|| < s;
hence |.f/.x1 - f/.x0.| < r by A3,A6;
end;
X c= dom f by A1;
hence thesis by A2,NFCONT_1:20;
end;
theorem Th9:
f is_Lipschitzian_on X implies f is_uniformly_continuous_on X
proof
assume
A1: f is_Lipschitzian_on X;
hence X c= dom f by NFCONT_1:def 9;
consider r be Real such that
A2: 0<r and
A3: for x1,x2 st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
.|| by A1,NFCONT_1:def 9;
let p be Real such that
A4: 0<p;
take s=p/r;
thus 0<s by A2,A4,XREAL_1:139;
let x1,x2;
assume x1 in X & x2 in X & ||.x1 -x2.|| < s;
then r*||.x1 -x2.|| < s*r & ||.f/.x1-f/.x2.||<=r*||.x1-x2.|| by A2,A3,
XREAL_1:68;
then ||.f/.x1-f/.x2.||<p/r*r by XXREAL_0:2;
hence thesis by A2,XCMPLX_1:87;
end;
theorem
for f, Y st Y is compact & f is_continuous_on Y holds f
is_uniformly_continuous_on Y
proof
let f, Y such that
A1: Y is compact and
A2: f is_continuous_on Y;
A3: Y c= dom f by A2,NFCONT_1:def 7;
assume not thesis;
then consider r such that
A4: 0<r and
A5: for s st 0<s ex x1,x2 st x1 in Y & x2 in Y & ||.x1 -x2.|| < s & not
||.f/.x1 - f/.x2.||< r by A3;
defpred P[Nat,Point of S] means $2 in Y & ex x2 st x2 in Y & ||.
$2-x2.||<1/($1+1) & not ||.f/.($2)-f/.x2.|| < r;
A6: for n holds 0 < 1/(n+1) by XREAL_1:139;
A7: now
let n be Element of NAT;
consider x1 such that
A8: ex x2 st x1 in Y & x2 in Y & ||.x1 -x2.|| < 1/(n+1) & not ||.f/.
x1 - f/.x2.||< r by A5,A6;
take x1;
thus P[n,x1] by A8;
end;
consider s1 such that
A9: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A7);
defpred P[Nat, Point of S] means $2 in Y & ||.s1.$1-$2.|| < 1/($1
+1) & not ||.f/.(s1.$1)-f/.$2.|| < r;
A10: for n being Element of NAT ex x2 st P[n,x2] by A9;
consider s2 such that
A11: for n being Element of NAT holds P[n,s2.n] from FUNCT_2:sch 3(A10);
now
let x be object;
assume x in rng s1;
then consider n such that
A12: x=s1.n by NFCONT_1:6;
n in NAT by ORDINAL1:def 12;
hence x in Y by A9,A12;
end;
then
A13: rng s1 c= Y by TARSKI:def 3;
then consider q1 such that
A14: q1 is subsequence of s1 and
A15: q1 is convergent and
A16: (lim q1) in Y by A1,NFCONT_1:def 2;
consider Ns1 be increasing sequence of NAT such that
A17: q1=s1*Ns1 by A14,VALUED_0:def 17;
set q2 = q1 - (s1-s2)*Ns1;
A18: f|Y is_continuous_in (lim q1) by A2,A16,NFCONT_1:def 7;
now
let x be object;
assume x in rng s2;
then consider n such that
A19: x=s2.n by NFCONT_1:6;
n in NAT by ORDINAL1:def 12;
hence x in Y by A11,A19;
end;
then
A20: rng s2 c= Y by TARSKI:def 3;
now
let n be Element of NAT;
thus q2.n = (s1*Ns1).n - ((s1-s2)*Ns1).n by A17,NORMSP_1:def 3
.= s1.(Ns1.n) - ((s1-s2)*Ns1).n by FUNCT_2:15
.= s1.(Ns1.n) - (s1-s2).(Ns1.n) by FUNCT_2:15
.= s1.(Ns1.n) - (s1.(Ns1.n)-s2.(Ns1.n)) by NORMSP_1:def 3
.= (s1.(Ns1.n) - s1.(Ns1.n)) + s2.(Ns1.n) by RLVECT_1:29
.= 0.S + s2.(Ns1.n) by RLVECT_1:15
.= s2.(Ns1.n) by RLVECT_1:4
.= (s2*Ns1).n by FUNCT_2:15;
end;
then
A21: q2 = s2*Ns1 by FUNCT_2:63;
then rng q2 c= rng s2 by VALUED_0:21;
then
A22: rng q2 c= Y by A20,XBOOLE_1:1;
then rng q2 c= dom f by A3,XBOOLE_1:1;
then rng q2 c= dom f /\ Y by A22,XBOOLE_1:19;
then
A23: rng q2 c= dom (f|Y) by RELAT_1:61;
A24: now
let p be Real such that
A25: 0<p;
consider k be Nat such that
A26: p" < k by SEQ_4:3;
take k;
let m be Nat;
A27: m in NAT by ORDINAL1:def 12;
assume k <= m;
then k+1 <= m+1 by XREAL_1:6;
then 1/(m+1) <= 1/(k+1) by XREAL_1:118;
then
A28: ||.s1.m - s2.m.|| < 1/(k+1) by A11,XXREAL_0:2,A27;
k < k+1 by NAT_1:13;
then p" < k+1 by A26,XXREAL_0:2;
then 1/(k+1) < 1/p" by A25,XREAL_1:76;
then
A29: 1/(k+1) < p by XCMPLX_1:216;
||.(s1-s2).m - 0.S.|| = ||.s1.m - s2.m - 0.S.|| by NORMSP_1:def 3
.= ||.s1.m - s2.m .|| by RLVECT_1:13;
hence ||.(s1-s2).m - 0.S.|| < p by A29,A28,XXREAL_0:2;
end;
then
A30: s1-s2 is convergent by NORMSP_1:def 6;
then
A31: (s1-s2)*Ns1 is convergent by LOPBAN_3:7;
then
A32: q2 is convergent by A15,NORMSP_1:20;
rng q1 c= rng s1 by A14,VALUED_0:21;
then
A33: rng q1 c= Y by A13,XBOOLE_1:1;
then rng q1 c= dom f by A3,XBOOLE_1:1;
then rng q1 c= dom f /\ Y by A33,XBOOLE_1:19;
then
A34: rng q1 c= dom (f|Y) by RELAT_1:61;
then
A35: (f|Y)/.(lim q1)=lim((f|Y)/*q1) by A15,A18,NFCONT_1:def 5;
A36: (f|Y)/*q1 is convergent by A15,A18,A34,NFCONT_1:def 5;
lim (s1-s2) = 0.S by A24,A30,NORMSP_1:def 7;
then lim ((s1-s2)*Ns1) = 0.S by A30,LOPBAN_3:8;
then
A37: lim q2 = lim q1 - 0.S by A15,A31,NORMSP_1:26
.= lim q1 by RLVECT_1:13;
then
A38: (f|Y)/*q2 is convergent by A18,A32,A23,NFCONT_1:def 5;
then
A39: (f|Y)/*q1 - (f|Y)/*q2 is convergent by A36,NORMSP_1:20;
(f|Y)/.(lim q1) = lim ((f|Y)/*q2) by A18,A32,A37,A23,NFCONT_1:def 5;
then
A40: lim ((f|Y)/*q1 - (f|Y)/*q2) = (f|Y)/.(lim q1) - (f|Y)/.(lim q1) by A36,A35
,A38,NORMSP_1:26
.= 0.T by RLVECT_1:15;
now
let n;
reconsider r as Real;
consider k be Nat such that
A41: for m being Nat st k<=m
holds ||.((f|Y)/*q1 - (f|Y)/*q2).m-0.T .||<r by A4,A39,A40,
NORMSP_1:def 7;
A42: k in NAT by ORDINAL1:def 12;
A43: q1.k in rng q1 by NFCONT_1:6;
A44: q2.k in rng q2 by NFCONT_1:6;
||.((f|Y)/*q1 - (f|Y)/*q2).k - 0.T .|| = ||.((f|Y)/*q1 - (f|Y)/*q2).k
.|| by RLVECT_1:13
.= ||.((f|Y)/*q1).k - ((f|Y)/*q2).k.|| by NORMSP_1:def 3
.= ||.(f|Y)/.(q1.k) - ((f|Y)/*q2).k.|| by A34,FUNCT_2:109,A42
.= ||.(f|Y)/.(q1.k) - (f|Y)/.(q2.k) .|| by A23,FUNCT_2:109,A42
.= ||.f/.(q1.k) - (f|Y)/.(q2.k).|| by A34,A43,PARTFUN2:15
.= ||.f/.(q1.k) - f/.(q2.k).|| by A23,A44,PARTFUN2:15
.= ||.f/.(s1.(Ns1.k)) - f/.((s2*Ns1).k).|| by A17,A21,FUNCT_2:15,A42
.= ||.f/.(s1.(Ns1.k)) - f/.(s2.(Ns1.k)).|| by FUNCT_2:15,A42;
hence contradiction by A11,A41;
end;
hence contradiction;
end;
theorem
Y c= dom f & Y is compact & f is_uniformly_continuous_on Y implies f.:
Y is compact by Th7,NFCONT_1:32;
theorem
for f be PartFunc of the carrier of S, REAL for Y st Y <> {} & Y c=
dom f & Y is compact & f is_uniformly_continuous_on Y ex x1,x2 st x1 in Y & x2
in Y & f/.x1 = upper_bound (f.:Y) & f/.x2 = lower_bound (f.:Y) by Th8,
NFCONT_1:37;
theorem
X c= dom f & f|X is constant implies f is_uniformly_continuous_on X by Th9,
NFCONT_1:43;
begin :: Contraction Mapping Principle on Normed Linear Spaces
definition
let M be non empty NORMSTR;
let f be Function of M,M;
attr f is contraction means
:Def3:
ex L being Real st 0 < L & L < 1 & for x,y being Point of M holds
||.f.x - f.y.|| <=L*||.x - y.||;
end;
registration
let M be RealNormSpace;
cluster contraction for Function of M,M;
existence
proof
set x = the Point of M;
reconsider f = (the carrier of M) --> x as Function of the carrier of M,
the carrier of M;
reconsider jd=1/2 as Real;
take f, jd;
thus 0<jd & jd<1;
let z,y be Point of M;
f.z=x & f.y=x by FUNCOP_1:7;
then
A1: ||.f.z-f.y.|| = 0 by NORMSP_1:6;
thus thesis by A1;
end;
end;
definition
let M be RealNormSpace;
mode Contraction of M is contraction Function of M,M;
end;
Lm1:
(for X be RealNormSpace for x, y be Point of X holds ||.x-y.|| = 0 iff x= y)
& (for X be RealNormSpace for x, y be Point of X holds ||.x-y.|| <> 0 iff
x <> y) &
(for X be RealNormSpace for x, y be Point of X holds ||.x-y.|| > 0
iff x <> y) & (for X be RealNormSpace for x, y be Point of X holds ||.x-y.|| =
||.y-x.||) & (for X be RealNormSpace for x, y, z be Point of X
for e be Real st
e > 0 holds ((||.x-z.|| <e/2 & ||.z-y.|| <e/2) implies ||.x-y.|| <e)) & (for X
be RealNormSpace for x,y,z be Point of X
for e be Real st e>0 holds ((||.x-z.||
<e/2 & ||.y-z.|| <e/2) implies ||.x-y.|| <e)) & (for X be RealNormSpace for x
be Point of X st
(for e be Real st e>0 holds ||.x.|| <e) holds x=0.X ) & for X
be RealNormSpace for x,y be Point of X st
(for e be Real st e>0 holds ||.x-y.||
<e) holds x=y
proof
A1: for X be RealNormSpace for x, y, z be Point of X
for e be Real st e > 0
holds ( ||.x-z.|| < e/2 & ||.z-y.|| < e/2 implies ||.x-y.|| <e)
proof
let X be RealNormSpace;
let x, y, z be Point of X;
let e be Real such that
e > 0;
assume ||.x-z.|| < e/2 & ||.z-y.|| < e/2;
then ||.x-z.|| + ||.z-y.|| < e/2 + e/2 by XREAL_1:8;
then ||.x-y.|| + (||.x-z.|| + ||.z-y.||) < (||.x-z.|| + ||.z-y.||) + e by
NORMSP_1:10,XREAL_1:8;
then ||.x-y.|| + (||.x-z.|| + ||.z-y.||) +- (||.x-z.|| + ||.z-y.||) < e +
(||.x-z.|| + ||.z-y.||) +- (||.x-z.|| + ||.z-y.||) by XREAL_1:8;
hence thesis;
end;
A2: for X be RealNormSpace for x, y, z be Point of X
for e be Real st e > 0
holds ( ||.x-z.|| < e/2 & ||.y-z.|| < e/2 implies ||.x-y.|| < e)
proof
let X be RealNormSpace;
let x, y, z be Point of X;
let e be Real such that
A3: e > 0;
assume that
A4: ||.x-z.|| < e/2 and
A5: ||.y-z.|| < e/2;
||.-(y-z).|| < e/2 by A5,NORMSP_1:2;
then ||.z-y.|| < e/2 by RLVECT_1:33;
hence thesis by A1,A3,A4;
end;
A6: for X be RealNormSpace for x, y be Point of X holds ||.x-y.|| > 0 iff x
<> y
proof
let X be RealNormSpace;
let x, y be Point of X;
0 < ||.x-y.|| implies x-y <> 0.X by NORMSP_0:def 6;
hence 0 < ||.x-y.|| implies x <> y by RLVECT_1:15;
now
assume x <> y;
then 0 <> ||.x-y.|| by NORMSP_1:11;
hence 0 < ||.x-y.||;
end;
hence thesis;
end;
A7: for X be RealNormSpace for x, y be Point of X holds ||.x-y.|| = ||.y-x .||
proof
let X be RealNormSpace;
let x, y be Point of X;
thus ||.x-y.|| = ||.-(x-y).|| by NORMSP_1:2
.= ||.y-x.|| by RLVECT_1:33;
end;
A8: for X be RealNormSpace for x be Point of X st
(for e be Real st e>0
holds ||.x.|| <e) holds x=0.X
proof
let X be RealNormSpace;
let x be Point of X such that
A9: for e be Real st e > 0 holds ||.x.|| <e;
now
assume x<>0.X;
then 0<> ||.x.|| by NORMSP_0:def 5;
then 0< ||.x.||;
hence contradiction by A9;
end;
hence thesis;
end;
thus thesis by A6,A7,A1,A2,A8;
end;
Lm2: for K, L, e be Real st 0 < K & K < 1 & 0 < e
ex n be Nat st |.L * (K to_power n ).| < e
proof
let K, L, e be Real such that
A1: 0 < K & K < 1 and
A2: 0 < e;
deffunc P(Nat)=K to_power ($1+1);
consider rseq be Real_Sequence such that
A3: for n be Nat holds rseq.n=P(n) from SEQ_1:sch 1;
A4: L(#)rseq is convergent by A1,A3,SEQ_2:7,SERIES_1:1;
A5: lim rseq = 0 by A1,A3,SERIES_1:1;
lim ( L(#)rseq ) = L* lim rseq by A1,A3,SEQ_2:8,SERIES_1:1
.=0 by A5;
then consider n be Nat such that
A6: for m be Nat st n<=m holds |. (L(#)rseq).m-0 .| < e by A2,A4,
SEQ_2:def 7;
|. (L(#)rseq).n-0 .| < e by A6;
then |. L*rseq.n .| < e by SEQ_1:9;
then |. L*(K to_power (n+1)) .| < e by A3;
hence thesis;
end;
theorem Th14:
for X be RealBanachSpace
for f be Function of X, X st f is Contraction of X
ex xp be Point of X st f.xp=xp & for x be Point of X st f.x=x
holds xp=x
proof
let X be RealBanachSpace;
set x0 = the Element of X;
let f be Function of X,X;
assume f is Contraction of X;
then consider K be Real such that
A1: 0 < K and
A2: K < 1 and
A3: for x,y be Point of X holds ||.f.x - f.y.|| <=K*||.x - y.|| by Def3;
deffunc G(set,set)=f.$2;
consider g be Function such that
A4: dom g = NAT & g.0 = x0 & for n being Nat holds g.(n+1) = G(n,g.n)
from NAT_1:sch 11;
defpred P[Nat] means g.$1 in the carrier of X;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A6: P[k];
g.(k+1)=f.(g.k) by A4;
hence thesis by A6,FUNCT_2:5;
end;
A7: P[0] by A4;
for n be Nat holds P[n] from NAT_1:sch 2(A7,A5);
then for n be object st n in NAT holds g.n in the carrier of X;
then reconsider g as sequence of X by A4,FUNCT_2:3;
A8: now
let n be Nat;
||. (g^\1).n - f. (lim g) .|| = ||. g.(n+1) - f. (lim g) .|| by NAT_1:def 3
.= ||. f.(g.n)- f. (lim g) .|| by A4;
hence ||. (g^\1).n - f. (lim g) .|| <= K* ||. g.n - lim g .|| by A3;
end;
A9: for n be Nat holds ||.g.(n+1) - g.n .|| <= ||. g.1-g.0 .||*
(K to_power n )
proof
defpred P[Nat] means
||.g.($1+1) - g.($1) .|| <= ||. g.1-g.0 .||* (K to_power $1 );
A10: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then
A11: K* ||. g.(k+1) - g.k .|| <= K*( ||. g.1-g.0 .||* (K to_power k ) )
by A1,XREAL_1:64;
||.f.(g.(k+1)) - f.(g.k) .|| <= K* ||. g.(k+1) - g.k .|| by A3;
then
||.f.(g.(k+1)) - f.(g.k) .|| <=||. g.1-g.0 .||*(K* (K to_power k ))
by A11,XXREAL_0:2;
then
A12: ||.f.(g.(k+1)) - f.(g.k) .|| <=||. g.1-g.0 .||*((K to_power 1)* (K
to_power k )) by POWER:25;
g.(k+1) =f.(g.k) by A4;
then
||.g.((k+1)+1) - g.(k+1) .|| = ||.f.(g.(k+1)) - f.(g.k) .|| by A4;
hence thesis by A1,A12,POWER:27;
end;
||.g.(0+1) - g.(0) .|| = ||. g.1-g.0 .|| * 1
.= ||. g.1-g.0 .|| * (K to_power 0 ) by POWER:24;
then
A13: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A13,A10);
hence thesis;
end;
A14: for k, n be Nat holds ||.g.(n+k) - g.n .|| <= ||. g.1-g.0
.||* ((K to_power n - K to_power (n+k)) /(1-K))
proof
defpred P[Nat] means
for n be Nat holds ||.g.(n+$1)
- g.n .|| <= ||. g.1-g.0 .||*( (K to_power n-K to_power (n+$1)) /(1-K));
A15: now
let k be Nat such that
A16: P[k];
now
let n be Nat;
1- K <> 0 by A2;
then
A17: ||. g.1-g.0 .||*((K to_power n - K to_power (n+k)) /(1-K)) + ||.
g.1-g.0 .||*(K to_power (n+k)) = ||. g.1-g.0 .||*((K to_power n - K to_power (n
+k))/(1-K)) + ||. g.1-g.0 .||*(K to_power (n+k))*(1-K)/(1-K) by XCMPLX_1:89
.= ||. g.1-g.0 .||*((K to_power n - K to_power (n+k))/(1-K)) + ||.
g.1-g.0 .||*((K to_power (n+k))*(1-K))/(1-K)
.= ||. g.1-g.0 .||*((K to_power n - K to_power (n+k))/(1-K)) + ||.
g.1-g.0 .||*((K to_power (n+k)*(1-K))/(1-K)) by XCMPLX_1:74
.= ||. g.1-g.0 .||*(((K to_power n - K to_power (n+k))/(1-K)) + ((
K to_power (n+k)*(1-K))/(1-K)))
.= ||. g.1-g.0 .||*( ((K to_power n - K to_power (n+k)) +(K
to_power (n+k)*(1-K)))/(1-K) ) by XCMPLX_1:62
.= ||. g.1-g.0 .||*((K to_power n- K*K to_power (n+k)) /(1-K))
.= ||. g.1-g.0 .||*((K to_power n- (K to_power 1) *K to_power (n+k
)) /(1-K)) by POWER:25
.= ||. g.1-g.0 .||*((K to_power n - K to_power (n+k+1))/(1-K)) by A1,
POWER:27;
||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .||* ((K to_power n - K
to_power (n+k)) / (1-K)) & ||.g.((n+k)+1) - g.(n+k) .|| <= ||. g.1-g.0 .||* (K
to_power (n+k)) by A9,A16;
then
||.g.(n+(k+1)) - g.n .|| <= ||.g.(n+(k+1)) - g.(n+k) .|| + ||.g.(
n+k) - g.n .|| & ||.g.(n+(k+1)) - g.(n+k) .|| + ||.g.(n+k) - g.n .|| <= ||. g.1
-g.0 .||* (K to_power (n+k)) + ||. g.1-g.0 .|| * ((K to_power n - K to_power (n
+k)) /(1-K )) by NORMSP_1:10,XREAL_1:7;
hence ||.g.(n+(k+1)) - g.n .|| <= ||. g.1-g.0 .||*((K to_power n - K
to_power (n+(k+1)))/(1-K)) by A17,XXREAL_0:2;
end;
hence P[k+1];
end;
now
let n be Nat;
||.g.(n+0) - g.n .||= ||.0.X.|| by RLVECT_1:15
.=0 by NORMSP_1:1;
hence ||.g.(n+0) - g.n .|| <= ||. g.1-g.0 .||* ((K to_power n-K to_power
(n+0))/(1-K));
end;
then
A18: P[0];
for k be Nat holds P[k] from NAT_1: sch 2(A18,A15);
hence thesis;
end;
A19: for k,n be Nat holds ||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .||
* (K to_power n /(1-K))
proof
let k be Nat;
now
let n be Nat;
K to_power (n+k) > 0 by A1,POWER:34;
then
A20: K to_power n - K to_power (n+k) <= K to_power n - 0 by XREAL_1:13;
1-K > 1-1 by A2,XREAL_1:15;
then
(K to_power n - K to_power (n+k)) /(1-K) <= (( K to_power n ) /(1-K
)) by A20,XREAL_1:72;
then
A21: ||. g.1-g.0 .||*( (K to_power n - K to_power (n+k)) /(1-K) ) <= ||.
g.1-g.0 .||*( ( K to_power n ) /(1-K) ) by XREAL_1:64;
||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .||*( (K to_power n - K
to_power (n+k)) /(1-K)) by A14;
hence
||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .||* ((K to_power n) /(1-K)) by A21,
XXREAL_0:2;
end;
hence thesis;
end;
now
let e be Real such that
A22: e >0;
e/2 > 0 by A22,XREAL_1:215;
then consider n be Nat such that
A23: |. ||. g.1-g.0 .||/(1-K)* (K to_power n) .| < e/2 by A1,A2,Lm2;
reconsider nn=n+1 as Nat;
take nn;
||. g.1-g.0 .||/(1-K)* (K to_power n) <= |. ||. g.1-g.0 .||/(1-K)*
(K to_power n) .| by ABSVALUE:4;
then ||. g.1-g.0 .||/(1-K)* (K to_power n) < e/2 by A23,XXREAL_0:2;
then
A24: ||. g.1-g.0 .|| *( (K to_power n)/(1-K)) < e/2 by XCMPLX_1:75;
now
let m,l be Nat such that
A25: nn <= m and
A26: nn <= l;
n < m by A25,NAT_1:13;
then consider k1 being Nat such that
A27: n+k1 =m by NAT_1:10;
n < l by A26,NAT_1:13;
then consider k2 being Nat such that
A28: n+k2 =l by NAT_1:10;
reconsider k2 as Nat;
||.g.(n+k2) - g.n .|| <= ||. g.1-g.0 .||*( (K to_power n) /(1-K) )
by A19;
then
A29: ||.g.l - g.n .|| < e/2 by A24,A28,XXREAL_0:2;
reconsider k1 as Nat;
||.g.(n+k1) - g.n .|| <= ||. g.1-g.0 .||*( (K to_power n) /(1-K)) by A19;
then ||.g.m - g.n .|| < e/2 by A24,A27,XXREAL_0:2;
hence ||.g.l - g.m .|| < e by A22,A29,Lm1;
end;
hence
for n, m be Nat st n >= nn & m >= nn holds ||.g.n - g.m.|| < e;
end;
then g is Cauchy_sequence_by_Norm by RSSPACE3:8;
then
A30: g is convergent by LOPBAN_1:def 15;
then
A31: K(#)||. g - lim g .|| is convergent by NORMSP_1:24,SEQ_2:7;
A32: lim (K(#)(||.g - lim g.||)) =K*lim ||.(g - lim g).|| by A30,NORMSP_1:24
,SEQ_2:8
.=K*0 by A30,NORMSP_1:24
.=0;
A33: for e be Real st e >0
ex n be Nat st for m be Nat
st n<=m holds ||. (g^\1).m - f. (lim g) .|| <e
proof
let e be Real;
assume e >0;
then consider n be Nat such that
A34: for m be Nat st n<=m holds |. (K(#)||. g - lim g .||
).m-0 .| <e by A31,A32,SEQ_2:def 7;
take n;
now
let m be Nat;
assume n<=m;
then |. (K(#)||. g - lim g .||).m-0 .|<e by A34;
then |. K*||. g - lim g .||.m.| < e by SEQ_1:9;
then |. K*||. (g - lim g).m .||.| < e by NORMSP_0:def 4;
then
A35: |. K*||. g.m - lim g .||.| < e by NORMSP_1:def 4;
K*||. g.m - lim g .|| <=|. K*||. g.m - lim g .||.| by ABSVALUE:4;
then
A36: K*||. g.m - lim g .|| < e by A35,XXREAL_0:2;
||. (g^\1).m - f. (lim g) .|| <= K* ||. g.m - lim g .|| by A8;
hence ||. (g^\1).m - f. (lim g) .|| < e by A36,XXREAL_0:2;
end;
hence thesis;
end;
take xp=lim g;
A37: g^\1 is convergent & lim (g^\1) = lim g by A30,LOPBAN_3:9;
then
A38: lim g = f. (lim g) by A33,NORMSP_1:def 7;
now
let x be Point of X such that
A39: f.x=x;
A40: for k be Nat holds ||.x-xp.|| <= ||.x-xp.||*(K to_power k)
proof
defpred P[Nat] means
||.x-xp .|| <= ||.x-xp.||*(K to_power $1);
A41: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then
A42: K* ||. x-xp .|| <= K*( ||.x-xp.||*(K to_power k) ) by A1,XREAL_1:64;
||.f.x - f.xp .|| <= K* ||. x-xp .|| by A3;
then ||.f.x - f.xp .|| <= ||. x-xp .||*(K* (K to_power k )) by A42,
XXREAL_0:2;
then ||.f.x - f.xp .|| <= ||. x-xp .||*((K to_power 1)* (K to_power k
)) by POWER:25;
hence thesis by A1,A38,A39,POWER:27;
end;
||.x-xp .|| = ||. x-xp .|| * 1
.= ||. x-xp .|| * (K to_power 0 ) by POWER:24;
then
A43: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A43,A41);
hence thesis;
end;
for e be Real st 0 <e holds ||.x-xp.|| < e
proof
let e be Real;
assume 0 < e;
then consider n be Nat such that
A44: |.||.x-xp.||*(K to_power n) .| < e by A1,A2,Lm2;
||.x-xp.||*(K to_power n) <=|.||.x-xp.||*(K to_power n).| by ABSVALUE:4;
then
A45: ||.x-xp.||*(K to_power n) <e by A44,XXREAL_0:2;
||.x-xp.|| <= ||.x-xp.||*(K to_power n) by A40;
hence thesis by A45,XXREAL_0:2;
end;
hence x=xp by Lm1;
end;
hence thesis by A37,A33,NORMSP_1:def 7;
end;
theorem
for X be RealBanachSpace for f be Function of X,X st
ex n0 be Nat st iter(f,n0) is Contraction of X
ex xp be Point of X st f.xp=xp &
for x be Point of X st f.x=x holds xp=x
proof
let X be RealBanachSpace;
let f be Function of X, X;
given n0 be Nat such that
A1: iter(f,n0) is Contraction of X;
consider xp be Point of X such that
A2: (iter(f,n0)).xp=xp and
A3: for x be Point of X st iter(f,n0).x=x holds xp=x by A1,Th14;
A4: now
let x be Point of X such that
A5: f.x=x;
for n be Nat holds (iter(f,n)).x=x
proof
defpred P[Nat] means (iter(f,$1)).x=x;
A6: now
let n be Nat such that
A7: P[n];
(iter(f,n+1)).x =(f*iter(f,n)).x by FUNCT_7:71
.=x by A5,A7,FUNCT_2:15;
hence P[n+1];
end;
(iter(f,0)).x=(id the carrier of X).x by FUNCT_7:84
.=x;
then
A8: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A8,A6);
hence thesis;
end;
then (iter(f,n0)).x=x;
hence xp=x by A3;
end;
(iter(f,n0)).(f.xp) =(iter(f,n0)*f).xp by FUNCT_2:15
.=(iter(f,n0+1)).xp by FUNCT_7:69
.=(f*iter(f,n0)).xp by FUNCT_7:71
.=f.xp by A2,FUNCT_2:15;
then f.xp=xp by A3;
hence thesis by A4;
end;
theorem
for K, L, e be Real st 0 < K & K < 1 & 0 < e
ex n be Nat st |.L * (K to_power n).| < e by Lm2;