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 α] [AddCommMonoid β] (a : α) : τ a 0 = 0

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

theorem translate_sum_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommMonoid β] (a : α) (f : ι → α → β) (s : Finset ι) : τ a (∑ i ∈ s, f i) = ∑ i ∈ s, τ a (f i)

theorem sum_translate {α : Type u_2} {β : Type u_3} [AddCommGroup α] [AddCommMonoid β] [Fintype α] (a : α) (f : α → β) : ∑ b : α, τ a f b = ∑ b : α, f b

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

@[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 (∏ i ∈ s, f i) = ∏ i ∈ s, τ a (f i)

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

Equations

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

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