Documentation

Mathlib.Data.Fin.Tuple.NatAntidiagonal

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 #

Main results #

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} :
    x List.Nat.antidiagonalTuple k n i : Fin k, x i = n

    The antidiagonal of n does not contain duplicate entries.

    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 #

    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} :
      x Multiset.Nat.antidiagonalTuple k n i : Fin k, x i = n

      Finsets #

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

      Equations
      Instances For
        theorem Finset.Nat.mem_antidiagonalTuple {n : } {k : } {x : Fin k} :
        x Finset.Nat.antidiagonalTuple k n i : Fin k, x i = n
        @[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

        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