Documentation

Mathlib.Algebra.Group.EvenFunction

Even and odd functions #

We define even functions α → β assuming α has a negation, and odd functions assuming both α and β have negation.

These definitions are Function.Even and Function.Odd; and they are protected, to avoid conflicting with the root-level definitions Even and Odd (which, for functions, mean that the function takes even resp. odd values, a wholly different concept).

source
def Function.Even {α : Type u_1} {β : Type u_2} [Neg α] (f : α → β) :
Prop

A function f is even if it satisfies f (-x) = f x for all x.

Instances For
    source
    def Function.Odd {α : Type u_1} {β : Type u_2} [Neg α] [Neg β] (f : α → β) :
    Prop

    A function f is odd if it satisfies f (-x) = -f x for all x.

    Instances For
      source
      theorem Function.Even.const {α : Type u_1} {β : Type u_2} [Neg α] (b : β) :
      Function.Even fun (x : α) => b

      Any constant function is even.

      source
      theorem Function.Even.zero {α : Type u_1} {β : Type u_2} [Neg α] [Zero β] :
      Function.Even fun (x : α) => 0

      The zero function is even.

      source
      theorem Function.Odd.zero {α : Type u_1} {β : Type u_2} [Neg α] [NegZeroClass β] :
      Function.Odd fun (x : α) => 0

      The zero function is odd.

      source
      theorem Function.Even.left_comp {α : Type u_1} {β : Type u_2} [Neg α] {γ : Type u_3} {g : α → β} (hg : Function.Even g) (f : β → γ) :
      Function.Even (f ∘ g)

      If f is arbitrary and g is even, then f ∘ g is even.

      source
      theorem Function.Even.comp_odd {α : Type u_1} {β : Type u_2} [Neg α] {γ : Type u_3} [Neg β] {f : β → γ} (hf : Function.Even f) {g : α → β} (hg : Function.Odd g) :
      Function.Even (f ∘ g)

      If f is even and g is odd, then f ∘ g is even.

      source
      theorem Function.Odd.comp_odd {α : Type u_1} {β : Type u_2} [Neg α] {γ : Type u_3} [Neg β] [Neg γ] {f : β → γ} (hf : Function.Odd f) {g : α → β} (hg : Function.Odd g) :
      Function.Odd (f ∘ g)

      If f and g are odd, then f ∘ g is odd.

      source
      theorem Function.Even.add {α : Type u_1} {β : Type u_2} [Neg α] [Add β] {f g : α → β} (hf : Function.Even f) (hg : Function.Even g) :
      Function.Even (f + g)
      source
      theorem Function.Odd.add {α : Type u_1} {β : Type u_2} [Neg α] [SubtractionCommMonoid β] {f g : α → β} (hf : Function.Odd f) (hg : Function.Odd g) :
      Function.Odd (f + g)
      source
      theorem Function.Even.smul_even {α : Type u_1} {β : Type u_2} [Neg α] {γ : Type u_3} {f : α → β} {g : α → γ} [SMul β γ] (hf : Function.Even f) (hg : Function.Even g) :
      Function.Even (f • g)
      source
      theorem Function.Even.smul_odd {α : Type u_1} {β : Type u_2} [Neg α] {γ : Type u_3} {f : α → β} {g : α → γ} [Monoid β] [AddGroup γ] [DistribMulAction β γ] (hf : Function.Even f) (hg : Function.Odd g) :
      Function.Odd (f • g)
      source
      theorem Function.Odd.smul_even {α : Type u_1} {β : Type u_2} [Neg α] {γ : Type u_3} {f : α → β} {g : α → γ} [Ring β] [AddCommGroup γ] [Module β γ] (hf : Function.Odd f) (hg : Function.Even g) :
      Function.Odd (f • g)
      source
      theorem Function.Odd.smul_odd {α : Type u_1} {β : Type u_2} [Neg α] {γ : Type u_3} {f : α → β} {g : α → γ} [Ring β] [AddCommGroup γ] [Module β γ] (hf : Function.Odd f) (hg : Function.Odd g) :
      Function.Even (f • g)
      source
      theorem Function.Even.const_smul {α : Type u_1} {β : Type u_2} [Neg α] {γ : Type u_3} {g : α → γ} [SMul β γ] (hg : Function.Even g) (r : β) :
      Function.Even (r • g)
      source
      theorem Function.Odd.const_smul {α : Type u_1} {β : Type u_2} [Neg α] {γ : Type u_3} {g : α → γ} [Monoid β] [AddGroup γ] [DistribMulAction β γ] (hg : Function.Odd g) (r : β) :
      Function.Odd (r • g)
      source
      theorem Function.Even.mul_even {α : Type u_1} [Neg α] {R : Type u_3} [Mul R] {f g : α → R} (hf : Function.Even f) (hg : Function.Even g) :
      Function.Even (f * g)
      source
      theorem Function.Even.mul_odd {α : Type u_1} [Neg α] {R : Type u_3} [Mul R] {f g : α → R} [HasDistribNeg R] (hf : Function.Even f) (hg : Function.Odd g) :
      Function.Odd (f * g)
      source
      theorem Function.Odd.mul_even {α : Type u_1} [Neg α] {R : Type u_3} [Mul R] {f g : α → R} [HasDistribNeg R] (hf : Function.Odd f) (hg : Function.Even g) :
      Function.Odd (f * g)
      source
      theorem Function.Odd.mul_odd {α : Type u_1} [Neg α] {R : Type u_3} [Mul R] {f g : α → R} [HasDistribNeg R] (hf : Function.Odd f) (hg : Function.Odd g) :
      Function.Even (f * g)
      source
      theorem Function.zero_of_even_and_odd {α : Type u_3} {β : Type u_4} [AddCommGroup β] [IsAddTorsionFree β] {f : α → β} [Neg α] (he : Function.Even f) (ho : Function.Odd f) :
      f = 0

      If f is both even and odd, and its target is a torsion-free commutative additive group, then f = 0.

      source
      theorem Function.Odd.finset_sum_eq_zero {α : Type u_3} {β : Type u_4} [AddCommGroup β] [IsAddTorsionFree β] [InvolutiveNeg α] {f : α → β} (hf : Function.Odd f) {s : Finset α} (hs : Finset.map (Equiv.toEmbedding (Equiv.neg α)) s = s) :
      s.sum f = 0

      The sum of values of an odd function over a symmetric finite set is zero.

      source
      theorem Function.Odd.sum_eq_zero {α : Type u_3} {β : Type u_4} [AddCommGroup β] [IsAddTorsionFree β] [Fintype α] [InvolutiveNeg α] {f : α → β} (hf : Function.Odd f) :
      ∑ a : α, f a = 0

      The sum of the values of an odd function is 0.

      source
      theorem Function.Odd.map_zero {α : Type u_3} {β : Type u_4} [AddCommGroup β] [IsAddTorsionFree β] {f : α → β} [NegZeroClass α] (hf : Function.Odd f) :
      f 0 = 0

      An odd function vanishes at zero.