:: Algebra of Complex Vector Valued Functions
::  by Noboru Endou
::
:: Received August 20, 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 XBOOLE_0, CLVECT_1, PARTFUN1, XCMPLX_0, SUBSET_1, ARYTM_3,
      ARYTM_1, RELAT_1, NUMBERS, VALUED_1, NORMSP_1, FUNCT_1, SUPINF_2, CARD_1,
      TARSKI, COMPLEX1, VFUNCT_1, REAL_1, XXREAL_0, XXREAL_2, RLVECT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, FUNCT_1, RELSET_1, PARTFUN1, STRUCT_0, RLVECT_1, VALUED_1,
      COMSEQ_2, COMPLEX1, NORMSP_0, CLVECT_1, XXREAL_0, VFUNCT_1;
 constructors REAL_1, COMPLEX1, CLVECT_1, VALUED_1, RELSET_1, VFUNCT_1,
      COMSEQ_2;
 registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, VALUED_0,
      RFUNCT_1, XCMPLX_0;
 requirements SUBSET, BOOLE, ARITHM, NUMERALS;


begin

reserve M for non empty set;
reserve V for ComplexNormSpace;
reserve f,f1,f2,f3 for PartFunc of M,V;
reserve z,z1,z2 for Complex;

::
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF COMPLEX NUMBERS
::

