mathlib documentation

algebra.periodic

Periodicity #

In this file we define and then prove facts about periodic and antiperiodic functions.

Main definitions #

Note that any c-antiperiodic function will necessarily also be 2*c-periodic.

Tags #

period, periodic, periodicity, antiperiodic

Periodicity #

@[simp]
def function.periodic {α : Type u_1} {β : Type u_2} [has_add α] (f : α → β) (c : α) :
Prop

A function f is said to be periodic with period c if for all x, f (x + c) = f x.

Equations
theorem function.periodic.funext {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [has_add α] (h : function.periodic f c) :
(λ (x : α), f (x + c)) = f
theorem function.periodic.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [has_add α] (h : function.periodic f c) (g : β → γ) :
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) :
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) :
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) :
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) :
theorem list.periodic_sum {α : Type u_1} {β : Type u_2} {c : α} [has_add α] [add_comm_monoid β] (l : list (α → β)) (hl : ∀ (f : α → β), f lfunction.periodic f c) :
theorem list.periodic_prod {α : Type u_1} {β : Type u_2} {c : α} [has_add α] [comm_monoid β] (l : list (α → β)) (hl : ∀ (f : α → β), f lfunction.periodic f c) :
theorem multiset.periodic_sum {α : Type u_1} {β : Type u_2} {c : α} [has_add α] [add_comm_monoid β] (s : multiset (α → β)) (hs : ∀ (f : α → β), f sfunction.periodic f c) :
theorem multiset.periodic_prod {α : Type u_1} {β : Type u_2} {c : α} [has_add α] [comm_monoid β] (s : multiset (α → β)) (hs : ∀ (f : α → β), f sfunction.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 sfunction.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 sfunction.periodic (f i) c) :
function.periodic (s.prod (λ (i : ι), f i)) c
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 : γ) :
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 : γ) :
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 : α) :
f (x - c) = f x
theorem function.periodic.sub_eq' {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [add_comm_group α] (h : function.periodic f c) :
f (c - x) = f (-x)
theorem function.periodic.neg {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [add_group α] (h : 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.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 : ) :
theorem function.periodic.nat_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [semiring α] (h : function.periodic f c) (n : ) :
theorem function.periodic.neg_nsmul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [add_group α] (h : function.periodic f c) (n : ) :
theorem function.periodic.neg_nat_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [ring α] (h : function.periodic f c) (n : ) :
theorem function.periodic.sub_nsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [add_group α] (h : function.periodic f c) (n : ) :
f (x - n c) = f x
theorem function.periodic.sub_nat_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [ring α] (h : function.periodic f c) (n : ) :
f (x - n * c) = f x
theorem function.periodic.nsmul_sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [add_comm_group α] (h : function.periodic f c) (n : ) :
f (n c - x) = f (-x)
theorem function.periodic.nat_mul_sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [ring α] (h : function.periodic f c) (n : ) :
f (n * c - x) = f (-x)
theorem function.periodic.zsmul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [add_group α] (h : function.periodic f c) (n : ) :
theorem function.periodic.int_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [ring α] (h : function.periodic f c) (n : ) :
theorem function.periodic.sub_zsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [add_group α] (h : function.periodic f c) (n : ) :
f (x - n c) = f x
theorem function.periodic.sub_int_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [ring α] (h : function.periodic f c) (n : ) :
f (x - n * c) = f x
theorem function.periodic.zsmul_sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [add_comm_group α] (h : function.periodic f c) (n : ) :
f (n c - x) = f (-x)
theorem function.periodic.int_mul_sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [ring α] (h : function.periodic f c) (n : ) :
f (n * c - x) = f (-x)
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) :
f (-c) = f 0
theorem function.periodic.nsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [add_monoid α] (h : function.periodic f c) (n : ) :
f (n c) = f 0
theorem function.periodic.nat_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [semiring α] (h : function.periodic f c) (n : ) :
f (n * c) = f 0
theorem function.periodic.zsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [add_group α] (h : function.periodic f c) (n : ) :
f (n c) = f 0
theorem function.periodic.int_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [ring α] (h : function.periodic f c) (n : ) :
f (n * c) = f 0
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 : α) :
∃ (y : α) (H : y set.Ico 0 c), f x = f y

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 : α) :
∃ (y : α) (H : y set.Ico a (a + c)), 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.

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 : α) :
∃ (y : α) (H : y set.Ioc a (a + c)), 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.

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 : α) :
f '' set.Ioc a (a + c) = set.range f
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 : α) :
f (a +ᵥ x) = f 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 : α) :
f (a +ᵥ x) = f 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
@[simp]
theorem function.periodic.lift_coe {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [add_group α] (h : function.periodic f c) (a : α) :
h.lift a = f 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
theorem function.antiperiodic.funext {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [has_add α] [has_neg β] (h : function.antiperiodic f c) :
(λ (x : α), f (x + c)) = -f
theorem function.antiperiodic.funext' {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [has_add α] [has_involutive_neg β] (h : function.antiperiodic f c) :
(λ (x : α), -f (x + c)) = f
theorem function.antiperiodic.periodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [semiring α] [has_involutive_neg β] (h : function.antiperiodic f 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) :
f c = -f 0
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 : ) :
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 : ) :
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 : ) :
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 : ) :
theorem function.antiperiodic.nat_mul_eq_of_eq_zero {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [comm_semiring α] [subtraction_monoid β] (h : function.antiperiodic f c) (hi : f 0 = 0) (n : ) :
f (n * c) = 0
theorem function.antiperiodic.int_mul_eq_of_eq_zero {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [comm_ring α] [subtraction_monoid β] (h : function.antiperiodic f c) (hi : f 0 = 0) (n : ) :
f (n * c) = 0
theorem function.antiperiodic.sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [add_group α] [has_involutive_neg β] (h : function.antiperiodic f c) (x : α) :
f (x - c) = -f 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) :
f (c - x) = -f (-x)
theorem function.antiperiodic.neg {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [add_group α] [has_involutive_neg β] (h : 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) :
f (-c) = -f 0
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
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 : γ) :
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 α] [has_involutive_neg β] (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 α] [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_comm_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₂) :
f (c₁ + c₂) = -f 0
theorem function.periodic.sub_antiperiod_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [add_comm_group α] [has_involutive_neg β] (h1 : function.periodic f c₁) (h2 : function.antiperiodic f c₂) :
f (c₁ - c₂) = -f 0
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) :
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) :