Documentation

Mathlib.Data.Finsupp.Antidiagonal

The Finsupp counterpart of Multiset.antidiagonal. #

The antidiagonal of s : α →₀ ℕ consists of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s.

source
def Finsupp.antidiagonal' {α : Type u} [DecidableEq α] (f : α →₀ ℕ) :
(α →₀ ℕ) × (α →₀ ℕ) →₀ ℕ

The Finsupp counterpart of Multiset.antidiagonal: the antidiagonal of s : α →₀ ℕ consists of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s. The finitely supported function antidiagonal s is equal to the multiplicities of these pairs.

Equations
Instances For
    source
    def Finsupp.antidiagonal {α : Type u} [DecidableEq α] (f : α →₀ ℕ) :
    Finset ((α →₀ ℕ) × (α →₀ ℕ))

    The antidiagonal of s : α →₀ ℕ is the finset of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s.

    Equations
    Instances For
      source
      @[simp]
      theorem Finsupp.mem_antidiagonal {α : Type u} [DecidableEq α] {f : α →₀ ℕ} {p : (α →₀ ℕ) × (α →₀ ℕ)} :
      p ∈ Finsupp.antidiagonal f ↔ p.fst + p.snd = f
      source
      theorem Finsupp.swap_mem_antidiagonal {α : Type u} [DecidableEq α] {n : α →₀ ℕ} {f : (α →₀ ℕ) × (α →₀ ℕ)} :
      Prod.swap f ∈ Finsupp.antidiagonal n ↔ f ∈ Finsupp.antidiagonal n
      source
      theorem Finsupp.antidiagonal_filter_fst_eq {α : Type u} [DecidableEq α] (f : α →₀ ℕ) (g : α →₀ ℕ) [D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = g)] :
      Finset.filter (fun p => p.fst = g) (Finsupp.antidiagonal f) = if g ≤ f then {(g, f - g)} else ∅
      source
      theorem Finsupp.antidiagonal_filter_snd_eq {α : Type u} [DecidableEq α] (f : α →₀ ℕ) (g : α →₀ ℕ) [D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)] :
      Finset.filter (fun p => p.snd = g) (Finsupp.antidiagonal f) = if g ≤ f then {(f - g, g)} else ∅
      source
      @[simp]
      theorem Finsupp.antidiagonal_zero {α : Type u} [DecidableEq α] :
      Finsupp.antidiagonal 0 = {(0, 0)}
      source
      theorem Finsupp.sum_antidiagonal_swap {α : Type u} [DecidableEq α] {M : Type u_1} [AddCommMonoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M) :
      (Finset.sum (Finsupp.antidiagonal n) fun p => f p.fst p.snd) = Finset.sum (Finsupp.antidiagonal n) fun p => f p.snd p.fst
      source
      theorem Finsupp.prod_antidiagonal_swap {α : Type u} [DecidableEq α] {M : Type u_1} [CommMonoid M] (n : α →₀ ℕ) (f : (α →₀ ℕ) → (α →₀ ℕ) → M) :
      (Finset.prod (Finsupp.antidiagonal n) fun p => f p.fst p.snd) = Finset.prod (Finsupp.antidiagonal n) fun p => f p.snd p.fst
      source
      @[simp]
      theorem Finsupp.antidiagonal_single {α : Type u} [DecidableEq α] (a : α) (n : ℕ) :
      (Finsupp.antidiagonal fun₀ | a => n) = Finset.map (Function.Embedding.prodMap { toFun := Finsupp.single a, inj' := (_ : Function.Injective (Finsupp.single a)) } { toFun := Finsupp.single a, inj' := (_ : Function.Injective (Finsupp.single a)) }) (Finset.Nat.antidiagonal n)