noncomputable def
transfer
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[DecidableEq β]
[AddCommMonoid γ]
(f : α → β)
(g : α → γ)
:
β → γ
Equations
- (f # g) x = Finset.sum (Finset.filter (fun (y : α) => f y = x) Finset.univ) fun (y : α) => g y
Instances For
Equations
- «term_#_» = Lean.ParserDescr.trailingNode `term_#_ 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " # ") (Lean.ParserDescr.cat `term 75))
Instances For
theorem
transfer_add
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[DecidableEq β]
[AddCommMonoid γ]
(f : α → β)
(g : α → γ)
(h : α → γ)
:
theorem
comp_transfer
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{γ₂ : Type u_4}
{G : Type u_5}
[Fintype α]
[DecidableEq β]
[AddCommMonoid γ]
[AddCommMonoid γ₂]
[FunLike G γ γ₂]
[AddMonoidHomClass G γ γ₂]
(f : α → β)
(g : α → γ)
(h : G)
:
theorem
equiv_transfer
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[DecidableEq β]
[AddCommMonoid γ]
(f : α ≃ β)
(g : α → γ)
(x : β)
:
theorem
transfer_transfer
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{γ₂ : Type u_4}
[Fintype α]
[DecidableEq β]
[AddCommMonoid γ]
[Fintype β]
[DecidableEq γ₂]
(f : α → β)
(g : α → γ)
(h : β → γ₂)
:
theorem
transfer_id
{α : Type u_1}
{β : Type u_2}
[Fintype α]
(f : α → β)
[DecidableEq α]
[AddCommMonoid β]
:
theorem
transfer_sub
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[DecidableEq β]
[SubtractionCommMonoid γ]
(f : α → β)
(g : α → γ)
(h : α → γ)
:
theorem
transfer_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[DecidableEq β]
[Fintype β]
[Semiring γ]
(f : α → β)
(g : α → γ)
(h : β → γ)
:
(Finset.sum Finset.univ fun (x : β) => (f # g) x * h x) = Finset.sum Finset.univ fun (x : α) => g x * h (f x)
theorem
transfer_expect
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[DecidableEq β]
[Fintype β]
[Semiring γ]
[Module ℚ≥0 γ]
[Nonempty β]
[Nonempty α]
(f : α → β)
(g : α → γ)
(h : β → γ)
:
(Finset.expect Finset.univ fun (x : β) => (f # g) x * h x) = (↑(Fintype.card α) / ↑(Fintype.card β)) • Finset.expect Finset.univ fun (x : α) => g x * h (f x)
theorem
transfer_ne_zero
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Fintype α]
[DecidableEq β]
[AddCommMonoid γ]
(f : α → β)
(g : α → γ)
(x : β)
(h : (f # g) x ≠ 0)
:
∃ (i : α), x = f i