Antidiagonal of functions as finsets

This file provides the finset of functions summing to a specific value on a finset. Such finsets should be thought of as the "antidiagonals" in the space of functions.

TODO

Finset.finAntidiagonal is strictly more general than Finset.Nat.antidiagonalTuple. Deduplicate.

Fin d → μ

In this section, we define the antidiagonals in Fin d → μ by recursion on d. Note that this is computationally efficient, although probably not as efficient as Finset.Nat.antidiagonalTuple.

def Finset.finAntidiagonal {μ : Type u_2} [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] (d : ℕ) (n : μ) : Finset (Fin d → μ)

finAntidiagonal d n is the type of d-tuples with sum n.

TODO: deduplicate with the less general Finset.Nat.antidiagonalTuple.

Equations

• Finset.finAntidiagonal d n = ↑(Finset.finAntidiagonal.aux d n)

def Finset.finAntidiagonal.aux {μ : Type u_2} [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] (d : ℕ) (n : μ) : { s : Finset (Fin d → μ) // ∀ (f : Fin d → μ), f ∈ s ↔ ∑ i : Fin d, f i = n }

Auxiliary construction for finAntidiagonal that bundles a proof of lawfulness (mem_finAntidiagonal), as this is needed to invoke disjiUnion. Using Finset.disjiUnion makes this computationally much more efficient than using Finset.biUnion.

Equations

• One or more equations did not get rendered due to their size.
• Finset.finAntidiagonal.aux 0 n = if h : n = 0 then ⟨{0}, ⋯⟩ else ⟨∅, ⋯⟩

@[simp]

theorem Finset.mem_finAntidiagonal {μ : Type u_2} [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {n : μ} {d : ℕ} {f : Fin d → μ} : f ∈ Finset.finAntidiagonal d n ↔ ∑ i : Fin d, f i = n