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 : 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 : 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 : 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 : 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
      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
        Instances For
          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
          @[simp]
          theorem conjneg_sub {G : Type u_2} {R : Type u_3} [AddGroup G] [CommRing R] [StarRing R] (f 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