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).
A function f is even if it satisfies f (-x) = f x for all x.
Equations
- Function.Even f = ∀ (a : α), f (-a) = f a
Instances For
theorem
Function.Even.const
{α : Type u_1}
{β : Type u_2}
[Neg α]
(b : β)
:
Function.Even fun (x : α) => b
Any constant function is even.
theorem
Function.Even.zero
{α : Type u_1}
{β : Type u_2}
[Neg α]
[Zero β]
:
Function.Even fun (x : α) => 0
The zero function is even.
theorem
Function.Odd.zero
{α : Type u_1}
{β : Type u_2}
[Neg α]
[NegZeroClass β]
:
Function.Odd fun (x : α) => 0
The zero function is odd.
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.
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.
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.
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)
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)
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)
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)
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)
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)
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)
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)
theorem
Function.Even.mul_even
{α : Type u_1}
[Neg α]
{R : Type u_3}
[Mul R]
{f : α → R}
{g : α → R}
(hf : Function.Even f)
(hg : Function.Even g)
:
Function.Even (f * g)
theorem
Function.Even.mul_odd
{α : Type u_1}
[Neg α]
{R : Type u_3}
[Mul R]
{f : α → R}
{g : α → R}
[HasDistribNeg R]
(hf : Function.Even f)
(hg : Function.Odd g)
:
Function.Odd (f * g)
theorem
Function.Odd.mul_even
{α : Type u_1}
[Neg α]
{R : Type u_3}
[Mul R]
{f : α → R}
{g : α → R}
[HasDistribNeg R]
(hf : Function.Odd f)
(hg : Function.Even g)
:
Function.Odd (f * g)
theorem
Function.Odd.mul_odd
{α : Type u_1}
[Neg α]
{R : Type u_3}
[Mul R]
{f : α → R}
{g : α → R}
[HasDistribNeg R]
(hf : Function.Odd f)
(hg : Function.Odd g)
:
Function.Even (f * g)
theorem
Function.zero_of_even_and_odd
{α : Type u_1}
{β : Type u_2}
[Neg α]
[AddCommGroup β]
[NoZeroSMulDivisors ℕ β]
{f : α → β}
(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.