Periodicity

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

Main definitions

• Function.Periodic: A function f is periodic if ∀ x, f (x + c) = f x. f is referred to as periodic with period c or c-periodic.

• Function.Antiperiodic: A function f is antiperiodic if ∀ x, f (x + c) = -f x. f is referred to as antiperiodic with antiperiod c or c-antiperiodic.

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

Tags

period, periodic, periodicity, antiperiodic

Periodicity

def Function.Periodic {α : Type u_1} {β : Type u_2} [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

• Function.Periodic f c = ∀ (x : α), f (x + c) = f x

theorem Function.Periodic.funext {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [Add α] (h : Periodic f c) : (fun (x : α) => f (x + c)) = f

theorem Function.Periodic.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [Add α] (h : Periodic f c) (g : β → γ) : Periodic (g ∘ f) c

theorem Function.Periodic.comp_addHom {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [Add α] [Add γ] (h : Periodic f c) (g : γ →ₙ+ α) (g_inv : α → γ) (hg : RightInverse g_inv ⇑g) : Periodic (f ∘ ⇑g) (g_inv c)

theorem Function.Periodic.mul {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [Add α] [Mul β] (hf : Periodic f c) (hg : Periodic g c) : Periodic (f * g) c

theorem Function.Periodic.add {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [Add α] [Add β] (hf : Periodic f c) (hg : Periodic g c) : Periodic (f + g) c

theorem Function.Periodic.div {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [Add α] [Div β] (hf : Periodic f c) (hg : Periodic g c) : Periodic (f / g) c

theorem Function.Periodic.sub {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [Add α] [Sub β] (hf : Periodic f c) (hg : Periodic g c) : Periodic (f - g) c

theorem List.periodic_prod {α : Type u_1} {β : Type u_2} {c : α} [Add α] [MulOneClass β] (l : List (α → β)) (hl : ∀ f ∈ l, Function.Periodic f c) : Function.Periodic l.prod c

theorem List.periodic_sum {α : Type u_1} {β : Type u_2} {c : α} [Add α] [AddZeroClass β] (l : List (α → β)) (hl : ∀ f ∈ l, Function.Periodic f c) : Function.Periodic l.sum c

theorem Multiset.periodic_prod {α : Type u_1} {β : Type u_2} {c : α} [Add α] [CommMonoid β] (s : Multiset (α → β)) (hs : ∀ f ∈ s, Function.Periodic f c) : Function.Periodic s.prod c

theorem Multiset.periodic_sum {α : Type u_1} {β : Type u_2} {c : α} [Add α] [AddCommMonoid β] (s : Multiset (α → β)) (hs : ∀ f ∈ s, Function.Periodic f c) : Function.Periodic s.sum c

theorem Finset.periodic_prod {α : Type u_1} {β : Type u_2} {c : α} [Add α] [CommMonoid β] {ι : Type u_4} {f : ι → α → β} (s : Finset ι) (hs : ∀ i ∈ s, Function.Periodic (f i) c) : Function.Periodic (∏ i ∈ s, f i) c

theorem Finset.periodic_sum {α : Type u_1} {β : Type u_2} {c : α} [Add α] [AddCommMonoid β] {ι : Type u_4} {f : ι → α → β} (s : Finset ι) (hs : ∀ i ∈ s, Function.Periodic (f i) c) : Function.Periodic (∑ i ∈ s, f i) c

theorem Function.Periodic.smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [Add α] [SMul γ β] (h : Periodic f c) (a : γ) : Periodic (a • f) c

theorem Function.Periodic.vadd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [Add α] [VAdd γ β] (h : Periodic f c) (a : γ) : Periodic (a +ᵥ f) c

theorem Function.Periodic.const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [AddMonoid α] [Group γ] [DistribMulAction γ α] (h : Periodic f c) (a : γ) : Periodic (fun (x : α) => f (a • x)) (a⁻¹ • c)

theorem Function.Periodic.const_inv_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [AddMonoid α] [Group γ] [DistribMulAction γ α] (h : Periodic f c) (a : γ) : Periodic (fun (x : α) => f (a⁻¹ • x)) (a • c)

theorem Function.Periodic.add_period {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [AddSemigroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) : Periodic f (c₁ + c₂)

theorem Function.Periodic.sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] (h : Periodic f c) (x : α) : f (x - c) = f x

theorem Function.Periodic.sub_eq' {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [SubtractionCommMonoid α] (h : Periodic f c) : f (c - x) = f (-x)

theorem Function.Periodic.neg {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] (h : Periodic f c) : Periodic f (-c)

theorem Function.Periodic.sub_period {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [AddGroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) : Periodic f (c₁ - c₂)

theorem Function.Periodic.const_add {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddSemigroup α] (h : Periodic f c) (a : α) : Periodic (fun (x : α) => f (a + x)) c

theorem Function.Periodic.add_const {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommSemigroup α] (h : Periodic f c) (a : α) : Periodic (fun (x : α) => f (x + a)) c

theorem Function.Periodic.const_sub {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommGroup α] (h : Periodic f c) (a : α) : Periodic (fun (x : α) => f (a - x)) c

theorem Function.Periodic.sub_const {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [SubtractionCommMonoid α] (h : Periodic f c) (a : α) : Periodic (fun (x : α) => f (x - a)) c

theorem Function.Periodic.nsmul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddMonoid α] (h : Periodic f c) (n : ℕ) : Periodic f (n • c)

theorem Function.Periodic.nat_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocSemiring α] (h : Periodic f c) (n : ℕ) : Periodic f (↑n * c)

theorem Function.Periodic.neg_nsmul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] (h : Periodic f c) (n : ℕ) : Periodic f (-(n • c))

theorem Function.Periodic.neg_nat_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocRing α] (h : Periodic f c) (n : ℕ) : Periodic f (-(↑n * c))

theorem Function.Periodic.sub_nsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [AddGroup α] (h : 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 : α} [NonAssocRing α] (h : 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 : α} [SubtractionCommMonoid α] (h : 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 : α} [NonAssocRing α] (h : Periodic f c) (n : ℕ) : f (↑n * c - x) = f (-x)

theorem Function.Periodic.zsmul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] (h : Periodic f c) (n : ℤ) : Periodic f (n • c)

theorem Function.Periodic.int_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocRing α] (h : Periodic f c) (n : ℤ) : Periodic f (↑n * c)

theorem Function.Periodic.sub_zsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [AddGroup α] (h : 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 : α} [NonAssocRing α] (h : 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 : α} [AddCommGroup α] (h : 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 : α} [NonAssocRing α] (h : Periodic f c) (n : ℤ) : f (↑n * c - x) = f (-x)

theorem Function.Periodic.eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddZeroClass α] (h : Periodic f c) : f c = f 0

theorem Function.Periodic.neg_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] (h : Periodic f c) : f (-c) = f 0

theorem Function.Periodic.nsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddMonoid α] (h : Periodic f c) (n : ℕ) : f (n • c) = f 0