definition

  let M be non empty set;
  let V be ComplexNormSpace;
  let f1 be PartFunc of M, COMPLEX;
  let f2 be PartFunc of M, V;
  func f1(#)f2 -> PartFunc of M,V means
:: VFUNCT_2:def 1

  dom it = dom f1 /\ dom f2 &
  for c be Element of M st c in dom it holds it/.c = (f1/.c) * (f2/.c);
end;

definition

  let X be non empty set;
  let V be ComplexNormSpace;
  let f be PartFunc of X,V;
  let z be Complex;
  func z(#)f -> PartFunc of X,V means
:: VFUNCT_2:def 2

  dom it = dom f &
  for x be Element of X st x in dom it holds it/.x = z * (f/.x);
end;

theorem :: VFUNCT_2:1
  for f1 be PartFunc of M,COMPLEX, f2 be PartFunc of M,V
holds dom (f1(#)f2) \ (f1(#)f2)"{0.V} = (dom f1 \ (f1)"{0}) /\ (dom f2 \ (f2)"{
  0.V});

theorem :: VFUNCT_2:2
  (||.f.||)"{0} = f"{0.V} & (-f)"{0.V} = f"{0.V};

theorem :: VFUNCT_2:3
  z<>0c implies (z(#)f)"{0.V} = f"{0.V};

::
:: BASIC PROPERTIES OF OPERATIONS
::

theorem :: VFUNCT_2:4
  f1 + f2 = f2 + f1;

definition
  let M,V; let f1,f2;
  redefine func f1+f2;
  commutativity;
end;

theorem :: VFUNCT_2:5
  (f1 + f2) + f3 = f1 + (f2 + f3);

theorem :: VFUNCT_2:6
  for f1,f2 be PartFunc of M,COMPLEX,f3 be PartFunc of M,V
  holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3);

theorem :: VFUNCT_2:7
  for f1,f2 be PartFunc of M,COMPLEX holds
  (f1 + f2) (#) f3 = f1 (#) f3 + f2 (#) f3;

theorem :: VFUNCT_2:8
  for f3 be PartFunc of M,COMPLEX holds f3(#)(f1 + f2) = f3(#)f1 + f3(#) f2;

theorem :: VFUNCT_2:9
  for f1 be PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = z (#) f1 (#) f2;

theorem :: VFUNCT_2:10
  for f1 be PartFunc of M,COMPLEX holds z (#) (f1 (#) f2) = f1 (#) (z (#) f2);

theorem :: VFUNCT_2:11
  for f1,f2 be PartFunc of M,COMPLEX holds (f1 - f2) (#) f3 = f1(#)f3 - f2(#)f3
;

theorem :: VFUNCT_2:12
  for f3 be PartFunc of M,COMPLEX holds f3(#)f1 - f3(#)f2 = f3(#)(f1 - f2);

theorem :: VFUNCT_2:13
  z(#)(f1 + f2) = z(#)f1 + z(#)f2;

theorem :: VFUNCT_2:14
  (z1*z2)(#)f = z1(#)(z2(#)f);

theorem :: VFUNCT_2:15
  z(#)(f1 - f2) = z(#)f1 - z(#)f2;

theorem :: VFUNCT_2:16
  f1-f2 = (-1r)(#)(f2-f1);

theorem :: VFUNCT_2:17
  f1 - (f2 + f3) = f1 - f2 - f3;

theorem :: VFUNCT_2:18
  1r(#)f = f;

theorem :: VFUNCT_2:19
  f1 - (f2 - f3) = f1 - f2 + f3;

theorem :: VFUNCT_2:20
  f1 + (f2 - f3) = f1 + f2 - f3;

theorem :: VFUNCT_2:21
  for f1 be PartFunc of M,COMPLEX holds ||.f1(#)f2.|| = |.f1.|(#)||.f2 .||;

theorem :: VFUNCT_2:22
  ||.z(#)f.|| = |.z.|(#)||.f.||;

theorem :: VFUNCT_2:23
  -f = (-1r)(#)f;

theorem :: VFUNCT_2:24
  -(-f) = f;

theorem :: VFUNCT_2:25
  f1 - f2 = f1 + -f2;

theorem :: VFUNCT_2:26
  f1 - (-f2) = f1 + f2;

reserve X,Y for set;

theorem :: VFUNCT_2:27
  (f1+f2)|X = f1|X + f2|X & (f1+f2)|X = f1|X + f2 & (f1+f2)|X = f1 + f2|X;

theorem :: VFUNCT_2:28
  for f1 be PartFunc of M,COMPLEX holds (f1(#)f2)|X = f1|X (#) f2|X & (
  f1(#)f2)|X = f1|X (#) f2 & (f1(#)f2)|X = f1 (#) f2|X;

theorem :: VFUNCT_2:29
  (-f)|X = -(f|X) & (||.f.||)|X = ||.(f|X).||;

theorem :: VFUNCT_2:30
  (f1-f2)|X = f1|X - f2|X & (f1-f2)|X = f1|X - f2 &(f1-f2)|X = f1 - f2|X;

theorem :: VFUNCT_2:31
  (z(#)f)|X = z(#)(f|X);

::
:: TOTAL PARTIAL FUNCTIONS FROM A DOMAIN TO COMPLEX
::

theorem :: VFUNCT_2:32
  (f1 is total & f2 is total iff f1+f2 is total) & (f1 is total &
  f2 is total iff f1-f2 is total);

theorem :: VFUNCT_2:33
  for f1 be PartFunc of M,COMPLEX holds (f1 is total & f2 is total
  iff f1(#)f2 is total);

theorem :: VFUNCT_2:34
  f is total iff z(#)f is total;

theorem :: VFUNCT_2:35
  f is total iff -f is total;

theorem :: VFUNCT_2:36
  f is total iff ||.f.|| is total;

theorem :: VFUNCT_2:37
  for x be Element of M st f1 is total & f2 is total holds (f1+f2)/.x =
  (f1/.x) + (f2/.x) & (f1-f2)/.x = (f1/.x) - (f2/.x);

theorem :: VFUNCT_2:38
  for f1 be PartFunc of M,COMPLEX, x be Element of M holds f1 is total &
  f2 is total implies (f1(#)f2)/.x = f1/.x * (f2/.x);

theorem :: VFUNCT_2:39
  for x be Element of M st f is total holds (z(#)f)/.x = z * (f/.x);

theorem :: VFUNCT_2:40
  for x be Element of M st f is total holds (-f)/.x = - f/.x & (||.f.||)
  .x = ||. f/.x .||;

::
:: BOUNDED AND CONSTANT PARTIAL FUNCTIONS
::   FROM A DOMAIN TO A NORMED COMPLEX SPACE
::

definition
  let M;
  let V;
  let f,Y;
  pred f is_bounded_on Y means
:: VFUNCT_2:def 3

  ex r be Real st for x be Element of M st
  x in Y /\ dom f holds ||.f/.x.|| <= r;
end;

theorem :: VFUNCT_2:41
  Y c= X & f is_bounded_on X implies f is_bounded_on Y;

theorem :: VFUNCT_2:42
  X misses dom f implies f is_bounded_on X;

theorem :: VFUNCT_2:43
  0c(#)f is_bounded_on Y;

theorem :: VFUNCT_2:44
  f is_bounded_on Y implies z(#)f is_bounded_on Y;

theorem :: VFUNCT_2:45
  f is_bounded_on Y implies ||.f.|||Y is bounded & -f is_bounded_on Y;

theorem :: VFUNCT_2:46
  f1 is_bounded_on X & f2 is_bounded_on Y implies f1+f2 is_bounded_on (X /\ Y);

theorem :: VFUNCT_2:47
  for f1 be PartFunc of M,COMPLEX holds f1|X is bounded & f2
  is_bounded_on Y implies f1(#)f2 is_bounded_on (X /\ Y);

theorem :: VFUNCT_2:48
  f1 is_bounded_on X & f2 is_bounded_on Y implies f1-f2 is_bounded_on X /\ Y;

theorem :: VFUNCT_2:49
  f is_bounded_on X & f is_bounded_on Y implies f is_bounded_on X \/ Y;

theorem :: VFUNCT_2:50
  f1|X is constant & f2|Y is constant implies (f1+f2)|(X /\ Y) is
  constant & (f1-f2)|(X /\ Y) is constant;

theorem :: VFUNCT_2:51
  for f1 be PartFunc of M,COMPLEX holds f1|X is constant & f2|Y is
  constant implies (f1(#)f2)|(X /\ Y) is constant;

theorem :: VFUNCT_2:52
  f|Y is constant implies (z(#)f)|Y is constant;

theorem :: VFUNCT_2:53
  f|Y is constant implies ||.f.|||Y is constant & (-f)|Y is constant;

theorem :: VFUNCT_2:54
  f|Y is constant implies f is_bounded_on Y;

theorem :: VFUNCT_2:55
  f|Y is constant implies (for z holds z(#)f is_bounded_on Y) & -f
  is_bounded_on Y & ||.f.|||Y is bounded;

theorem :: VFUNCT_2:56
  f1 is_bounded_on X & f2|Y is constant implies f1+f2 is_bounded_on (X /\ Y);

theorem :: VFUNCT_2:57
  f1 is_bounded_on X & f2|Y is constant implies f1-f2 is_bounded_on X /\
  Y & f2-f1 is_bounded_on X /\ Y;