Mathlib.Algebra.Ring.Periodic

Function.Periodic definition

[Add α] (f : α → β) (c : α) : Prop

Full source

/-- A function `f` is said to be `Periodic` with period `c` if for all `x`, `f (x + c) = f x`. -/
@[simp]
def Periodic [Add α] (f : α → β) (c : α) : Prop :=
  ∀ x : α, f (x + c) = f x

Periodic function

Informal description

A function $ f : \alpha \to \beta $ is called *periodic* with period $ c \in \alpha $ if for all $ x \in \alpha $, $ f(x + c) = f(x) $.

Function.Periodic.funext theorem

[Add α] (h : Periodic f c) : (fun x => f (x + c)) = f

Full source

protected theorem Periodic.funext [Add α] (h : Periodic f c) : (fun x => f (x + c)) = f :=
  funext h

Periodic Function Equality: $f(x + c) = f(x)$ for All $x$

Informal description

If a function $f : \alpha \to \beta$ is periodic with period $c \in \alpha$, then the function $x \mapsto f(x + c)$ is equal to $f$ itself.

Function.Periodic.comp theorem

[Add α] (h : Periodic f c) (g : β → γ) : Periodic (g ∘ f) c

Full source

protected theorem Periodic.comp [Add α] (h : Periodic f c) (g : β → γ) : Periodic (g ∘ f) c := by
  simp_all

Periodicity Preservation under Function Composition

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$, and let $g : \beta \to \gamma$ be any function. Then the composition $g \circ f$ is also periodic with period $c$.

Function.Periodic.comp_addHom theorem

 [Add α] [Add γ] (h : Periodic f c) (g : AddHom γ α) (g_inv : α → γ) (hg : RightInverse g_inv g) :
  Periodic (f ∘ g) (g_inv c)

Full source

theorem Periodic.comp_addHom [Add α] [Add γ] (h : Periodic f c) (g : AddHom γ α) (g_inv : α → γ)
    (hg : RightInverse g_inv g) : Periodic (f ∘ g) (g_inv c) := fun x => by
  simp only [hg c, h (g x), map_add, comp_apply]

Periodicity Preservation under Composition with Additive Homomorphism

Informal description

Let $\alpha$ and $\gamma$ be additive types, and let $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Given an additive homomorphism $g : \gamma \to \alpha$ with a right inverse $g_{\text{inv}} : \alpha \to \gamma$ (i.e., $g \circ g_{\text{inv}} = \text{id}_\alpha$), the composition $f \circ g$ is periodic with period $g_{\text{inv}}(c) \in \gamma$.

Function.Periodic.mul theorem

[Add α] [Mul β] (hf : Periodic f c) (hg : Periodic g c) : Periodic (f * g) c

Full source

@[to_additive]
protected theorem Periodic.mul [Add α] [Mul β] (hf : Periodic f c) (hg : Periodic g c) :
    Periodic (f * g) c := by simp_all

Periodicity of Pointwise Product of Periodic Functions

Informal description

Let $f, g : \alpha \to \beta$ be functions from an additive monoid $\alpha$ to a multiplicative monoid $\beta$. If $f$ is periodic with period $c$ and $g$ is periodic with period $c$, then their pointwise product $f \cdot g$ is also periodic with period $c$.

Function.Periodic.div theorem

[Add α] [Div β] (hf : Periodic f c) (hg : Periodic g c) : Periodic (f / g) c

Full source

@[to_additive]
protected theorem Periodic.div [Add α] [Div β] (hf : Periodic f c) (hg : Periodic g c) :
    Periodic (f / g) c := by simp_all

Periodicity of Pointwise Quotient of Periodic Functions

Informal description

Let $f, g : \alpha \to \beta$ be periodic functions with period $c \in \alpha$, where $\alpha$ is an additive type and $\beta$ has a division operation. Then the pointwise quotient function $f/g$ is also periodic with period $c$, i.e., for all $x \in \alpha$, $(f/g)(x + c) = (f/g)(x)$.

List.periodic_prod theorem

[Add α] [MulOneClass β] (l : List (α → β)) (hl : ∀ f ∈ l, Periodic f c) : Periodic l.prod c

Full source

@[to_additive]
theorem _root_.List.periodic_prod [Add α] [MulOneClass β] (l : List (α → β))
    (hl : ∀ f ∈ l, Periodic f c) : Periodic l.prod c := by
  induction l with
  | nil => simp
  | cons g l ih =>
    rw [List.forall_mem_cons] at hl
    simpa only [List.prod_cons] using hl.1.mul (ih hl.2)

Periodicity of the Product of a List of Periodic Functions

Informal description

Let $\alpha$ be an additive type and $\beta$ be a multiplicative monoid. Given a list $l$ of functions from $\alpha$ to $\beta$, if every function $f$ in $l$ is periodic with period $c \in \alpha$, then the pointwise product of the functions in $l$ is also periodic with period $c$. That is, for all $x \in \alpha$, we have $\left(\prod_{f \in l} f\right)(x + c) = \left(\prod_{f \in l} f\right)(x)$.

Multiset.periodic_prod theorem

[Add α] [CommMonoid β] (s : Multiset (α → β)) (hs : ∀ f ∈ s, Periodic f c) : Periodic s.prod c

Full source

@[to_additive]
theorem _root_.Multiset.periodic_prod [Add α] [CommMonoid β] (s : Multiset (α → β))
    (hs : ∀ f ∈ s, Periodic f c) : Periodic s.prod c :=
  (s.prod_toList ▸ s.toList.periodic_prod) fun f hf => hs f <| Multiset.mem_toList.mp hf

Periodicity of the Product of a Multiset of Periodic Functions

Informal description

Let $\alpha$ be an additive type and $\beta$ be a commutative monoid. Given a multiset $s$ of functions from $\alpha$ to $\beta$, if every function $f$ in $s$ is periodic with period $c \in \alpha$, then the pointwise product of the functions in $s$ is also periodic with period $c$. That is, for all $x \in \alpha$, we have $\left(\prod_{f \in s} f\right)(x + c) = \left(\prod_{f \in s} f\right)(x)$.

Finset.periodic_prod theorem

 [Add α] [CommMonoid β] {ι : Type*} {f : ι → α → β} (s : Finset ι) (hs : ∀ i ∈ s, Periodic (f i) c) :
  Periodic (∏ i ∈ s, f i) c

Full source

@[to_additive]
theorem _root_.Finset.periodic_prod [Add α] [CommMonoid β] {ι : Type*} {f : ι → α → β}
    (s : Finset ι) (hs : ∀ i ∈ s, Periodic (f i) c) : Periodic (∏ i ∈ s, f i) c :=
  s.prod_map_toList f ▸ (s.toList.map f).periodic_prod (by simpa [-Periodic] )

Periodicity of Finite Product of Periodic Functions

Informal description

Let $\alpha$ be an additive type and $\beta$ be a commutative monoid. Given a finite set $s$ indexed by type $\iota$ and a family of functions $f_i : \alpha \to \beta$ for $i \in s$, if each $f_i$ is periodic with period $c \in \alpha$, then the product function $\prod_{i \in s} f_i$ is also periodic with period $c$. That is, for all $x \in \alpha$, we have $\left(\prod_{i \in s} f_i\right)(x + c) = \left(\prod_{i \in s} f_i\right)(x)$.

Function.Periodic.smul theorem

[Add α] [SMul γ β] (h : Periodic f c) (a : γ) : Periodic (a • f) c

Full source

@[to_additive]
protected theorem Periodic.smul [Add α] [SMul γ β] (h : Periodic f c) (a : γ) :
    Periodic (a • f) c := by simp_all

Scalar Multiplication Preserves Periodicity

Informal description

Let $\alpha$ be an additive type, $\beta$ and $\gamma$ be types with a scalar multiplication operation $\gamma \times \beta \to \beta$. If a function $f : \alpha \to \beta$ is periodic with period $c \in \alpha$, then for any scalar $a \in \gamma$, the scalar multiple function $a \cdot f$ is also periodic with period $c$.

Function.Periodic.const_smul theorem

 [AddMonoid α] [Group γ] [DistribMulAction γ α] (h : Periodic f c) (a : γ) : Periodic (fun x => f (a • x)) (a⁻¹ • c)

Full source

protected theorem Periodic.const_smul [AddMonoid α] [Group γ] [DistribMulAction γ α]
    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
  simpa only [smul_add, smul_inv_smul] using h (a • x)

