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
.
The antidiagonal of a natural number n
is
the finset of pairs (i, j)
such that i + j = n
.
Equations
- Finset.Nat.antidiagonal n = { val := Multiset.Nat.antidiagonal n, nodup := (_ : Multiset.Nodup (Multiset.Nat.antidiagonal n)) }
@[simp]
The cardinality of the antidiagonal of n
is n + 1
.
@[simp]
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)))
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
theorem
Finset.Nat.antidiagonal.fst_le
{n : ℕ}
{kl : ℕ × ℕ}
(hlk : kl ∈ Finset.Nat.antidiagonal n)
:
kl.fst ≤ n
theorem
Finset.Nat.antidiagonal.snd_le
{n : ℕ}
{kl : ℕ × ℕ}
(hlk : kl ∈ Finset.Nat.antidiagonal n)
:
kl.snd ≤ n
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.sigmaAntidiagonalEquivProd_symm_apply_snd_coe
(x : ℕ × ℕ)
:
↑(↑(Equiv.symm Finset.Nat.sigmaAntidiagonalEquivProd) x).snd = x
@[simp]
theorem
Finset.Nat.sigmaAntidiagonalEquivProd_symm_apply_fst
(x : ℕ × ℕ)
:
(↑(Equiv.symm Finset.Nat.sigmaAntidiagonalEquivProd) x).fst = x.fst + x.snd
@[simp]
theorem
Finset.Nat.sigmaAntidiagonalEquivProd_apply
(x : (n : ℕ) × { x // x ∈ Finset.Nat.antidiagonal n })
:
↑Finset.Nat.sigmaAntidiagonalEquivProd x = ↑x.snd
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)
.
Equations
- One or more equations did not get rendered due to their size.