let F be Function of REAL,REAL; :: thesis: for a, b, c, d being Real st ( for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ) holds
F is periodic
let a, b, c, d be Real; :: thesis: ( ( for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ) implies F is periodic )
assume A0: for x being Real holds F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ; :: thesis: F is periodic
ex t being Real st F is t -periodic
proof
per cases ( a <> 0 or a = 0 ) ;
suppose A1: a <> 0 ; :: thesis: ex t being Real st F is t -periodic
take ((2 * PI) / a) * 1 ; :: thesis: F is ((2 * PI) / a) * 1 -periodic
thus F is ((2 * PI) / a) * 1 -periodic by TrF160, A0, A1; :: thesis: verum
end;
suppose A5: a = 0 ; :: thesis: ex t being Real st F is t -periodic
take 1 ; :: thesis: F is 1 -periodic
for x being Real st x in dom F holds
( x + 1 in dom F & x - 1 in dom F & F . x = F . (x + 1) )
proof
let x be Real; :: thesis: ( x in dom F implies ( x + 1 in dom F & x - 1 in dom F & F . x = F . (x + 1) ) )
assume x in dom F ; :: thesis: ( x + 1 in dom F & x - 1 in dom F & F . x = F . (x + 1) )
A4A: ( x + 1 in REAL & x - 1 in REAL ) by XREAL_0:def 1;
F . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) by A0
.= max (0,(min (1,((c * (sin ((0 * (x + 1)) + b))) + d)))) by A5 ;
hence ( x + 1 in dom F & x - 1 in dom F & F . x = F . (x + 1) ) by A4A, FUNCT_2:def 1, A0, A5; :: thesis: verum
end;
hence F is 1 -periodic by FUNCT_9:1; :: thesis: verum
end;
end;
end;
hence F is periodic by FUNCT_9:def 2; :: thesis: verum