theorem Function.Periodic.nat_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocSemiring α] (h : Periodic f c) (n : ℕ) : f (↑n * c) = f 0

theorem Function.Periodic.zsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] (h : Periodic f c) (n : ℤ) : f (n • c) = f 0

theorem Function.Periodic.int_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocRing α] (h : Periodic f c) (n : ℤ) : f (↑n * c) = f 0

theorem Function.periodic_with_period_zero {α : Type u_1} {β : Type u_2} [AddZeroClass α] (f : α → β) : Periodic f 0

theorem Function.periodic_iterate_iff {α : Type u_1} {f : α → α} {n : ℕ} {a : α} : Periodic (fun (x : ℕ) => f^[x] a) n ↔ IsPeriodicPt f n a

The iterates a, f a, f^[2] a etc form a periodic sequence with period n iff a is a periodic point for f.

theorem Function.Periodic.isPeriodicPt {α : Type u_1} {f : α → α} {n : ℕ} {a : α} : Periodic (fun (x : ℕ) => f^[x] a) n → IsPeriodicPt f n a

Alias of the forward direction of Function.periodic_iterate_iff.

---

The iterates a, f a, f^[2] a etc form a periodic sequence with period n iff a is a periodic point for f.

theorem Function.IsPeriodicPt.periodic_iterate {α : Type u_1} {f : α → α} {n : ℕ} {a : α} : IsPeriodicPt f n a → Periodic (fun (x : ℕ) => f^[x] a) n

