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
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
  • conjnegRingHom = { toFun := conjneg, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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