:: Arithmetic Operations on Short Finite Sequences
:: by Rafa{\l} Ziobro
::
:: Received September 29, 2018
:: Copyright (c) 2018-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, NAT_1, INT_1, FINSEQ_1, ARYTM_3, XXREAL_0, FINSEQ_2,
CARD_1, ARYTM_1, COMPLEX1, RELAT_1, FUNCT_1, CARD_3, TARSKI, REAL_1,
XCMPLX_0, ORDINAL1, ORDINAL4, NEWTON, PARTFUN3, SUBSET_1, VALUED_0,
FINSEQ_9, XBOOLE_0, MEMBERED, PARTFUN1, VALUED_1, FOMODEL0, ZFMISC_1;
notations TARSKI, XBOOLE_0, ORDINAL1, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0,
RVSUM_3, CARD_1, RELAT_1, FUNCT_1, INT_1, NEWTON, PARTFUN3, ABSVALUE,
RVSUM_1, FINSEQ_1, FINSEQ_2, SUBSET_1, VALUED_0, FUNCT_2, FINSEQ_4,
MEMBERED, PARTFUN1, VALUED_1, FOMODEL0, RELSET_1;
constructors NEWTON, WSIERP_1, RELSET_1, RVSUM_3, FINSEQ_4, NEWTON04;
registrations FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
FINSEQ_1, NEWTON, XBOOLE_0, VALUED_0, FINSET_1, CARD_1, RVSUM_1, RVSUM_3,
FINSEQ_2, PARTFUN3, FOMODEL0, MEMBERED, NEWTON02, FUNCT_2, NEWTON04,
RELAT_1, ABSVALUE, NAT_2, EUCLID_9, VALUED_1, COMPLEX1, FINSEQ_4,
FUNCOP_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
:: empty Relations are full of adjectives
registration
cluster empty -> positive-yielding for Relation;
cluster empty -> negative-yielding for Relation;
end;
registration
cluster natural-valued -> NAT-valued for Relation;
end;
registration
let f be complex-valued Function, k be object;
reduce (0(#)f).k to 0;
end;
registration
let f be complex-valued Function;
reduce 1(#)f to f;
reduce (-1)(#)(-f) to f;
cluster 0(#)f -> empty-yielding;
cluster f - f -> empty-yielding;
end;
registration
let D be set;
cluster empty-yielding for D-valued FinSequence;
end;
registration
cluster empty-yielding -> NAT-valued for FinSequence;
cluster non empty for empty-yielding FinSequence;
end;
registration
let n be Nat;
cluster n-element for empty-yielding NAT-valued FinSequence;
cluster min (n,0) -> zero;
reduce max (n,0) to n;
end;
registration
let a be non zero Nat;
reduce min(a,1) to 1;
reduce max(a,1) to a;
end;
registration
let a be non trivial Nat;
reduce min(a,2) to 2;
reduce max(a,2) to a;
end;
registration
let a be positive Real;
let b be positive Nat;
cluster b|->a -> positive;
end;
registration
cluster empty-yielding -> Function-like for Relation;
cluster empty-yielding -> natural-valued for Function;
cluster empty-yielding -> nonpositive-yielding for real-valued Function;
cluster empty-yielding -> nonnegative-yielding for real-valued Function;
cluster empty-yielding -> non positive-yielding
for non empty real-valued Function;
cluster empty-yielding -> non negative-yielding
for non empty real-valued Function;
cluster positive-yielding -> non nonpositive-yielding
for non empty real-valued Function;
cluster negative-yielding -> non nonnegative-yielding
for non empty real-valued Function;
end;
registration
let f be empty-yielding Function, c be Complex;
cluster c(#)f -> empty-yielding;
end;
registration let f be empty-yielding Function, g be complex-valued Function;
cluster f(#)g -> empty-yielding;
end;
:: length of FinSequences
registration
let f be complex-valued FinSequence, x be Complex;
cluster f + x -> (len f)-element;
cluster f - x -> (len f)-element;
end;
registration
let f be complex-valued FinSequence;
cluster abs f -> (len f)-element;
cluster -f -> (len f)-element;
cluster f" -> (len f)-element;
end;
registration
let n,m be Nat;
let f be n-element complex-valued FinSequence,
g be m-element complex-valued FinSequence;
cluster f+g -> min(n,m)-element;
cluster f(#)g -> min(n,m)-element;
cluster f-g -> min(n,m)-element;
cluster f /" g -> min(n,m)-element;
end;
registration let n,m be Nat, f be n-element complex-valued FinSequence,
g be (n+m)-element empty-yielding complex-valued FinSequence;
reduce f + g to f;
end;
registration let n be Nat, f be n-element complex-valued FinSequence,
g be n-element empty-yielding complex-valued FinSequence;
reduce f+g to f;
end;
registration
let X be non empty set;
cluster total for X-defined empty-yielding Function;
end;
registration
let X be non empty set;
let f be total X-defined complex-valued Function;
let g be total X-defined empty-yielding Function;
reduce f + g to f;
end;
registration
let f be Relation;
cluster (dom f)-defined for Relation;
cluster f null f -> (dom f)-defined;
cluster total for (dom f)-defined Relation;
end;
registration
let f be complex-valued Function;
cluster total for (dom f)-defined empty-yielding Function;
cluster -f -> (dom f)-defined;
cluster -f -> total;
cluster f" -> (dom f)-defined;
cluster f" -> total;
cluster abs f -> (dom f)-defined;
cluster abs f -> total;
end;
registration
let f be complex-valued Function, c be Complex;
cluster c + f -> (dom f)-defined;
cluster c + f -> total;
cluster f - c -> (dom f)-defined;
cluster f - c -> total;
cluster c(#)f -> (dom f)-defined;
cluster c(#)f -> total;
end;
registration
let f be FinSequence;
cluster (len f)-element -> (dom f)-defined for FinSequence;
end;
registration
let n be Nat;
cluster n-element -> (Seg n)-defined for FinSequence;
cluster total (Seg n)-defined -> n-element for FinSequence;
end;
theorem :: FINSEQ_9:1
for f be complex-valued FinSequence holds 0(#)f = (len f)|-> 0;
registration let f be complex-valued FinSequence;
reduce f + ((len f)|->0) to f;
end;
registration
let n be Nat;
let D be non empty set;
let X be non empty Subset of D;
cluster n-element for X-valued FinSequence;
cluster n-element for FinSequence of X;
end;
registration
let f be real-valued Function;
cluster f + (abs f) -> nonnegative-yielding;
cluster (abs f) - f -> nonnegative-yielding;
end;
registration
let f be nonnegative-yielding real-valued Function, x be object;
cluster f.x -> non negative;
end;
registration
let f be nonpositive-yielding real-valued Function, x be object;
cluster f.x -> non positive;
end;
registration
let f be nonnegative-yielding real-valued Function, r be non negative Real;
cluster r(#)f -> nonnegative-yielding;
cluster (-r)(#)f -> nonpositive-yielding;
end;
registration
let f be nonnegative-yielding real-valued Function;
cluster -f -> nonpositive-yielding;
end;
registration
let f be nonpositive-yielding real-valued Function, r be non negative Real;
cluster r(#)f -> nonpositive-yielding;
cluster (-r)(#)f -> nonnegative-yielding;
end;
registration
let f be nonpositive-yielding real-valued Function;
cluster -f -> nonnegative-yielding;
end;
registration
cluster nonnegative-yielding -> natural-valued for INT-valued Function;
end;
registration
let f be INT-valued Function;
cluster (1/2)(#)(f+(abs f)) -> natural-valued;
cluster (1/2)(#)((abs f)- f) -> natural-valued;
end;
:: Values are members of the range
theorem :: FINSEQ_9:2
for f be Relation holds rng f is natural-membered iff f is natural-valued;
theorem :: FINSEQ_9:3
for f be Relation holds f is NAT-valued iff rng f is natural-membered;
theorem :: FINSEQ_9:4
for f be Relation holds rng f is integer-membered iff f is INT-valued;
theorem :: FINSEQ_9:5
for f be Relation holds rng f is rational-membered iff f is RAT-valued;
theorem :: FINSEQ_9:6
for f be Relation holds rng f is real-membered iff f is real-valued;
theorem :: FINSEQ_9:7
for f be Relation holds f is REAL-valued iff rng f is real-membered;
theorem :: FINSEQ_9:8
for f be Relation holds rng f is complex-membered iff f is complex-valued;
theorem :: FINSEQ_9:9
for f be Relation holds f is COMPLEX-valued iff rng f is complex-membered;
:: similarly: Relations are defined over members of their domain
theorem :: FINSEQ_9:10
for f be Relation holds dom f is natural-membered iff f is NAT-defined;
registration
let f be INT-defined Relation;
cluster dom f -> integer-membered;
end;
theorem :: FINSEQ_9:11
for f be Relation holds dom f is integer-membered iff f is INT-defined;
registration
let f be RAT-defined Relation;
cluster dom f -> rational-membered;
end;
theorem :: FINSEQ_9:12
for f be Relation holds dom f is rational-membered iff f is RAT-defined;
registration
let f be REAL-defined Relation;
cluster dom f -> real-membered;
end;
theorem :: FINSEQ_9:13
for f be Relation holds dom f is real-membered iff f is REAL-defined;
registration
let f be COMPLEX-defined Relation;
cluster dom f -> complex-membered;
end;
theorem :: FINSEQ_9:14
for f be Relation holds dom f is complex-membered iff f is COMPLEX-defined;
theorem :: FINSEQ_9:15
for D be set, f be Function holds
f is D-valued iff f is Function of dom f,D;
theorem :: FINSEQ_9:16
for C be set, f be total C-defined Function holds f is Function of C, rng f;
theorem :: FINSEQ_9:17
for C,D be set, f be total C-defined Function holds
f is Function of C,D iff f is D-valued;
theorem :: FINSEQ_9:18
for f be real-valued Function holds f is Function of dom f,REAL;
theorem :: FINSEQ_9:19
for f be complex-valued FinSequence holds f-f = 0(#)f & f-f = ((len f)|-> 0);
theorem :: FINSEQ_9:20
for a be Complex, f be FinSequence, k be Nat st k in dom f holds
((len f) |-> a).k = a;
registration
let a be Real, k be non zero Nat, l be Nat, f be (k+l)-element FinSequence;
reduce ((len f) |-> a).k to a;
end;
definition
let f be complex-valued Function;
func delneg f -> complex-valued Function equals
:: FINSEQ_9:def 1
(1/2)(#)(f + (abs f));
func delpos f -> complex-valued Function equals
:: FINSEQ_9:def 2
(1/2)(#)((abs f) - f);
func delall f -> complex-valued Function equals
:: FINSEQ_9:def 3
0(#)f;
end;
theorem :: FINSEQ_9:21
for f be complex-valued Function holds dom f = dom (delpos f)
& dom f = dom (delneg f) & dom f = dom (delall f);
theorem :: FINSEQ_9:22
for f be complex-valued Function, x be object holds
f.x = (delneg f).x - (delpos f).x;
theorem :: FINSEQ_9:23
for f be complex-valued Function holds f = delneg f - delpos f;
theorem :: FINSEQ_9:24
for f be real-valued Function, x be object holds
f.x = (delneg f).x or f.x = -(delpos f).x;
theorem :: FINSEQ_9:25
for f be real-valued Function, x be object holds
(delneg f).x = 0 or (delpos f).x = 0;
registration
let f be real-valued Function;
cluster (delneg f)(#)(delpos f) -> empty-yielding;
end;
theorem :: FINSEQ_9:26
for f be real-valued Function holds delall f = (delneg f)(#)(delpos f);
registration
let f be complex-valued Function;
let f1 be total (dom f)-defined empty-yielding Function;
reduce f + f1 to f;
reduce (f - f1) to f;
end;
registration
let f be complex-valued Function;
let f1 be total (dom f)-defined complex-valued Function;
let f2 be total (dom f)-defined empty-yielding Function;
reduce f1 + f2 to f1;
reduce f1 - f2 to f1;
end;
registration
let f be complex-valued Function;
cluster f - f -> (dom f)-defined;
cluster f - f -> total;
end;
theorem :: FINSEQ_9:27
for f be complex-valued Function holds abs f = delneg f + delpos f;
registration
let f be empty FinSequence;
cluster Product f -> natural;
cluster Product f -> non zero;
end;
registration
let f be positive-yielding real-valued FinSequence;
cluster Product f -> positive;
end;
registration
let f be complex-valued FinSequence;
cluster delneg f -> (len f)-element;
cluster delpos f -> (len f)-element;
end;
theorem :: FINSEQ_9:28
for f be complex-valued Function holds delneg f = delpos (-f);
registration
let f be nonnegative-yielding real-valued Function;
reduce (abs f) to f;
reduce delneg f to f;
identify delpos f with delall f;
identify delall f with delpos f;
end;
registration
let f be nonpositive-yielding real-valued Function;
reduce - delpos f to f;
cluster delneg f -> empty-yielding;
identify delneg f with delall f;
identify delall f with delneg f;
end;
theorem :: FINSEQ_9:29
for f be FinSequence of INT holds ex f1,f2 be FinSequence of NAT st
f = f1 - f2;
registration
let a be Integer, n be Nat;
cluster n|->a -> INT-valued;
end;
registration
let f be non empty empty-yielding FinSequence;
cluster Product f -> zero;
end;
theorem :: FINSEQ_9:30
for f1,f2 being FinSequence of REAL st len f1 = len f2 & (for k
being Element of NAT st k in dom f1 holds f1.k>=f2.k & f2.k>0) holds
Product f1 >= Product f2;
theorem :: FINSEQ_9:31
for a be Real for f be FinSequence of REAL st
(for k be Element of NAT st k in dom f holds 0 < f.k <= a)
holds Product f <= Product ((len f) |-> a);
theorem :: FINSEQ_9:32
for a be non negative Real, f be FinSequence of REAL st (for k be Nat
st k in dom f holds f.k >= a) holds Product (f) >= a|^(len f);
theorem :: FINSEQ_9:33
for f1,f2 be nonnegative-yielding FinSequence of REAL st len f1 = len f2
& (for k be Element of NAT st k in dom f2 holds f1.k>=f2.k) holds
Product f1 >= Product f2;
theorem :: FINSEQ_9:34 ::NAT454:
for f1,f2 being FinSequence of REAL st len f1 = len f2 &
(for k be Element of NAT
st k in dom f2 holds f1.k>=f2.k & f2.k>=0) holds Product f1 >= Product f2;
theorem :: FINSEQ_9:35
for a be positive Real, f be nonnegative-yielding FinSequence of REAL st
(for k be Element of NAT st k in dom f holds f.k <= a)
holds Product (f) <= a|^(len f);
:: Basic operations on short finsequences
registration
let a be Complex;
reduce (-<*(-a)*>).1 to a;
reduce (<*(a")*>").1 to a;
end;
theorem :: FINSEQ_9:36
for a,b be Complex holds <*a*>+<*b*> = <*(a+b)*>;
theorem :: FINSEQ_9:37
for a,b be Complex holds <*a*>-<*b*> = <*(a-b)*>;
theorem :: FINSEQ_9:38
for a,b be Complex holds <*a*>(#)<*b*> = <*(a*b)*>;
theorem :: FINSEQ_9:39
for a,b be Complex holds <*a*>/"<*b*> = <*(a*b")*>;
registration
let n be Nat, f be n-element FinSequence, a be Complex;
reduce (f^<*a*>).(n+1) to a;
reduce (f^<*a*>)|n to f;
end;
registration
let a,b,c,d be Complex;
cluster <*a,b,c,d*> -> complex-valued;
end;
registration
let a,b be Complex;
reduce (-<*(-a),b*>).1 to a;
reduce (-<*a,(-b)*>).2 to b;
reduce (<*(a"),b*>").1 to a;
reduce (<*a,(b")*>").2 to b;
end;
registration
let a,b,c be Complex;
reduce <*a,b,c*>.1 to a;
reduce <*a,b,c*>.2 to b;
reduce (-<*(-a),b,c*>).1 to a;
reduce (-<*a,(-b),c*>).2 to b;
reduce (-<*a,b,(-c)*>).3 to c;
reduce (<*(a"),b,c*>").1 to a;
reduce (<*a,(b"),c*>").2 to b;
reduce (<*a,b,(c")*>").3 to c;
end;
theorem :: FINSEQ_9:40
for a,b be Complex, n be Nat,
f,g be n-element complex-valued FinSequence holds
(f^<*a*>)+(g^<*b*>) = (f+g)^<*a+b*>;
theorem :: FINSEQ_9:41
for a,b,x,y be Complex holds <*a,b*>+<*x,y*> = <*a+x,b+y*>;
theorem :: FINSEQ_9:42
for a,b,c,x,y,z be Complex holds <*a,b,c*>+<*x,y,z*> = <*a+x,b+y,c+z*>;
theorem :: FINSEQ_9:43
for a,b,c,d,x,y,z,v be Complex holds
<*a,b,c,d*>+<*x,y,z,v*> = <*a+x,b+y,c+z,d+v*>;
theorem :: FINSEQ_9:44
for a,b be Complex, n be Nat,
f,g be n-element complex-valued FinSequence holds
(f^<*a*>)(#)(g^<*b*>) = (f(#)g)^<*a*b*>;
theorem :: FINSEQ_9:45
for a,b,x,y be Complex holds <*a,b*>(#)<*x,y*> = <*a*x,b*y*>;
theorem :: FINSEQ_9:46
for a,b,c,x,y,z be Complex holds
<*a,b,c*>(#)<*x,y,z*> = <*a*x,b*y,c*z*>;
theorem :: FINSEQ_9:47
for a,b,c,d,x,y,z,v be Complex holds
<*a,b,c,d*>(#)<*x,y,z,v*> = <*a*x,b*y,c*z,d*v*>;
theorem :: FINSEQ_9:48
for a be Complex, n be non zero Nat,
f be n-element complex-valued FinSequence holds <*a*>+f = <*(a+f.1)*>;
theorem :: FINSEQ_9:49
for a,b be Complex, n be non trivial Nat,
f be n-element complex-valued FinSequence holds
<*a,b*>+f = <*a+f.1,b+f.2*>;
theorem :: FINSEQ_9:50
for a be Complex, n be non zero Nat,
f be n-element complex-valued FinSequence holds <*a*>(#)f = <*a*f.1*>;
theorem :: FINSEQ_9:51
for a,b be Complex, n be non trivial Nat,
f be n-element complex-valued FinSequence holds
<*a,b*>(#)f = <*a*f.1,b*f.2*>;