:: Algebra of Complex Vector Valued Functions :: by Noboru Endou :: :: Received August 20, 2004 :: Copyright (c) 2004-2018 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;