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.

Precisely, for a commutative monoid μ with antidiagonals (see Finset.HasAntidiagonal), Finset.piAntidiag s n is the finset of all functions f : ι → μ with support contained in s and such that the sum of its values equals n : μ.

We define it recursively on s using Finset.HasAntidiagonal.antidiagonal : μ → Finset (μ × μ). Technically, we non-canonically identify s with Fin n where n = s.card, recurse on n using that (Fin (n + 1) → μ) ≃ (Fin n → μ) × μ, and show the end result doesn't depend on our identification. See Finset.finAntidiag for the details.

Main declarations

• Finset.piAntidiag s n: Finset of all functions f : ι → μ with support contained in s and such that the sum of its values equals n : μ.
• Finset.finAntidiagonal d n: Computationally efficient special case of Finset.piAntidiag when ι := Fin d.

TODO

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

See also

Finset.finsuppAntidiag for the Finset (ι →₀ μ)-valued version of Finset.piAntidiag.

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.aux {μ : Type u_2} [AddCommMonoid μ] [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 ⟨∅, ⋯⟩

def Finset.finAntidiagonal {μ : Type u_2} [AddCommMonoid μ] [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)

@[simp]

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

ι → μ

In this section, we transfer the antidiagonals in Fin s.card → μ to antidiagonals in ι → s by choosing an identification s ≃ Fin s.card and proving that the end result does not depend on that choice.

def Finset.piAntidiag {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (s : Finset ι) (n : μ) : Finset (ι → μ)

The finset of functions ι → μ with support contained in s and sum n.

Equations

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

@[simp]

theorem Finset.mem_piAntidiag {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {s : Finset ι} {n : μ} {f : ι → μ} : f ∈ s.piAntidiag n ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

@[simp]

theorem Finset.piAntidiag_empty_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] : ∅.piAntidiag 0 = {0}

@[simp]

theorem Finset.piAntidiag_empty_of_ne_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {n : μ} (hn : n ≠ 0) : ∅.piAntidiag n = ∅

theorem Finset.piAntidiag_empty {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (n : μ) : ∅.piAntidiag n = if n = 0 then {0} else ∅

theorem Finset.finsetCongr_piAntidiag_eq_antidiag {μ : Type u_2} [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (n : μ) : (Equiv.boolArrowEquivProd μ).finsetCongr (univ.piAntidiag n) = antidiagonal n

theorem Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbedding {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCancelCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {i : ι} {s : Finset ι} (hi : i ∉ s) (n : μ) : (↑(antidiagonal n)).PairwiseDisjoint fun (p : μ × μ) => map (addRightEmbedding fun (j : ι) => if j = i then p.1 else 0) (s.piAntidiag p.2)

theorem Finset.piAntidiag_cons {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCancelCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {i : ι} {s : Finset ι} (hi : i ∉ s) (n : μ) : (cons i s hi).piAntidiag n = (antidiagonal n).disjiUnion (fun (p : μ × μ) => map (addRightEmbedding fun (t : ι) => if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯

theorem Finset.piAntidiag_insert {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCancelCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {i : ι} {s : Finset ι} [DecidableEq (ι → μ)] (hi : i ∉ s) (n : μ) : (insert i s).piAntidiag n = (antidiagonal n).biUnion fun (p : μ × μ) => image (fun (f : ι → μ) (j : ι) => f j + if j = i then p.1 else 0) (s.piAntidiag p.2)

@[simp]

theorem Finset.piAntidiag_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [PartialOrder μ] [CanonicallyOrderedAdd μ] [HasAntidiagonal μ] [DecidableEq μ] (s : Finset ι) : s.piAntidiag 0 = {0}

theorem Finset.piAntidiag_univ_fin_eq_antidiagonalTuple (n k : ℕ) : univ.piAntidiag n = Nat.antidiagonalTuple k n

theorem Finset.nsmul_piAntidiag {ι : Type u_1} [DecidableEq ι] [DecidableEq (ι → ℕ)] (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0) : SMul.smul n (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

theorem Finset.map_nsmul_piAntidiag {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0) : map { toFun := fun (x : ι → ℕ) => n • x, inj' := ⋯ } (s.piAntidiag m) = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

theorem Finset.nsmul_piAntidiag_univ {ι : Type u_1} [DecidableEq ι] [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) : SMul.smul n (univ.piAntidiag m) = {f ∈ univ.piAntidiag (n * m) | ∀ (i : ι), n ∣ f i}

theorem Finset.map_nsmul_piAntidiag_univ {ι : Type u_1} [DecidableEq ι] [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) : map { toFun := fun (x : ι → ℕ) => n • x, inj' := ⋯ } (univ.piAntidiag m) = {f ∈ univ.piAntidiag (n * m) | ∀ (i : ι), n ∣ f i}

theorem Finset.map_sym_eq_piAntidiag {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (n : ℕ) : map { toFun := fun (m : Sym ι n) (a : ι) => Multiset.count a ↑m, inj' := ⋯ } (s.sym n) = s.piAntidiag n