finset from a finite subset of an infinite set

Stream: Is there code for X?

[Michael Stoll]

I have the following.

import tactic
open_locale big_operators

def weight (n d : ℕ) : Type := fin n.succ → ℕ
def wsum {n d : ℕ} (w : weight n d) : ℕ := ∑ j, w j
def testvecs (n d : ℕ) : set (weight n d) := {w | w.wsum = d}

Now I would like to produce a finset from testvecs n d. docs#set.to_finset requires a fintype instance on the subtype, but fintype needs the finset as a component. This looks like a chicken-and-egg problem. (docs#set.finite has the same problem.)

So what is the recommended way to produce a finset in such a case?

[Michael Stoll]

Or equivalently, a fintype instance on the subtype?

[Kyle Miller]

docs#finset.nat.antidiagonal_tuple is the finset

[Michael Stoll]

How on earth would I find that?

[Kyle Miller]

By asking here :smile:

[Kyle Miller]

But if you follow the Zulip and mathlib changelogs long enough you know that the key phrase is "antidiagonal"

[Kyle Miller]

If you do want a fintype (or a set.finite) you generally don't use their constructors, and there are instead usually other functions that will help you out. For example, if you want a fintype instance on testvecs you can use docs#fintype.of_finset (there are a number of example instances in https://leanprover-community.github.io/mathlib_docs/data/set/finite.html) along with finset.nat.antidiagonal_tuple

[Michael Stoll]

Why is it called "antidiagonal"?

[Kyle Miller]

I think you're supposed to think about how the diagonal consists of all coordinates where all indices are equal, and these are orthogonal complements of that

[Kyle Miller]

or, it's a minor diagonal of a matrix when there are two components, which is also known as the antidiagonal

[Michael Stoll]

I was looking for partition :smile:

[Yaël Dillies]

Usually a partition is considered unordered, which is the key difference here. See docs#nat.partition

[Michael Stoll]

That's what I figuered out, but then I didn't know what else to look for...

[Eric Wieser]

It's also worth noting that fin n → α is often called a tuple

[Eric Wieser]

I named that definition after docs#finset.nat.antidiagonal, which is the binary version

[Eric Wieser]

My original intent was to be able to use it for some generalized version of docs#exp_sum to match docs#exp_add_of_commute_of_mem_ball, but decided I didn't care enough to go through with it

[Michael Stoll]

My first thought when reading "antidiagonal" is "complement of the diagonal" or perhaps "graph of a nontrivial involution".

[Eric Wieser]

Complement of the diagonal is a good intuition; the antidiagonal tuples are a complement (in the sense of an affine subspace) to the diagonal formed by function.const

[Michael Stoll]

For my taste, this is one or two steps too removed. I'd probably have chosen ordered_partitions...

[Eric Wieser]

What names would you have chosen for docs#finset.nat.antidiagonal and docs#list.nat.antidiagonal (the prod rather than tuple versions)?

[Michael Stoll]

ordered_partitions_two? As the special case ordered_partitions n 2...

[Michael Stoll]

(Even though it is not formally a specialization from fin n → nat.)

[Michael Stoll]

Or pairs_with_sum :smile: