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.piAntidiagonal s n is the finite set of all functions with finite support contained in s and sum n : μ That condition is expressed by Finset.mem_piAntidiagonal
• Finset.mem_piAntidiagonal' rewrites the Finsupp.sum condition as a Finset.sum.
• Finset.finAntidiagonal, a more general case of Finset.Nat.antidiagonalTuple (TODO: deduplicate).

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.

TODO: deduplicate with the less general Finset.Nat.antidiagonalTuple.

Equations

• Finset.finAntidiagonal d n = ↑(Finset.finAntidiagonal.aux d n)

def Finset.finAntidiagonal.aux {μ : Type u_2} [AddCommMonoid μ] [DecidableEq μ] [Finset.HasAntidiagonal μ] (d : ℕ) (n : μ) : { s : Finset (Fin d → μ) // ∀ (f : Fin d → μ), f ∈ s ↔ (Finset.sum Finset.univ fun (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 { val := {0}, property := ⋯ } else { val := ∅, property := ⋯ }

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

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 ↔ (Finset.sum Finset.univ fun (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 ↔ (Finsupp.sum f fun (x : Fin d) (x : μ) => x) = n

def Finset.piAntidiagonal {ι : 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_piAntidiagonal {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {s : Finset ι} {n : μ} {f : ι →₀ μ} : f ∈ Finset.piAntidiagonal s n ↔ f.support ⊆ s ∧ (Finsupp.sum f fun (x : ι) (x : μ) => x) = n

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

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

@[simp]

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

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

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

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

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

theorem Finset.mapRange_piAntidiagonal_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 (Equiv.toEmbedding (Finsupp.mapRange.addEquiv e).toEquiv) (Finset.piAntidiagonal s n) ⊆ Finset.piAntidiagonal s (e n)

theorem Finset.mapRange_piAntidiagonal_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 (Equiv.toEmbedding (Finsupp.mapRange.addEquiv e).toEquiv) (Finset.piAntidiagonal s n) = Finset.piAntidiagonal s (e n)

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