:: Uniform Continuity of Functions on Normed Complex Linear Spaces :: by Noboru Endou :: :: Received October 6, 2004 :: Copyright (c) 2004-2012 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, REAL_1, CFUNCT_1, NORMSP_1, CLVECT_1, PARTFUN1, NFCONT_2, TARSKI, RELAT_1, CARD_1, ARYTM_3, PRE_TOPC, ARYTM_1, STRUCT_0, COMPLEX1, XBOOLE_0, XXREAL_0, VALUED_1, SUPINF_2, FUNCT_1, CFCONT_1, NFCONT_1, SUBSET_1, RCOMP_1, NAT_1, VALUED_0, SEQ_2, ORDINAL2, FCONT_1, FUNCT_2, SEQ_4, CLOPBAN1, ALI2, FUNCOP_1, POWER, RSSPACE3, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PRE_TOPC, VALUED_0, STRUCT_0, RLVECT_1, FUNCOP_1, VALUED_1, SEQ_2, SEQ_4, FUNCT_7, VFUNCT_1, SQUARE_1, POWER, CFUNCT_1, VFUNCT_2, NORMSP_0, NORMSP_1, CLVECT_1, NFCONT_1, CLOPBAN1, NFCONT_2, NCFCONT1, CSSPACE3; constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_2, SEQ_4, POWER, FUNCT_7, CSSPACE3, NFCONT_1, NFCONT_2, CLOPBAN3, VFUNCT_2, NCFCONT1, SEQ_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, FUNCT_7, CLVECT_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions RLVECT_1; theorems TARSKI, ABSVALUE, XBOOLE_1, RLVECT_1, XCMPLX_1, SEQ_2, NAT_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, SEQ_4, NORMSP_1, LOPBAN_3, PARTFUN2, CLVECT_1, CLOPBAN3, VFUNCT_2, NFCONT_1, CLOPBAN1, COMPLEX1, NCFCONT1, NFCONT_2, FUNCOP_1, POWER, CSSPACE3, FUNCT_7, SEQ_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, VALUED_0, NORMSP_0; schemes FUNCT_2, NAT_1; begin :: Uniform Continuity of Functions on Real and Complex Normed Linear Spaces reserve X,X1 for set, r,s for Real, z for Complex, RNS for RealNormSpace, CNS, CNS1,CNS2 for ComplexNormSpace; definition let X be set; let CNS1,CNS2 be ComplexNormSpace; let f be PartFunc of CNS1,CNS2; pred f is_uniformly_continuous_on X means :Def1: X c= dom f & for r st 0 < r ex s st 0 < s & for x1,x2 be Point of CNS1 st x1 in X & x2 in X & ||.x1 - x2.|| < s holds ||. f/.x1 - f/.x2 .|| < r; end; definition let X be set; let RNS be RealNormSpace; let CNS be ComplexNormSpace; let f be PartFunc of CNS,RNS; pred f is_uniformly_continuous_on X means :Def2: X c= dom f & for r st 0 < r ex s st 0 < s & for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1 - x2.|| < s holds ||. f/.x1 - f/.x2 .|| < r; end; definition let X be set; let RNS be RealNormSpace; let CNS be ComplexNormSpace; let f be PartFunc of RNS,CNS; pred f is_uniformly_continuous_on X means :Def3: X c= dom f & for r st 0 < r ex s st 0 < s & for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1 - x2.|| < s holds ||. f/.x1 - f/.x2 .|| < r; end; definition let X be set; let CNS be ComplexNormSpace; let f be PartFunc of the carrier of CNS,COMPLEX; pred f is_uniformly_continuous_on X means :Def4: X c= dom f & for r st 0 < r ex s st 0 < s & for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1 - x2.|| < s holds |.(f/.x1 - f/.x2).| < r; end; definition let X be set; let CNS be ComplexNormSpace; let f be PartFunc of the carrier of CNS,REAL; pred f is_uniformly_continuous_on X means :Def5: X c= dom f & for r st 0 < r ex s st 0 < s & for x1,x2 be Point of CNS st x1 in X & x2 in X & ||.x1 - x2.|| < s holds abs(f/.x1 - f/.x2) < r; end; definition let X be set; let RNS be RealNormSpace; let f be PartFunc of the carrier of RNS,COMPLEX; pred f is_uniformly_continuous_on X means :Def6: X c= dom f & for r st 0 < r ex s st 0 < s & for x1,x2 be Point of RNS st x1 in X & x2 in X & ||.x1 - x2.|| < s holds |.(f/.x1 - f/.x2).| < r; end; theorem Th1: for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X & X1 c= X holds f is_uniformly_continuous_on X1 proof let f be PartFunc of CNS1,CNS2; assume that A1: f is_uniformly_continuous_on X and A2: X1 c= X; X c= dom f by A1,Def1; 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 be Point of CNS1 st x1 in X & x2 in X & ||.x1-x2.|| < s holds ||.f/.x1-f/.x2.||0; let r; A9: 0<|.z.| by A8,COMPLEX1:47; assume 00; let p be Real; A9: 00; let r; A9: 0<|.z.| by A8,COMPLEX1:47; assume 0 {} & Y c= dom f & Y is compact & f is_uniformly_continuous_on Y ex x1,x2 be Point of CNS st x1 in Y & x2 in Y & f/.x1 = upper_bound (f.:Y) & f/.x2 = lower_bound (f.:Y) by Th23,NCFCONT1:96; theorem for f be PartFunc of CNS1,CNS2 st X c= dom f & f|X is constant holds f is_uniformly_continuous_on X by Th25,NCFCONT1:112; theorem for f be PartFunc of CNS,RNS st X c= dom f & f|X is constant holds f is_uniformly_continuous_on X by Th26,NCFCONT1:113; theorem for f be PartFunc of RNS,CNS st X c= dom f & f|X is constant holds f is_uniformly_continuous_on X by Th27,NCFCONT1:114; begin :: Contraction Mapping Principle on Normed Complex Linear Spaces definition let M be non empty CNORMSTR; let f be Function of M,M; attr f is contraction means :Def7: 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 ComplexBanachSpace; 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; take f, 1/2; thus 0<1/2 & 1/2<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 CLVECT_1:107; ||.z-y.||>=0 by CLVECT_1:105; hence thesis by A1; end; end; definition let M be ComplexBanachSpace; mode Contraction of M is contraction Function of M,M; end; theorem for X be ComplexNormSpace, x,y be Point of X holds ||.x-y.|| > 0 iff x <> y proof let X be ComplexNormSpace; 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 CLVECT_1:112; hence 0 < ||.x-y.|| by CLVECT_1:105; end; hence thesis; end; theorem for X be ComplexNormSpace, x, y be Point of X holds ||.x-y.|| = ||.y-x .|| proof let X be ComplexNormSpace; let x, y be Point of X; thus ||.x-y.|| = ||.-(x-y).|| by CLVECT_1:103 .= ||.y-x.|| by RLVECT_1:33; end; Lm1: for X be ComplexNormSpace, x,y,z be Point of X, e be Real holds ( ||.x-z .|| 0 holds ||.x.|| 0 holds ||.x.|| 0.X; then 0 <> ||.x.|| by NORMSP_0:def 5; then 0 < ||.x.|| by CLVECT_1:105; hence contradiction by A1; end; hence thesis; end; Lm4: for X be ComplexNormSpace, x,y be Point of X st (for e be Real st e>0 holds ||.x-y.|| 0 holds ||.x-y.|| 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) + (1*K to_power (n+k) - K*K to_power (n+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 CLVECT_1:111,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 Element of NAT; ||.g.(n+0) - g.n .|| = ||.0.X.|| by RLVECT_1:15 .= 0 by CLVECT_1:102; 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 Element of NAT holds P[k] from NAT_1:sch 1(A18,A15); hence thesis; end; A19: for k,n be Element of NAT holds ||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .|| * (K to_power n/(1-K)) proof let k be Element of NAT; now let n be Element of NAT; A20: 0 <= ||. g.1-g.0 .|| by CLVECT_1:105; K to_power (n+k) > 0 by A1,POWER:34; then A21: 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 A21,XREAL_1:72; then A22: ||. 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 A20,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 A22, XXREAL_0:2; end; hence thesis; end; now let e be Real such that A23: e >0; e/2 > 0 by A23,XREAL_1:215; then consider n be Element of NAT such that A24: abs( ||. g.1-g.0 .||/(1-K)* (K to_power n) ) < e/2 by A1,A2,NFCONT_2:16; take nn=n+1; ||. g.1-g.0 .||/(1-K)* (K to_power n) <= abs( ||. 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 A24,XXREAL_0:2; then A25: ||. g.1-g.0 .|| *( (K to_power n)/(1-K)) < e/2 by XCMPLX_1:75; now let m,l be Element of NAT such that A26: nn <= m and A27: nn <= l; n < m by A26,NAT_1:13; then consider k1 being Nat such that A28: n+k1 =m by NAT_1:10; n < l by A27,NAT_1:13; then consider k2 being Nat such that A29: n+k2 =l by NAT_1:10; reconsider k2 as Element of NAT by ORDINAL1:def 12; ||.g.(n+k2) - g.n .|| <= ||. g.1-g.0 .||*( (K to_power n) /(1-K) ) by A19; then A30: ||.g.l - g.n .|| < e/2 by A25,A29,XXREAL_0:2; reconsider k1 as Element of NAT by ORDINAL1:def 12; ||.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 A25,A28,XXREAL_0:2; hence ||.g.l - g.m .|| < e by A30,Lm2; end; hence for n, m be Element of NAT st n >= nn & m >= nn holds ||.g.n - g.m.|| < e; end; then g is Cauchy_sequence_by_Norm by CSSPACE3:8; then A31: g is convergent by CLOPBAN1:def 13; then A32: K(#)||. g - lim g .|| is convergent by CLVECT_1:118,SEQ_2:7; A33: lim (K(#)(||.g - lim g.||)) =K*lim ||.(g - lim g).|| by A31,CLVECT_1:118 ,SEQ_2:8 .=K*0 by A31,CLVECT_1:118 .=0; A34: for e be Real st e >0 ex n be Element of NAT st for m be Element of NAT st n<=m holds ||. (g^\1).m - f. (lim g) .|| 0; then consider n be Element of NAT such that A35: for m be Element of NAT st n<=m holds abs( (K(#)||. g - lim g .|| ).m-0) < e by A32,A33,SEQ_2:def 7; take n; now let m be Element of NAT; assume n<=m; then abs( (K(#)||. g - lim g .||).m-0)