Periodicity under Scalar Multiplication: $f(a \cdot x)$ has period $a^{-1} \cdot c$

Informal description

Let $\alpha$ be an additive monoid, $\gamma$ be a group acting distributively on $\alpha$, and $f : \alpha \to \beta$ be a function. If $f$ is periodic with period $c \in \alpha$, then for any $a \in \gamma$, the function $x \mapsto f(a \cdot x)$ is periodic with period $a^{-1} \cdot c$.

Function.Periodic.const_inv_smul theorem

 [AddMonoid α] [Group γ] [DistribMulAction γ α] (h : Periodic f c) (a : γ) : Periodic (fun x => f (a⁻¹ • x)) (a • c)

Full source

theorem Periodic.const_inv_smul [AddMonoid α] [Group γ] [DistribMulAction γ α] (h : Periodic f c)
    (a : γ) : Periodic (fun x => f (a⁻¹ • x)) (a • c) := by
  simpa only [inv_inv] using h.const_smul a⁻¹

Periodicity under Inverse Scalar Multiplication: $f(a^{-1} \cdot x)$ has period $a \cdot c$

Informal description

Let $\alpha$ be an additive monoid, $\gamma$ be a group acting distributively on $\alpha$, and $f : \alpha \to \beta$ be a function. If $f$ is periodic with period $c \in \alpha$, then for any $a \in \gamma$, the function $x \mapsto f(a^{-1} \cdot x)$ is periodic with period $a \cdot c$.

Function.Periodic.add_period theorem

[AddSemigroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) : Periodic f (c₁ + c₂)

Full source

theorem Periodic.add_period [AddSemigroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) :
    Periodic f (c₁ + c₂) := by simp_all [← add_assoc]

Sum of Periods is a Period for Periodic Functions

Informal description

Let $\alpha$ be an additive semigroup and $f : \alpha \to \beta$ be a function. If $f$ is periodic with period $c_1$ and also periodic with period $c_2$, then $f$ is periodic with period $c_1 + c_2$. That is, if $f(x + c_1) = f(x)$ and $f(x + c_2) = f(x)$ for all $x \in \alpha$, then $f(x + (c_1 + c_2)) = f(x)$ for all $x \in \alpha$.

Function.Periodic.sub_eq theorem

[AddGroup α] (h : Periodic f c) (x : α) : f (x - c) = f x

Full source

theorem Periodic.sub_eq [AddGroup α] (h : Periodic f c) (x : α) : f (x - c) = f x := by
  simpa only [sub_add_cancel] using (h (x - c)).symm

Periodic Function Identity: $f(x - c) = f(x)$

Informal description

Let $\alpha$ be an additive group and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any $x \in \alpha$, we have $f(x - c) = f(x)$.

Function.Periodic.sub_eq' theorem

[SubtractionCommMonoid α] (h : Periodic f c) : f (c - x) = f (-x)

Full source

theorem Periodic.sub_eq' [SubtractionCommMonoid α] (h : Periodic f c) : f (c - x) = f (-x) := by
  simpa only [sub_eq_neg_add] using h (-x)

Periodic Function Identity: $f(c - x) = f(-x)$

Informal description

Let $\alpha$ be a commutative subtraction monoid and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any $x \in \alpha$, we have $f(c - x) = f(-x)$.

Function.Periodic.neg theorem

[AddGroup α] (h : Periodic f c) : Periodic f (-c)

Full source

protected theorem Periodic.neg [AddGroup α] (h : Periodic f c) : Periodic f (-c) := by
  simpa only [sub_eq_add_neg, Periodic] using h.sub_eq

Periodicity with Negative Period: $f$ is $-c$-periodic when $c$-periodic

Informal description

Let $\alpha$ be an additive group and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then $f$ is also periodic with period $-c$.

Function.Periodic.sub_period theorem

[AddGroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) : Periodic f (c₁ - c₂)

Full source

theorem Periodic.sub_period [AddGroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) :
    Periodic f (c₁ - c₂) := fun x => by
  rw [sub_eq_add_neg, ← add_assoc, h2.neg, h1]

Periodicity under Difference of Periods: $f$ is $(c_1 - c_2)$-periodic when $c_1$-periodic and $c_2$-periodic

Informal description

Let $\alpha$ be an additive group and $f : \alpha \to \beta$ be a function. If $f$ is periodic with periods $c_1$ and $c_2$, then $f$ is also periodic with period $c_1 - c_2$.

Function.Periodic.const_add theorem

[AddSemigroup α] (h : Periodic f c) (a : α) : Periodic (fun x => f (a + x)) c

Full source

theorem Periodic.const_add [AddSemigroup α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (a + x)) c := fun x => by simpa [add_assoc] using h (a + x)

Periodicity Preservation under Constant Addition

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$). Then for any fixed $a \in \alpha$, the function $x \mapsto f(a + x)$ is also periodic with period $c$.

Function.Periodic.add_const theorem

[AddCommSemigroup α] (h : Periodic f c) (a : α) : Periodic (fun x => f (x + a)) c

Full source

theorem Periodic.add_const [AddCommSemigroup α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (x + a)) c := fun x => by
  simpa only [add_right_comm] using h (x + a)

Periodicity Preservation under Right Addition in Commutative Semigroup

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$) in an additive commutative semigroup $\alpha$. Then for any fixed $a \in \alpha$, the function $x \mapsto f(x + a)$ is also periodic with period $c$.

Function.Periodic.const_sub theorem

[AddCommGroup α] (h : Periodic f c) (a : α) : Periodic (fun x => f (a - x)) c

Full source

theorem Periodic.const_sub [AddCommGroup α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (a - x)) c := fun x => by
  simp only [← sub_sub, h.sub_eq]

Periodicity Preservation under Constant Subtraction in Commutative Group

Informal description

Let $\alpha$ be an additive commutative group and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any fixed $a \in \alpha$, the function $x \mapsto f(a - x)$ is also periodic with period $c$.

Function.Periodic.sub_const theorem

[SubtractionCommMonoid α] (h : Periodic f c) (a : α) : Periodic (fun x => f (x - a)) c

Full source

theorem Periodic.sub_const [SubtractionCommMonoid α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (x - a)) c := by
  simpa only [sub_eq_add_neg] using h.add_const (-a)

Periodicity Preservation under Right Subtraction in Commutative Subtraction Monoid

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$) in a commutative subtraction monoid $\alpha$. Then for any fixed $a \in \alpha$, the function $x \mapsto f(x - a)$ is also periodic with period $c$.

Function.Periodic.nsmul theorem

[AddMonoid α] (h : Periodic f c) (n : ℕ) : Periodic f (n • c)

Full source

theorem Periodic.nsmul [AddMonoid α] (h : Periodic f c) (n : ℕ) : Periodic f (n • c) := by
  induction n <;> simp_all [add_nsmul, ← add_assoc, zero_nsmul]

Periodicity Preservation under Natural Number Scalar Multiplication: $f$ is periodic with period $n \cdot c$ for any $n \in \mathbb{N}$

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$) in an additive monoid $\alpha$. Then for any natural number $n \in \mathbb{N}$, the function $f$ is also periodic with period $n \cdot c$, where $n \cdot c$ denotes the $n$-fold sum of $c$ with itself.

Function.Periodic.nat_mul theorem

[NonAssocSemiring α] (h : Periodic f c) (n : ℕ) : Periodic f (n * c)

Full source

theorem Periodic.nat_mul [NonAssocSemiring α] (h : Periodic f c) (n : ℕ) : Periodic f (n * c) := by
  simpa only [nsmul_eq_mul] using h.nsmul n

Periodicity Preservation under Natural Number Multiplication: $f$ is periodic with period $n \cdot c$ for any $n \in \mathbb{N}$

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$) in a non-associative semiring $\alpha$. Then for any natural number $n \in \mathbb{N}$, the function $f$ is also periodic with period $n \cdot c$, where $n \cdot c$ denotes the product of $n$ and $c$ in $\alpha$.

Function.Periodic.neg_nsmul theorem

[AddGroup α] (h : Periodic f c) (n : ℕ) : Periodic f (-(n • c))

Full source

theorem Periodic.neg_nsmul [AddGroup α] (h : Periodic f c) (n : ℕ) : Periodic f (-(n • c)) :=
  (h.nsmul n).neg

