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 : G → R) : G → R

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

Equations

• conjneg f = (starRingEnd (G → R)) fun (x : G) => f (-x)

@[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) : conjneg (conjneg f) = f

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_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

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

@[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]

theorem conjneg_zero {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] : conjneg 0 = 0

@[simp]

theorem conjneg_one {G : Type u_2} {R : Type u_3} [AddGroup G] [CommSemiring R] [StarRing R] : conjneg 1 = 1

@[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

@[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

@[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)

@[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)

@[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

@[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

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

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

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) : Function.support (conjneg f) = -Function.support f

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' := ⋯ }

@[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✝

@[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

@[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