Applying a function to a distribution

Stream: Is there code for X?

[Frédéric Dupuis]

Is something like the following somewhere in mathlib?

open Finset in
def AddMonoid.domain_apply {α β E : Type*} [Fintype α] [DecidableEq β] [AddCommMonoid E]
    (f : α → β) (g : α → E) : β → E :=
  fun x => ∑ z in filter (fun y => f y = x) univ, g z

I'm not too sure what to call this, but this is the operation that happens when e.g. g x is a quantum state that depends on a classical label x, and we apply a function to the classical label.

[Bhavik Mehta]

Not directly, but there's a few lemmas about functions like this that might be useful to you, usually with the name 'fiberwise' in there somewhere

[Junyan Xu]

Actually, there is docs#Finsupp.mapDomain

[Frédéric Dupuis]

Great, thanks!

[Junyan Xu]

You may want to combine it with docs#Finsupp.equivFunOnFinite :)