Periodicity Preservation under Negative Natural Number Scalar Multiplication: $f$ is periodic with period $-(n \cdot c)$ for any $n \in \mathbb{N}$

Informal description

Let $\alpha$ be an additive group and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any natural number $n \in \mathbb{N}$, the function $f$ is also periodic with period $-(n \cdot c)$, where $n \cdot c$ denotes the $n$-fold sum of $c$ with itself.

Function.Periodic.neg_nat_mul theorem

[NonAssocRing α] (h : Periodic f c) (n : ℕ) : Periodic f (-(n * c))

Full source

theorem Periodic.neg_nat_mul [NonAssocRing α] (h : Periodic f c) (n : ℕ) : Periodic f (-(n * c)) :=
  (h.nat_mul n).neg

Periodicity with Negative Integer Multiple Period: $f$ is $-(n \cdot c)$-periodic when $c$-periodic

Informal description

Let $\alpha$ be a non-associative ring and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any natural number $n \in \mathbb{N}$, the function $f$ is also periodic with period $- (n \cdot c)$, where $n \cdot c$ denotes the product of $n$ and $c$ in $\alpha$.

Function.Periodic.sub_nsmul_eq theorem

[AddGroup α] (h : Periodic f c) (n : ℕ) : f (x - n • c) = f x

Full source

theorem Periodic.sub_nsmul_eq [AddGroup α] (h : Periodic f c) (n : ℕ) : f (x - n • c) = f x := by
  simpa only [sub_eq_add_neg] using h.neg_nsmul n x

Periodic Function Identity: $f(x - n \cdot c) = f(x)$

Informal description

Let $\alpha$ be an additive group and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any natural number $n \in \mathbb{N}$ and any $x \in \alpha$, we have $f(x - n \cdot c) = f(x)$, where $n \cdot c$ denotes the $n$-fold sum of $c$ with itself.

Function.Periodic.sub_nat_mul_eq theorem

[NonAssocRing α] (h : Periodic f c) (n : ℕ) : f (x - n * c) = f x

Full source

theorem Periodic.sub_nat_mul_eq [NonAssocRing α] (h : Periodic f c) (n : ℕ) :
    f (x - n * c) = f x := by
  simpa only [nsmul_eq_mul] using h.sub_nsmul_eq n

Periodic Function Identity: $f(x - n \cdot c) = f(x)$ for $n \in \mathbb{N}$

Informal description

Let $\alpha$ be a non-associative ring and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any natural number $n \in \mathbb{N}$ and any $x \in \alpha$, we have $f(x - n \cdot c) = f(x)$, where $n \cdot c$ denotes the product of $n$ and $c$ in $\alpha$.

Function.Periodic.nsmul_sub_eq theorem

[SubtractionCommMonoid α] (h : Periodic f c) (n : ℕ) : f (n • c - x) = f (-x)

Full source

theorem Periodic.nsmul_sub_eq [SubtractionCommMonoid α] (h : Periodic f c) (n : ℕ) :
    f (n • c - x) = f (-x) :=
  (h.nsmul n).sub_eq'

Periodic Function Identity: $f(n \cdot c - x) = f(-x)$

Informal description

Let $\alpha$ be a commutative subtraction monoid and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any natural number $n \in \mathbb{N}$ and any $x \in \alpha$, we have $f(n \cdot c - x) = f(-x)$, where $n \cdot c$ denotes the $n$-fold sum of $c$ with itself.

Function.Periodic.nat_mul_sub_eq theorem

[NonAssocRing α] (h : Periodic f c) (n : ℕ) : f (n * c - x) = f (-x)

Full source

theorem Periodic.nat_mul_sub_eq [NonAssocRing α] (h : Periodic f c) (n : ℕ) :
    f (n * c - x) = f (-x) := by
  simpa only [sub_eq_neg_add] using h.nat_mul n (-x)

Periodic Function Identity: $f(n \cdot c - x) = f(-x)$ for $n \in \mathbb{N}$

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$) in a non-associative ring $\alpha$. Then for any natural number $n \in \mathbb{N}$ and any $x \in \alpha$, we have $f(n \cdot c - x) = f(-x)$, where $n \cdot c$ denotes the product of $n$ and $c$ in $\alpha$.

Function.Periodic.zsmul theorem

[AddGroup α] (h : Periodic f c) (n : ℤ) : Periodic f (n • c)

Full source

protected theorem Periodic.zsmul [AddGroup α] (h : Periodic f c) (n : ℤ) : Periodic f (n • c) := by
  rcases n with n | n
  · simpa only [Int.ofNat_eq_coe, natCast_zsmul] using h.nsmul n
  · simpa only [negSucc_zsmul] using (h.nsmul (n + 1)).neg

Periodicity Preservation under Integer Scalar Multiplication: $f$ is periodic with period $n \cdot c$ for any $n \in \mathbb{Z}$

Informal description

Let $\alpha$ be an additive group and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any integer $n \in \mathbb{Z}$, the function $f$ is also periodic with period $n \cdot c$, where $n \cdot c$ denotes the integer scalar multiple of $c$.

Function.Periodic.int_mul theorem

[NonAssocRing α] (h : Periodic f c) (n : ℤ) : Periodic f (n * c)

Full source

protected theorem Periodic.int_mul [NonAssocRing α] (h : Periodic f c) (n : ℤ) :
    Periodic f (n * c) := by
  simpa only [zsmul_eq_mul] using h.zsmul n

Periodicity Preservation under Integer Ring Multiplication: $f$ is periodic with period $n \cdot c$ for any $n \in \mathbb{Z}$

Informal description

Let $\alpha$ be a non-associative ring and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any integer $n \in \mathbb{Z}$, the function $f$ is also periodic with period $n \cdot c$, where $n \cdot c$ denotes the ring multiplication of $n$ and $c$.

Function.Periodic.sub_zsmul_eq theorem

[AddGroup α] (h : Periodic f c) (n : ℤ) : f (x - n • c) = f x

Full source

theorem Periodic.sub_zsmul_eq [AddGroup α] (h : Periodic f c) (n : ℤ) : f (x - n • c) = f x :=
  (h.zsmul n).sub_eq x

Periodic Function Identity: $f(x - n \cdot c) = f(x)$ for any integer $n$

Informal description

Let $\alpha$ be an additive group and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have $f(x - n \cdot c) = f(x)$, where $n \cdot c$ denotes the integer scalar multiple of $c$.

Function.Periodic.sub_int_mul_eq theorem

[NonAssocRing α] (h : Periodic f c) (n : ℤ) : f (x - n * c) = f x

Full source

theorem Periodic.sub_int_mul_eq [NonAssocRing α] (h : Periodic f c) (n : ℤ) : f (x - n * c) = f x :=
  (h.int_mul n).sub_eq x

Periodic Function Identity: $f(x - n \cdot c) = f(x)$ for any integer $n$

Informal description

Let $\alpha$ be a non-associative ring and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have $f(x - n \cdot c) = f(x)$, where $n \cdot c$ denotes the ring multiplication of $n$ and $c$.

Function.Periodic.zsmul_sub_eq theorem

[AddCommGroup α] (h : Periodic f c) (n : ℤ) : f (n • c - x) = f (-x)

Full source

theorem Periodic.zsmul_sub_eq [AddCommGroup α] (h : Periodic f c) (n : ℤ) :
    f (n • c - x) = f (-x) :=
  (h.zsmul _).sub_eq'

Periodic Function Identity: $f(n \cdot c - x) = f(-x)$

Informal description

Let $\alpha$ be an additive commutative group and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have $f(n \cdot c - x) = f(-x)$, where $n \cdot c$ denotes the integer scalar multiple of $c$.

Function.Periodic.int_mul_sub_eq theorem

[NonAssocRing α] (h : Periodic f c) (n : ℤ) : f (n * c - x) = f (-x)

Full source

theorem Periodic.int_mul_sub_eq [NonAssocRing α] (h : Periodic f c) (n : ℤ) :
    f (n * c - x) = f (-x) :=
  (h.int_mul _).sub_eq'

Periodic Function Identity: $f(n \cdot c - x) = f(-x)$ for Integer $n$

Informal description

Let $\alpha$ be a non-associative ring and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have $f(n \cdot c - x) = f(-x)$, where $n \cdot c$ denotes the ring multiplication of $n$ and $c$.

Function.Periodic.eq theorem

[AddZeroClass α] (h : Periodic f c) : f c = f 0

