finsum of sum

Stream: Is there code for X?

[Scott Carnahan]

Is there a standard way to manipulate finsums containing sums? Do we typically reduce to a sum using docs#finsum_eq_sum_of_support_subset ?

import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Data.Finset.NatAntidiagonal
import Mathlib.Data.Finsupp.Defs

open BigOperators Finset

example {R : Type*} [AddCommMonoid R] (f : ℕ × ℕ →₀ R) :
    ∑ᶠ (n : ℕ), (∑ ij ∈ antidiagonal n, f ij) = ∑ᶠ (mn : ℕ × ℕ), f mn := by
  sorry

[Yury G. Kudryashov]

There is very little API about finsums in the library. I think that you'll need to figure out what lemmas are missing and add them.

[Yury G. Kudryashov]

E.g., we don't have a lemma saying that RHS of your equality is equal to f.sum fun _ y => y.

[Yury G. Kudryashov]

BTW, you can use Finsupp API instead of finsum, if your function is a Finsupp anyway.

[Yury G. Kudryashov]

You need to prove f.mapDomain (fun (a, b) => a + b) n = ∑ ij ∈ antidiagonal n, f ij

[Yury G. Kudryashov]

Probably, you'll need a version of docs#Finsupp.mapDomain_apply that says something like

theorem Finsupp.mapDomain_apply_of_preimage (f : α → β) (v : α →₀ M) (b : β) (s : Finset α) (hs : ∀ x, x ∈ s ↔ f x = b) :
  v.mapDomain f b = ∑ a in s, f a := _

[Scott Carnahan]

Thank you for letting me know. I'll try to add something.