Partial HasAntidiagonal for functions with finite support

For an AddCommMonoid μ, Finset.HasAntidiagonal μ provides a function antidiagonal : μ → Finset (μ × μ) which maps n : μ to a Finset of pairs (a, b) such that a + b = n.

In this file, we provide an analogous definition for ι →₀ μ, with an explicit finiteness condition on the support, assuming AddCommMonoid μ, HasAntidiagonal μ, For computability reasons, we also need DecidableEq ι and DecidableEq μ.

This Finset could be viewed inside ι → μ, but the Finsupp condition provides a natural DecidableEq instance.

Main definitions

• Finset.finsuppAntidiag s n is the finite set of all functions f : ι →₀ μ with finite support contained in s and such that the sum of its values equals n : μ That condition is expressed by Finset.mem_finsuppAntidiag
• Finset.mem_finsuppAntidiag' rewrites the Finsupp.sum condition as a Finset.sum.

def Finset.finAntidiagonal₀ {μ : Type u_2} [AddCommMonoid μ] [DecidableEq μ] [Finset.HasAntidiagonal μ] (d : ℕ) (n : μ) : Finset (Fin d →₀ μ)

finAntidiagonal₀ d n is the type of d-tuples with sum n

Equations

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

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

theorem Finset.mem_finAntidiagonal₀ {μ : Type u_2} [AddCommMonoid μ] [DecidableEq μ] [Finset.HasAntidiagonal μ] (d : ℕ) (n : μ) (f : Fin d →₀ μ) : f ∈ Finset.finAntidiagonal₀ d n ↔ (f.sum fun (x : Fin d) (x : μ) => x) = n

def Finset.finsuppAntidiag {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.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.

theorem Finset.mem_finsuppAntidiag {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {s : Finset ι} {n : μ} {f : ι →₀ μ} : f ∈ s.finsuppAntidiag n ↔ f.support ⊆ s ∧ (f.sum fun (x : ι) (x : μ) => x) = n

A function belongs to finsuppAntidiag s n iff its support is contained in s and the sum of its components is equal to n

theorem Finset.mem_finsuppAntidiag' {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] (s : Finset ι) (n : μ) (f : ι →₀ μ) : f ∈ s.finsuppAntidiag n ↔ f.support ⊆ s ∧ s.sum ⇑f = n

@[simp]

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

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

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

theorem Finset.mem_finsuppAntidiag_insert {ι : Type u_1} {μ : Type u_2} [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] [DecidableEq ι] {a : ι} {s : Finset ι} (h : a ∉ s) (n : μ) {f : ι →₀ μ} : f ∈ (insert a s).finsuppAntidiag n ↔ ∃ m ∈ Finset.antidiagonal n, ∃ (g : ι →₀ μ), f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2

theorem Finset.finsuppAntidiag_insert {ι : Type u_1} {μ : Type u_2} [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq ι] [DecidableEq μ] {a : ι} {s : Finset ι} (h : a ∉ s) (n : μ) : (insert a s).finsuppAntidiag n = (Finset.antidiagonal n).biUnion fun (p : μ × μ) => Finset.map { toFun := fun (f : { x : ι →₀ μ // x ∈ s.finsuppAntidiag p.2 }) => (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

theorem Finset.mapRange_finsuppAntidiag_subset {ι : Type u_1} {μ : Type u_2} {μ' : Type u_3} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] [AddCommMonoid μ'] [Finset.HasAntidiagonal μ'] [DecidableEq μ'] {e : μ ≃+ μ'} {s : Finset ι} {n : μ} : Finset.map (Finsupp.mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) ⊆ s.finsuppAntidiag (e n)

theorem Finset.mapRange_finsuppAntidiag_eq {ι : Type u_1} {μ : Type u_2} {μ' : Type u_3} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] [AddCommMonoid μ'] [Finset.HasAntidiagonal μ'] [DecidableEq μ'] {e : μ ≃+ μ'} {s : Finset ι} {n : μ} : Finset.map (Finsupp.mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) = s.finsuppAntidiag (e n)

theorem Finset.finsuppAntidiag_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [CanonicallyOrderedAddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] (s : Finset ι) : s.finsuppAntidiag 0 = {0}