:: Basic Properties of Periodic Functions
:: by Bo Li , Yanhong Men , Dailu Li and Xiquan Liang
::
:: Received October 10, 2009
:: Copyright (c) 2009-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, VALUED_0, FUNCT_1, NAT_1, CARD_1, RELAT_1, ARYTM_3,
ARYTM_1, XBOOLE_0, TARSKI, VALUED_1, COMPLEX1, SQUARE_1, SIN_COS,
PARTFUN1, REAL_1, SIN_COS4, FUNCOP_1, XCMPLX_0, FUNCT_9, INT_1, SUBSET_1;
notations TARSKI, XBOOLE_0, SUBSET_1, COMPLEX1, XCMPLX_0, ORDINAL1, NUMBERS,
XREAL_0, REAL_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, SIN_COS,
VALUED_0, VALUED_1, INT_1, SQUARE_1, FDIFF_9;
constructors REAL_1, EUCLID, SQUARE_1, PBOOLE, RFUNCT_1, SIN_COS, FDIFF_9,
RELSET_1, COMPLEX1;
registrations XXREAL_0, MEMBERED, XCMPLX_0, NUMBERS, VALUED_0, RELAT_1,
VALUED_1, NAT_1, SIN_COS6, FUNCOP_1, XREAL_0, INT_1, SIN_COS, ORDINAL1;
requirements NUMERALS, SUBSET, ARITHM;
begin :: The Basic Properties of period function
reserve x,t,t1,t2,r,a,b for Real;
reserve F,G for real-valued Function;
reserve k for Nat;
reserve i for non zero Integer;
definition
let t be Real;
let F be Function;
attr F is t-periodic means
:: FUNCT_9:def 1
t <> 0 & for x holds (x in dom F iff x+t in dom F) &
(x in dom F implies F.x = F.(x+t));
end;
definition
let F be Function;
attr F is periodic means
:: FUNCT_9:def 2
ex t st F is t-periodic;
end;
theorem :: FUNCT_9:1
F is t-periodic iff t<>0 &
for x st x in dom F holds x+t in dom F & x-t in dom F & F.x=F.(x+t);
theorem :: FUNCT_9:2
F is t-periodic & G is t-periodic implies F+G is t-periodic;
theorem :: FUNCT_9:3
F is t-periodic & G is t-periodic implies F-G is t-periodic;
theorem :: FUNCT_9:4
F is t-periodic & G is t-periodic implies F(#)G is t-periodic;
theorem :: FUNCT_9:5
F is t-periodic & G is t-periodic implies F /" G is t-periodic;
theorem :: FUNCT_9:6
F is t-periodic implies -F is t-periodic;
theorem :: FUNCT_9:7
F is t-periodic implies r (#) F is t-periodic;
theorem :: FUNCT_9:8
F is t-periodic implies r+F is t-periodic;
theorem :: FUNCT_9:9
F is t-periodic implies F-r is t-periodic;
theorem :: FUNCT_9:10
F is t-periodic implies |. F .| is t-periodic;
theorem :: FUNCT_9:11
F is t-periodic implies F" is t-periodic;
theorem :: FUNCT_9:12
F is t-periodic implies F^2 is t-periodic;
theorem :: FUNCT_9:13
F is t-periodic implies for x st x in dom F holds F.x=F.(x-t);
theorem :: FUNCT_9:14
F is t-periodic implies F is -t -periodic;
theorem :: FUNCT_9:15
F is t1-periodic & F is t2-periodic & t1+t2<>0 implies F is (t1+t2)-periodic;
theorem :: FUNCT_9:16
F is t1-periodic & F is t2-periodic & t1-t2<>0 implies F is (t1-t2)-periodic;
theorem :: FUNCT_9:17
(t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F &
F.(x+t)=F.(x-t))) implies F is (2*t)-periodic & F is periodic;
theorem :: FUNCT_9:18
(t1+t2<>0 & for x st x in dom F holds (x+t1 in dom F & x-t1 in dom F &
x+t2 in dom F & x-t2 in dom F &
F.(x+t1)=F.(x-t2))) implies F is (t1+t2)-periodic & F is periodic;
theorem :: FUNCT_9:19
(t1-t2<>0 & for x st x in dom F holds (x+t1 in dom F & x-t1 in dom F &
x+t2 in dom F & x-t2 in dom F &
F.(x+t1)=F.(x+t2))) implies F is (t1-t2)-periodic & F is periodic;
theorem :: FUNCT_9:20
(t<>0 & for x st x in dom F holds (x+t in dom F & x-t in dom F &
F.(x+t)=(F.x)")) implies F is (2*t)-periodic & F is periodic;
registration
cluster periodic real-valued for Function;
cluster periodic for PartFunc of REAL, REAL;
end;
registration
let t be non zero Real;
cluster REAL --> t -> t-periodic;
cluster t-periodic real-valued for Function;
end;
registration
let t be non zero Real;
let F,G be t-periodic real-valued Function;
cluster F + G -> t-periodic;
cluster F - G -> t-periodic;
cluster F (#) G -> t-periodic;
cluster F /" G -> t-periodic;
end;
registration let F be periodic real-valued Function;
cluster -F -> periodic;
end;
registration let F be periodic real-valued Function;
let r be Real;
cluster r (#) F -> periodic;
cluster r+F -> periodic;
cluster F-r -> periodic;
end;
registration let F be periodic real-valued Function;
cluster |. F .| -> periodic;
cluster F" -> periodic;
cluster F^2 -> periodic;
end;
begin
registration
cluster sin -> periodic;
cluster cos -> periodic;
end;
theorem :: FUNCT_9:21
sin is (2*PI*i)-periodic;
theorem :: FUNCT_9:22
cos is (2*PI*i)-periodic;
registration
cluster cosec -> periodic;
cluster sec -> periodic;
end;
theorem :: FUNCT_9:23
sec is (2*PI*i)-periodic;
theorem :: FUNCT_9:24
cosec is (2*PI*i)-periodic;
registration
cluster tan -> periodic;
cluster cot -> periodic;
end;
theorem :: FUNCT_9:25
tan is (PI*i)-periodic;
theorem :: FUNCT_9:26
cot is (PI*i)-periodic;
theorem :: FUNCT_9:27
|. sin .| is (PI*i)-periodic;
theorem :: FUNCT_9:28
|. cos .| is (PI*i)-periodic;
theorem :: FUNCT_9:29
|. sin .| + |. cos .| is (PI/2*i)-periodic;
theorem :: FUNCT_9:30
sin^2 is (PI*i)-periodic;
theorem :: FUNCT_9:31
cos^2 is (PI*i)-periodic;
theorem :: FUNCT_9:32
sin (#) cos is (PI*i)-periodic;
theorem :: FUNCT_9:33
b + a (#) sin is (2*PI*i)-periodic;
theorem :: FUNCT_9:34
a (#) sin - b is (2*PI*i)-periodic;
theorem :: FUNCT_9:35
b + a (#) cos is (2*PI*i)-periodic;
theorem :: FUNCT_9:36
a (#) cos - b is (2*PI*i)-periodic;
theorem :: FUNCT_9:37
t <> 0 implies REAL --> a is t -periodic;
registration
let a;
cluster REAL --> a -> periodic;
end;
registration
let t be non zero Real;
cluster t-periodic for Function of REAL,REAL;
end;