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

• List.Nat.antidiagonalTuple 0 0 = [![]]
• List.Nat.antidiagonalTuple 0 n.succ = []
• List.Nat.antidiagonalTuple k.succ x = (List.Nat.antidiagonal x).flatMap fun (ni : ℕ × ℕ) => List.map (fun (x : Fin k → ℕ) => Fin.cons ni.1 x) (List.Nat.antidiagonalTuple k ni.2)

@[simp]

theorem List.Nat.antidiagonalTuple_zero_zero : List.Nat.antidiagonalTuple 0 0 = [![]]

@[simp]

theorem List.Nat.antidiagonalTuple_zero_succ (n : ℕ) : List.Nat.antidiagonalTuple 0 (n + 1) = []

theorem List.Nat.mem_antidiagonalTuple {n : ℕ} {k : ℕ} {x : Fin k → ℕ} : x ∈ List.Nat.antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n

theorem List.Nat.nodup_antidiagonalTuple (k : ℕ) (n : ℕ) : (List.Nat.antidiagonalTuple k n).Nodup

The antidiagonal of n does not contain duplicate entries.

theorem List.Nat.antidiagonalTuple_zero_right (k : ℕ) : List.Nat.antidiagonalTuple k 0 = [0]

@[simp]

theorem List.Nat.antidiagonalTuple_one (n : ℕ) : List.Nat.antidiagonalTuple 1 n = [![n]]

theorem List.Nat.antidiagonalTuple_two (n : ℕ) : List.Nat.antidiagonalTuple 2 n = List.map (fun (i : ℕ × ℕ) => ![i.1, i.2]) (List.Nat.antidiagonal n)

theorem List.Nat.antidiagonalTuple_pairwise_pi_lex (k : ℕ) (n : ℕ) : List.Pairwise (Pi.Lex (fun (x1 x2 : Fin k) => x1 < x2) fun (x : Fin k) (x1 x2 : ℕ) => x1 < x2) (List.Nat.antidiagonalTuple k n)

Multisets

def Multiset.Nat.antidiagonalTuple (k : ℕ) (n : ℕ) : Multiset (Fin k → ℕ)

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

Equations

• Multiset.Nat.antidiagonalTuple k n = ↑(List.Nat.antidiagonalTuple k n)

@[simp]

theorem Multiset.Nat.antidiagonalTuple_zero_zero : Multiset.Nat.antidiagonalTuple 0 0 = {![]}

@[simp]

theorem Multiset.Nat.antidiagonalTuple_zero_succ (n : ℕ) : Multiset.Nat.antidiagonalTuple 0 n.succ = 0

theorem Multiset.Nat.mem_antidiagonalTuple {n : ℕ} {k : ℕ} {x : Fin k → ℕ} : x ∈ Multiset.Nat.antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n

theorem Multiset.Nat.nodup_antidiagonalTuple (k : ℕ) (n : ℕ) : (Multiset.Nat.antidiagonalTuple k n).Nodup

theorem Multiset.Nat.antidiagonalTuple_zero_right (k : ℕ) : Multiset.Nat.antidiagonalTuple k 0 = {0}

@[simp]

theorem Multiset.Nat.antidiagonalTuple_one (n : ℕ) : Multiset.Nat.antidiagonalTuple 1 n = {![n]}

theorem Multiset.Nat.antidiagonalTuple_two (n : ℕ) : Multiset.Nat.antidiagonalTuple 2 n = Multiset.map (fun (i : ℕ × ℕ) => ![i.1, i.2]) (Multiset.Nat.antidiagonal n)

Finsets

def Finset.Nat.antidiagonalTuple (k : ℕ) (n : ℕ) : Finset (Fin k → ℕ)

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

Equations

• Finset.Nat.antidiagonalTuple k n = { val := Multiset.Nat.antidiagonalTuple k n, nodup := ⋯ }

@[simp]

theorem Finset.Nat.antidiagonalTuple_zero_zero : Finset.Nat.antidiagonalTuple 0 0 = {![]}

@[simp]

theorem Finset.Nat.antidiagonalTuple_zero_succ (n : ℕ) : Finset.Nat.antidiagonalTuple 0 n.succ = ∅

theorem Finset.Nat.mem_antidiagonalTuple {n : ℕ} {k : ℕ} {x : Fin k → ℕ} : x ∈ Finset.Nat.antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n

theorem Finset.Nat.antidiagonalTuple_zero_right (k : ℕ) : Finset.Nat.antidiagonalTuple k 0 = {0}

@[simp]

theorem Finset.Nat.antidiagonalTuple_one (n : ℕ) : Finset.Nat.antidiagonalTuple 1 n = {![n]}

theorem Finset.Nat.antidiagonalTuple_two (n : ℕ) : Finset.Nat.antidiagonalTuple 2 n = Finset.map (piFinTwoEquiv fun (x : Fin 2) => ℕ).symm.toEmbedding (Finset.antidiagonal n)

def Finset.Nat.sigmaAntidiagonalTupleEquivTuple (k : ℕ) : (n : ℕ) × { x : Fin k → ℕ // x ∈ Finset.Nat.antidiagonalTuple k n } ≃ (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.

@[simp]

theorem Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe (k : ℕ) (x : Fin k → ℕ) : ∀ (a : Fin k), ↑((Finset.Nat.sigmaAntidiagonalTupleEquivTuple k).symm x).snd a = x a

@[simp]

theorem Finset.Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst (k : ℕ) (x : Fin k → ℕ) : ((Finset.Nat.sigmaAntidiagonalTupleEquivTuple k).symm x).fst = ∑ i : Fin k, x i

@[simp]

theorem Finset.Nat.sigmaAntidiagonalTupleEquivTuple_apply (k : ℕ) (x : (n : ℕ) × { x : Fin k → ℕ // x ∈ Finset.Nat.antidiagonalTuple k n }) : ∀ (a : Fin k), (Finset.Nat.sigmaAntidiagonalTupleEquivTuple k) x a = ↑x.snd a