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