Precomposition operators

Translation operator

def translate {α : Type u_2} {β : Type u_3} [AddCommGroup α] (a : α) (f : α → β) : α → β

Equations

• τ a f x = f (x - a)

def termτ : Lean.ParserDescr

Equations

• termτ = Lean.ParserDescr.node `termτ 1024 (Lean.ParserDescr.symbol "τ ")

@[simp]

theorem translate_apply {α : Type u_2} {β : Type u_3} [AddCommGroup α] (a : α) (f : α → β) (x : α) : τ a f x = f (x - a)

@[simp]

theorem translate_zero {α : Type u_2} {β : Type u_3} [AddCommGroup α] (f : α → β) : τ 0 f = f

theorem translate_translate {α : Type u_2} {β : Type u_3} [AddCommGroup α] (a : α) (b : α) (f : α → β) : τ a (τ b f) = τ (a + b) f

theorem translate_add {α : Type u_2} {β : Type u_3} [AddCommGroup α] (a : α) (b : α) (f : α → β) : τ (a + b) f = τ a (τ b f)

theorem translate_add' {α : Type u_2} {β : Type u_3} [AddCommGroup α] (a : α) (b : α) (f : α → β) : τ (a + b) f = τ b (τ a f)

theorem translate_comm {α : Type u_2} {β : Type u_3} [AddCommGroup α] (a : α) (b : α) (f : α → β) : τ a (τ b f) = τ b (τ a f)

@[simp]

theorem comp_translate {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommGroup α] (a : α) (f : α → β) (g : β → γ) : g ∘ τ a f = τ a (g ∘ f)

@[simp]

theorem translate_smul_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommGroup α] [SMul γ β] (a : α) (f : α → β) (c : γ) : τ a (c • f) = c • τ a f

@[simp]

theorem translate_zero_right {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (a : α) : τ a 0 = 0

theorem translate_add_right {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (a : α) (f : α → β) (g : α → β) : τ a (f + g) = τ a f + τ a g

theorem translate_sub_right {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (a : α) (f : α → β) (g : α → β) : τ a (f - g) = τ a f - τ a g

theorem translate_neg_right {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (a : α) (f : α → β) : τ a (-f) = -τ a f

theorem translate_sum_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (a : α) (f : ι → α → β) (s : Finset ι) : τ a (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => τ a (f i)

theorem sum_translate {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] [Fintype α] (a : α) (f : α → β) : (Finset.sum Finset.univ fun (b : α) => τ a f b) = Finset.sum Finset.univ fun (b : α) => f b

@[simp]

theorem support_translate {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommGroup β] (a : α) (f : α → β) : Function.support (τ a f) = a +ᵥ Function.support f

theorem translate_prod_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [CommRing β] (a : α) (f : ι → α → β) (s : Finset ι) : τ a (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => τ a (f i)

Conjugation negation operator

def conjneg {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] (f : α → β) : α → β

Equations

• conjneg f = (starRingEnd (α → β)) fun (x : α) => f (-x)

@[simp]

theorem conjneg_apply {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] (f : α → β) (x : α) : conjneg f x = (starRingEnd β) (f (-x))

@[simp]

theorem conjneg_conjneg {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] (f : α → β) : conjneg (conjneg f) = f

theorem conjneg_injective {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] : Function.Injective conjneg

@[simp]

theorem conjneg_inj {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] {f : α → β} {g : α → β} : conjneg f = conjneg g ↔ f = g

theorem conjneg_ne_conjneg {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] {f : α → β} {g : α → β} : conjneg f ≠ conjneg g ↔ f ≠ g

@[simp]

theorem conjneg_conj {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] (f : α → β) : conjneg ((starRingEnd (α → β)) f) = (starRingEnd (α → β)) (conjneg f)

@[simp]

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

@[simp]

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

@[simp]

theorem conjneg_add {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] (f : α → β) (g : α → β) : conjneg (f + g) = conjneg f + conjneg g

@[simp]

theorem conjneg_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] (s : Finset ι) (f : ι → α → β) : conjneg (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => conjneg (f i)

@[simp]

theorem conjneg_prod {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] (s : Finset ι) (f : ι → α → β) : conjneg (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => conjneg (f i)

@[simp]

theorem conjneg_eq_zero {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] {f : α → β} : conjneg f = 0 ↔ f = 0

@[simp]

theorem conjneg_eq_one {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] {f : α → β} : conjneg f = 1 ↔ f = 1

theorem conjneg_ne_zero {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] {f : α → β} : conjneg f ≠ 0 ↔ f ≠ 0

theorem conjneg_ne_one {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] {f : α → β} : conjneg f ≠ 1 ↔ f ≠ 1

theorem sum_conjneg {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] [Fintype α] (f : α → β) : (Finset.sum Finset.univ fun (a : α) => conjneg f a) = Finset.sum Finset.univ fun (a : α) => (starRingEnd β) (f a)

@[simp]

theorem support_conjneg {α : Type u_2} {β : Type u_3} [AddGroup α] [CommSemiring β] [StarRing β] (f : α → β) : Function.support (conjneg f) = -Function.support f

@[simp]

theorem conjneg_sub {α : Type u_2} {β : Type u_3} [AddGroup α] [CommRing β] [StarRing β] (f : α → β) (g : α → β) : conjneg (f - g) = conjneg f - conjneg g

@[simp]

theorem conjneg_neg {α : Type u_2} {β : Type u_3} [AddGroup α] [CommRing β] [StarRing β] (f : α → β) : conjneg (-f) = -conjneg f

@[simp]

theorem conjneg_nonneg {α : Type u_2} {β : Type u_3} [AddGroup α] [OrderedCommSemiring β] [StarRing β] [StarOrderedRing β] {f : α → β} : 0 ≤ conjneg f ↔ 0 ≤ f

@[simp]

theorem conjneg_pos {α : Type u_2} {β : Type u_3} [AddGroup α] [OrderedCommSemiring β] [StarRing β] [StarOrderedRing β] {f : α → β} : 0 < conjneg f ↔ 0 < f

@[simp]

theorem conjneg_nonpos {α : Type u_2} {β : Type u_3} [AddGroup α] [OrderedCommRing β] [StarRing β] [StarOrderedRing β] {f : α → β} : conjneg f ≤ 0 ↔ f ≤ 0

@[simp]

theorem conjneg_neg' {α : Type u_2} {β : Type u_3} [AddGroup α] [OrderedCommRing β] [StarRing β] [StarOrderedRing β] {f : α → β} : conjneg f < 0 ↔ f < 0

noncomputable def dilate {G : Type u_3} {𝕜 : Type u_4} [AddCommGroup G] (f : G → 𝕜) (n : ℕ) : G → 𝕜

Equations

• dilate f n a = f (ZMod.val (↑n)⁻¹ • a)

theorem IsSelfAdjoint.dilate {G : Type u_3} {𝕜 : Type u_4} [AddCommGroup G] [Star 𝕜] {f : G → 𝕜} (hf : IsSelfAdjoint f) (n : ℕ) : IsSelfAdjoint (dilate f n)