Periodicity #
In this file we define and then prove facts about periodic and antiperiodic functions.
Main definitions #
Function.Periodic
: A functionf
is periodic if∀ x, f (x + c) = f x
.f
is referred to as periodic with periodc
orc
-periodic.Function.Antiperiodic
: A functionf
is antiperiodic if∀ x, f (x + c) = -f x
.f
is referred to as antiperiodic with antiperiodc
orc
-antiperiodic.
Note that any c
-antiperiodic function will necessarily also be 2 • c
-periodic.
Tags #
period, periodic, periodicity, antiperiodic
Periodicity #
A function f
is said to be Periodic
with period c
if for all x
, f (x + c) = f x
.
Instances For
If a function f
is Periodic
with positive period c
, then for all x
there exists some
y ∈ Ico 0 c
such that f x = f y
.
If a function f
is Periodic
with positive period c
, then for all x
there exists some
y ∈ Ico a (a + c)
such that f x = f y
.
If a function f
is Periodic
with positive period c
, then for all x
there exists some
y ∈ Ioc a (a + c)
such that f x = f y
.
Lift a periodic function to a function from the quotient group.
Equations
Instances For
A periodic function f : R → X
on a semiring (or, more generally, AddZeroClass
)
of non-zero period is not injective.
Antiperiodicity #
A function f
is said to be antiperiodic
with antiperiod c
if for all x
,
f (x + c) = -f x
.
Instances For
If a function is antiperiodic
with antiperiod c
, then it is also Periodic
with period
2 • c
.
If a function is antiperiodic
with antiperiod c
, then it is also Periodic
with period
2 * c
.