Alias of the reverse direction of Function.periodic_iterate_iff.

---

The iterates a, f a, f^[2] a etc form a periodic sequence with period n iff a is a periodic point for f.

theorem Function.Periodic.map_vadd_zmultiples {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommGroup α] (hf : Periodic f c) (a : ↥(AddSubgroup.zmultiples c)) (x : α) : f (a +ᵥ x) = f x

theorem Function.Periodic.map_vadd_multiples {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommMonoid α] (hf : Periodic f c) (a : ↥(AddSubmonoid.multiples c)) (x : α) : f (a +ᵥ x) = f x

def Function.Periodic.lift {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] (h : Periodic f c) (x : α ⧸ AddSubgroup.zmultiples c) : β

Lift a periodic function to a function from the quotient group.

Equations

• h.lift x = Quotient.liftOn' x f ⋯

@[simp]

theorem Function.Periodic.lift_coe {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] (h : Periodic f c) (a : α) : h.lift ↑a = f a

theorem Function.Periodic.not_injective {R : Type u_4} {X : Type u_5} [AddZeroClass R] {f : R → X} {c : R} (hf : Periodic f c) (hc : c ≠ 0) : ¬Injective f

A periodic function f : R → X on a semiring (or, more generally, AddZeroClass) of non-zero period is not injective.

Antiperiodicity

def Function.Antiperiodic {α : Type u_1} {β : Type u_2} [Add α] [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 : α} [Add α] [Neg β] (h : Antiperiodic f c) : (fun (x : α) => f (x + c)) = -f

theorem Function.Antiperiodic.funext' {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [Add α] [InvolutiveNeg β] (h : Antiperiodic f c) : (fun (x : α) => -f (x + c)) = f

theorem Function.Antiperiodic.periodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c) : Periodic f (2 • c)

If a function is antiperiodic with antiperiod c, then it is also Periodic with period 2 • c.

theorem Function.Antiperiodic.periodic_two_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocSemiring α] [InvolutiveNeg β] (h : Antiperiodic f c) : 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 : α} [AddZeroClass α] [Neg β] (h : Antiperiodic f c) : f c = -f 0

theorem Function.Antiperiodic.even_nsmul_periodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) : Periodic f ((2 * n) • c)

theorem Function.Antiperiodic.nat_even_mul_periodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocSemiring α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) : Periodic f (↑n * (2 * c))

theorem Function.Antiperiodic.odd_nsmul_antiperiodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) : Antiperiodic f ((2 * n + 1) • c)

theorem Function.Antiperiodic.nat_odd_mul_antiperiodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocSemiring α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) : Antiperiodic f (↑n * (2 * c) + c)

theorem Function.Antiperiodic.even_zsmul_periodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) : Periodic f ((2 * n) • c)

theorem Function.Antiperiodic.int_even_mul_periodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocRing α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) : Periodic f (↑n * (2 * c))

theorem Function.Antiperiodic.odd_zsmul_antiperiodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) : Antiperiodic f ((2 * n + 1) • c)

theorem Function.Antiperiodic.int_odd_mul_antiperiodic {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocRing α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) : Antiperiodic f (↑n * (2 * c) + c)

theorem Function.Antiperiodic.sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (x : α) : f (x - c) = -f x

theorem Function.Antiperiodic.sub_eq' {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [SubtractionCommMonoid α] [Neg β] (h : Antiperiodic f c) : f (c - x) = -f (-x)

theorem Function.Antiperiodic.neg {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) : Antiperiodic f (-c)

theorem Function.Antiperiodic.neg_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) : f (-c) = -f 0

theorem Function.Antiperiodic.nat_mul_eq_of_eq_zero {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [NonAssocSemiring α] [NegZeroClass β] (h : 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 : α} [NonAssocRing α] [SubtractionMonoid β] (h : Antiperiodic f c) (hi : f 0 = 0) (n : ℤ) : f (↑n * c) = 0

theorem Function.Antiperiodic.add_zsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℤ) : f (x + n • c) = ↑n.negOnePow • f x

theorem Function.Antiperiodic.sub_zsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℤ) : f (x - n • c) = ↑n.negOnePow • f x

theorem Function.Antiperiodic.zsmul_sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [AddCommGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℤ) : f (n • c - x) = ↑n.negOnePow • f (-x)

theorem Function.Antiperiodic.add_int_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c) (n : ℤ) : f (x + ↑n * c) = ↑↑n.negOnePow * f x

theorem Function.Antiperiodic.sub_int_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c) (n : ℤ) : f (x - ↑n * c) = ↑↑n.negOnePow * f x

theorem Function.Antiperiodic.int_mul_sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c) (n : ℤ) : f (↑n * c - x) = ↑↑n.negOnePow * f (-x)

theorem Function.Antiperiodic.add_nsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [AddMonoid α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℕ) : f (x + n • c) = (-1) ^ n • f x

theorem Function.Antiperiodic.sub_nsmul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℕ) : f (x - n • c) = (-1) ^ n • f x

theorem Function.Antiperiodic.nsmul_sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [AddCommGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℕ) : f (n • c - x) = (-1) ^ n • f (-x)

theorem Function.Antiperiodic.const_add {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) : Antiperiodic (fun (x : α) => f (a + x)) c

theorem Function.Antiperiodic.add_const {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) : Antiperiodic (fun (x : α) => f (x + a)) c

theorem Function.Antiperiodic.const_sub {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (a : α) : Antiperiodic (fun (x : α) => f (a - x)) c

theorem Function.Antiperiodic.sub_const {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [SubtractionCommMonoid α] [Neg β] (h : Antiperiodic f c) (a : α) : Antiperiodic (fun (x : α) => f (x - a)) c

theorem Function.Antiperiodic.smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [Add α] [Monoid γ] [AddGroup β] [DistribMulAction γ β] (h : Antiperiodic f c) (a : γ) : Antiperiodic (a • f) c

theorem Function.Antiperiodic.const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α] (h : Antiperiodic f c) (a : γ) : Antiperiodic (fun (x : α) => f (a • x)) (a⁻¹ • c)

theorem Function.Antiperiodic.const_inv_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α] (h : Antiperiodic f c) (a : γ) : Antiperiodic (fun (x : α) => f (a⁻¹ • x)) (a • c)

theorem Function.Antiperiodic.add {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [AddSemigroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁) (h2 : Antiperiodic f c₂) : Periodic f (c₁ + c₂)

theorem Function.Antiperiodic.sub {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [AddGroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁) (h2 : Antiperiodic f c₂) : Periodic f (c₁ - c₂)

theorem Function.Periodic.add_antiperiod {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [AddSemigroup α] [Neg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) : Antiperiodic f (c₁ + c₂)

theorem Function.Periodic.sub_antiperiod {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [AddGroup α] [InvolutiveNeg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) : Antiperiodic f (c₁ - c₂)

theorem Function.Periodic.add_antiperiod_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [AddMonoid α] [Neg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) : f (c₁ + c₂) = -f 0

theorem Function.Periodic.sub_antiperiod_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [AddGroup α] [InvolutiveNeg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) : f (c₁ - c₂) = -f 0

theorem Function.Antiperiodic.mul {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [Add α] [Mul β] [HasDistribNeg β] (hf : Antiperiodic f c) (hg : Antiperiodic g c) : Periodic (f * g) c

theorem Function.Antiperiodic.div {α : Type u_1} {β : Type u_2} {f g : α → β} {c : α} [Add α] [DivisionMonoid β] [HasDistribNeg β] (hf : Antiperiodic f c) (hg : Antiperiodic g c) : Periodic (f / g) c