:: Basic Properties of Periodic Functions
:: by Bo Li , Yanhong Men , Dailu Li and Xiquan Liang
::
:: 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 ;

registration
existence
ex b1 being Function st
( b1 is periodic & b1 is real-valued )
by ;
existence
ex b1 being PartFunc of REAL,REAL st b1 is periodic
proof end;
end;

registration
let t be non zero Real;
coherence
REAL --> t is t -periodic
by Lm1;
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;
coherence
|.F.| is periodic
proof end;
cluster F " -> periodic ;
coherence
F " is periodic
proof end;
coherence
F ^2 is periodic
proof end;
end;

Lm3: cos is 2 * PI -periodic
by ;

registration
coherence by Lm2;
coherence 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:
proof end;

Lm7: sec is 2 * PI -periodic
proof end;

registration
coherence by Lm6;
coherence 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:
proof end;

Lm11:
proof end;

registration
coherence by Lm10;
coherence 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:
proof end;

Lm15:
proof end;

Lm16: for k being Nat holds is PI * (k + 1) -periodic
proof end;

theorem :: FUNCT_9:27
for i being non zero Integer holds is PI * i -periodic
proof end;

Lm17: for k being Nat holds is PI * (k + 1) -periodic
proof end;

theorem :: FUNCT_9:28
for i being non zero Integer holds is PI * i -periodic
proof end;

Lm18:
proof end;

Lm19: for k being Nat holds + is (PI / 2) * (k + 1) -periodic
proof end;

theorem :: FUNCT_9:29
for i being non zero Integer holds + is (PI / 2) * i -periodic
proof end;

Lm20:
proof end;

Lm21:
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:
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 + () is 2 * PI -periodic
proof end;

Lm27: for a, b being Real holds b + () is 2 * PI -periodic
proof end;

Lm28: for a, b being Real
for k being Nat holds b + () 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 + () is (2 * PI) * i -periodic
proof end;

theorem :: FUNCT_9:34
for a, b being Real
for i being non zero Integer holds () - b is (2 * PI) * i -periodic by Th33;

Lm29: for a, b being Real
for k being Nat holds b + () 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 + () is (2 * PI) * i -periodic
proof end;

theorem :: FUNCT_9:36
for a, b being Real
for i being non zero Integer holds () - 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;
coherence
proof end;
end;

registration
let t be non zero Real;
existence
ex b1 being Function of REAL,REAL st b1 is t -periodic
proof end;
end;