Documentation

Mathlib.Data.Finset.PiAntidiagonal

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 #

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
Instances For
    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.
    Instances For
      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

      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.
      Instances For
        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.
        Instances For
          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
          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 : as) (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 : as) (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' := (_ : ∀ (x x_1 : { x : ι →₀ μ // x Finset.piAntidiagonal s p.2 }), (fun (f : { x : ι →₀ μ // x Finset.piAntidiagonal s p.2 }) => Finsupp.update (f) a p.1) x = (fun (f : { x : ι →₀ μ // x Finset.piAntidiagonal s p.2 }) => Finsupp.update (f) a p.1) x_1x = x_1) } (Finset.attach (Finset.piAntidiagonal s p.2))