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.

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

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

Equations
Instances For
    source
    @[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))
    source
    @[simp]
    theorem conjneg_conjneg {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : G → R) :
    conjneg (conjneg f) = f
    source
    theorem conjneg_involutive {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    Function.Involutive conjneg
    source
    theorem conjneg_bijective {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    Function.Bijective conjneg
    source
    theorem conjneg_injective {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    Function.Injective conjneg
    source
    theorem conjneg_surjective {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    Function.Surjective conjneg
    source
    @[simp]
    theorem conjneg_inj {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : G → R} {g : G → R} :
    conjneg f = conjneg g ↔ f = g
    source
    theorem conjneg_ne_conjneg {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : G → R} {g : G → R} :
    conjneg f ≠ conjneg g ↔ f ≠ g
    source
    @[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)
    source
    @[simp]
    theorem conjneg_zero {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    conjneg 0 = 0
    source
    @[simp]
    theorem conjneg_one {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] :
    conjneg 1 = 1
    source
    @[simp]
    theorem conjneg_add {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) :
    conjneg (f + g) = conjneg f + conjneg g
    source
    @[simp]
    theorem conjneg_mul {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : G → R) (g : G → R) :
    conjneg (f * g) = conjneg f * conjneg g
    source
    @[simp]
    theorem conjneg_sum {ι : Type u_1} {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (s : Finset ι) (f : ι → G → R) :
    conjneg (∑ i ∈ s, f i) = ∑ i ∈ s, conjneg (f i)
    source
    @[simp]
    theorem conjneg_prod {ι : Type u_1} {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (s : Finset ι) (f : ι → G → R) :
    conjneg (∏ i ∈ s, f i) = ∏ i ∈ s, conjneg (f i)
    source
    @[simp]
    theorem conjneg_eq_zero {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : G → R} :
    conjneg f = 0 ↔ f = 0
    source
    @[simp]
    theorem conjneg_eq_one {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : G → R} :
    conjneg f = 1 ↔ f = 1
    source
    theorem conjneg_ne_zero {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : G → R} :
    conjneg f ≠ 0 ↔ f ≠ 0
    source
    theorem conjneg_ne_one {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] {f : G → R} :
    conjneg f ≠ 1 ↔ f ≠ 1
    source
    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)
    source
    @[simp]
    theorem support_conjneg {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : G → R) :
    Function.support (conjneg f) = -Function.support f
    source
    @[simp]
    theorem conjnegRingHom_apply {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] (f : G → R) :
    ∀ (a : G), conjnegRingHom f a = conjneg f a
    source
    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' := ⋯ }
    Instances For
      source
      @[simp]
      theorem conjneg_sub {G : Type u_2} {R : Type u_3} [AddGroup G] [CommRing R] [StarRing R] (f : G → R) (g : G → R) :
      conjneg (f - g) = conjneg f - conjneg g
      source
      @[simp]
      theorem conjneg_neg {G : Type u_2} {R : Type u_3} [AddGroup G] [CommRing R] [StarRing R] (f : G → R) :
      conjneg (-f) = -conjneg f