Periodicity #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
@[protected]
theorem
function.periodic.funext
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[has_add α]
(h : function.periodic f c) :
@[protected]
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)
@[protected]
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
@[protected]
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
@[protected]
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
@[protected]
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
list.periodic_sum
{α : Type u_1}
{β : Type u_2}
{c : α}
[has_add α]
[add_monoid β]
(l : list (α → β))
(hl : ∀ (f : α → β), f ∈ l → function.periodic f c) :
function.periodic l.sum c
theorem
multiset.periodic_sum
{α : Type u_1}
{β : Type u_2}
{c : α}
[has_add α]
[add_comm_monoid β]
(s : multiset (α → β))
(hs : ∀ (f : α → β), f ∈ s → function.periodic f c) :
function.periodic s.sum c
theorem
multiset.periodic_prod
{α : Type u_1}
{β : Type u_2}
{c : α}
[has_add α]
[comm_monoid β]
(s : multiset (α → β))
(hs : ∀ (f : α → β), f ∈ s → function.periodic f c) :
theorem
finset.periodic_sum
{α : Type u_1}
{β : Type u_2}
{c : α}
[has_add α]
[add_comm_monoid β]
{ι : Type u_3}
{f : ι → α → β}
(s : finset ι)
(hs : ∀ (i : ι), i ∈ s → function.periodic (f i) c) :
function.periodic (s.sum (λ (i : ι), f i)) c
theorem
finset.periodic_prod
{α : Type u_1}
{β : Type u_2}
{c : α}
[has_add α]
[comm_monoid β]
{ι : Type u_3}
{f : ι → α → β}
(s : finset ι)
(hs : ∀ (i : ι), i ∈ s → function.periodic (f i) c) :
function.periodic (s.prod (λ (i : ι), f i)) c
@[protected]
theorem
function.periodic.smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[has_add α]
[has_smul γ β]
(h : function.periodic f c)
(a : γ) :
function.periodic (a • f) c
@[protected]
theorem
function.periodic.vadd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[has_add α]
[has_vadd γ β]
(h : function.periodic f c)
(a : γ) :
function.periodic (a +ᵥ f) c
@[protected]
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_semiring γ]
[module γ α]
(h : function.periodic f c)
(a : γ) :
function.periodic (λ (x : α), f (a • x)) (a⁻¹ • c)
@[protected]
theorem
function.periodic.const_mul
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_semiring α]
(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_semiring γ]
[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_semiring α]
(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_semiring α]
(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_semiring α]
(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_semiring α]
(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_semiring α]
(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) :
@[protected]
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_group α]
(h1 : function.periodic f c₁)
(h2 : function.periodic f c₂) :
function.periodic f (c₁ - c₂)
theorem
function.periodic.const_add
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_semigroup α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (a + x)) c
theorem
function.periodic.add_const
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_comm_semigroup α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (x + a)) c
theorem
function.periodic.const_sub
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_comm_group α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (a - x)) c
theorem
function.periodic.sub_const
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_comm_group α]
(h : function.periodic f c)
(a : α) :
function.periodic (λ (x : α), f (x - a)) 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.nsmul_sub_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[add_comm_group α]
(h : function.periodic f c)
(n : ℕ) :
@[protected]
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)
@[protected]
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.zsmul_sub_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[add_comm_group α]
(h : function.periodic f c)
(n : ℤ) :
@[protected]
theorem
function.periodic.eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_zero_class α]
(h : function.periodic f c) :
f c = f 0
@[protected]
theorem
function.periodic.neg_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
(h : function.periodic f c) :
@[protected]
theorem
function.periodic.nsmul_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_monoid α]
(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.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 #
@[protected]
theorem
function.antiperiodic.funext'
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[has_add α]
[has_involutive_neg β]
(h : function.antiperiodic f c) :
@[protected]
theorem
function.antiperiodic.periodic
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[semiring α]
[has_involutive_neg β]
(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.
@[protected]
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 α]
[has_involutive_neg β]
(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 α]
[has_involutive_neg β]
(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 α]
[has_involutive_neg β]
(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 α]
[has_involutive_neg β]
(h : function.antiperiodic f c)
(n : ℤ) :
function.antiperiodic f (↑n * (2 * c) + c)
theorem
function.antiperiodic.sub_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
[has_involutive_neg β]
(h : function.antiperiodic f c)
(x : α) :
theorem
function.antiperiodic.sub_eq'
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c x : α}
[add_comm_group α]
[has_neg β]
(h : function.antiperiodic f c) :
@[protected]
theorem
function.antiperiodic.neg
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
[has_involutive_neg β]
(h : function.antiperiodic f c) :
function.antiperiodic f (-c)
theorem
function.antiperiodic.neg_eq
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_group α]
[has_involutive_neg β]
(h : function.antiperiodic f c) :
theorem
function.antiperiodic.nat_mul_eq_of_eq_zero
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[ring α]
[neg_zero_class β]
(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 : α}
[ring α]
[subtraction_monoid β]
(h : function.antiperiodic f c)
(hi : f 0 = 0)
(n : ℤ) :
theorem
function.antiperiodic.const_add
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_semigroup α]
[has_neg β]
(h : function.antiperiodic f c)
(a : α) :
function.antiperiodic (λ (x : α), f (a + x)) c
theorem
function.antiperiodic.add_const
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_comm_semigroup α]
[has_neg β]
(h : function.antiperiodic f c)
(a : α) :
function.antiperiodic (λ (x : α), f (x + a)) c
theorem
function.antiperiodic.const_sub
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_comm_group α]
[has_involutive_neg β]
(h : function.antiperiodic f c)
(a : α) :
function.antiperiodic (λ (x : α), f (a - x)) c
theorem
function.antiperiodic.sub_const
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[add_comm_group α]
[has_neg β]
(h : function.antiperiodic f c)
(a : α) :
function.antiperiodic (λ (x : α), f (x - a)) c
@[protected]
theorem
function.antiperiodic.smul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{c : α}
[has_add α]
[monoid γ]
[add_group β]
[distrib_mul_action γ β]
(h : function.antiperiodic f c)
(a : γ) :
function.antiperiodic (a • 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_semiring γ]
[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_semiring α]
[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_semiring γ]
[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_semiring α]
[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_semiring α]
[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_semiring α]
[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_semiring α]
[has_neg β]
(h : function.antiperiodic f c)
{a : α}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (x * a⁻¹)) (c * a)
@[protected]
theorem
function.antiperiodic.div_inv
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c : α}
[division_semiring α]
[has_neg β]
(h : function.antiperiodic f c)
{a : α}
(ha : a ≠ 0) :
function.antiperiodic (λ (x : α), f (x / a)) (c * a)
@[protected]
theorem
function.antiperiodic.add
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_group α]
[has_involutive_neg β]
(h1 : function.antiperiodic f c₁)
(h2 : function.antiperiodic f c₂) :
function.periodic f (c₁ + c₂)
@[protected]
theorem
function.antiperiodic.sub
{α : Type u_1}
{β : Type u_2}
{f : α → β}
{c₁ c₂ : α}
[add_group α]
[has_involutive_neg β]
(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 α]
[has_neg β]
(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_group α]
[has_involutive_neg β]
(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 α]
[has_neg β]
(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_group α]
[has_involutive_neg β]
(h1 : function.periodic f c₁)
(h2 : function.antiperiodic f c₂) :
@[protected]
theorem
function.antiperiodic.mul
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{c : α}
[has_add α]
[has_mul β]
[has_distrib_neg β]
(hf : function.antiperiodic f c)
(hg : function.antiperiodic g c) :
function.periodic (f * g) c
@[protected]
theorem
function.antiperiodic.div
{α : Type u_1}
{β : Type u_2}
{f g : α → β}
{c : α}
[has_add α]
[division_monoid β]
[has_distrib_neg β]
(hf : function.antiperiodic f c)
(hg : function.antiperiodic g c) :
function.periodic (f / g) c