:: Uniform Continuity of Functions on Normed Complex Linear Spaces
:: by Noboru Endou
::
:: Received October 6, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

definition
let X be set ;
let CNS1, CNS2 be ComplexNormSpace;
let f be PartFunc of CNS1,CNS2;
predf is_uniformly_continuous_on X means :Def1: :: NCFCONT2:def 1
( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of CNS1 st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) );
end;

:: deftheorem Def1 defines is_uniformly_continuous_on NCFCONT2:def_1_:_
 for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 holds
( f is_uniformly_continuous_on X iff ( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of CNS1 st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );

definition
let X be set ;
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let f be PartFunc of CNS,RNS;
predf is_uniformly_continuous_on X means :Def2: :: NCFCONT2:def 2
( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) );
end;

:: deftheorem Def2 defines is_uniformly_continuous_on NCFCONT2:def_2_:_
 for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS holds
( f is_uniformly_continuous_on X iff ( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );

definition
let X be set ;
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let f be PartFunc of RNS,CNS;
predf is_uniformly_continuous_on X means :Def3: :: NCFCONT2:def 3
( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of RNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) );
end;

:: deftheorem Def3 defines is_uniformly_continuous_on NCFCONT2:def_3_:_
 for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS holds
( f is_uniformly_continuous_on X iff ( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of RNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );

definition
let X be set ;
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,COMPLEX;
predf is_uniformly_continuous_on X means :Def4: :: NCFCONT2:def 4
( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) );
end;

:: deftheorem Def4 defines is_uniformly_continuous_on NCFCONT2:def_4_:_
 for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX holds
( f is_uniformly_continuous_on X iff ( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) ) );

definition
let X be set ;
let CNS be ComplexNormSpace;
let f be PartFunc of the carrier of CNS,REAL;
predf is_uniformly_continuous_on X means :Def5: :: NCFCONT2:def 5
( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
abs ((f /. x1) - (f /. x2)) < r ) ) ) );
end;

:: deftheorem Def5 defines is_uniformly_continuous_on NCFCONT2:def_5_:_
 for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL holds
( f is_uniformly_continuous_on X iff ( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of CNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
abs ((f /. x1) - (f /. x2)) < r ) ) ) ) );

definition
let X be set ;
let RNS be RealNormSpace;
let f be PartFunc of the carrier of RNS,COMPLEX;
predf is_uniformly_continuous_on X means :Def6: :: NCFCONT2:def 6
( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of RNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) );
end;

:: deftheorem Def6 defines is_uniformly_continuous_on NCFCONT2:def_6_:_
 for X being set
for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX holds
( f is_uniformly_continuous_on X iff ( X c= dom f &amp; ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Point of RNS st x1 in X &amp; x2 in X &amp; ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) ) );

theorem Th1: :: NCFCONT2:1
for X, X1 being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X &amp; X1 c= X holds
f is_uniformly_continuous_on X1
proofend;

theorem Th2: :: NCFCONT2:2
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X &amp; X1 c= X holds
f is_uniformly_continuous_on X1
proofend;

theorem Th3: :: NCFCONT2:3
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X &amp; X1 c= X holds
f is_uniformly_continuous_on X1
proofend;

theorem :: NCFCONT2:4
for X, X1 being set
for CNS1, CNS2 being ComplexNormSpace
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X &amp; f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
proofend;

theorem :: NCFCONT2:5
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X &amp; f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
proofend;

theorem :: NCFCONT2:6
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X &amp; f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1
proofend;

theorem :: NCFCONT2:7
for X, X1 being set
for CNS1, CNS2 being ComplexNormSpace
for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X &amp; f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
proofend;

theorem :: NCFCONT2:8
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X &amp; f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
proofend;

theorem :: NCFCONT2:9
for X, X1 being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X &amp; f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1
proofend;

theorem Th10: :: NCFCONT2:10
for X being set
for z being Complex
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
proofend;

