Antidiagonals in ℕ × ℕ as finsets

This file defines the antidiagonals of ℕ × ℕ as finsets: the n-th antidiagonal is the finset 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 files Data.List.NatAntidiagonal and Data.Multiset.NatAntidiagonal.

def Finset.Nat.antidiagonal (n : ℕ) : Finset (ℕ × ℕ)

The antidiagonal of a natural number n is the finset of pairs (i, j) such that i + j = n.

@[simp]

theorem Finset.Nat.mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ Finset.Nat.antidiagonal n ↔ x.fst + x.snd = n

A pair (i, j) is contained in the antidiagonal of n if and only if i + j = n.

@[simp]

theorem Finset.Nat.card_antidiagonal (n : ℕ) : Finset.card (Finset.Nat.antidiagonal n) = n + 1

The cardinality of the antidiagonal of n is n + 1.

@[simp]

theorem Finset.Nat.antidiagonal_zero : Finset.Nat.antidiagonal 0 = {(0, 0)}

The antidiagonal of 0 is the list [(0, 0)]

theorem Finset.Nat.antidiagonal_succ (n : ℕ) : Finset.Nat.antidiagonal (n + 1) = Finset.cons (0, n + 1) (Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl ℕ)) (Finset.Nat.antidiagonal n)) (_ : ¬(0, n + 1) ∈ Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl ℕ)) (Finset.Nat.antidiagonal n))

theorem Finset.Nat.antidiagonal_succ' (n : ℕ) : Finset.Nat.antidiagonal (n + 1) = Finset.cons (n + 1, 0) (Finset.map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.Nat.antidiagonal n)) (_ : ¬(n + 1, 0) ∈ Finset.map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.Nat.antidiagonal n))

theorem Finset.Nat.antidiagonal_succ_succ' {n : ℕ} : Finset.Nat.antidiagonal (n + 2) = Finset.cons (0, n + 2) (Finset.cons (n + 2, 0) (Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.Nat.antidiagonal n)) (_ : ¬(n + 2, 0) ∈ Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.Nat.antidiagonal n))) (_ : ¬(0, n + 2) ∈ Finset.cons (n + 2, 0) (Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.Nat.antidiagonal n)) (_ : ¬(n + 2, 0) ∈ Finset.map (Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.Nat.antidiagonal n)))

@[simp]

theorem Finset.Nat.map_swap_antidiagonal {n : ℕ} : Finset.map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (Finset.Nat.antidiagonal n) = Finset.Nat.antidiagonal n

See also Finset.map.map_prodComm_antidiagonal.

@[simp]

theorem Finset.Nat.map_prodComm_antidiagonal {n : ℕ} : Finset.map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (Finset.Nat.antidiagonal n) = Finset.Nat.antidiagonal n

theorem Finset.Nat.antidiagonal_congr {n : ℕ} {p : ℕ × ℕ} {q : ℕ × ℕ} (hp : p ∈ Finset.Nat.antidiagonal n) (hq : q ∈ Finset.Nat.antidiagonal n) : p = q ↔ p.fst = q.fst

A point in the antidiagonal is determined by its first co-ordinate.

