:: 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 b1 being Function st
( b1 is periodic & b1 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 b1 being PartFunc of REAL,REAL st b1 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 b1 being Function st
( b1 is t -periodic & b1 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 b1 being Function of REAL,REAL st b1 is t -periodic
proof end;
end;