Periodicity #
In this file we define and then prove facts about periodic and antiperiodic functions.
Main definitions #
-
function.periodic: A functionfis periodic if∀ x, f (x + c) = f x.fis referred to as periodic with periodcorc-periodic. -
function.antiperiodic: A functionfis antiperiodic if∀ x, f (x + c) = -f x.fis referred to as antiperiodic with antiperiodcorc-antiperiodic.
Note that any c-antiperiodic function will necessarily also be 2*c-periodic.
Tags #
period, periodic, periodicity, antiperiodic
Periodicity #
@[simp]
A function f is said to be periodic with period c if for all x, f (x + c) = f x.
Equations
- function.periodic f c = ∀ (x : α), f (x + c) = f x
theorem
function.periodic.funext
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[has_add α]
(h : function.periodic f c) :
theorem
function.periodic.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[has_add α]
(h : function.periodic f c)
(g : β → γ) :
function.periodic (g ∘ f) c
theorem
function.periodic.comp_add_hom
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[has_add α]
[has_add γ]
(h : function.periodic f c)
(g : add_hom γ α)
(g_inv : α → γ)
(hg : function.right_inverse g_inv ⇑g) :
function.periodic (f ∘ ⇑g) (g_inv c)
theorem
function.periodic.mul
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{c : α}
[has_add α]
[has_mul β]
(hf : function.periodic f c)
(hg : function.periodic g c) :
function.periodic (f * g) c
theorem
function.periodic.add
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{c : α}
[has_add α]
[has_add β]
(hf : function.periodic f c)
(hg : function.periodic g c) :
function.periodic (f + g) c
theorem
function.periodic.sub
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{c : α}
[has_add α]
[has_sub β]
(hf : function.periodic f c)
(hg : function.periodic g c) :
function.periodic (f - g) c
theorem
function.periodic.div
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{c : α}
[has_add α]
[has_div β]
(hf : function.periodic f c)
(hg : function.periodic g c) :
function.periodic (f / g) c
theorem
function.periodic.const_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[add_monoid α]
[group γ]
[distrib_mul_action γ α]
(h : function.periodic f c)
(a : γ) :
function.periodic (λ (x : α), f (a • x)) (a⁻¹ • c)
theorem
function.periodic.const_smul₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[add_comm_monoid α]
[division_ring γ]
[module γ α]
(h : function.periodic f c)
(a : γ) :
function.periodic (λ (x : α), f (a • x)) (a⁻¹ • c)
theorem
function.periodic.const_mul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (a * x)) (a⁻¹ * c)
theorem
function.periodic.const_inv_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[add_monoid α]
[group γ]
[distrib_mul_action γ α]
(h : function.periodic f c)
(a : γ) :
function.periodic (λ (x : α), f (a⁻¹ • x)) (a • c)
theorem
function.periodic.const_inv_smul₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[add_comm_monoid α]
[division_ring γ]
[module γ α]
(h : function.periodic f c)
(a : γ) :
function.periodic (λ (x : α), f (a⁻¹ • x)) (a • c)
theorem
function.periodic.const_inv_mul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (a⁻¹ * x)) (a * c)
theorem
function.periodic.mul_const
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (x * a)) (c * a⁻¹)
theorem
function.periodic.mul_const'
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (x * a)) (c / a)
theorem
function.periodic.mul_const_inv
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (x * a⁻¹)) (c * a)
theorem
function.periodic.div_const
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (x / a)) (c * a)
theorem
function.periodic.add_period
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_semigroup α]
(h1 : function.periodic f c₁)
(h2 : function.periodic f c₂) :
function.periodic f (c₁ + c₂)
theorem
function.periodic.sub_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
(h : function.periodic f c)
(x : α) :
theorem
function.periodic.sub_eq'
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[add_comm_group α]
(h : function.periodic f c) :
theorem
function.periodic.neg
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
(h : function.periodic f c) :
function.periodic f (-c)
theorem
function.periodic.sub_period
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_comm_group α]
(h1 : function.periodic f c₁)
(h2 : function.periodic f c₂) :
function.periodic f (c₁ - c₂)
theorem
function.periodic.nsmul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_monoid α]
(h : function.periodic f c)
(n : ℕ) :
function.periodic f (n • c)
theorem
function.periodic.nat_mul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[semiring α]
(h : function.periodic f c)
(n : ℕ) :
function.periodic f ((↑n) * c)
theorem
function.periodic.neg_nsmul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
(h : function.periodic f c)
(n : ℕ) :
function.periodic f (-(n • c))
theorem
function.periodic.neg_nat_mul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[ring α]
(h : function.periodic f c)
(n : ℕ) :
function.periodic f (-(↑n) * c)
theorem
function.periodic.sub_nsmul_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[add_group α]
(h : function.periodic f c)
(n : ℕ) :
theorem
function.periodic.sub_nat_mul_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[ring α]
(h : function.periodic f c)
(n : ℕ) :
theorem
function.periodic.nsmul_sub_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[add_comm_group α]
(h : function.periodic f c)
(n : ℕ) :
theorem
function.periodic.nat_mul_sub_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[ring α]
(h : function.periodic f c)
(n : ℕ) :
theorem
function.periodic.zsmul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
(h : function.periodic f c)
(n : ℤ) :
function.periodic f (n • c)
theorem
function.periodic.int_mul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[ring α]
(h : function.periodic f c)
(n : ℤ) :
function.periodic f ((↑n) * c)
theorem
function.periodic.sub_zsmul_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[add_group α]
(h : function.periodic f c)
(n : ℤ) :
theorem
function.periodic.sub_int_mul_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[ring α]
(h : function.periodic f c)
(n : ℤ) :
theorem
function.periodic.zsmul_sub_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[add_comm_group α]
(h : function.periodic f c)
(n : ℤ) :
theorem
function.periodic.int_mul_sub_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[ring α]
(h : function.periodic f c)
(n : ℤ) :
theorem
function.periodic.eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_zero_class α]
(h : function.periodic f c) :
f c = f 0
theorem
function.periodic.neg_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
(h : function.periodic f c) :
theorem
function.periodic.nsmul_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_monoid α]
(h : function.periodic f c)
(n : ℕ) :
theorem
function.periodic.nat_mul_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[semiring α]
(h : function.periodic f c)
(n : ℕ) :
theorem
function.periodic.zsmul_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
(h : function.periodic f c)
(n : ℤ) :
theorem
function.periodic.int_mul_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[ring α]
(h : function.periodic f c)
(n : ℤ) :
theorem
function.periodic.exists_mem_Ico₀
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[linear_ordered_add_comm_group α]
[archimedean α]
(h : function.periodic f c)
(hc : 0 < c)
(x : α) :
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.
theorem
function.periodic.exists_mem_Ico
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[linear_ordered_add_comm_group α]
[archimedean α]
(h : function.periodic f c)
(hc : 0 < c)
(x a : α) :
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.
theorem
function.periodic.exists_mem_Ioc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[linear_ordered_add_comm_group α]
[archimedean α]
(h : function.periodic f c)
(hc : 0 < c)
(x a : α) :
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.
theorem
function.periodic.image_Ioc
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[linear_ordered_add_comm_group α]
[archimedean α]
(h : function.periodic f c)
(hc : 0 < c)
(a : α) :
theorem
function.periodic_with_period_zero
{α : Type u_1}
{β : Type u_2}
[add_zero_class α]
(f : α → β) :
theorem
function.periodic.map_vadd_zmultiples
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_comm_group α]
(hf : function.periodic f c)
(a : ↥(add_subgroup.zmultiples c))
(x : α) :
theorem
function.periodic.map_vadd_multiples
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_comm_monoid α]
(hf : function.periodic f c)
(a : ↥(add_submonoid.multiples c))
(x : α) :
def
function.periodic.lift
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
(h : function.periodic f c)
(x : α ⧸ add_subgroup.zmultiples c) :
β
Lift a periodic function to a function from the quotient group.
Equations
- h.lift x = quotient.lift_on' x f _
@[simp]
theorem
function.periodic.lift_coe
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
(h : function.periodic f c)
(a : α) :
Antiperiodicity #
@[simp]
def
function.antiperiodic
{α : Type u_1}
{β : Type u_2}
[has_add α]
[has_neg β]
(f : α → β)
(c : α) :
Prop
A function f is said to be antiperiodic with antiperiod c if for all x,
f (x + c) = -f x.
Equations
- function.antiperiodic f c = ∀ (x : α), f (x + c) = -f x
theorem
function.antiperiodic.funext
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[has_add α]
[has_neg β]
(h : function.antiperiodic f c) :
theorem
function.antiperiodic.funext'
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[has_add α]
[add_group β]
(h : function.antiperiodic f c) :
theorem
function.antiperiodic.periodic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[semiring α]
[add_group β]
(h : function.antiperiodic f c) :
function.periodic f (2 * c)
If a function is antiperiodic with antiperiod c, then it is also periodic with period
2 * c.
theorem
function.antiperiodic.eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_zero_class α]
[has_neg β]
(h : function.antiperiodic f c) :
theorem
function.antiperiodic.nat_even_mul_periodic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[semiring α]
[add_group β]
(h : function.antiperiodic f c)
(n : ℕ) :
function.periodic f ((↑n) * 2 * c)
theorem
function.antiperiodic.nat_odd_mul_antiperiodic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[semiring α]
[add_group β]
(h : function.antiperiodic f c)
(n : ℕ) :
function.antiperiodic f ((↑n) * 2 * c + c)
theorem
function.antiperiodic.int_even_mul_periodic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[ring α]
[add_group β]
(h : function.antiperiodic f c)
(n : ℤ) :
function.periodic f ((↑n) * 2 * c)
theorem
function.antiperiodic.int_odd_mul_antiperiodic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[ring α]
[add_group β]
(h : function.antiperiodic f c)
(n : ℤ) :
function.antiperiodic f ((↑n) * 2 * c + c)
theorem
function.antiperiodic.nat_mul_eq_of_eq_zero
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[comm_semiring α]
[add_group β]
(h : function.antiperiodic f c)
(hi : f 0 = 0)
(n : ℕ) :
theorem
function.antiperiodic.int_mul_eq_of_eq_zero
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[comm_ring α]
[add_group β]
(h : function.antiperiodic f c)
(hi : f 0 = 0)
(n : ℤ) :
theorem
function.antiperiodic.sub_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
[add_group β]
(h : function.antiperiodic f c)
(x : α) :
theorem
function.antiperiodic.sub_eq'
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[add_comm_group α]
[add_group β]
(h : function.antiperiodic f c) :
theorem
function.antiperiodic.neg
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
[add_group β]
(h : function.antiperiodic f c) :
function.antiperiodic f (-c)
theorem
function.antiperiodic.neg_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
[add_group β]
(h : function.antiperiodic f c) :
theorem
function.antiperiodic.const_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[add_monoid α]
[has_neg β]
[group γ]
[distrib_mul_action γ α]
(h : function.antiperiodic f c)
(a : γ) :
function.antiperiodic (λ (x : α), f (a • x)) (a⁻¹ • c)
theorem
function.antiperiodic.const_smul₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[add_comm_monoid α]
[has_neg β]
[division_ring γ]
[module γ α]
(h : function.antiperiodic f c)
{a : γ}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (a • x)) (a⁻¹ • c)
theorem
function.antiperiodic.const_mul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
[has_neg β]
(h : function.antiperiodic f c)
{a : α}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (a * x)) (a⁻¹ * c)
theorem
function.antiperiodic.const_inv_smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[add_monoid α]
[has_neg β]
[group γ]
[distrib_mul_action γ α]
(h : function.antiperiodic f c)
(a : γ) :
function.antiperiodic (λ (x : α), f (a⁻¹ • x)) (a • c)
theorem
function.antiperiodic.const_inv_smul₀
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[add_comm_monoid α]
[has_neg β]
[division_ring γ]
[module γ α]
(h : function.antiperiodic f c)
{a : γ}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (a⁻¹ • x)) (a • c)
theorem
function.antiperiodic.const_inv_mul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
[has_neg β]
(h : function.antiperiodic f c)
{a : α}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (a⁻¹ * x)) (a * c)
theorem
function.antiperiodic.mul_const
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
[has_neg β]
(h : function.antiperiodic f c)
{a : α}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (x * a)) (c * a⁻¹)
theorem
function.antiperiodic.mul_const'
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
[has_neg β]
(h : function.antiperiodic f c)
{a : α}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (x * a)) (c / a)
theorem
function.antiperiodic.mul_const_inv
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
[has_neg β]
(h : function.antiperiodic f c)
{a : α}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (x * a⁻¹)) (c * a)
theorem
function.antiperiodic.div_inv
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_ring α]
[has_neg β]
(h : function.antiperiodic f c)
{a : α}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (x / a)) (c * a)
theorem
function.antiperiodic.add
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_group α]
[add_group β]
(h1 : function.antiperiodic f c₁)
(h2 : function.antiperiodic f c₂) :
function.periodic f (c₁ + c₂)
theorem
function.antiperiodic.sub
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_comm_group α]
[add_group β]
(h1 : function.antiperiodic f c₁)
(h2 : function.antiperiodic f c₂) :
function.periodic f (c₁ - c₂)
theorem
function.periodic.add_antiperiod
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_group α]
[add_group β]
(h1 : function.periodic f c₁)
(h2 : function.antiperiodic f c₂) :
function.antiperiodic f (c₁ + c₂)
theorem
function.periodic.sub_antiperiod
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_comm_group α]
[add_group β]
(h1 : function.periodic f c₁)
(h2 : function.antiperiodic f c₂) :
function.antiperiodic f (c₁ - c₂)
theorem
function.periodic.add_antiperiod_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_group α]
[add_group β]
(h1 : function.periodic f c₁)
(h2 : function.antiperiodic f c₂) :
theorem
function.periodic.sub_antiperiod_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_comm_group α]
[add_group β]
(h1 : function.periodic f c₁)
(h2 : function.antiperiodic f c₂) :
theorem
function.antiperiodic.mul
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{c : α}
[has_add α]
[ring β]
(hf : function.antiperiodic f c)
(hg : function.antiperiodic g c) :
function.periodic (f * g) c
theorem
function.antiperiodic.div
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{c : α}
[has_add α]
[division_ring β]
(hf : function.antiperiodic f c)
(hg : function.antiperiodic g c) :
function.periodic (f / g) c