:: Uniform Continuity of Functions on Normed Complex Linear Spaces
::  by Noboru Endou
::
:: Received October 6, 2004
:: Copyright (c) 2004-2021 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, XCMPLX_0, 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, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
      COMPLEX1, XREAL_0, REAL_1, 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, POWER, 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, 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, XCMPLX_0, NAT_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;



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
:: NCFCONT2:def 1

  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
:: NCFCONT2:def 2

  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
:: NCFCONT2:def 3

  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
:: NCFCONT2:def 4

  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
:: NCFCONT2:def 5

  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 f be PartFunc of the carrier of RNS,COMPLEX;
  pred f is_uniformly_continuous_on X means
:: NCFCONT2:def 6

  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 :: NCFCONT2:1
  for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X
  & X1 c= X holds f is_uniformly_continuous_on X1;

theorem :: NCFCONT2:2
  for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X &
  X1 c= X holds f is_uniformly_continuous_on X1;

theorem :: NCFCONT2:3
  for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X &
  X1 c= X holds f is_uniformly_continuous_on X1;

theorem :: NCFCONT2:4
  for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X
& f2 is_uniformly_continuous_on X1 holds f1+f2 is_uniformly_continuous_on X/\X1
;

theorem :: NCFCONT2:5
  for f1,f2 be PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X &
  f2 is_uniformly_continuous_on X1 holds f1+f2 is_uniformly_continuous_on X/\X1
;

theorem :: NCFCONT2:6
  for f1,f2 be PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X &
  f2 is_uniformly_continuous_on X1 holds f1+f2 is_uniformly_continuous_on X/\X1
;

theorem :: NCFCONT2:7
  for f1,f2 be PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X
& f2 is_uniformly_continuous_on X1 holds f1-f2 is_uniformly_continuous_on X/\X1
;

theorem :: NCFCONT2:8
  for f1,f2 be PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X &
  f2 is_uniformly_continuous_on X1 holds f1-f2 is_uniformly_continuous_on X/\X1
;

theorem :: NCFCONT2:9
  for f1,f2 be PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X &
  f2 is_uniformly_continuous_on X1 holds f1-f2 is_uniformly_continuous_on X/\X1
;

theorem :: NCFCONT2:10
  for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X
  holds z(#)f is_uniformly_continuous_on X;

theorem :: NCFCONT2:11
  for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X
  holds r(#)f is_uniformly_continuous_on X;

theorem :: NCFCONT2:12
  for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X
  holds z(#)f is_uniformly_continuous_on X;

theorem :: NCFCONT2:13
  for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
  -f is_uniformly_continuous_on X;

theorem :: NCFCONT2:14
  for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds -
  f is_uniformly_continuous_on X;

theorem :: NCFCONT2:15
  for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds -
  f is_uniformly_continuous_on X;

theorem :: NCFCONT2:16
  for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds
  ||.f.|| is_uniformly_continuous_on X;

theorem :: NCFCONT2:17
  for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds
  ||.f.|| is_uniformly_continuous_on X;

theorem :: NCFCONT2:18
  for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds
  ||.f.|| is_uniformly_continuous_on X;

theorem :: NCFCONT2:19
  for f be PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X
  holds f is_continuous_on X;

theorem :: NCFCONT2:20
  for f be PartFunc of CNS,RNS st f is_uniformly_continuous_on X
  holds f is_continuous_on X;

theorem :: NCFCONT2:21
  for f be PartFunc of RNS,CNS st f is_uniformly_continuous_on X
  holds f is_continuous_on X;

theorem :: NCFCONT2:22
  for f be PartFunc of the carrier of CNS, COMPLEX st f
  is_uniformly_continuous_on X holds f is_continuous_on X;

theorem :: NCFCONT2:23
  for f be PartFunc of the carrier of CNS, REAL st f
  is_uniformly_continuous_on X holds f is_continuous_on X;

theorem :: NCFCONT2:24
  for f be PartFunc of the carrier of RNS, COMPLEX st f
  is_uniformly_continuous_on X holds f is_continuous_on X;

theorem :: NCFCONT2:25
  for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds f
  is_uniformly_continuous_on X;

theorem :: NCFCONT2:26
  for f be PartFunc of CNS,RNS st f is_Lipschitzian_on X holds f
  is_uniformly_continuous_on X;

theorem :: NCFCONT2:27
  for f be PartFunc of RNS,CNS st f is_Lipschitzian_on X holds f
  is_uniformly_continuous_on X;

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

theorem :: NCFCONT2:29
  for f be PartFunc of CNS,RNS, Y be Subset of CNS st Y is compact & f
  is_continuous_on Y holds f is_uniformly_continuous_on Y;

theorem :: NCFCONT2:30
  for f be PartFunc of RNS,CNS, Y be Subset of RNS st Y is compact & f
  is_continuous_on Y holds f is_uniformly_continuous_on Y;

theorem :: NCFCONT2:31
  for f be PartFunc of CNS1,CNS2, Y be Subset of CNS1 st Y c= dom f & Y
  is compact & f is_uniformly_continuous_on Y holds f.:Y is compact;

theorem :: NCFCONT2:32
  for f be PartFunc of CNS,RNS, Y be Subset of CNS st Y c= dom f & Y is
compact & f is_uniformly_continuous_on Y holds f.:Y is compact;

theorem :: NCFCONT2:33
  for f be PartFunc of RNS,CNS, Y be Subset of RNS st Y c= dom f & Y is
compact & f is_uniformly_continuous_on Y holds f.:Y is compact;

theorem :: NCFCONT2:34
  for f be PartFunc of the carrier of CNS,REAL, Y be Subset of CNS st Y
<> {} & 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);

theorem :: NCFCONT2:35
  for f be PartFunc of CNS1,CNS2 st X c= dom f & f|X is constant holds f
  is_uniformly_continuous_on X;

theorem :: NCFCONT2:36
  for f be PartFunc of CNS,RNS st X c= dom f & f|X is constant holds f
  is_uniformly_continuous_on X;

theorem :: NCFCONT2:37
  for f be PartFunc of RNS,CNS st X c= dom f & f|X is constant holds f
  is_uniformly_continuous_on X;

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
:: NCFCONT2:def 7

    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;
end;

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

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

theorem :: NCFCONT2:39
  for X be ComplexNormSpace, x, y be Point of X holds ||.x-y.|| = ||.y-x .||;

theorem :: NCFCONT2:40
  for X be ComplexBanachSpace, 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;

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