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, providing an instance enabling Finset.antidiagonal on Nat.

instance Finset.Nat.instHasAntidiagonal : Finset.HasAntidiagonal ℕ

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

Equations

• One or more equations did not get rendered due to their size.

theorem Finset.Nat.antidiagonal_eq_map (n : ℕ) : Finset.antidiagonal n = Finset.map { toFun := fun (i : ℕ) => (i, n - i), inj' := (_ : ∀ (x x_1 : ℕ), (fun (i : ℕ) => (i, n - i)) x = (fun (i : ℕ) => (i, n - i)) x_1 → ((fun (i : ℕ) => (i, n - i)) x).1 = ((fun (i : ℕ) => (i, n - i)) x_1).1) } (Finset.range (n + 1))

theorem Finset.Nat.antidiagonal_eq_map' (n : ℕ) : Finset.antidiagonal n = Finset.map { toFun := fun (i : ℕ) => (n - i, i), inj' := (_ : ∀ (x x_1 : ℕ), (fun (i : ℕ) => (n - i, i)) x = (fun (i : ℕ) => (n - i, i)) x_1 → ((fun (i : ℕ) => (n - i, i)) x).2 = ((fun (i : ℕ) => (n - i, i)) x_1).2) } (Finset.range (n + 1))

theorem Finset.Nat.antidiagonal_eq_image (n : ℕ) : Finset.antidiagonal n = Finset.image (fun (i : ℕ) => (i, n - i)) (Finset.range (n + 1))

theorem Finset.Nat.antidiagonal_eq_image' (n : ℕ) : Finset.antidiagonal n = Finset.image (fun (i : ℕ) => (n - i, i)) (Finset.range (n + 1))

@[simp]

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

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

@[simp]

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

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

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

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

theorem Finset.Nat.antidiagonal_succ_succ' {n : ℕ} : Finset.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.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.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.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.antidiagonal n)))

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

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

@[simp]

theorem Finset.Nat.antidiagonal_filter_snd_le_of_le {n : ℕ} {k : ℕ} (h : k ≤ n) : Finset.filter (fun (a : ℕ × ℕ) => a.2 ≤ k) (Finset.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.antidiagonal k)

@[simp]

theorem Finset.Nat.antidiagonal_filter_fst_le_of_le {n : ℕ} {k : ℕ} (h : k ≤ n) : Finset.filter (fun (a : ℕ × ℕ) => a.1 ≤ k) (Finset.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.antidiagonal k)

@[simp]

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

@[simp]

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

@[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.antidiagonal n }), ↑((Finset.Nat.antidiagonalEquivFin n) x) = x.1.1

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

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

Equations

• One or more equations did not get rendered due to their size.