# 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`.

source
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)

Instances For

source
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 ⟨∅, ⋯⟩

Instances For

source
@[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.

source
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.

Instances For

source
@[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
source
@[simp]
theorem Finset.piAntidiag_empty_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] :
∅.piAntidiag 0 = {0}
source
@[simp]
theorem Finset.piAntidiag_empty_of_ne_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] {n : μ} (hn : n ≠ 0) :
∅.piAntidiag n = ∅
source
theorem Finset.piAntidiag_empty {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (n : μ) :
∅.piAntidiag n = if n = 0 then {0} else ∅
source
theorem Finset.finsetCongr_piAntidiag_eq_antidiag {μ : Type u_2} [AddCommMonoid μ] [HasAntidiagonal μ] [DecidableEq μ] (n : μ) :
(Equiv.boolArrowEquivProd μ).finsetCongr (univ.piAntidiag n) = antidiagonal n
source
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)
source
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)) ⋯
source
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)
source
@[simp]
theorem Finset.piAntidiag_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [PartialOrder μ] [CanonicallyOrderedAdd μ] [HasAntidiagonal μ] [DecidableEq μ] (s : Finset ι) :
s.piAntidiag 0 = {0}
source
theorem Finset.piAntidiag_univ_fin_eq_antidiagonalTuple (n k : ℕ) :
univ.piAntidiag n = Nat.antidiagonalTuple k n
source
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}
source
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}
source
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}
source
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}
source
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