Full source

protected theorem Periodic.eq [AddZeroClass α] (h : Periodic f c) : f c = f 0 := by
  simpa only [zero_add] using h 0

Periodic Function Value at Period Equals Value at Zero

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$). Then $f(c) = f(0)$.

Function.Periodic.neg_eq theorem

[AddGroup α] (h : Periodic f c) : f (-c) = f 0

Full source

protected theorem Periodic.neg_eq [AddGroup α] (h : Periodic f c) : f (-c) = f 0 :=
  h.neg.eq

Periodic Function Value at Negative Period Equals Value at Zero

Informal description

Let $\alpha$ be an additive group and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then $f(-c) = f(0)$.

Function.Periodic.nsmul_eq theorem

[AddMonoid α] (h : Periodic f c) (n : ℕ) : f (n • c) = f 0

Full source

protected theorem Periodic.nsmul_eq [AddMonoid α] (h : Periodic f c) (n : ℕ) : f (n • c) = f 0 :=
  (h.nsmul n).eq

Periodic Function Value at $n$-Fold Period Equals Value at Zero

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c$ in an additive monoid $\alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$). Then for any natural number $n \in \mathbb{N}$, the function evaluated at the $n$-fold sum of $c$ equals its value at zero, i.e., $f(n \cdot c) = f(0)$.

Function.Periodic.nat_mul_eq theorem

[NonAssocSemiring α] (h : Periodic f c) (n : ℕ) : f (n * c) = f 0

Full source

theorem Periodic.nat_mul_eq [NonAssocSemiring α] (h : Periodic f c) (n : ℕ) : f (n * c) = f 0 :=
  (h.nat_mul n).eq

Periodic Function Value at Natural Multiple of Period Equals Value at Zero

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c$ in a non-associative semiring $\alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$). Then for any natural number $n \in \mathbb{N}$, the function evaluated at $n \cdot c$ equals its value at zero, i.e., $f(n \cdot c) = f(0)$.

Function.Periodic.zsmul_eq theorem

[AddGroup α] (h : Periodic f c) (n : ℤ) : f (n • c) = f 0

Full source

theorem Periodic.zsmul_eq [AddGroup α] (h : Periodic f c) (n : ℤ) : f (n • c) = f 0 :=
  (h.zsmul n).eq

Periodic Function Value at Integer Multiple of Period Equals Value at Zero

Informal description

Let $f : \alpha \to \beta$ be a periodic function with period $c$ in an additive group $\alpha$ (i.e., $f(x + c) = f(x)$ for all $x \in \alpha$). Then for any integer $n \in \mathbb{Z}$, the function evaluated at the integer scalar multiple $n \cdot c$ equals its value at zero, i.e., $f(n \cdot c) = f(0)$.

Function.Periodic.int_mul_eq theorem

[NonAssocRing α] (h : Periodic f c) (n : ℤ) : f (n * c) = f 0

Full source

theorem Periodic.int_mul_eq [NonAssocRing α] (h : Periodic f c) (n : ℤ) : f (n * c) = f 0 :=
  (h.int_mul n).eq

Periodic Function Value at Integer Multiple of Period Equals Value at Zero

Informal description

Let $\alpha$ be a non-associative ring and $f : \alpha \to \beta$ be a periodic function with period $c \in \alpha$. Then for any integer $n \in \mathbb{Z}$, the function evaluated at $n \cdot c$ equals its value at zero, i.e., $f(n \cdot c) = f(0)$.

Function.periodic_with_period_zero theorem

[AddZeroClass α] (f : α → β) : Periodic f 0

Full source

theorem periodic_with_period_zero [AddZeroClass α] (f : α → β) : Periodic f 0 := fun x => by
  rw [add_zero]

Zero is a Period for Any Function in an Additive Zero Class

Informal description

For any function $f : \alpha \to \beta$ where $\alpha$ is an additive zero class (i.e., equipped with a zero element $0$ and an addition operation $+$), $f$ is periodic with period $0$. That is, for all $x \in \alpha$, $f(x + 0) = f(x)$.

Function.Periodic.map_vadd_zmultiples theorem

[AddCommGroup α] (hf : Periodic f c) (a : AddSubgroup.zmultiples c) (x : α) : f (a +ᵥ x) = f x

Full source

theorem Periodic.map_vadd_zmultiples [AddCommGroup α] (hf : Periodic f c)
    (a : AddSubgroup.zmultiples c) (x : α) : f (a +ᵥ x) = f x := by
  rcases a with ⟨_, m, rfl⟩
  simp [AddSubgroup.vadd_def, add_comm _ x, hf.zsmul m x]

Periodic Function Invariance under Translation by Integer Multiples of its Period

Informal description

Let $\alpha$ be an additive commutative group and $f \colon \alpha \to \beta$ be a periodic function with period $c \in \alpha$. For any element $a$ in the additive subgroup generated by $c$ (i.e., $a = n \cdot c$ for some integer $n \in \mathbb{Z}$) and any $x \in \alpha$, we have $f(a + x) = f(x)$.

Function.Periodic.map_vadd_multiples theorem

[AddCommMonoid α] (hf : Periodic f c) (a : AddSubmonoid.multiples c) (x : α) : f (a +ᵥ x) = f x

Full source

theorem Periodic.map_vadd_multiples [AddCommMonoid α] (hf : Periodic f c)
    (a : AddSubmonoid.multiples c) (x : α) : f (a +ᵥ x) = f x := by
  rcases a with ⟨_, m, rfl⟩
  simp [AddSubmonoid.vadd_def, add_comm _ x, hf.nsmul m x]

Periodic Function Invariance under Translation by Multiples of its Period

Informal description

Let $\alpha$ be an additive commutative monoid and $f \colon \alpha \to \beta$ be a periodic function with period $c \in \alpha$. For any element $a$ in the additive submonoid generated by $c$ (i.e., $a = n \cdot c$ for some $n \in \mathbb{N}$) and any $x \in \alpha$, we have $f(a + x) = f(x)$.

Function.Periodic.lift definition

[AddGroup α] (h : Periodic f c) (x : α ⧸ AddSubgroup.zmultiples c) : β

Full source

/-- Lift a periodic function to a function from the quotient group. -/
def Periodic.lift [AddGroup α] (h : Periodic f c) (x : α ⧸ AddSubgroup.zmultiples c) : β :=
  Quotient.liftOn' x f fun a b h' => by
    rw [QuotientAddGroup.leftRel_apply] at h'
    obtain ⟨k, hk⟩ := h'
    exact (h.zsmul k _).symm.trans (congr_arg f (add_eq_of_eq_neg_add hk))

Lift of a periodic function to the quotient by its period

Informal description

Given an additive group $\alpha$ and a periodic function $f \colon \alpha \to \beta$ with period $c \in \alpha$, the function `Function.Periodic.lift` maps an element $x$ of the quotient group $\alpha ⧸ \mathbb{Z}c$ to $\beta$ by lifting $f$ to the quotient. Here, $\mathbb{Z}c$ denotes the additive subgroup of $\alpha$ generated by $c$. The function is well-defined because $f$ is periodic with period $c$, ensuring that the value of $f$ is the same on all representatives of the equivalence class $x$.

Function.Periodic.lift_coe theorem

[AddGroup α] (h : Periodic f c) (a : α) : h.lift (a : α ⧸ AddSubgroup.zmultiples c) = f a

Full source

@[simp]
theorem Periodic.lift_coe [AddGroup α] (h : Periodic f c) (a : α) :
    h.lift (a : α ⧸ AddSubgroup.zmultiples c) = f a :=
  rfl

Lift of Periodic Function Preserves Value on Quotient

Informal description

Let $\alpha$ be an additive group and $f \colon \alpha \to \beta$ be a periodic function with period $c \in \alpha$. For any element $a \in \alpha$, the lift of $f$ to the quotient group $\alpha ⧸ \mathbb{Z}c$ evaluated at the equivalence class of $a$ equals $f(a)$, i.e., $h.\text{lift}([a]) = f(a)$, where $[a]$ denotes the equivalence class of $a$ in $\alpha ⧸ \mathbb{Z}c$.

Function.Periodic.not_injective theorem

{R X : Type*} [AddZeroClass R] {f : R → X} {c : R} (hf : Periodic f c) (hc : c ≠ 0) : ¬Injective f

Full source

