Precomposition operators #
Translation operator #
Equations
- termτ = Lean.ParserDescr.node `termτ 1024 (Lean.ParserDescr.symbol "τ ")
Instances For
@[simp]
theorem
translate_apply
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
(a : α)
(f : α → β)
(x : α)
:
@[simp]
theorem
translate_translate
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
(a : α)
(b : α)
(f : α → β)
:
@[simp]
theorem
translate_zero_right
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[AddCommGroup β]
(a : α)
:
theorem
translate_add_right
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[AddCommGroup β]
(a : α)
(f : α → β)
(g : α → β)
:
theorem
translate_sub_right
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[AddCommGroup β]
(a : α)
(f : α → β)
(g : α → β)
:
theorem
translate_neg_right
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[AddCommGroup β]
(a : α)
(f : α → β)
:
theorem
translate_sum_right
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[AddCommGroup β]
(a : α)
(f : ι → α → β)
(s : Finset ι)
:
theorem
sum_translate
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[AddCommGroup β]
[Fintype α]
(a : α)
(f : α → β)
:
@[simp]
theorem
support_translate
{α : Type u_2}
{β : Type u_3}
[AddCommGroup α]
[AddCommGroup β]
(a : α)
(f : α → β)
:
Function.support (τ a f) = a +ᵥ Function.support f
Conjugation negation operator #
@[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 : α → β)
:
theorem
conjneg_injective
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[CommSemiring β]
[StarRing β]
:
Function.Injective conjneg
@[simp]
theorem
conjneg_conj
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[CommSemiring β]
[StarRing β]
(f : α → β)
:
conjneg ((starRingEnd (α → β)) f) = (starRingEnd (α → β)) (conjneg f)
@[simp]
@[simp]
theorem
sum_conjneg
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[CommSemiring β]
[StarRing β]
[Fintype α]
(f : α → β)
:
(Finset.univ.sum fun (a : α) => conjneg f a) = Finset.univ.sum fun (a : α) => (starRingEnd β) (f a)
@[simp]
theorem
support_conjneg
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[CommSemiring β]
[StarRing β]
(f : α → β)
:
@[simp]
theorem
conjneg_nonneg
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[OrderedCommSemiring β]
[StarRing β]
[StarOrderedRing β]
{f : α → β}
:
@[simp]
theorem
conjneg_pos
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[OrderedCommSemiring β]
[StarRing β]
[StarOrderedRing β]
{f : α → β}
:
@[simp]
theorem
conjneg_nonpos
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[OrderedCommRing β]
[StarRing β]
[StarOrderedRing β]
{f : α → β}
:
@[simp]
theorem
conjneg_neg'
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[OrderedCommRing β]
[StarRing β]
[StarOrderedRing β]
{f : α → β}
:
theorem
IsSelfAdjoint.dilate
{G : Type u_3}
{𝕜 : Type u_4}
[AddCommGroup G]
[Star 𝕜]
{f : G → 𝕜}
(hf : IsSelfAdjoint f)
(n : ℕ)
:
IsSelfAdjoint (dilate f n)