Mathlib.Data.List.NatAntidiagonal

Module docstring

{"# Antidiagonals in ℕ × ℕ as lists

This file defines the antidiagonals of ℕ × ℕ as lists: the n-th antidiagonal is the list 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

Files Data.Multiset.NatAntidiagonal and Data.Finset.NatAntidiagonal successively turn the List definition we have here into Multiset and Finset. "}

List.Nat.antidiagonal definition

(n : ℕ) : List (ℕ × ℕ)

Full source

/-- The antidiagonal of a natural number `n` is the list of pairs `(i, j)` such that `i + j = n`. -/
def antidiagonal (n : ℕ) : List (ℕℕ × ℕ) :=
  (range (n + 1)).map fun i ↦ (i, n - i)

Antidiagonal of a natural number

Informal description

For a natural number $ n $, the antidiagonal is the list 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)$.

List.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_map]; constructor
  · rintro ⟨i, hi, rfl⟩
    rw [mem_range, Nat.lt_succ_iff] at hi
    exact Nat.add_sub_cancel' hi
  · rintro rfl
    refine ⟨x.fst, ?_, ?_⟩
    · rw [mem_range]
      omega
    · exact Prod.ext rfl (by simp only [Nat.add_sub_cancel_left])

Membership in Antidiagonal of Natural Numbers: $(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 of $n$ if and only if $i + j = n$.

List.Nat.length_antidiagonal theorem

(n : ℕ) : (antidiagonal n).length = n + 1

Full source

/-- The length of the antidiagonal of `n` is `n + 1`. -/
@[simp]
theorem length_antidiagonal (n : ℕ) : (antidiagonal n).length = n + 1 := by
  rw [antidiagonal, length_map, length_range]

Length of Antidiagonal List: $\operatorname{length}(\operatorname{antidiagonal}(n)) = n + 1$

Informal description

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

List.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 is Singleton Pair $(0, 0)$

Informal description

The antidiagonal list for the natural number $0$ is the singleton list containing the pair $(0, 0)$, i.e., $\mathrm{antidiagonal}(0) = [(0, 0)]$.

List.Nat.nodup_antidiagonal theorem

(n : ℕ) : Nodup (antidiagonal n)

Full source

/-- The antidiagonal of `n` does not contain duplicate entries. -/
theorem nodup_antidiagonal (n : ℕ) : Nodup (antidiagonal n) :=
  nodup_range.map ((@LeftInverse.injective ℕ (ℕℕ × ℕ) Prod.fst fun i ↦ (i, n - i)) fun _ ↦ rfl)

Antidiagonal List of Natural Numbers is Duplicate-Free

Informal description

For any natural number $n$, the list of pairs $(i, j)$ such that $i + j = n$ contains no duplicate elements.

List.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, range_succ_eq_map, map_cons, Nat.add_succ_sub_one,
    Nat.add_zero, id, eq_self_iff_true, Nat.sub_zero, map_map, Prod.map_apply]
  apply congr rfl (congr rfl _)
  ext; simp

Recursive Construction of Antidiagonal for Successor Natural Number

Informal description

For any natural number $n$, the antidiagonal list for $n+1$ is obtained by prepending the pair $(0, n+1)$ to the list formed by applying the function $(i, j) \mapsto (i+1, j)$ to each element of the antidiagonal list for $n$. In other words, the antidiagonal of $n+1$ is: \[ \text{antidiagonal}(n+1) = (0, n+1) :: \text{map} \big( (i,j) \mapsto (i+1, j) \big) \big( \text{antidiagonal}(n) \big) \]

List.Nat.antidiagonal_succ' theorem

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

Full source

theorem antidiagonal_succ' {n : ℕ} :
    antidiagonal (n + 1) = (antidiagonal n).map (Prod.map id Nat.succ) ++ [(n + 1, 0)] := by
  simp only [antidiagonal, range_succ, Nat.add_sub_cancel_left, map_append, append_assoc,
    Nat.sub_self, singleton_append, map_map, map]
  congr 1
  apply map_congr_left
  simp +contextual [le_of_lt, Nat.sub_add_comm]

Recursive Construction of Antidiagonal via Right Successor and Append

Informal description

For any natural number $n$, the antidiagonal list for $n+1$ is obtained by applying the function $(i, j) \mapsto (i, j+1)$ to each element of the antidiagonal list for $n$ and then appending the pair $(n+1, 0)$. In other words: \[ \text{antidiagonal}(n+1) = \text{map}\big((i,j) \mapsto (i, j+1)\big)\big(\text{antidiagonal}(n)\big) \mathbin{+\!\!+} [(n+1, 0)] \]

List.Nat.antidiagonal_succ_succ' theorem

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

Full source

theorem antidiagonal_succ_succ' {n : ℕ} :
    antidiagonal (n + 2) =
      (0, n + 2)(0, n + 2) :: (antidiagonal n).map (Prod.map Nat.succ Nat.succ) ++ [(n + 2, 0)] := by
  rw [antidiagonal_succ']
  simp only [antidiagonal_succ, map_cons, Prod.map_apply, id_eq, map_map, cons_append, cons.injEq,
    append_cancel_right_eq, true_and]
  ext
  simp

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

Informal description

For any natural number $n$, the antidiagonal list for $n+2$ is obtained by: 1. Prepending the pair $(0, n+2)$ to 2. The list formed by applying the function $(i, j) \mapsto (i+1, j+1)$ to each element of the antidiagonal list for $n$, and then 3. Appending the pair $(n+2, 0)$. In other words: \[ \text{antidiagonal}(n+2) = (0, n+2) :: \text{map}\big((i,j) \mapsto (i+1, j+1)\big)\big(\text{antidiagonal}(n)\big) \mathbin{+\!\!+} [(n+2, 0)] \]

List.Nat.map_swap_antidiagonal theorem

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

Full source

theorem map_swap_antidiagonal {n : ℕ} :
    (antidiagonal n).map Prod.swap = (antidiagonal n).reverse := by
  rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ←
    range_eq_range', map_map]
  apply map_congr_left
  simp +contextual [Nat.sub_sub_self, Nat.lt_succ_iff]

Swapping Components of Antidiagonal Pairs Yields Reverse List

Informal description

For any natural number $n$, the list obtained by swapping the components of each pair in the antidiagonal list of $n$ is equal to the reverse of the original antidiagonal list. That is, if the antidiagonal list is $[(0, n), (1, n-1), \ldots, (n, 0)]$, then applying the swap operation $(i, j) \mapsto (j, i)$ to each pair yields $[(n, 0), (n-1, 1), \ldots, (0, n)]$, which is the reverse of the original list.