Documentation

Mathlib.Algebra.Order.Antidiag.Finsupp

Antidiagonal of finitely supported functions as finsets #

This file defines the finset of finitely functions summing to a specific value on a finset. Such finsets should be thought of as the "antidiagonals" in the space of finitely supported functions.

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

We define it using Finset.piAntidiag s n, the corresponding antidiagonal in ι → μ.

Main declarations #

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 equal to n.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Finset.mem_finsuppAntidiag {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {s : Finset ι} {n : μ} {f : ι →₀ μ} :
    f s.finsuppAntidiag n s.sum f = n f.support s
    theorem Finset.mem_finsuppAntidiag' {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {s : Finset ι} {n : μ} {f : ι →₀ μ} :
    f s.finsuppAntidiag n (f.sum fun (x : ι) (x : μ) => x) = n f.support s
    @[simp]
    theorem Finset.finsuppAntidiag_empty_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] :
    .finsuppAntidiag 0 = {0}
    @[simp]
    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} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {a : ι} {s : Finset ι} (h : as) (n : μ) {f : ι →₀ μ} :
    f (insert a s).finsuppAntidiag n mFinset.antidiagonal n, ∃ (g : ι →₀ μ), f = g.update a m.1 g s.finsuppAntidiag m.2
    theorem Finset.finsuppAntidiag_insert {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {a : ι} {s : Finset ι} (h : as) (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)
    @[simp]
    theorem Finset.finsuppAntidiag_zero {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [DecidableEq μ] [CanonicallyOrderedAddCommMonoid μ] [Finset.HasAntidiagonal μ] (s : Finset ι) :
    s.finsuppAntidiag 0 = {0}