Finsupp.sum restriction

Stream: Is there code for X?

[Patrick Massot]

Do we have something like

import Mathlib.Algebra.BigOperators.Finsupp

open Finset Set

noncomputable
def Finsupp.restrict {α β : Type*} [Zero β] (f : α →₀ β) (s : Set α) : s →₀ β where
  support := f.support.preimage ((↑) : s → α) injOn_subtype_val
  toFun := fun x ↦ f x
  mem_support_toFun := by simp

@[simp]
lemma Finsupp.restrict_apply {α β : Type*} [Zero β] (f : α →₀ β) (s : Set α) (x : s) :
  f.restrict s x = f x := rfl

lemma Finsupp.sum_restrict {α β M : Type*} [Zero β] [AddCommMonoid M] {w : α →₀ β} {s : Set α}
    (h : (w.support : Set α) ⊆ s) (f : α → β → M) : (w.restrict s).sum (fun a ↦ f a) = w.sum f := by
  sorry

The lemma is hopefully correct (but it's getting very late here).

[Timo Carlin-Burns]

docs#Finsupp.subtypeDomain is essentially your Finsupp.restrict

import Mathlib.Data.Finsupp.Basic
import Mathlib.Algebra.BigOperators.Finsupp

open Finset Set

noncomputable
def Finsupp.restrict {α β : Type*} [Zero β] (f : α →₀ β) (s : Set α) : s →₀ β where
  support := f.support.preimage ((↑) : s → α) injOn_subtype_val
  toFun := fun x ↦ f x
  mem_support_toFun := by simp

@[simp]
lemma Finsupp.restrict_apply {α β : Type*} [Zero β] (f : α →₀ β) (s : Set α) (x : s) :
  f.restrict s x = f x := rfl

lemma Finsupp.restrict_eq_subtypeDomain {α β : Type*} [Zero β] (f : α →₀ β) (s : Set α) :
    f.restrict s = f.subtypeDomain (· ∈ s) := by ext; simp

lemma Finsupp.sum_restrict {α β M : Type*} [Zero β] [AddCommMonoid M] {w : α →₀ β} {s : Set α}
    (h : (w.support : Set α) ⊆ s) (f : α → β → M) : (w.restrict s).sum (fun a ↦ f a) = w.sum f := by
  rw [Finsupp.restrict_eq_subtypeDomain]
  exact sum_subtypeDomain_index h

[Patrick Massot]

Thanks a lot. I couldn't find docs#Finsupp.subtypeDomain . I guess I needed to sleep.