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

definition

let t be Real;
let F be Function;

attr F is t -periodic means :: FUNCT_9:def 1
( 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) ) ) ) );

end;

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

definition

let F be Function;

attr F is periodic means :Def2: :: FUNCT_9:def 2
ex t being Real 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 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) ) ) ) )

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

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

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

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

proof end;

theorem Th6: :: FUNCT_9:6

for t being Real
for F being real-valued Function st F is t -periodic holds
- F 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

proof end;

theorem Th8: :: FUNCT_9:8

for t, r being Real
for F being real-valued Function st F is t -periodic holds
r + F is t -periodic

proof end;

theorem :: FUNCT_9:9

for t, r being Real
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
for F being real-valued Function st F is t -periodic holds
|.F.| is t -periodic

proof end;

theorem Th11: :: FUNCT_9:11

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

proof end;

theorem :: FUNCT_9:12

for t being Real
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
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 Th14: :: FUNCT_9:14

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

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

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

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 )

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 )

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 )

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 )

proof end;

Lm2: sin is 2 * PI -periodic
by SIN_COS:24, SIN_COS:78, XREAL_0:def 1;

registration

cluster Relation-like Function-like real-valued periodic for set ;

existence
ex b₁ being Function st
( b₁ is periodic & b₁ is real-valued ) by Lm2, Def2;

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

existence
ex b₁ being PartFunc of REAL,REAL st b₁ is periodic

proof end;

end;

registration

let t be non zero Real;

cluster REAL --> t -> t -periodic ;

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

cluster Relation-like Function-like real-valued t -periodic for set ;

existence
ex b₁ being Function st
( b₁ is t -periodic & b₁ is real-valued )

proof end;

end;

registration

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

cluster F + G -> t -periodic ;

coherence
F + G is t -periodic by Th2;

cluster F - G -> t -periodic ;

coherence
F - G is t -periodic by Th3;

cluster F (#) G -> t -periodic ;

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

cluster F /" 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

proof end;

end;

registration

let F be real-valued periodic Function;
let r be Real;

cluster r (#) F -> periodic ;

coherence
r (#) F is periodic

proof end;

cluster r + F -> periodic ;

coherence
r + F is periodic

proof end;

cluster F - r -> periodic ;

coherence
F - r is periodic ;

end;

registration

let F be real-valued periodic Function;

cluster |.F.| -> periodic ;

coherence
|.F.| is periodic

proof end;

cluster F " -> periodic ;

coherence
F " is periodic

proof end;

cluster F ^2 -> periodic ;

coherence
F ^2 is periodic

proof end;

end;

Lm3: cos is 2 * PI -periodic
by SIN_COS:24, SIN_COS:78, XREAL_0:def 1;

registration

cluster sin -> periodic ;

coherence
sin is periodic by Lm2;

cluster cos -> periodic ;

coherence
cos is periodic by Lm3;

end;

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

proof end;

theorem :: FUNCT_9:21

for i being non zero Integer holds sin is (2 * PI) * i -periodic

proof end;

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

proof end;

theorem :: FUNCT_9:22

for i being non zero Integer holds cos is (2 * PI) * i -periodic

proof end;

Lm6: cosec is 2 * PI -periodic

proof end;

Lm7: sec is 2 * PI -periodic

proof end;

registration

cluster cosec -> periodic ;

coherence
cosec is periodic by Lm6;

cluster sec -> periodic ;

coherence
sec is periodic by Lm7;

end;

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

proof end;

theorem :: FUNCT_9:23

for i being non zero Integer holds sec is (2 * PI) * i -periodic

proof end;

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

proof end;

theorem :: FUNCT_9:24

for i being non zero Integer holds cosec is (2 * PI) * i -periodic

proof end;

Lm10: tan is PI -periodic

proof end;

Lm11: cot is PI -periodic

proof end;

registration

cluster tan -> periodic ;

coherence
tan is periodic by Lm10;

cluster cot -> periodic ;

coherence
cot is periodic by Lm11;

end;

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

proof end;

theorem :: FUNCT_9:25

for i being non zero Integer holds tan is PI * i -periodic

proof end;

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

proof end;

theorem :: FUNCT_9:26

for i being non zero Integer holds cot is PI * i -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;

theorem :: FUNCT_9:27

for i being non zero Integer holds |.sin.| is PI * i -periodic

proof end;

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

proof end;

theorem :: FUNCT_9:28

for i being non zero Integer holds |.cos.| is PI * i -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;

theorem :: FUNCT_9:29

for i being non zero Integer holds |.sin.| + |.cos.| is (PI / 2) * i -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;

theorem :: FUNCT_9:30

for i being non zero Integer holds sin ^2 is PI * i -periodic

proof end;

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

proof end;

theorem :: FUNCT_9:31

for i being non zero Integer holds cos ^2 is PI * i -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;

theorem :: FUNCT_9:32

for i being non zero Integer holds sin (#) cos is PI * i -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 Th33: :: FUNCT_9:33

for a, b being Real
for i being non zero Integer holds b + (a (#) sin) is (2 * PI) * i -periodic

proof end;

theorem :: FUNCT_9:34

for a, b being Real
for i being non zero Integer holds (a (#) sin) - b is (2 * PI) * i -periodic by Th33;

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

proof end;

theorem Th35: :: FUNCT_9:35

for a, b being Real
for i being non zero Integer holds b + (a (#) cos) is (2 * PI) * i -periodic

proof end;

theorem :: FUNCT_9:36

for a, b being Real
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 st t <> 0 holds
REAL --> a is t -periodic by Lm1;

registration

let a be Real;

cluster REAL --> a -> periodic ;

coherence
REAL --> a is periodic

proof end;

end;

registration

let t be non zero Real;

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₁ being Function of REAL,REAL st b₁ is t -periodic

proof end;

end;