/-- A periodic function `f : R → X` on a semiring (or, more generally, `AddZeroClass`)
of non-zero period is not injective. -/
lemma Periodic.not_injective {R X : Type*} [AddZeroClass R] {f : R → X} {c : R}
    (hf : Periodic f c) (hc : c ≠ 0) : ¬ Injective f := fun h ↦ hc <| h hf.eq

Non-injectivity of Nonzero-Periodic Functions

Informal description

Let $R$ be an additive zero class and $X$ be any type. If $f : R \to X$ is a periodic function with a nonzero period $c \in R$ (i.e., $f(x + c) = f(x)$ for all $x \in R$ and $c \neq 0$), then $f$ is not injective.

Function.Antiperiodic definition

[Add α] [Neg β] (f : α → β) (c : α) : Prop

Full source

/-- A function `f` is said to be `antiperiodic` with antiperiod `c` if for all `x`,
  `f (x + c) = -f x`. -/
@[simp]
def Antiperiodic [Add α] [Neg β] (f : α → β) (c : α) : Prop :=
  ∀ x : α, f (x + c) = -f x

Antiperiodic function

Informal description

A function $ f : \alpha \to \beta $ is called *antiperiodic* with antiperiod $ c \in \alpha $ if for all $ x \in \alpha $, the equation $ f(x + c) = -f(x) $ holds.

Function.Antiperiodic.funext theorem

[Add α] [Neg β] (h : Antiperiodic f c) : (fun x => f (x + c)) = -f

Full source

protected theorem Antiperiodic.funext [Add α] [Neg β] (h : Antiperiodic f c) :
    (fun x => f (x + c)) = -f :=
  funext h

Antiperiodic Function Shift Equals Negation

Informal description

For any antiperiodic function $f : \alpha \to \beta$ with antiperiod $c \in \alpha$, the function $x \mapsto f(x + c)$ is equal to the function $x \mapsto -f(x)$.

Function.Antiperiodic.funext' theorem

[Add α] [InvolutiveNeg β] (h : Antiperiodic f c) : (fun x => -f (x + c)) = f

Full source

protected theorem Antiperiodic.funext' [Add α] [InvolutiveNeg β] (h : Antiperiodic f c) :
    (fun x => -f (x + c)) = f :=
  neg_eq_iff_eq_neg.mpr h.funext

Negated Shift of Antiperiodic Function Equals Original Function

Informal description

For any antiperiodic function $f : \alpha \to \beta$ with antiperiod $c \in \alpha$, where $\beta$ has an involutive negation, the function $x \mapsto -f(x + c)$ is equal to $f$.

Function.Antiperiodic.periodic theorem

[AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c) : Periodic f (2 • c)

Full source

/-- If a function is `antiperiodic` with antiperiod `c`, then it is also `Periodic` with period
`2 • c`. -/
protected theorem Antiperiodic.periodic [AddMonoid α] [InvolutiveNeg β]
    (h : Antiperiodic f c) : Periodic f (2 • c) := by simp [two_nsmul, ← add_assoc, h _]

Antiperiodic functions are periodic with double the antiperiod

Informal description

Let $\alpha$ be an additive monoid and $\beta$ a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then $f$ is periodic with period $2 \cdot c$.

Function.Antiperiodic.periodic_two_mul theorem

[NonAssocSemiring α] [InvolutiveNeg β] (h : Antiperiodic f c) : Periodic f (2 * c)

Full source

/-- If a function is `antiperiodic` with antiperiod `c`, then it is also `Periodic` with period
  `2 * c`. -/
protected theorem Antiperiodic.periodic_two_mul [NonAssocSemiring α] [InvolutiveNeg β]
    (h : Antiperiodic f c) : Periodic f (2 * c) := nsmul_eq_mul 2 c ▸ h.periodic

Antiperiodic functions are periodic with double the antiperiod (multiplicative version)

Informal description

Let $\alpha$ be a non-associative semiring and $\beta$ a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then $f$ is periodic with period $2c$.

Function.Antiperiodic.eq theorem

[AddZeroClass α] [Neg β] (h : Antiperiodic f c) : f c = -f 0

Full source

protected theorem Antiperiodic.eq [AddZeroClass α] [Neg β] (h : Antiperiodic f c) : f c = -f 0 := by
  simpa only [zero_add] using h 0

Value of Antiperiodic Function at Antiperiod: $f(c) = -f(0)$

Informal description

Let $f : \alpha \to \beta$ be an antiperiodic function with antiperiod $c \in \alpha$, where $\alpha$ is equipped with an addition operation and a zero element, and $\beta$ has a negation operation. Then $f(c) = -f(0)$.

Function.Antiperiodic.even_nsmul_periodic theorem

[AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) : Periodic f ((2 * n) • c)

Full source

theorem Antiperiodic.even_nsmul_periodic [AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℕ) : Periodic f ((2 * n) • c) := mul_nsmul c 2 n ▸ h.periodic.nsmul n

Antiperiodic Functions are Periodic at Even Multiples of the Antiperiod

Informal description

Let $\alpha$ be an additive monoid and $\beta$ a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any natural number $n \in \mathbb{N}$, $f$ is periodic with period $2n \cdot c$.

Function.Antiperiodic.nat_even_mul_periodic theorem

[NonAssocSemiring α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) : Periodic f (n * (2 * c))

Full source

theorem Antiperiodic.nat_even_mul_periodic [NonAssocSemiring α] [InvolutiveNeg β]
    (h : Antiperiodic f c) (n : ℕ) : Periodic f (n * (2 * c)) :=
  h.periodic_two_mul.nat_mul n

Antiperiodic Functions are Periodic at Even Integer Multiples of the Antiperiod

Informal description

Let $\alpha$ be a non-associative semiring and $\beta$ a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any natural number $n \in \mathbb{N}$, $f$ is periodic with period $n \cdot (2c)$.

Function.Antiperiodic.odd_nsmul_antiperiodic theorem

[AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) : Antiperiodic f ((2 * n + 1) • c)

Full source

theorem Antiperiodic.odd_nsmul_antiperiodic [AddMonoid α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℕ) : Antiperiodic f ((2 * n + 1) • c) := fun x => by
  rw [add_nsmul, one_nsmul, ← add_assoc, h, h.even_nsmul_periodic]

Antiperiodicity at Odd Multiples of the Antiperiod

Informal description

Let $\alpha$ be an additive monoid and $\beta$ a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any natural number $n \in \mathbb{N}$, $f$ is antiperiodic with antiperiod $(2n + 1) \cdot c$.

Function.Antiperiodic.nat_odd_mul_antiperiodic theorem

[NonAssocSemiring α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℕ) : Antiperiodic f (n * (2 * c) + c)

Full source

theorem Antiperiodic.nat_odd_mul_antiperiodic [NonAssocSemiring α] [InvolutiveNeg β]
    (h : Antiperiodic f c) (n : ℕ) : Antiperiodic f (n * (2 * c) + c) := fun x => by
  rw [← add_assoc, h, h.nat_even_mul_periodic]

Antiperiodicity at Odd Multiples of the Antiperiod Plus Antiperiod

Informal description

Let $\alpha$ be a non-associative semiring and $\beta$ a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any natural number $n \in \mathbb{N}$, $f$ is antiperiodic with antiperiod $n \cdot (2c) + c$.

Function.Antiperiodic.even_zsmul_periodic theorem

[AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) : Periodic f ((2 * n) • c)

Full source

theorem Antiperiodic.even_zsmul_periodic [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℤ) : Periodic f ((2 * n) • c) := by
  rw [mul_comm, mul_zsmul, two_zsmul, ← two_nsmul]
  exact h.periodic.zsmul n

Even Integer Multiples of Antiperiod Yield Periodicity

Informal description

Let $\alpha$ be an additive group and $\beta$ a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any integer $n \in \mathbb{Z}$, the function $f$ is periodic with period $(2n) \cdot c$.

Function.Antiperiodic.int_even_mul_periodic theorem

[NonAssocRing α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) : Periodic f (n * (2 * c))

Full source

theorem Antiperiodic.int_even_mul_periodic [NonAssocRing α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℤ) : Periodic f (n * (2 * c)) :=
  h.periodic_two_mul.int_mul n

Periodicity of Antiperiodic Functions at Even Integer Multiples of Antiperiod

Informal description

Let $\alpha$ be a non-associative ring and $\beta$ a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any integer $n \in \mathbb{Z}$, the function $f$ is periodic with period $n \cdot (2c)$.

