mathlib3 documentation

data.fin.tuple.nat_antidiagonal

Collections of tuples of naturals with the same sum #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Main results #

Implementation notes #

While we could implement this by filtering (fintype.pi_finset $ λ _, range (n + 1)) or similar, this implementation would be much slower.

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

Lists #

source
def list.nat.antidiagonal_tuple (k : ℕ) :
ℕ → list (fin k → ℕ)

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

This list contains no duplicates (list.nat.nodup_antidiagonal_tuple), and is sorted lexicographically (list.nat.antidiagonal_tuple_pairwise_pi_lex), starting with ![0, ..., n] and ending with ![n, ..., 0].

#eval antidiagonal_tuple 3 2
-- [![0, 0, 2], ![0, 1, 1], ![0, 2, 0], ![1, 0, 1], ![1, 1, 0], ![2, 0, 0]]
Equations
source
@[simp]
theorem list.nat.antidiagonal_tuple_zero_zero  :
list.nat.antidiagonal_tuple 0 0 = [matrix.vec_empty]
source
@[simp]
theorem list.nat.antidiagonal_tuple_zero_succ (n : ℕ) :
list.nat.antidiagonal_tuple 0 n.succ = list.nil
source
theorem list.nat.mem_antidiagonal_tuple {n k : ℕ} {x : fin k → ℕ} :
x ∈ list.nat.antidiagonal_tuple k n ↔ finset.univ.sum (λ (i : fin k), x i) = n
source
theorem list.nat.nodup_antidiagonal_tuple (k n : ℕ) :
(list.nat.antidiagonal_tuple k n).nodup

The antidiagonal of n does not contain duplicate entries.

source
theorem list.nat.antidiagonal_tuple_zero_right (k : ℕ) :
list.nat.antidiagonal_tuple k 0 = [0]
source
@[simp]
theorem list.nat.antidiagonal_tuple_one (n : ℕ) :
list.nat.antidiagonal_tuple 1 n = [![n]]
source
theorem list.nat.antidiagonal_tuple_two (n : ℕ) :
list.nat.antidiagonal_tuple 2 n = list.map (λ (i : ℕ × ℕ), ![i.fst, i.snd]) (list.nat.antidiagonal n)
source
theorem list.nat.antidiagonal_tuple_pairwise_pi_lex (k n : ℕ) :
list.pairwise (pi.lex has_lt.lt (λ (_x : fin k), has_lt.lt)) (list.nat.antidiagonal_tuple k n)

Multisets #

source
def multiset.nat.antidiagonal_tuple (k n : ℕ) :
multiset (fin k → ℕ)

multiset.antidiagonal_tuple k n is a multiset of k-tuples summing to n

Equations
source
@[simp]
theorem multiset.nat.antidiagonal_tuple_zero_zero  :
multiset.nat.antidiagonal_tuple 0 0 = {matrix.vec_empty}
source
@[simp]
theorem multiset.nat.antidiagonal_tuple_zero_succ (n : ℕ) :
multiset.nat.antidiagonal_tuple 0 n.succ = 0
source
theorem multiset.nat.mem_antidiagonal_tuple {n k : ℕ} {x : fin k → ℕ} :
x ∈ multiset.nat.antidiagonal_tuple k n ↔ finset.univ.sum (λ (i : fin k), x i) = n
source
theorem multiset.nat.nodup_antidiagonal_tuple (k n : ℕ) :
(multiset.nat.antidiagonal_tuple k n).nodup
source
theorem multiset.nat.antidiagonal_tuple_zero_right (k : ℕ) :
multiset.nat.antidiagonal_tuple k 0 = {0}
source
@[simp]
theorem multiset.nat.antidiagonal_tuple_one (n : ℕ) :
multiset.nat.antidiagonal_tuple 1 n = {![n]}
source
theorem multiset.nat.antidiagonal_tuple_two (n : ℕ) :
multiset.nat.antidiagonal_tuple 2 n = multiset.map (λ (i : ℕ × ℕ), ![i.fst, i.snd]) (multiset.nat.antidiagonal n)

Finsets #

source
def finset.nat.antidiagonal_tuple (k n : ℕ) :
finset (fin k → ℕ)

finset.antidiagonal_tuple k n is a finset of k-tuples summing to n

Equations
source
@[simp]
theorem finset.nat.antidiagonal_tuple_zero_zero  :
finset.nat.antidiagonal_tuple 0 0 = {matrix.vec_empty}
source
@[simp]
theorem finset.nat.antidiagonal_tuple_zero_succ (n : ℕ) :
finset.nat.antidiagonal_tuple 0 n.succ = ∅
source
theorem finset.nat.mem_antidiagonal_tuple {n k : ℕ} {x : fin k → ℕ} :
x ∈ finset.nat.antidiagonal_tuple k n ↔ finset.univ.sum (λ (i : fin k), x i) = n
source
theorem finset.nat.antidiagonal_tuple_zero_right (k : ℕ) :
finset.nat.antidiagonal_tuple k 0 = {0}
source
@[simp]
theorem finset.nat.antidiagonal_tuple_one (n : ℕ) :
finset.nat.antidiagonal_tuple 1 n = {![n]}
source
theorem finset.nat.antidiagonal_tuple_two (n : ℕ) :
finset.nat.antidiagonal_tuple 2 n = finset.map (pi_fin_two_equiv (λ (_x : fin 2), ℕ)).symm.to_embedding (finset.nat.antidiagonal n)
source
@[simp]
theorem finset.nat.sigma_antidiagonal_tuple_equiv_tuple_symm_apply_snd_coe (k : ℕ) (x : fin k → ℕ) (ᾰ : fin k) :
↑((⇑((finset.nat.sigma_antidiagonal_tuple_equiv_tuple k).symm) x).snd) ᾰ = x ᾰ
source
@[simp]
theorem finset.nat.sigma_antidiagonal_tuple_equiv_tuple_apply (k : ℕ) (x : Σ (n : ℕ), ↥(finset.nat.antidiagonal_tuple k n)) (ᾰ : fin k) :
⇑(finset.nat.sigma_antidiagonal_tuple_equiv_tuple k) x ᾰ = ↑(x.snd) ᾰ
source
@[simp]
theorem finset.nat.sigma_antidiagonal_tuple_equiv_tuple_symm_apply_fst (k : ℕ) (x : fin k → ℕ) :
(⇑((finset.nat.sigma_antidiagonal_tuple_equiv_tuple k).symm) x).fst = finset.univ.sum (λ (i : fin k), x i)
source
def finset.nat.sigma_antidiagonal_tuple_equiv_tuple (k : ℕ) :
(Σ (n : ℕ), ↥(finset.nat.antidiagonal_tuple k n)) ≃ (fin k → ℕ)

The disjoint union of antidiagonal tuples Σ n, antidiagonal_tuple 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.nat.sigma_antidiagonal_equiv_prod.

Equations