theorem Th11: :: NCFCONT2:11
for X being set
for r being Real
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
r (#) f is_uniformly_continuous_on X
proofend;

theorem Th12: :: NCFCONT2:12
for X being set
for z being Complex
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
z (#) f is_uniformly_continuous_on X
proofend;

theorem :: NCFCONT2:13
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
proofend;

theorem :: NCFCONT2:14
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
proofend;

theorem :: NCFCONT2:15
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X
proofend;

theorem :: NCFCONT2:16
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
proofend;

theorem :: NCFCONT2:17
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
proofend;

theorem :: NCFCONT2:18
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
||.f.|| is_uniformly_continuous_on X
proofend;

theorem Th19: :: NCFCONT2:19
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
f is_continuous_on X
proofend;

theorem Th20: :: NCFCONT2:20
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
proofend;

theorem Th21: :: NCFCONT2:21
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
f is_continuous_on X
proofend;

theorem :: NCFCONT2:22
for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX st f is_uniformly_continuous_on X holds
f is_continuous_on X
proofend;

theorem Th23: :: NCFCONT2:23
for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL st f is_uniformly_continuous_on X holds
f is_continuous_on X
proofend;

theorem :: NCFCONT2:24
for X being set
for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX st f is_uniformly_continuous_on X holds
f is_continuous_on X
proofend;

theorem Th25: :: NCFCONT2:25
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
proofend;

theorem Th26: :: NCFCONT2:26
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
proofend;

theorem Th27: :: NCFCONT2:27
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
proofend;

theorem :: NCFCONT2:28
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for Y being Subset of CNS1 st Y is compact &amp; f is_continuous_on Y holds
f is_uniformly_continuous_on Y
proofend;

theorem :: NCFCONT2:29
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS
for Y being Subset of CNS st Y is compact &amp; f is_continuous_on Y holds
f is_uniformly_continuous_on Y
proofend;

theorem :: NCFCONT2:30
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y is compact &amp; f is_continuous_on Y holds
f is_uniformly_continuous_on Y
proofend;

theorem :: NCFCONT2:31
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2
for Y being Subset of CNS1 st Y c= dom f &amp; Y is compact &amp; f is_uniformly_continuous_on Y holds
f .: Y is compact by Th19, NCFCONT1:83;

theorem :: NCFCONT2:32
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS
for Y being Subset of CNS st Y c= dom f &amp; Y is compact &amp; f is_uniformly_continuous_on Y holds
f .: Y is compact by Th20, NCFCONT1:84;

theorem :: NCFCONT2:33
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS
for Y being Subset of RNS st Y c= dom f &amp; Y is compact &amp; f is_uniformly_continuous_on Y holds
f .: Y is compact by Th21, NCFCONT1:85;

theorem :: NCFCONT2:34
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,REAL
for Y being Subset of CNS st Y <> {} &amp; Y c= dom f &amp; Y is compact &amp; f is_uniformly_continuous_on Y holds
ex x1, x2 being Point of CNS st
( x1 in Y &amp; x2 in Y &amp; f /. x1 = upper_bound (f .: Y) &amp; f /. x2 = lower_bound (f .: Y) ) by Th23, NCFCONT1:96;

theorem :: NCFCONT2:35
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 st X c= dom f &amp; f | X is constant holds
f is_uniformly_continuous_on X by Th25, NCFCONT1:112;

theorem :: NCFCONT2:36
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS st X c= dom f &amp; f | X is constant holds
f is_uniformly_continuous_on X by Th26, NCFCONT1:113;

theorem :: NCFCONT2:37
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS st X c= dom f &amp; f | X is constant holds
f is_uniformly_continuous_on X by Th27, NCFCONT1:114;

begin

definition
let M be non empty CNORMSTR ;
let f be Function of M,M;
attrf is contraction  means :Def7: :: NCFCONT2:def 7
 ex L being Real st
( 0 < L &amp; L < 1 &amp; ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) );
end;

:: deftheorem Def7 defines contraction NCFCONT2:def_7_:_
 for M being non empty CNORMSTR
for f being Function of M,M holds
( f is contraction iff ex L being Real st
( 0 < L &amp; L < 1 &amp; ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) ) );

registration
let M be ComplexBanachSpace;
cluster non empty Relation-like the carrier of M -defined the carrier of M -valued Function-like total quasi_total contraction for Element of K6(K7( the carrier of M, the carrier of M));
existence
 ex b1 being Function of M,M st b1 is contraction
proofend;
end;

definition
let M be ComplexBanachSpace;
mode Contraction of M is contraction Function of M,M;
end;

theorem :: NCFCONT2:38
for X being ComplexNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y )
proofend;

theorem :: NCFCONT2:39
for X being ComplexNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).||
proofend;

Lm1:  for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 &amp; ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
proofend;

Lm2:  for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 &amp; ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
proofend;

Lm3:  for X being ComplexNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
proofend;

Lm4:  for X being ComplexNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
proofend;

theorem Th40: :: NCFCONT2:40
for X being ComplexBanachSpace
for f being Function of X,X st f is Contraction of X holds
ex xp being Point of X st
( f . xp = xp &amp; ( for x being Point of X st f . x = x holds
xp = x ) )
proofend;

theorem :: NCFCONT2:41
for X being ComplexBanachSpace
for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is Contraction of X holds
ex xp being Point of X st
( f . xp = xp &amp; ( for x being Point of X st f . x = x holds
xp = x ) )
proofend;