:: by Bo Li , Yanhong Men , Dailu Li and Xiquan Liang

::

:: Received October 10, 2009

:: Copyright (c) 2009-2017 Association of Mizar Users

:: deftheorem defines -periodic FUNCT_9:def 1 :

for t being Real

for F being Function holds

( F is t -periodic iff ( t <> 0 & ( for x being Real 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) ) ) ) ) );

for t being Real

for F being Function holds

( F is t -periodic iff ( t <> 0 & ( for x being Real 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) ) ) ) ) );

:: deftheorem Def2 defines periodic FUNCT_9:def 2 :

for F being Function holds

( F is periodic iff ex t being Real st F is t -periodic );

for F being Function holds

( F is periodic iff ex t being Real st F is t -periodic );

theorem Th1: :: FUNCT_9:1

for t being Real

for F being real-valued Function holds

( F is t -periodic iff ( t <> 0 & ( for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) )

for F being real-valued Function holds

( F is t -periodic iff ( t <> 0 & ( for x being Real st x in dom F holds

( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) )

proof end;

theorem Th2: :: FUNCT_9:2

for t being Real

for F, G being real-valued Function st F is t -periodic & G is t -periodic holds

F + G is t -periodic

for F, G being real-valued Function st F is t -periodic & G is t -periodic holds

F + G is t -periodic

proof end;

Lm1: for t, a being Real st t <> 0 holds

REAL --> a is t -periodic

proof end;

theorem Th3: :: FUNCT_9:3

for t being Real

for F, G being real-valued Function st F is t -periodic & G is t -periodic holds

F - G is t -periodic

for F, G being real-valued Function st F is t -periodic & G is t -periodic holds

F - G is t -periodic

proof end;

theorem Th4: :: FUNCT_9:4

for t being Real

for F, G being real-valued Function st F is t -periodic & G is t -periodic holds

F (#) G is t -periodic

for F, G being real-valued Function st F is t -periodic & G is t -periodic holds

F (#) G is t -periodic

proof end;

theorem Th5: :: FUNCT_9:5

for t being Real

for F, G being real-valued Function st F is t -periodic & G is t -periodic holds

F /" G is t -periodic

for F, G being real-valued Function st F is t -periodic & G is t -periodic holds

F /" G is t -periodic

proof end;

theorem Th7: :: FUNCT_9:7

for t, r being Real

for F being real-valued Function st F is t -periodic holds

r (#) F is t -periodic

for F being real-valued Function st F is t -periodic holds

r (#) F is t -periodic

proof end;

theorem :: FUNCT_9:9

theorem :: FUNCT_9:12

theorem Th13: :: FUNCT_9:13

for t being Real

for F being real-valued Function st F is t -periodic holds

for x being Real st x in dom F holds

F . x = F . (x - t)

for F being real-valued Function st F is t -periodic holds

for x being Real st x in dom F holds

F . x = F . (x - t)

proof end;

theorem :: FUNCT_9:15

for t1, t2 being Real

for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 holds

F is t1 + t2 -periodic

for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 holds

F is t1 + t2 -periodic

proof end;

theorem :: FUNCT_9:16

for t1, t2 being Real

for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 holds

F is t1 - t2 -periodic

for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 holds

F is t1 - t2 -periodic

proof end;

theorem :: FUNCT_9:17

for t being Real

for F being real-valued Function st t <> 0 & ( for x being Real 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 )

for F being real-valued Function st t <> 0 & ( for x being Real 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 )

proof end;

theorem :: FUNCT_9:18

for t1, t2 being Real

for F being real-valued Function st t1 + t2 <> 0 & ( for x being Real 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 )

for F being real-valued Function st t1 + t2 <> 0 & ( for x being Real 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 )

proof end;

theorem :: FUNCT_9:19

for t1, t2 being Real

for F being real-valued Function st t1 - t2 <> 0 & ( for x being Real 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 )

for F being real-valued Function st t1 - t2 <> 0 & ( for x being Real 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 )

proof end;

theorem :: FUNCT_9:20

for t being Real

for F being real-valued Function st t <> 0 & ( for x being Real 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 )

for F being real-valued Function st t <> 0 & ( for x being Real 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 )

proof end;

Lm2: sin is 2 * PI -periodic

by SIN_COS:24, SIN_COS:78, XREAL_0:def 1;

registration

existence

ex b_{1} being Function st

( b_{1} is periodic & b_{1} is real-valued )
by Lm2, Def2;

ex b_{1} being PartFunc of REAL,REAL st b_{1} is periodic

end;
ex b

( b

cluster Relation-like Function-like complex-valued ext-real-valued real-valued periodic for Element of K16(K17(REAL,REAL));

existence ex b

proof end;

registration

let t be non zero Real;

coherence

REAL --> t is t -periodic by Lm1;

existence

ex b_{1} being Function st

( b_{1} is t -periodic & b_{1} is real-valued )

end;
coherence

REAL --> t is t -periodic by Lm1;

existence

ex b

( b

proof end;

registration

let t be non zero Real;

let F, G be real-valued t -periodic Function;

coherence

F + G is t -periodic by Th2;

coherence

F - G is t -periodic by Th3;

coherence

F (#) G is t -periodic by Th4;

coherence

F /" G is t -periodic by Th5;

end;
let F, G be real-valued t -periodic Function;

coherence

F + G is t -periodic by Th2;

coherence

F - G is t -periodic by Th3;

coherence

F (#) G is t -periodic by Th4;

coherence

F /" G is t -periodic by Th5;

registration

let F be real-valued periodic Function;

let r be Real;

coherence

r (#) F is periodic

r + F is periodic

F - r is periodic ;

end;
let r be Real;

coherence

r (#) F is periodic

proof end;

coherence r + F is periodic

proof end;

coherence F - r is periodic ;

registration

let F be real-valued periodic Function;

coherence

|.F.| is periodic

F " is periodic

F ^2 is periodic

end;
coherence

|.F.| is periodic

proof end;

coherence F " is periodic

proof end;

coherence F ^2 is periodic

proof end;

Lm3: cos is 2 * PI -periodic

by SIN_COS:24, SIN_COS:78, XREAL_0:def 1;

Lm4: for k being Nat holds sin is (2 * PI) * (k + 1) -periodic

proof end;

Lm5: for k being Nat holds cos is (2 * PI) * (k + 1) -periodic

proof end;

Lm6: cosec is 2 * PI -periodic

proof end;

Lm7: sec is 2 * PI -periodic

proof end;

Lm8: for k being Nat holds sec is (2 * PI) * (k + 1) -periodic

proof end;

Lm9: for k being Nat holds cosec is (2 * PI) * (k + 1) -periodic

proof end;

Lm10: tan is PI -periodic

proof end;

Lm11: cot is PI -periodic

proof end;

Lm12: for k being Nat holds tan is PI * (k + 1) -periodic

proof end;

Lm13: for k being Nat holds cot is PI * (k + 1) -periodic

proof end;

Lm14: |.sin.| is PI -periodic

proof end;

Lm15: |.cos.| is PI -periodic

proof end;

Lm16: for k being Nat holds |.sin.| is PI * (k + 1) -periodic

proof end;

Lm17: for k being Nat holds |.cos.| is PI * (k + 1) -periodic

proof end;

Lm18: |.sin.| + |.cos.| is PI / 2 -periodic

proof end;

Lm19: for k being Nat holds |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic

proof end;

Lm20: sin ^2 is PI -periodic

proof end;

Lm21: cos ^2 is PI -periodic

proof end;

Lm22: for k being Nat holds sin ^2 is PI * (k + 1) -periodic

proof end;

Lm23: for k being Nat holds cos ^2 is PI * (k + 1) -periodic

proof end;

Lm24: sin (#) cos is PI -periodic

proof end;

Lm25: for k being Nat holds sin (#) cos is PI * (k + 1) -periodic

proof end;

Lm26: for a, b being Real holds b + (a (#) sin) is 2 * PI -periodic

proof end;

Lm27: for a, b being Real holds b + (a (#) cos) is 2 * PI -periodic

proof end;

Lm28: for a, b being Real

for k being Nat holds b + (a (#) sin) is (2 * PI) * (k + 1) -periodic

proof end;

theorem :: FUNCT_9:34

Lm29: for a, b being Real

for k being Nat holds b + (a (#) cos) is (2 * PI) * (k + 1) -periodic

proof end;

theorem :: FUNCT_9:36

registration
end;

registration

let t be non zero Real;

ex b_{1} being Function of REAL,REAL st b_{1} is t -periodic

end;
cluster Relation-like Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued t -periodic for Element of K16(K17(REAL,REAL));

existence ex b

proof end;