Documentation

Mathlib.Algebra.Star.Conjneg

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.

def conjneg {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : GR) :
GR

Conjugation-negation. Sends f to fun x ↦ conj (f (-x)).

Equations
Instances For
    @[simp]
    theorem conjneg_apply {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : GR) (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 : GR) :
    theorem conjneg_involutive {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    theorem conjneg_bijective {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    theorem conjneg_injective {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    theorem conjneg_surjective {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    @[simp]
    theorem conjneg_inj {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : GR} {g : GR} :
    theorem conjneg_ne_conjneg {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : GR} {g : GR} :
    @[simp]
    theorem conjneg_conj {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : GR) :
    conjneg ((starRingEnd (GR)) f) = (starRingEnd (GR)) (conjneg f)
    @[simp]
    theorem conjneg_zero {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    @[simp]
    theorem conjneg_one {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    @[simp]
    theorem conjneg_add {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : GR) (g : GR) :
    @[simp]
    theorem conjneg_mul {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : GR) (g : GR) :
    @[simp]
    theorem conjneg_sum {ι : Type u_1} {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (s : Finset ι) (f : ιGR) :
    conjneg (∑ is, f i) = is, conjneg (f i)
    @[simp]
    theorem conjneg_prod {ι : Type u_1} {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (s : Finset ι) (f : ιGR) :
    conjneg (∏ is, f i) = is, conjneg (f i)
    @[simp]
    theorem conjneg_eq_zero {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : GR} :
    conjneg f = 0 f = 0
    @[simp]
    theorem conjneg_eq_one {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : GR} :
    conjneg f = 1 f = 1
    theorem conjneg_ne_zero {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : GR} :
    conjneg f 0 f 0
    theorem conjneg_ne_one {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : GR} :
    conjneg f 1 f 1
    theorem sum_conjneg {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] [Fintype G] (f : GR) :
    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 : GR) :
    @[simp]
    theorem conjnegRingHom_apply {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : GR) :
    ∀ (a : G), conjnegRingHom f a = conjneg f a
    def conjnegRingHom {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    (GR) →+* GR

    conjneg bundled as a ring homomorphism.

    Equations
    • conjnegRingHom = { toFun := conjneg, map_one' := , map_mul' := , map_zero' := , map_add' := }
    Instances For
      @[simp]
      theorem conjneg_sub {G : Type u_2} {R : Type u_3} [AddGroup G] [CommRing R] [StarRing R] (f : GR) (g : GR) :
      @[simp]
      theorem conjneg_neg {G : Type u_2} {R : Type u_3} [AddGroup G] [CommRing R] [StarRing R] (f : GR) :