Periodic functions

This file proves facts about periodic and antiperiodic functions from and to a field.

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

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

theorem Function.Periodic.const_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] (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 : α} [AddCommMonoid α] [DivisionSemiring γ] [Module γ α] (h : Periodic f c) (a : γ) : Periodic (fun (x : α) => f (a⁻¹ • x)) (a • c)

theorem Function.Periodic.const_inv_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] (h : Periodic f c) (a : α) : Periodic (fun (x : α) => f (a⁻¹ * x)) (a * c)

theorem Function.Periodic.mul_const {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] (h : Periodic f c) (a : α) : Periodic (fun (x : α) => f (x * a)) (c * a⁻¹)

theorem Function.Periodic.mul_const' {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] (h : Periodic f c) (a : α) : Periodic (fun (x : α) => f (x * a)) (c / a)

theorem Function.Periodic.mul_const_inv {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] (h : Periodic f c) (a : α) : Periodic (fun (x : α) => f (x * a⁻¹)) (c * a)

theorem Function.Periodic.div_const {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] (h : Periodic f c) (a : α) : Periodic (fun (x : α) => f (x / a)) (c * a)

theorem Function.Periodic.exists_mem_Ico₀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x : α) : ∃ 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 : α} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x a : α) : ∃ 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 : α} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x a : α) : ∃ 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 : α} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (a : α) : f '' Set.Ioc a (a + c) = Set.range f

theorem Function.Periodic.image_Icc {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (a : α) : f '' Set.Icc a (a + c) = Set.range f

theorem Function.Periodic.image_uIcc {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c) (hc : c ≠ 0) (a : α) : f '' Set.uIcc a (a + c) = Set.range f

Antiperiodicity

theorem Function.Antiperiodic.add_nat_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [NonAssocSemiring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) : f (x + ↑n * c) = (-1) ^ n * f x

theorem Function.Antiperiodic.sub_nat_mul_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [NonAssocRing α] [Ring β] (h : Antiperiodic f c) (n : ℕ) : f (x - ↑n * c) = (-1) ^ n * f x

theorem Function.Antiperiodic.nat_mul_sub_eq {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [NonAssocRing α] [Ring β] (h : Antiperiodic f c) (n : ℕ) : f (↑n * c - x) = (-1) ^ n * f (-x)

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

theorem Function.Antiperiodic.const_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} (ha : a ≠ 0) : 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 β] [GroupWithZero γ] [DistribMulAction γ α] (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun (x : α) => f (a⁻¹ • x)) (a • c)

theorem Function.Antiperiodic.const_inv_mul {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} (ha : a ≠ 0) : Antiperiodic (fun (x : α) => f (a⁻¹ * x)) (a * c)

theorem Function.Antiperiodic.mul_const {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} (ha : a ≠ 0) : Antiperiodic (fun (x : α) => f (x * a)) (c * a⁻¹)

theorem Function.Antiperiodic.mul_const' {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} (ha : a ≠ 0) : Antiperiodic (fun (x : α) => f (x * a)) (c / a)

theorem Function.Antiperiodic.mul_const_inv {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} (ha : a ≠ 0) : Antiperiodic (fun (x : α) => f (x * a⁻¹)) (c * a)

theorem Function.Antiperiodic.div_inv {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α} (ha : a ≠ 0) : Antiperiodic (fun (x : α) => f (x / a)) (c * a)

theorem Int.fract_periodic (α : Type u_4) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] : Function.Periodic fract 1