Function.Antiperiodic.odd_zsmul_antiperiodic theorem

[AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) : Antiperiodic f ((2 * n + 1) • c)

Full source

theorem Antiperiodic.odd_zsmul_antiperiodic [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℤ) : Antiperiodic f ((2 * n + 1) • c) := by
  intro x
  rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]

Odd Integer Multiples Preserve Antiperiodicity

Informal description

Let $\alpha$ be an additive group and $\beta$ be a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any integer $n \in \mathbb{Z}$, the function $f$ is antiperiodic with antiperiod $(2n + 1) \cdot c$.

Function.Antiperiodic.int_odd_mul_antiperiodic theorem

[NonAssocRing α] [InvolutiveNeg β] (h : Antiperiodic f c) (n : ℤ) : Antiperiodic f (n * (2 * c) + c)

Full source

theorem Antiperiodic.int_odd_mul_antiperiodic [NonAssocRing α] [InvolutiveNeg β]
    (h : Antiperiodic f c) (n : ℤ) : Antiperiodic f (n * (2 * c) + c) := fun x => by
  rw [← add_assoc, h, h.int_even_mul_periodic]

Odd Integer Multiples Plus Antiperiod Preserve Antiperiodicity

Informal description

Let $\alpha$ be a non-associative ring and $\beta$ a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any integer $n \in \mathbb{Z}$, the function $f$ is antiperiodic with antiperiod $n \cdot (2c) + c$.

Function.Antiperiodic.sub_eq theorem

[AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (x : α) : f (x - c) = -f x

Full source

theorem Antiperiodic.sub_eq [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (x : α) :
    f (x - c) = -f x := by simp only [← neg_eq_iff_eq_neg, ← h (x - c), sub_add_cancel]

Antiperiodic function identity: $f(x - c) = -f(x)$

Informal description

Let $\alpha$ be an additive group and $\beta$ be a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any $x \in \alpha$, we have $f(x - c) = -f(x)$.

Function.Antiperiodic.sub_eq' theorem

[SubtractionCommMonoid α] [Neg β] (h : Antiperiodic f c) : f (c - x) = -f (-x)

Full source

theorem Antiperiodic.sub_eq' [SubtractionCommMonoid α] [Neg β] (h : Antiperiodic f c) :
    f (c - x) = -f (-x) := by simpa only [sub_eq_neg_add] using h (-x)

Antiperiodic function identity: $f(c - x) = -f(-x)$

Informal description

Let $\alpha$ be a subtraction commutative monoid and $\beta$ be a type with negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any $x \in \alpha$, we have $f(c - x) = -f(-x)$.

Function.Antiperiodic.neg theorem

[AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) : Antiperiodic f (-c)

Full source

protected theorem Antiperiodic.neg [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) :
    Antiperiodic f (-c) := by simpa only [sub_eq_add_neg, Antiperiodic] using h.sub_eq

Antiperiodicity with Negated Antiperiod

Informal description

Let $\alpha$ be an additive group and $\beta$ be a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then $f$ is also antiperiodic with antiperiod $-c$.

Function.Antiperiodic.neg_eq theorem

[AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) : f (-c) = -f 0

Full source

theorem Antiperiodic.neg_eq [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) :
    f (-c) = -f 0 := by
  simpa only [zero_add] using h.neg 0

Value of Antiperiodic Function at Negated Antiperiod: $f(-c) = -f(0)$

Informal description

Let $\alpha$ be an additive group and $\beta$ be a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then $f(-c) = -f(0)$.

Function.Antiperiodic.nat_mul_eq_of_eq_zero theorem

[NonAssocSemiring α] [NegZeroClass β] (h : Antiperiodic f c) (hi : f 0 = 0) : ∀ n : ℕ, f (n * c) = 0

Full source

theorem Antiperiodic.nat_mul_eq_of_eq_zero [NonAssocSemiring α] [NegZeroClass β]
    (h : Antiperiodic f c) (hi : f 0 = 0) : ∀ n : ℕ, f (n * c) = 0
  | 0 => by rwa [Nat.cast_zero, zero_mul]
  | n + 1 => by simp [add_mul, h _, Antiperiodic.nat_mul_eq_of_eq_zero h hi n]

Vanishing of Antiperiodic Function at Integer Multiples of Antiperiod

Informal description

Let $\alpha$ be a non-associative semiring and $\beta$ be a negation-zero class. If a function $f : \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$) and satisfies $f(0) = 0$, then for every natural number $n$, we have $f(n \cdot c) = 0$.

Function.Antiperiodic.int_mul_eq_of_eq_zero theorem

[NonAssocRing α] [SubtractionMonoid β] (h : Antiperiodic f c) (hi : f 0 = 0) : ∀ n : ℤ, f (n * c) = 0

Full source

theorem Antiperiodic.int_mul_eq_of_eq_zero [NonAssocRing α] [SubtractionMonoid β]
    (h : Antiperiodic f c) (hi : f 0 = 0) : ∀ n : ℤ, f (n * c) = 0
  | (n : ℕ) => by rw [Int.cast_natCast, h.nat_mul_eq_of_eq_zero hi n]
  | .negSucc n => by rw [Int.cast_negSucc, neg_mul, ← mul_neg, h.neg.nat_mul_eq_of_eq_zero hi]

Vanishing of Antiperiodic Function at Integer Multiples of Antiperiod

Informal description

Let $\alpha$ be a non-associative ring and $\beta$ be a subtraction monoid. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$) and satisfies $f(0) = 0$, then for every integer $n$, we have $f(n \cdot c) = 0$.

Function.Antiperiodic.add_zsmul_eq theorem

[AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℤ) : f (x + n • c) = (n.negOnePow : ℤ) • f x

Full source

theorem Antiperiodic.add_zsmul_eq [AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c)
    (n : ℤ) : f (x + n • c) = (n.negOnePow : ℤ) • f x := by
  rcases Int.even_or_odd' n with ⟨k, rfl | rfl⟩
  · rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]
  · rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
      Units.val_one, neg_zsmul, one_zsmul]

Antiperiodic Function Evaluation at Integer Multiples: $f(x + n \cdot c) = (-1)^n f(x)$

Informal description

Let $\alpha$ be an additive group and $\beta$ a subtraction monoid. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$), then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have: \[ f(x + n \cdot c) = (-1)^n \cdot f(x). \]

Function.Antiperiodic.sub_zsmul_eq theorem

[AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℤ) : f (x - n • c) = (n.negOnePow : ℤ) • f x

Full source

theorem Antiperiodic.sub_zsmul_eq [AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c)
    (n : ℤ) : f (x - n • c) = (n.negOnePow : ℤ) • f x := by
  simpa only [sub_eq_add_neg, neg_zsmul, Int.negOnePow_neg] using h.add_zsmul_eq (-n)

Antiperiodic Function Evaluation at Negative Integer Multiples: $f(x - n \cdot c) = (-1)^n f(x)$

Informal description

Let $\alpha$ be an additive group and $\beta$ a subtraction monoid. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$), then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have: \[ f(x - n \cdot c) = (-1)^n \cdot f(x). \]

Function.Antiperiodic.zsmul_sub_eq theorem

 [AddCommGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℤ) : f (n • c - x) = (n.negOnePow : ℤ) • f (-x)

Full source

theorem Antiperiodic.zsmul_sub_eq [AddCommGroup α] [SubtractionMonoid β] (h : Antiperiodic f c)
    (n : ℤ) : f (n • c - x) = (n.negOnePow : ℤ) • f (-x) := by
  rw [sub_eq_add_neg, add_comm]
  exact h.add_zsmul_eq n

Antiperiodic Function Evaluation at Scaled Antiperiod Minus Argument: $f(n \cdot c - x) = (-1)^n f(-x)$

Informal description

Let $\alpha$ be an additive commutative group and $\beta$ a subtraction monoid. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$), then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have: \[ f(n \cdot c - x) = (-1)^n \cdot f(-x). \]

Function.Antiperiodic.add_int_mul_eq theorem

[NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c) (n : ℤ) : f (x + n * c) = (n.negOnePow : ℤ) * f x

Full source

theorem Antiperiodic.add_int_mul_eq [NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c)
    (n : ℤ) : f (x + n * c) = (n.negOnePow : ℤ) * f x := by
  simpa only [zsmul_eq_mul] using h.add_zsmul_eq n