theorem Finset.Nat.antidiagonal_subtype_ext {n : ℕ} {p : { x // x ∈ Finset.Nat.antidiagonal n }} {q : { x // x ∈ Finset.Nat.antidiagonal n }} (h : (↑p).fst = (↑q).fst) : p = q

A point in the antidiagonal is determined by its first co-ordinate (subtype version of antidiagonal_congr). This lemma is used by the ext tactic.

theorem Finset.Nat.antidiagonal.fst_le {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ Finset.Nat.antidiagonal n) : kl.fst ≤ n

theorem Finset.Nat.antidiagonal.fst_lt {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ Finset.Nat.antidiagonal n) : kl.fst < n + 1

theorem Finset.Nat.antidiagonal.snd_le {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ Finset.Nat.antidiagonal n) : kl.snd ≤ n

theorem Finset.Nat.antidiagonal.snd_lt {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ Finset.Nat.antidiagonal n) : kl.snd < n + 1

theorem Finset.Nat.filter_fst_eq_antidiagonal (n : ℕ) (m : ℕ) : Finset.filter (fun x => x.fst = m) (Finset.Nat.antidiagonal n) = if m ≤ n then {(m, n - m)} else ∅

theorem Finset.Nat.filter_snd_eq_antidiagonal (n : ℕ) (m : ℕ) : Finset.filter (fun x => x.snd = m) (Finset.Nat.antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅

@[simp]

theorem Finset.Nat.antidiagonal_filter_snd_le_of_le {n : ℕ} {k : ℕ} (h : k ≤ n) : Finset.filter (fun a => a.snd ≤ k) (Finset.Nat.antidiagonal n) = Finset.map (Function.Embedding.prodMap { toFun := fun x => x + (n - k), inj' := (_ : Function.Injective fun x => x + (n - k)) } (Function.Embedding.refl ℕ)) (Finset.Nat.antidiagonal k)

@[simp]

theorem Finset.Nat.antidiagonal_filter_fst_le_of_le {n : ℕ} {k : ℕ} (h : k ≤ n) : Finset.filter (fun a => a.fst ≤ k) (Finset.Nat.antidiagonal n) = Finset.map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := fun x => x + (n - k), inj' := (_ : Function.Injective fun x => x + (n - k)) }) (Finset.Nat.antidiagonal k)

@[simp]

theorem Finset.Nat.antidiagonal_filter_le_fst_of_le {n : ℕ} {k : ℕ} (h : k ≤ n) : Finset.filter (fun a => k ≤ a.fst) (Finset.Nat.antidiagonal n) = Finset.map (Function.Embedding.prodMap { toFun := fun x => x + k, inj' := (_ : Function.Injective fun x => x + k) } (Function.Embedding.refl ℕ)) (Finset.Nat.antidiagonal (n - k))

@[simp]

theorem Finset.Nat.antidiagonal_filter_le_snd_of_le {n : ℕ} {k : ℕ} (h : k ≤ n) : Finset.filter (fun a => k ≤ a.snd) (Finset.Nat.antidiagonal n) = Finset.map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := fun x => x + k, inj' := (_ : Function.Injective fun x => x + k) }) (Finset.Nat.antidiagonal (n - k))

@[simp]

theorem Finset.Nat.sigmaAntidiagonalEquivProd_symm_apply_snd_coe (x : ℕ × ℕ) : ↑(↑Finset.Nat.sigmaAntidiagonalEquivProd.symm x).snd = x

@[simp]

theorem Finset.Nat.sigmaAntidiagonalEquivProd_apply (x : (n : ℕ) × { x // x ∈ Finset.Nat.antidiagonal n }) : ↑Finset.Nat.sigmaAntidiagonalEquivProd x = ↑x.snd

@[simp]

theorem Finset.Nat.sigmaAntidiagonalEquivProd_symm_apply_fst (x : ℕ × ℕ) : (↑Finset.Nat.sigmaAntidiagonalEquivProd.symm x).fst = x.fst + x.snd

def Finset.Nat.sigmaAntidiagonalEquivProd : (n : ℕ) × { x // x ∈ Finset.Nat.antidiagonal n } ≃ ℕ × ℕ

The disjoint union of antidiagonals Σ (n : ℕ), antidiagonal n is equivalent to the product ℕ × ℕ. This is such an equivalence, obtained by mapping (n, (k, l)) to (k, l).

@[simp]

theorem Finset.Nat.antidiagonalEquivFin_symm_apply_coe (n : ℕ) : ∀ (x : Fin (n + 1)), ↑(↑(Finset.Nat.antidiagonalEquivFin n).symm x) = (↑x, n - ↑x)

@[simp]

theorem Finset.Nat.antidiagonalEquivFin_apply_val (n : ℕ) : ∀ (x : { x // x ∈ Finset.Nat.antidiagonal n }), ↑(↑(Finset.Nat.antidiagonalEquivFin n) x) = x.1.fst

def Finset.Nat.antidiagonalEquivFin (n : ℕ) : { x // x ∈ Finset.Nat.antidiagonal n } ≃ Fin (n + 1)

The set antidiagonal n is equivalent to Fin (n+1), via the first projection. -