Conjugation-negation operator #
This file defines the conjugation-negation operator, useful in Fourier analysis.
The way this operator enters the picture is that the adjoint of convolution with a function f
is
convolution with conjneg f
.
@[simp]
theorem
conjneg_apply
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
(f : G → R)
(x : G)
:
conjneg f x = (starRingEnd R) (f (-x))
@[simp]
theorem
conjneg_conjneg
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
(f : G → R)
:
theorem
conjneg_involutive
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
:
Function.Involutive conjneg
theorem
conjneg_bijective
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
:
Function.Bijective conjneg
theorem
conjneg_injective
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
:
Function.Injective conjneg
theorem
conjneg_surjective
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
:
Function.Surjective conjneg
@[simp]
theorem
conjneg_conj
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
(f : G → R)
:
conjneg ((starRingEnd (G → R)) f) = (starRingEnd (G → R)) (conjneg f)
@[simp]
@[simp]
theorem
sum_conjneg
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
[Fintype G]
(f : G → R)
:
∑ a : G, conjneg f a = ∑ a : G, (starRingEnd R) (f a)
@[simp]
theorem
support_conjneg
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
(f : G → R)
:
@[simp]
theorem
conjnegRingHom_apply
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
(f : G → R)
:
def
conjnegRingHom
{G : Type u_2}
{R : Type u_3}
[AddGroup G]
[CommSemiring R]
[StarRing R]
:
(G → R) →+* G → R
conjneg
bundled as a ring homomorphism.
Equations
- conjnegRingHom = { toFun := conjneg, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }