:: Basic Properties of Periodic Functions :: by Bo Li , Yanhong Men , Dailu Li and Xiquan Liang :: :: Received October 10, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin definition let t be real number ; let F be Function; attrF is t -periodic means :Def1: :: FUNCT_9:def 1 ( t <> 0 & ( for x being real number holds ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) ) ); end; :: deftheorem Def1 defines -periodic FUNCT_9:def_1_:_ for t being real number for F being Function holds ( F is t -periodic iff ( t <> 0 & ( for x being real number holds ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) ) ) ); definition let F be Function; attrF is periodic means :Def2: :: FUNCT_9:def 2 ex t being real number st F is t -periodic ; end; :: deftheorem Def2 defines periodic FUNCT_9:def_2_:_ for F being Function holds ( F is periodic iff ex t being real number st F is t -periodic ); theorem Th1: :: FUNCT_9:1 for t being real number for F being real-valued Function holds ( F is t -periodic iff ( t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ) proofend; theorem Th2: :: FUNCT_9:2 for t being real number for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F + G is t -periodic proofend; Lm1: for t, a being real number st t <> 0 holds REAL --> a is t -periodic proofend; theorem Th3: :: FUNCT_9:3 for t being real number for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F - G is t -periodic proofend; theorem Th4: :: FUNCT_9:4 for t being real number for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F (#) G is t -periodic proofend; theorem Th5: :: FUNCT_9:5 for t being real number for F, G being real-valued Function st F is t -periodic & G is t -periodic holds F /" G is t -periodic proofend; theorem Th6: :: FUNCT_9:6 for t being real number for F being real-valued Function st F is t -periodic holds - F is t -periodic proofend; theorem Th7: :: FUNCT_9:7 for t, r being real number for F being real-valued Function st F is t -periodic holds r (#) F is t -periodic proofend; theorem Th8: :: FUNCT_9:8 for t, r being real number for F being real-valued Function st F is t -periodic holds r + F is t -periodic proofend; theorem :: FUNCT_9:9 for t, r being real number for F being real-valued Function st F is t -periodic holds F - r is t -periodic by Th8; theorem Th10: :: FUNCT_9:10 for t being real number for F being real-valued Function st F is t -periodic holds |.F.| is t -periodic proofend; theorem Th11: :: FUNCT_9:11 for t being real number for F being real-valued Function st F is t -periodic holds F " is t -periodic proofend; theorem :: FUNCT_9:12 for t being real number for F being real-valued Function st F is t -periodic holds F ^2 is t -periodic by Th4; theorem Th13: :: FUNCT_9:13 for t being real number for F being real-valued Function st F is t -periodic holds for x being real number st x in dom F holds F . x = F . (x - t) proofend; theorem Th14: :: FUNCT_9:14 for t being real number for F being real-valued Function st F is t -periodic holds F is - t -periodic proofend; theorem :: FUNCT_9:15 for t1, t2 being real number for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 holds F is t1 + t2 -periodic proofend; theorem :: FUNCT_9:16 for t1, t2 being real number for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 holds F is t1 - t2 -periodic proofend; theorem :: FUNCT_9:17 for t being real number for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = F . (x - t) ) ) holds ( F is 2 * t -periodic & F is periodic ) proofend; theorem :: FUNCT_9:18 for t1, t2 being real number for F being real-valued Function st t1 + t2 <> 0 & ( for x being real number 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) ) ) holds ( F is t1 + t2 -periodic & F is periodic ) proofend; theorem :: FUNCT_9:19 for t1, t2 being real number for F being real-valued Function st t1 - t2 <> 0 & ( for x being real number 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) ) ) holds ( F is t1 - t2 -periodic & F is periodic ) proofend; theorem :: FUNCT_9:20 for t being real number for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds ( x + t in dom F & x - t in dom F & F . (x + t) = (F . x) " ) ) holds ( F is 2 * t -periodic & F is periodic ) proofend; Lm2: sin is 2 * PI -periodic proofend; registration cluster Relation-like Function-like real-valued periodic for set ; existence ex b1 being Function st ( b1 is periodic & b1 is real-valued ) proofend; cluster Relation-like Function-like complex-valued ext-real-valued real-valued periodic for Element of K6(K7(REAL,REAL)); existence ex b1 being PartFunc of REAL,REAL st b1 is periodic proofend; end; registration let t be non zero real number ; clusterREAL --> t -> t -periodic ; coherence REAL --> t is t -periodic by Lm1; cluster Relation-like Function-like real-valued t -periodic for set ; existence ex b1 being Function st ( b1 is t -periodic & b1 is real-valued ) proofend; end; registration let t be non zero real number ; let F, G be real-valued t -periodic Function; clusterF + G -> t -periodic ; coherence F + G is t -periodic by Th2; clusterF - G -> t -periodic ; coherence F - G is t -periodic by Th3; clusterF (#) G -> t -periodic ; coherence F (#) G is t -periodic by Th4; clusterF /" G -> t -periodic ; coherence F /" G is t -periodic by Th5; end; registration let F be real-valued periodic Function; cluster - F -> periodic ; coherence - F is periodic proofend; end; registration let F be real-valued periodic Function; let r be real number ; clusterr (#) F -> periodic ; coherence r (#) F is periodic proofend; clusterr + F -> periodic ; coherence r + F is periodic proofend; clusterF - r -> periodic ; coherence F - r is periodic ; end; registration let F be real-valued periodic Function; cluster|.F.| -> periodic ; coherence |.F.| is periodic proofend; clusterF " -> periodic ; coherence F " is periodic proofend; clusterF ^2 -> periodic ; coherence F ^2 is periodic proofend; end; begin Lm3: cos is 2 * PI -periodic proofend; registration cluster sin -> periodic ; coherence sin is periodic by Def2, Lm2; cluster cos -> periodic ; coherence cos is periodic by Def2, Lm3; end; Lm4: for k being Nat holds sin is (2 * PI) * (k + 1) -periodic proofend; theorem :: FUNCT_9:21 for i being non zero Integer holds sin is (2 * PI) * i -periodic proofend; Lm5: for k being Nat holds cos is (2 * PI) * (k + 1) -periodic proofend; theorem :: FUNCT_9:22 for i being non zero Integer holds cos is (2 * PI) * i -periodic proofend; Lm6: cosec is 2 * PI -periodic proofend; Lm7: sec is 2 * PI -periodic proofend; registration cluster cosec -> periodic ; coherence cosec is periodic by Def2, Lm6; cluster sec -> periodic ; coherence sec is periodic by Def2, Lm7; end; Lm8: for k being Nat holds sec is (2 * PI) * (k + 1) -periodic proofend; theorem :: FUNCT_9:23 for i being non zero Integer holds sec is (2 * PI) * i -periodic proofend; Lm9: for k being Nat holds cosec is (2 * PI) * (k + 1) -periodic proofend; theorem :: FUNCT_9:24 for i being non zero Integer holds cosec is (2 * PI) * i -periodic proofend; Lm10: tan is PI -periodic proofend; Lm11: cot is PI -periodic proofend; registration cluster tan -> periodic ; coherence tan is periodic by Def2, Lm10; cluster cot -> periodic ; coherence cot is periodic by Def2, Lm11; end; Lm12: for k being Nat holds tan is PI * (k + 1) -periodic proofend; theorem :: FUNCT_9:25 for i being non zero Integer holds tan is PI * i -periodic proofend; Lm13: for k being Nat holds cot is PI * (k + 1) -periodic proofend; theorem :: FUNCT_9:26 for i being non zero Integer holds cot is PI * i -periodic proofend; Lm14: |.sin.| is PI -periodic proofend; Lm15: |.cos.| is PI -periodic proofend; Lm16: for k being Nat holds |.sin.| is PI * (k + 1) -periodic proofend; theorem :: FUNCT_9:27 for i being non zero Integer holds |.sin.| is PI * i -periodic proofend; Lm17: for k being Nat holds |.cos.| is PI * (k + 1) -periodic proofend; theorem :: FUNCT_9:28 for i being non zero Integer holds |.cos.| is PI * i -periodic proofend; Lm18: |.sin.| + |.cos.| is PI / 2 -periodic proofend; Lm19: for k being Nat holds |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic proofend; theorem :: FUNCT_9:29 for i being non zero Integer holds |.sin.| + |.cos.| is (PI / 2) * i -periodic proofend; Lm20: sin ^2 is PI -periodic proofend; Lm21: cos ^2 is PI -periodic proofend; Lm22: for k being Nat holds sin ^2 is PI * (k + 1) -periodic proofend; theorem :: FUNCT_9:30 for i being non zero Integer holds sin ^2 is PI * i -periodic proofend; Lm23: for k being Nat holds cos ^2 is PI * (k + 1) -periodic proofend; theorem :: FUNCT_9:31 for i being non zero Integer holds cos ^2 is PI * i -periodic proofend; Lm24: sin (#) cos is PI -periodic proofend; Lm25: for k being Nat holds sin (#) cos is PI * (k + 1) -periodic proofend; theorem :: FUNCT_9:32 for i being non zero Integer holds sin (#) cos is PI * i -periodic proofend; Lm26: for b, a being real number holds b + (a (#) sin) is 2 * PI -periodic proofend; Lm27: for b, a being real number holds b + (a (#) cos) is 2 * PI -periodic proofend; Lm28: for b, a being real number for k being Nat holds b + (a (#) sin) is (2 * PI) * (k + 1) -periodic proofend; theorem Th33: :: FUNCT_9:33 for b, a being real number for i being non zero Integer holds b + (a (#) sin) is (2 * PI) * i -periodic proofend; theorem :: FUNCT_9:34 for a, b being real number for i being non zero Integer holds (a (#) sin) - b is (2 * PI) * i -periodic by Th33; Lm29: for b, a being real number for k being Nat holds b + (a (#) cos) is (2 * PI) * (k + 1) -periodic proofend; theorem Th35: :: FUNCT_9:35 for b, a being real number for i being non zero Integer holds b + (a (#) cos) is (2 * PI) * i -periodic proofend; theorem :: FUNCT_9:36 for a, b being real number for i being non zero Integer holds (a (#) cos) - b is (2 * PI) * i -periodic by Th35; theorem :: FUNCT_9:37 for t, a being real number st t <> 0 holds REAL --> a is t -periodic by Lm1; registration let a be real number ; clusterREAL --> a -> periodic ; coherence REAL --> a is periodic proofend; end; registration let t be non zero real number ; cluster Relation-like Function-like V27( REAL , REAL ) complex-valued ext-real-valued real-valued t -periodic for Element of K6(K7(REAL,REAL)); existence ex b1 being Function of REAL,REAL st b1 is t -periodic proofend; end;