Antiperiodic Function Evaluation at Integer Multiples: $f(x + n \cdot c) = (-1)^n f(x)$

Informal description

Let $\alpha$ and $\beta$ be non-associative rings. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$), then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have: \[ f(x + n \cdot c) = (-1)^n \cdot f(x). \]

Function.Antiperiodic.sub_int_mul_eq theorem

[NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c) (n : ℤ) : f (x - n * c) = (n.negOnePow : ℤ) * f x

Full source

theorem Antiperiodic.sub_int_mul_eq [NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c)
    (n : ℤ) : f (x - n * c) = (n.negOnePow : ℤ) * f x := by
  simpa only [zsmul_eq_mul] using h.sub_zsmul_eq n

Antiperiodic Function Evaluation at Negative Integer Multiples: $f(x - n \cdot c) = (-1)^n f(x)$

Informal description

Let $\alpha$ and $\beta$ be non-associative rings. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$), then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have: \[ f(x - n \cdot c) = (-1)^n \cdot f(x). \]

Function.Antiperiodic.int_mul_sub_eq theorem

[NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c) (n : ℤ) : f (n * c - x) = (n.negOnePow : ℤ) * f (-x)

Full source

theorem Antiperiodic.int_mul_sub_eq [NonAssocRing α] [NonAssocRing β] (h : Antiperiodic f c)
    (n : ℤ) : f (n * c - x) = (n.negOnePow : ℤ) * f (-x) := by
  simpa only [zsmul_eq_mul] using h.zsmul_sub_eq n

Antiperiodic function evaluation at scaled antiperiod minus argument: $f(n \cdot c - x) = (-1)^n f(-x)$

Informal description

Let $\alpha$ and $\beta$ be non-associative rings. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$), then for any integer $n \in \mathbb{Z}$ and any $x \in \alpha$, we have: \[ f(n \cdot c - x) = (-1)^n \cdot f(-x). \]

Function.Antiperiodic.add_nsmul_eq theorem

[AddMonoid α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℕ) : f (x + n • c) = (-1) ^ n • f x

Full source

theorem Antiperiodic.add_nsmul_eq [AddMonoid α] [SubtractionMonoid β] (h : Antiperiodic f c)
    (n : ℕ) : f (x + n • c) = (-1) ^ n • f x := by
  rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩
  · rw [h.even_nsmul_periodic]
    simp
  · rw [h.odd_nsmul_antiperiodic]
    simp [pow_add]

Antiperiodic Function Property at Integer Multiples: $f(x + n \cdot c) = (-1)^n f(x)$

Informal description

Let $\alpha$ be an additive monoid and $\beta$ a subtraction monoid. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any natural number $n \in \mathbb{N}$ and any $x \in \alpha$, we have $f(x + n \cdot c) = (-1)^n \cdot f(x)$.

Function.Antiperiodic.sub_nsmul_eq theorem

[AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℕ) : f (x - n • c) = (-1) ^ n • f x

Full source

theorem Antiperiodic.sub_nsmul_eq [AddGroup α] [SubtractionMonoid β] (h : Antiperiodic f c)
    (n : ℕ) : f (x - n • c) = (-1) ^ n • f x := by
  simpa only [Int.reduceNeg, natCast_zsmul] using h.sub_zsmul_eq n

Antiperiodic Function Evaluation at Negative Natural Multiples: $f(x - n \cdot c) = (-1)^n f(x)$

Informal description

Let $\alpha$ be an additive group and $\beta$ a subtraction monoid. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$), then for any natural number $n \in \mathbb{N}$ and any $x \in \alpha$, we have: \[ f(x - n \cdot c) = (-1)^n \cdot f(x). \]

Function.Antiperiodic.nsmul_sub_eq theorem

[AddCommGroup α] [SubtractionMonoid β] (h : Antiperiodic f c) (n : ℕ) : f (n • c - x) = (-1) ^ n • f (-x)

Full source

theorem Antiperiodic.nsmul_sub_eq [AddCommGroup α] [SubtractionMonoid β] (h : Antiperiodic f c)
    (n : ℕ) : f (n • c - x) = (-1) ^ n • f (-x) := by
  simpa only [Int.reduceNeg, natCast_zsmul] using h.zsmul_sub_eq n

Antiperiodic Function Evaluation at Scaled Antiperiod Minus Argument: $f(n \cdot c - x) = (-1)^n f(-x)$

Informal description

Let $\alpha$ be an additive commutative group and $\beta$ a subtraction monoid. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$ (i.e., $f(x + c) = -f(x)$ for all $x \in \alpha$), then for any natural number $n \in \mathbb{N}$ and any $x \in \alpha$, we have: \[ f(n \cdot c - x) = (-1)^n \cdot f(-x). \]

Function.Antiperiodic.const_add theorem

[AddSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) : Antiperiodic (fun x => f (a + x)) c

Full source

theorem Antiperiodic.const_add [AddSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) :
    Antiperiodic (fun x => f (a + x)) c := fun x => by simpa [add_assoc] using h (a + x)

Antiperiodicity under Left Translation

Informal description

Let $\alpha$ be an additive semigroup and $\beta$ be a type with negation. If a function $f : \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any fixed $a \in \alpha$, the function $x \mapsto f(a + x)$ is also antiperiodic with the same antiperiod $c$.

Function.Antiperiodic.add_const theorem

[AddCommSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) : Antiperiodic (fun x => f (x + a)) c

Full source

theorem Antiperiodic.add_const [AddCommSemigroup α] [Neg β] (h : Antiperiodic f c) (a : α) :
    Antiperiodic (fun x => f (x + a)) c := fun x => by
  simpa only [add_right_comm] using h (x + a)

Right Translation Preserves Antiperiodicity

Informal description

Let $\alpha$ be an additive commutative semigroup and $\beta$ be a type with negation. If a function $f : \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any fixed $a \in \alpha$, the function $x \mapsto f(x + a)$ is also antiperiodic with the same antiperiod $c$.

Function.Antiperiodic.const_sub theorem

[AddCommGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (a : α) : Antiperiodic (fun x => f (a - x)) c

Full source

theorem Antiperiodic.const_sub [AddCommGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) (a : α) :
    Antiperiodic (fun x => f (a - x)) c := fun x => by
  simp only [← sub_sub, h.sub_eq]

Antiperiodicity under Reflection and Translation

Informal description

Let $\alpha$ be an additive commutative group and $\beta$ be a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any fixed $a \in \alpha$, the function $x \mapsto f(a - x)$ is also antiperiodic with the same antiperiod $c$.

Function.Antiperiodic.sub_const theorem

[SubtractionCommMonoid α] [Neg β] (h : Antiperiodic f c) (a : α) : Antiperiodic (fun x => f (x - a)) c

Full source

theorem Antiperiodic.sub_const [SubtractionCommMonoid α] [Neg β] (h : Antiperiodic f c) (a : α) :
    Antiperiodic (fun x => f (x - a)) c := by
  simpa only [sub_eq_add_neg] using h.add_const (-a)

Left Translation Preserves Antiperiodicity

Informal description

Let $\alpha$ be a commutative subtraction monoid and $\beta$ be a type with negation. If a function $f : \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any fixed $a \in \alpha$, the function $x \mapsto f(x - a)$ is also antiperiodic with the same antiperiod $c$.

Function.Antiperiodic.smul theorem

[Add α] [Monoid γ] [AddGroup β] [DistribMulAction γ β] (h : Antiperiodic f c) (a : γ) : Antiperiodic (a • f) c

Full source

theorem Antiperiodic.smul [Add α] [Monoid γ] [AddGroup β] [DistribMulAction γ β]
    (h : Antiperiodic f c) (a : γ) : Antiperiodic (a • f) c := by simp_all

Scalar Multiplication Preserves Antiperiodicity

Informal description

Let $\alpha$ be an additive type, $\gamma$ a monoid, and $\beta$ an additive group with a distributive multiplicative action of $\gamma$ on $\beta$. If a function $f : \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any scalar $a \in \gamma$, the function $a \cdot f$ (defined pointwise) is also antiperiodic with the same antiperiod $c$.

Function.Antiperiodic.const_smul theorem

 [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α] (h : Antiperiodic f c) (a : γ) :
  Antiperiodic (fun x => f (a • x)) (a⁻¹ • c)

Full source

theorem Antiperiodic.const_smul [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α]
    (h : Antiperiodic f c) (a : γ) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
  simpa only [smul_add, smul_inv_smul] using h (a • x)

Antiperiodicity under Scalar Multiplication: $f(a \cdot x)$ has antiperiod $a^{-1} \cdot c$

Informal description

Let $\alpha$ be an additive monoid, $\beta$ a type with negation, and $\gamma$ a group acting distributively on $\alpha$. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any $a \in \gamma$, the function $x \mapsto f(a \cdot x)$ is antiperiodic with antiperiod $a^{-1} \cdot c$.

Function.Antiperiodic.const_inv_smul theorem

 [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α] (h : Antiperiodic f c) (a : γ) :
  Antiperiodic (fun x => f (a⁻¹ • x)) (a • c)

Full source

theorem Antiperiodic.const_inv_smul [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α]
    (h : Antiperiodic f c) (a : γ) : Antiperiodic (fun x => f (a⁻¹ • x)) (a • c) := by
  simpa only [inv_inv] using h.const_smul a⁻¹

Antiperiodicity under Inverse Scalar Multiplication: $f(a^{-1} \cdot x)$ has antiperiod $a \cdot c$

Informal description

Let $\alpha$ be an additive monoid, $\beta$ a type with negation, and $\gamma$ a group acting distributively on $\alpha$. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiod $c \in \alpha$, then for any $a \in \gamma$, the function $x \mapsto f(a^{-1} \cdot x)$ is antiperiodic with antiperiod $a \cdot c$.

Function.Antiperiodic.add theorem

[AddSemigroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁) (h2 : Antiperiodic f c₂) : Periodic f (c₁ + c₂)

Full source

theorem Antiperiodic.add [AddSemigroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁)
    (h2 : Antiperiodic f c₂) : Periodic f (c₁ + c₂) := by simp_all [← add_assoc]

Sum of Two Antiperiods Yields Periodicity

Informal description

Let $\alpha$ be an additive semigroup and $\beta$ be a type with involutive negation. If $f : \alpha \to \beta$ is antiperiodic with antiperiods $c_1$ and $c_2$, then $f$ is periodic with period $c_1 + c_2$. That is, for all $x \in \alpha$, we have $f(x + (c_1 + c_2)) = f(x)$.

Function.Antiperiodic.sub theorem

[AddGroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁) (h2 : Antiperiodic f c₂) : Periodic f (c₁ - c₂)

Full source

theorem Antiperiodic.sub [AddGroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁)
    (h2 : Antiperiodic f c₂) : Periodic f (c₁ - c₂) := by
  simpa only [sub_eq_add_neg] using h1.add h2.neg

Difference of Antiperiods Yields Periodicity: $f$ is $(c_1 - c_2)$-periodic

Informal description

Let $\alpha$ be an additive group and $\beta$ be a type with involutive negation. If a function $f \colon \alpha \to \beta$ is antiperiodic with antiperiods $c_1$ and $c_2$, then $f$ is periodic with period $c_1 - c_2$. That is, for all $x \in \alpha$, we have $f(x + (c_1 - c_2)) = f(x)$.

Function.Periodic.add_antiperiod theorem

[AddSemigroup α] [Neg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) : Antiperiodic f (c₁ + c₂)

Full source

theorem Periodic.add_antiperiod [AddSemigroup α] [Neg β] (h1 : Periodic f c₁)
    (h2 : Antiperiodic f c₂) : Antiperiodic f (c₁ + c₂) := by simp_all [← add_assoc]

Sum of Period and Antiperiod Yields Antiperiodicity

Informal description

Let $\alpha$ be an additive semigroup and $\beta$ be a type with negation. If $f : \alpha \to \beta$ is periodic with period $c_1$ and antiperiodic with antiperiod $c_2$, then $f$ is antiperiodic with antiperiod $c_1 + c_2$. That is, for all $x \in \alpha$, we have $f(x + (c_1 + c_2)) = -f(x)$.

Function.Periodic.sub_antiperiod theorem

[AddGroup α] [InvolutiveNeg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) : Antiperiodic f (c₁ - c₂)

Full source

theorem Periodic.sub_antiperiod [AddGroup α] [InvolutiveNeg β] (h1 : Periodic f c₁)
    (h2 : Antiperiodic f c₂) : Antiperiodic f (c₁ - c₂) := by
  simpa only [sub_eq_add_neg] using h1.add_antiperiod h2.neg

Antiperiodicity of Function with Difference of Period and Antiperiod

Informal description

Let $\alpha$ be an additive group and $\beta$ be a type with involutive negation. If a function $f \colon \alpha \to \beta$ is periodic with period $c_1$ and antiperiodic with antiperiod $c_2$, then $f$ is antiperiodic with antiperiod $c_1 - c_2$. That is, for all $x \in \alpha$, we have $f(x + (c_1 - c_2)) = -f(x)$.

Function.Periodic.add_antiperiod_eq theorem

[AddMonoid α] [Neg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) : f (c₁ + c₂) = -f 0

Full source

theorem Periodic.add_antiperiod_eq [AddMonoid α] [Neg β] (h1 : Periodic f c₁)
    (h2 : Antiperiodic f c₂) : f (c₁ + c₂) = -f 0 :=
  (h1.add_antiperiod h2).eq

Value of Periodic Plus Antiperiodic Function at Sum of Periods: $f(c_1 + c_2) = -f(0)$

Informal description

Let $\alpha$ be an additive monoid and $\beta$ be a type with negation. If $f : \alpha \to \beta$ is periodic with period $c_1$ and antiperiodic with antiperiod $c_2$, then $f(c_1 + c_2) = -f(0)$.

Function.Periodic.sub_antiperiod_eq theorem

[AddGroup α] [InvolutiveNeg β] (h1 : Periodic f c₁) (h2 : Antiperiodic f c₂) : f (c₁ - c₂) = -f 0

Full source

theorem Periodic.sub_antiperiod_eq [AddGroup α] [InvolutiveNeg β] (h1 : Periodic f c₁)
    (h2 : Antiperiodic f c₂) : f (c₁ - c₂) = -f 0 :=
  (h1.sub_antiperiod h2).eq

Value of Periodic Minus Antiperiodic Function at Difference: $f(c_1 - c_2) = -f(0)$

Informal description

Let $\alpha$ be an additive group and $\beta$ be a type with involutive negation. If a function $f \colon \alpha \to \beta$ is periodic with period $c_1$ and antiperiodic with antiperiod $c_2$, then $f$ evaluated at $c_1 - c_2$ equals $-f(0)$, i.e., $f(c_1 - c_2) = -f(0)$.

Function.Antiperiodic.mul theorem

[Add α] [Mul β] [HasDistribNeg β] (hf : Antiperiodic f c) (hg : Antiperiodic g c) : Periodic (f * g) c

Full source

theorem Antiperiodic.mul [Add α] [Mul β] [HasDistribNeg β] (hf : Antiperiodic f c)
    (hg : Antiperiodic g c) : Periodic (f * g) c := by simp_all

Product of Antiperiodic Functions is Periodic

Informal description

Let $\alpha$ be an additive type and $\beta$ a multiplicative type with distributive negation. If $f, g : \alpha \to \beta$ are both antiperiodic functions with the same antiperiod $c \in \alpha$, then their pointwise product $f \cdot g$ is periodic with period $c$. That is, for all $x \in \alpha$, $(f \cdot g)(x + c) = (f \cdot g)(x)$.

Function.Antiperiodic.div theorem

[Add α] [DivisionMonoid β] [HasDistribNeg β] (hf : Antiperiodic f c) (hg : Antiperiodic g c) : Periodic (f / g) c

Full source

theorem Antiperiodic.div [Add α] [DivisionMonoid β] [HasDistribNeg β] (hf : Antiperiodic f c)
    (hg : Antiperiodic g c) : Periodic (f / g) c := by simp_all [neg_div_neg_eq]

Quotient of Antiperiodic Functions is Periodic

Informal description

Let $\alpha$ be an additive type and $\beta$ a division monoid with distributive negation. If $f, g : \alpha \to \beta$ are both antiperiodic functions with the same antiperiod $c \in \alpha$, then their pointwise quotient $f / g$ is periodic with period $c$. That is, for all $x \in \alpha$, $(f / g)(x + c) = (f / g)(x)$.

Mathlib.Algebra.Ring.Periodic

Main definitions

Tags