Documentation

Mathlib.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 #

def Function.Periodic {α : Type u_1} {β : Type u_2} [Add α] (f : αβ) (c : α) :

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

Equations
Instances For
    theorem Function.Periodic.funext {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [Add α] (h : Function.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 : Function.Periodic f c) (g : βγ) :
    theorem Function.Periodic.comp_addHom {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {c : α} [Add α] [Add γ] (h : Function.Periodic f c) (g : AddHom γ α) (g_inv : αγ) (hg : Function.RightInverse g_inv g) :
    Function.Periodic (f g) (g_inv c)
    theorem Function.Periodic.add {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {c : α} [Add α] [Add β] (hf : Function.Periodic f c) (hg : Function.Periodic g c) :
    theorem Function.Periodic.mul {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {c : α} [Add α] [Mul β] (hf : Function.Periodic f c) (hg : Function.Periodic g c) :
    theorem Function.Periodic.sub {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {c : α} [Add α] [Sub β] (hf : Function.Periodic f c) (hg : Function.Periodic g c) :
    theorem Function.Periodic.div {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {c : α} [Add α] [Div β] (hf : Function.Periodic f c) (hg : Function.Periodic g c) :
    theorem List.periodic_sum {α : Type u_1} {β : Type u_2} {c : α} [Add α] [AddMonoid β] (l : List (αβ)) (hl : fl, Function.Periodic f c) :
    theorem List.periodic_prod {α : Type u_1} {β : Type u_2} {c : α} [Add α] [Monoid β] (l : List (αβ)) (hl : fl, Function.Periodic f c) :
    theorem Multiset.periodic_sum {α : Type u_1} {β : Type u_2} {c : α} [Add α] [AddCommMonoid β] (s : Multiset (αβ)) (hs : fs, Function.Periodic f c) :
    theorem Multiset.periodic_prod {α : Type u_1} {β : Type u_2} {c : α} [Add α] [CommMonoid β] (s : Multiset (αβ)) (hs : fs, Function.Periodic f c) :
    theorem Finset.periodic_sum {α : Type u_1} {β : Type u_2} {c : α} [Add α] [AddCommMonoid β] {ι : Type u_4} {f : ιαβ} (s : Finset ι) (hs : is, Function.Periodic (f i) c) :
    Function.Periodic (∑ is, f i) c
    theorem Finset.periodic_prod {α : Type u_1} {β : Type u_2} {c : α} [Add α] [CommMonoid β] {ι : Type u_4} {f : ιαβ} (s : Finset ι) (hs : is, Function.Periodic (f i) c) :
    Function.Periodic (∏ is, f i) c
    theorem Function.Periodic.vadd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {c : α} [Add α] [VAdd γ β] (h : Function.Periodic f c) (a : γ) :
    theorem Function.Periodic.smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {c : α} [Add α] [SMul γ β] (h : Function.Periodic f c) (a : γ) :
    theorem Function.Periodic.const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {c : α} [AddMonoid α] [Group γ] [DistribMulAction γ α] (h : Function.Periodic f c) (a : γ) :
    Function.Periodic (fun (x : α) => f (a x)) (a⁻¹ c)
    theorem Function.Periodic.const_smul₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {c : α} [AddCommMonoid α] [DivisionSemiring γ] [Module γ α] (h : Function.Periodic f c) (a : γ) :
    Function.Periodic (fun (x : α) => f (a x)) (a⁻¹ c)
    theorem Function.Periodic.const_mul {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] (h : Function.Periodic f c) (a : α) :
    Function.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 : Function.Periodic f c) (a : γ) :
    Function.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 : Function.Periodic f c) (a : γ) :
    Function.Periodic (fun (x : α) => f (a⁻¹ x)) (a c)
    theorem Function.Periodic.const_inv_mul {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] (h : Function.Periodic f c) (a : α) :
    Function.Periodic (fun (x : α) => f (a⁻¹ * x)) (a * c)
    theorem Function.Periodic.mul_const {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] (h : Function.Periodic f c) (a : α) :
    Function.Periodic (fun (x : α) => f (x * a)) (c * a⁻¹)
    theorem Function.Periodic.mul_const' {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] (h : Function.Periodic f c) (a : α) :
    Function.Periodic (fun (x : α) => f (x * a)) (c / a)
    theorem Function.Periodic.mul_const_inv {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] (h : Function.Periodic f c) (a : α) :
    Function.Periodic (fun (x : α) => f (x * a⁻¹)) (c * a)
    theorem Function.Periodic.div_const {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] (h : Function.Periodic f c) (a : α) :
    Function.Periodic (fun (x : α) => f (x / a)) (c * a)
    theorem Function.Periodic.add_period {α : Type u_1} {β : Type u_2} {f : αβ} {c₁ : α} {c₂ : α} [AddSemigroup α] (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 : α} [AddGroup α] (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 : α} [AddCommGroup α] (h : Function.Periodic f c) :
    f (c - x) = f (-x)
    theorem Function.Periodic.neg {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddGroup α] (h : Function.Periodic f c) :
    theorem Function.Periodic.sub_period {α : Type u_1} {β : Type u_2} {f : αβ} {c₁ : α} {c₂ : α} [AddGroup α] (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 : α} [AddSemigroup α] (h : Function.Periodic f c) (a : α) :
    Function.Periodic (fun (x : α) => f (a + x)) c
    theorem Function.Periodic.add_const {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddCommSemigroup α] (h : Function.Periodic f c) (a : α) :
    Function.Periodic (fun (x : α) => f (x + a)) c
    theorem Function.Periodic.const_sub {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddCommGroup α] (h : Function.Periodic f c) (a : α) :
    Function.Periodic (fun (x : α) => f (a - x)) c
    theorem Function.Periodic.sub_const {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddCommGroup α] (h : Function.Periodic f c) (a : α) :
    Function.Periodic (fun (x : α) => f (x - a)) c
    theorem Function.Periodic.nsmul {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddMonoid α] (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 : ) :
    Function.Periodic f (n * c)
    theorem Function.Periodic.neg_nsmul {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddGroup α] (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 : ) :
    Function.Periodic f (-(n * c))
    theorem Function.Periodic.sub_nsmul_eq {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} {x : α} [AddGroup α] (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 : α} [AddCommGroup α] (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 : α} [AddGroup α] (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 : ) :
    Function.Periodic f (n * c)
    theorem Function.Periodic.sub_zsmul_eq {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} {x : α} [AddGroup α] (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 : α} [AddCommGroup α] (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 : α} [AddZeroClass α] (h : Function.Periodic f c) :
    f c = f 0
    theorem Function.Periodic.neg_eq {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddGroup α] (h : Function.Periodic f c) :
    f (-c) = f 0
    theorem Function.Periodic.nsmul_eq {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddMonoid α] (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 : α} [AddGroup α] (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 : α} [LinearOrderedAddCommGroup α] [Archimedean α] (h : Function.Periodic f c) (hc : 0 < c) (x : α) :
    ySet.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 : α} [LinearOrderedAddCommGroup α] [Archimedean α] (h : Function.Periodic f c) (hc : 0 < c) (x : α) (a : α) :
    ySet.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 : α} [LinearOrderedAddCommGroup α] [Archimedean α] (h : Function.Periodic f c) (hc : 0 < c) (x : α) (a : α) :
    ySet.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 : α} [LinearOrderedAddCommGroup α] [Archimedean α] (h : Function.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 : α} [LinearOrderedAddCommGroup α] [Archimedean α] (h : Function.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 : α} [LinearOrderedAddCommGroup α] [Archimedean α] (h : Function.Periodic f c) (hc : c 0) (a : α) :
    f '' Set.uIcc a (a + c) = Set.range f
    theorem Function.periodic_with_period_zero {α : Type u_1} {β : Type u_2} [AddZeroClass α] (f : αβ) :
    theorem Function.Periodic.map_vadd_zmultiples {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddCommGroup α] (hf : Function.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 : Function.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 : Function.Periodic f c) (x : α AddSubgroup.zmultiples c) :
    β

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

    Equations
    Instances For
      @[simp]
      theorem Function.Periodic.lift_coe {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddGroup α] (h : Function.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 : RX} {c : R} (hf : Function.Periodic f c) (hc : c 0) :

      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 : α) :

      A function f is said to be antiperiodic with antiperiod c if for all x, f (x + c) = -f x.

      Equations
      Instances For
        theorem Function.Antiperiodic.funext {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [Add α] [Neg β] (h : Function.Antiperiodic f c) :
        (fun (x : α) => f (x + c)) = -f
        theorem Function.Antiperiodic.funext' {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [Add α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) :
        (fun (x : α) => -f (x + c)) = f
        theorem Function.Antiperiodic.periodic {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddMonoid α] [InvolutiveNeg β] (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.periodic_two_mul {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [Semiring α] [InvolutiveNeg β] (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 : α} [AddZeroClass α] [Neg β] (h : Function.Antiperiodic f c) :
        f c = -f 0
        theorem Function.Antiperiodic.even_nsmul_periodic {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddMonoid α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) (n : ) :
        Function.Periodic f ((2 * n) c)
        theorem Function.Antiperiodic.nat_even_mul_periodic {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [Semiring α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) (n : ) :
        Function.Periodic f (n * (2 * c))
        theorem Function.Antiperiodic.odd_nsmul_antiperiodic {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddMonoid α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) (n : ) :
        theorem Function.Antiperiodic.nat_odd_mul_antiperiodic {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [Semiring α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) (n : ) :
        Function.Antiperiodic f (n * (2 * c) + c)
        theorem Function.Antiperiodic.even_zsmul_periodic {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddGroup α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) (n : ) :
        Function.Periodic f ((2 * n) c)
        theorem Function.Antiperiodic.int_even_mul_periodic {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [Ring α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) (n : ) :
        Function.Periodic f (n * (2 * c))
        theorem Function.Antiperiodic.odd_zsmul_antiperiodic {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddGroup α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) (n : ) :
        theorem Function.Antiperiodic.int_odd_mul_antiperiodic {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [Ring α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) (n : ) :
        Function.Antiperiodic f (n * (2 * c) + c)
        theorem Function.Antiperiodic.sub_eq {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddGroup α] [InvolutiveNeg β] (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 : α} [AddCommGroup α] [Neg β] (h : Function.Antiperiodic f c) :
        f (c - x) = -f (-x)
        theorem Function.Antiperiodic.neg {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddGroup α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) :
        theorem Function.Antiperiodic.neg_eq {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddGroup α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) :
        f (-c) = -f 0
        theorem Function.Antiperiodic.nat_mul_eq_of_eq_zero {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [Semiring α] [NegZeroClass β] (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 : α} [Ring α] [SubtractionMonoid β] (h : Function.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 α] [AddGroup β] (h : Function.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 α] [AddGroup β] (h : Function.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 α] [AddGroup β] (h : Function.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 : α} [Ring α] [Ring β] (h : Function.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 : α} [Ring α] [Ring β] (h : Function.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 : α} [Ring α] [Ring β] (h : Function.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 α] [AddGroup β] (h : Function.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 α] [AddGroup β] (h : Function.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 α] [AddGroup β] (h : Function.Antiperiodic f c) (n : ) :
        f (n c - x) = (-1) ^ n f (-x)
        theorem Function.Antiperiodic.add_nat_mul_eq {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} {x : α} [Semiring α] [Ring β] (h : Function.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 : α} [Ring α] [Ring β] (h : Function.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 : α} [Ring α] [Ring β] (h : Function.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 : Function.Antiperiodic f c) (a : α) :
        Function.Antiperiodic (fun (x : α) => f (a + x)) c
        theorem Function.Antiperiodic.add_const {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddCommSemigroup α] [Neg β] (h : Function.Antiperiodic f c) (a : α) :
        Function.Antiperiodic (fun (x : α) => f (x + a)) c
        theorem Function.Antiperiodic.const_sub {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddCommGroup α] [InvolutiveNeg β] (h : Function.Antiperiodic f c) (a : α) :
        Function.Antiperiodic (fun (x : α) => f (a - x)) c
        theorem Function.Antiperiodic.sub_const {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [AddCommGroup α] [Neg β] (h : Function.Antiperiodic f c) (a : α) :
        Function.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 : Function.Antiperiodic f c) (a : γ) :
        theorem Function.Antiperiodic.const_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {c : α} [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α] (h : Function.Antiperiodic f c) (a : γ) :
        Function.Antiperiodic (fun (x : α) => f (a x)) (a⁻¹ c)
        theorem Function.Antiperiodic.const_smul₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {c : α} [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α] (h : Function.Antiperiodic f c) {a : γ} (ha : a 0) :
        Function.Antiperiodic (fun (x : α) => f (a x)) (a⁻¹ c)
        theorem Function.Antiperiodic.const_mul {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] [Neg β] (h : Function.Antiperiodic f c) {a : α} (ha : a 0) :
        Function.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 : Function.Antiperiodic f c) (a : γ) :
        Function.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 : α} [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α] (h : Function.Antiperiodic f c) {a : γ} (ha : a 0) :
        Function.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 : Function.Antiperiodic f c) {a : α} (ha : a 0) :
        Function.Antiperiodic (fun (x : α) => f (a⁻¹ * x)) (a * c)
        theorem Function.Antiperiodic.mul_const {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] [Neg β] (h : Function.Antiperiodic f c) {a : α} (ha : a 0) :
        Function.Antiperiodic (fun (x : α) => f (x * a)) (c * a⁻¹)
        theorem Function.Antiperiodic.mul_const' {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] [Neg β] (h : Function.Antiperiodic f c) {a : α} (ha : a 0) :
        Function.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 : Function.Antiperiodic f c) {a : α} (ha : a 0) :
        Function.Antiperiodic (fun (x : α) => f (x * a⁻¹)) (c * a)
        theorem Function.Antiperiodic.div_inv {α : Type u_1} {β : Type u_2} {f : αβ} {c : α} [DivisionSemiring α] [Neg β] (h : Function.Antiperiodic f c) {a : α} (ha : a 0) :
        Function.Antiperiodic (fun (x : α) => f (x / a)) (c * a)
        theorem Function.Antiperiodic.add {α : Type u_1} {β : Type u_2} {f : αβ} {c₁ : α} {c₂ : α} [AddGroup α] [InvolutiveNeg β] (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₂ : α} [AddGroup α] [InvolutiveNeg β] (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₂ : α} [AddGroup α] [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₂ : α} [AddGroup α] [InvolutiveNeg β] (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₂ : α} [AddGroup α] [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₂ : α} [AddGroup α] [InvolutiveNeg β] (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 : α} [Add α] [Mul β] [HasDistribNeg β] (hf : Function.Antiperiodic f c) (hg : Function.Antiperiodic g c) :
        theorem Function.Antiperiodic.div {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} {c : α} [Add α] [DivisionMonoid β] [HasDistribNeg β] (hf : Function.Antiperiodic f c) (hg : Function.Antiperiodic g c) :