Collections of tuples of naturals with the same sum #

This file generalizes List.Nat.Antidiagonal n, Multiset.Nat.Antidiagonal n, and Finset.Nat.Antidiagonal n from the pair of elements x : ℕ × ℕ such that n = x.1 + x.2, to the sequence of elements x : Fin k → ℕ such that n = ∑ i, x i.

Main definitions #

• List.Nat.antidiagonalTuple
• Multiset.Nat.antidiagonalTuple
• Finset.Nat.antidiagonalTuple

Main results #

• antidiagonalTuple 2 n is analogous to antidiagonal n:

• List.Nat.antidiagonalTuple_two
• Multiset.Nat.antidiagonalTuple_two
• Finset.Nat.antidiagonalTuple_two

Implementation notes #

While we could implement this by filtering (Fintype.PiFinset fun _ ↦ range (n + 1)) or similar, this implementation would be much slower.

In the future, we could consider generalizing Finset.Nat.antidiagonalTuple further to support finitely-supported functions, as is done with cut in archive/100-theorems-list/45_partition.lean.

Lists #

def List.Nat.antidiagonalTuple (k : ) :
List (Fin k)

List.antidiagonalTuple k n is a list of all k-tuples which sum to n.

This list contains no duplicates (List.Nat.nodup_antidiagonalTuple), and is sorted lexicographically (List.Nat.antidiagonalTuple_pairwise_pi_lex), starting with ![0, ..., n] and ending with ![n, ..., 0].

#eval antidiagonalTuple 3 2
-- [![0, 0, 2], ![0, 1, 1], ![0, 2, 0], ![1, 0, 1], ![1, 1, 0], ![2, 0, 0]]

Equations
Instances For
theorem List.Nat.mem_antidiagonalTuple {n : } {k : } {x : Fin k} :
i : Fin k, x i = n
theorem List.Nat.nodup_antidiagonalTuple (k : ) (n : ) :
.Nodup

The antidiagonal of n does not contain duplicate entries.

@[simp]
theorem List.Nat.antidiagonalTuple_one (n : ) :
= [![n]]
theorem List.Nat.antidiagonalTuple_two (n : ) :
= List.map (fun (i : ) => ![i.1, i.2])
theorem List.Nat.antidiagonalTuple_pairwise_pi_lex (k : ) (n : ) :
List.Pairwise (Pi.Lex (fun (x x_1 : Fin k) => x < x_1) fun (x : Fin k) (x x_1 : ) => x < x_1)

Multisets #

Multiset.Nat.antidiagonalTuple k n is a multiset of k-tuples summing to n

Equations
Instances For
theorem Multiset.Nat.mem_antidiagonalTuple {n : } {k : } {x : Fin k} :
i : Fin k, x i = n
@[simp]
theorem Multiset.Nat.antidiagonalTuple_two (n : ) :
= Multiset.map (fun (i : ) => ![i.1, i.2])

Finsets #

Finset.Nat.antidiagonalTuple k n is a finset of k-tuples summing to n

Equations
• = { val := , nodup := }
Instances For
theorem Finset.Nat.mem_antidiagonalTuple {n : } {k : } {x : Fin k} :
i : Fin k, x i = n
@[simp]
theorem Finset.Nat.antidiagonalTuple_one (n : ) :
= {![n]}
theorem Finset.Nat.antidiagonalTuple_two (n : ) :
= Finset.map (piFinTwoEquiv fun (x : Fin 2) => ).symm.toEmbedding
@[simp]
theorem Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst (k : ) (x : Fin k) :
().fst = i : Fin k, x i
@[simp]
theorem Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe (k : ) (x : Fin k) :
∀ (a : Fin k), ().snd a = x a
@[simp]
theorem Finset.Nat.sigmaAntidiagonalTupleEquivTuple_apply (k : ) (x : (n : ) × { x : Fin k // }) :
∀ (a : Fin k), = x.snd a
def Finset.Nat.sigmaAntidiagonalTupleEquivTuple (k : ) :
(n : ) × { x : Fin k // } (Fin k)

The disjoint union of antidiagonal tuples Σ n, antidiagonalTuple k n is equivalent to the k-tuple Fin k → ℕ. This is such an equivalence, obtained by mapping (n, x) to x.

This is the tuple version of Finset.sigmaAntidiagonalEquivProd.

Equations
• One or more equations did not get rendered due to their size.
Instances For