Mathlib.Data.Multiset.NatAntidiagonal

Module docstring

{"# Antidiagonals in ℕ × ℕ as multisets

This file defines the antidiagonals of ℕ × ℕ as multisets: the n-th antidiagonal is the multiset of pairs (i, j) such that i + j = n. This is useful for polynomial multiplication and more generally for sums going from 0 to n.

Notes

This refines file Data.List.NatAntidiagonal and is further refined by file Data.Finset.NatAntidiagonal. "}

Multiset.Nat.antidiagonal definition

(n : ℕ) : Multiset (ℕ × ℕ)

Full source

/-- The antidiagonal of a natural number `n` is
    the multiset of pairs `(i, j)` such that `i + j = n`. -/
def antidiagonal (n : ℕ) : Multiset (ℕℕ × ℕ) :=
  List.Nat.antidiagonal n

Antidiagonal of a natural number as a multiset

Informal description

For a natural number $ n $, the antidiagonal is the multiset of pairs $(i, j)$ of natural numbers such that $ i + j = n $. Specifically, it consists of the pairs $(0, n), (1, n-1), \ldots, (n, 0)$ with multiplicity one for each pair.

Multiset.Nat.mem_antidiagonal theorem

{n : ℕ} {x : ℕ × ℕ} : x ∈ antidiagonal n ↔ x.1 + x.2 = n

Full source

/-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`. -/
@[simp]
theorem mem_antidiagonal {n : ℕ} {x : ℕℕ × ℕ} : x ∈ antidiagonal nx ∈ antidiagonal n ↔ x.1 + x.2 = n := by
  rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]

Membership in Natural Number Antidiagonal Multiset: $(i, j) \in \text{antidiagonal}(n) \leftrightarrow i + j = n$

Informal description

For any natural number $n$ and any pair of natural numbers $(i, j)$, the pair $(i, j)$ belongs to the antidiagonal multiset of $n$ if and only if $i + j = n$.

Multiset.Nat.card_antidiagonal theorem

(n : ℕ) : card (antidiagonal n) = n + 1

Full source

/-- The cardinality of the antidiagonal of `n` is `n+1`. -/
@[simp]
theorem card_antidiagonal (n : ℕ) : card (antidiagonal n) = n + 1 := by
  rw [antidiagonal, coe_card, List.Nat.length_antidiagonal]

Cardinality of Antidiagonal Multiset: $|\text{antidiagonal}(n)| = n + 1$

Informal description

For any natural number $n$, the cardinality of the antidiagonal multiset (consisting of pairs $(i,j)$ with $i + j = n$) is $n + 1$.

Multiset.Nat.antidiagonal_zero theorem

: antidiagonal 0 = {(0, 0)}

Full source

/-- The antidiagonal of `0` is the list `[(0, 0)]` -/
@[simp]
theorem antidiagonal_zero : antidiagonal 0 = {(0, 0)} :=
  rfl

Antidiagonal of Zero: $\text{antidiagonal}(0) = \{(0, 0)\}$

Informal description

The antidiagonal multiset for the natural number $0$ is the singleton multiset containing only the pair $(0, 0)$, i.e., $\text{antidiagonal}(0) = \{(0, 0)\}$.

Multiset.Nat.nodup_antidiagonal theorem

(n : ℕ) : Nodup (antidiagonal n)

Full source

/-- The antidiagonal of `n` does not contain duplicate entries. -/
@[simp]
theorem nodup_antidiagonal (n : ℕ) : Nodup (antidiagonal n) :=
  coe_nodup.2 <| List.Nat.nodup_antidiagonal n

Antidiagonal Multiset is Duplicate-Free for Natural Numbers

Informal description

For any natural number $n$, the multiset $\text{antidiagonal}(n)$ consisting of pairs $(i,j)$ with $i + j = n$ contains no duplicate elements.

Multiset.Nat.antidiagonal_succ theorem

{n : ℕ} : antidiagonal (n + 1) = (0, n + 1) ::ₘ (antidiagonal n).map (Prod.map Nat.succ id)

Full source

@[simp]
theorem antidiagonal_succ {n : ℕ} :
    antidiagonal (n + 1) = (0, n + 1)(0, n + 1) ::ₘ (antidiagonal n).map (Prod.map Nat.succ id) := by
  simp only [antidiagonal, List.Nat.antidiagonal_succ, map_coe, cons_coe]

Recursive construction of the antidiagonal multiset: $\text{antidiagonal}(n+1) = (0, n+1) \cup \{(i+1, j)\}_{(i,j) \in \text{antidiagonal}(n)}$

Informal description

For any natural number $n$, the multiset antidiagonal of $n+1$ is obtained by adding the pair $(0, n+1)$ to the multiset formed by incrementing the first component of each pair in the antidiagonal of $n$. In other words: \[ \text{antidiagonal}(n+1) = \{(0, n+1)\} \cup \{(i+1, j) \mid (i, j) \in \text{antidiagonal}(n)\} \]

Multiset.Nat.antidiagonal_succ' theorem

{n : ℕ} : antidiagonal (n + 1) = (n + 1, 0) ::ₘ (antidiagonal n).map (Prod.map id Nat.succ)

Full source

theorem antidiagonal_succ' {n : ℕ} :
    antidiagonal (n + 1) = (n + 1, 0)(n + 1, 0) ::ₘ (antidiagonal n).map (Prod.map id Nat.succ) := by
  rw [antidiagonal, List.Nat.antidiagonal_succ', ← coe_add, Multiset.add_comm, antidiagonal,
    map_coe, coe_add, List.singleton_append, cons_coe]

Recursive construction of antidiagonal multiset via right successor: $\text{antidiagonal}(n+1) = \{(n+1, 0)\} \cup \{(i, j+1)\}_{(i,j) \in \text{antidiagonal}(n)}$

Informal description

For any natural number $n$, the antidiagonal multiset for $n+1$ is equal to the multiset obtained by inserting the pair $(n+1, 0)$ into the multiset formed by applying the function $(i, j) \mapsto (i, j+1)$ to each pair in the antidiagonal multiset for $n$. In symbols: \[ \text{antidiagonal}(n+1) = \{(n+1, 0)\} \cup \{(i, j+1) \mid (i, j) \in \text{antidiagonal}(n)\} \]

Multiset.Nat.antidiagonal_succ_succ' theorem

{n : ℕ} : antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ (antidiagonal n).map (Prod.map Nat.succ Nat.succ)

Full source

theorem antidiagonal_succ_succ' {n : ℕ} :
    antidiagonal (n + 2) =
      (0, n + 2)(0, n + 2) ::ₘ (n + 2, 0) ::ₘ (antidiagonal n).map (Prod.map Nat.succ Nat.succ) := by
  rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod.map_apply]
  rfl

Recursive Construction of Antidiagonal Multiset for $n+2$ via Double Successor

Informal description

For any natural number $n$, the antidiagonal multiset for $n+2$ is equal to the multiset obtained by inserting the pairs $(0, n+2)$ and $(n+2, 0)$ into the multiset formed by applying the function $(i, j) \mapsto (i+1, j+1)$ to each pair in the antidiagonal multiset for $n$. In symbols: \[ \text{antidiagonal}(n+2) = \{(0, n+2), (n+2, 0)\} \cup \{(i+1, j+1) \mid (i, j) \in \text{antidiagonal}(n)\} \]

Multiset.Nat.map_swap_antidiagonal theorem

{n : ℕ} : (antidiagonal n).map Prod.swap = antidiagonal n

Full source

theorem map_swap_antidiagonal {n : ℕ} : (antidiagonal n).map Prod.swap = antidiagonal n := by
  rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]

Invariance of Antidiagonal Multiset under Component Swapping

Informal description

For any natural number $n$, the multiset obtained by swapping the components of each pair in the antidiagonal multiset of $n$ is equal to the original antidiagonal multiset. That is, if the antidiagonal multiset consists of pairs $(i, j)$ such that $i + j = n$, then applying the swap operation $(i, j) \mapsto (j, i)$ to each pair yields the same multiset.