Mathlib.Algebra.BigOperators.NatAntidiagonal

Finset.Nat.prod_antidiagonal_succ theorem

 {n : ℕ} {f : ℕ × ℕ → M} : (∏ p ∈ antidiagonal (n + 1), f p) = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Full source

theorem prod_antidiagonal_succ {n : ℕ} {f : ℕℕ × ℕ → M} :
    (∏ p ∈ antidiagonal (n + 1), f p)
      = f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2) := by
  rw [antidiagonal_succ, prod_cons, prod_map]; rfl

Product over Antidiagonal Recursion: $\prod_{\text{antidiagonal}(n+1)} f = f(0,n+1) \cdot \prod_{\text{antidiagonal}(n)} f(i+1,j)$

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \times \mathbb{N} \to M$ be a function. For any natural number $n$, the product of $f$ over the antidiagonal set of $n+1$ satisfies: \[ \prod_{(i,j) \in \text{antidiagonal}(n+1)} f(i,j) = f(0, n+1) \cdot \prod_{(i,j) \in \text{antidiagonal}(n)} f(i+1, j) \] where $\text{antidiagonal}(k)$ denotes the finite set of pairs $(i,j)$ of natural numbers such that $i + j = k$.

Finset.Nat.sum_antidiagonal_succ theorem

 {n : ℕ} {f : ℕ × ℕ → N} : (∑ p ∈ antidiagonal (n + 1), f p) = f (0, n + 1) + ∑ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Full source

theorem sum_antidiagonal_succ {n : ℕ} {f : ℕℕ × ℕ → N} :
    (∑ p ∈ antidiagonal (n + 1), f p) = f (0, n + 1) + ∑ p ∈ antidiagonal n, f (p.1 + 1, p.2) :=
  @prod_antidiagonal_succ (Multiplicative N) _ _ _

Sum over Antidiagonal Recursion: $\sum_{\text{antidiagonal}(n+1)} f = f(0,n+1) + \sum_{\text{antidiagonal}(n)} f(i+1,j)$

Informal description

Let $N$ be an additive commutative monoid and $f : \mathbb{N} \times \mathbb{N} \to N$ be a function. For any natural number $n$, the sum of $f$ over the antidiagonal set of $n+1$ satisfies: \[ \sum_{(i,j) \in \text{antidiagonal}(n+1)} f(i,j) = f(0, n+1) + \sum_{(i,j) \in \text{antidiagonal}(n)} f(i+1, j), \] where $\text{antidiagonal}(k)$ denotes the finite set of pairs $(i,j)$ of natural numbers such that $i + j = k$.

Finset.Nat.prod_antidiagonal_swap theorem

{n : ℕ} {f : ℕ × ℕ → M} : ∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p

Full source

@[to_additive]
theorem prod_antidiagonal_swap {n : ℕ} {f : ℕℕ × ℕ → M} :
    ∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p := by
  conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]
  rfl

Product over Antidiagonal is Invariant under Pair Swapping

Informal description

For any natural number $n$ and any function $f : \mathbb{N} \times \mathbb{N} \to M$ where $M$ is a commutative monoid, the product of $f$ evaluated at the swapped pairs $(j, i)$ over all pairs $(i, j)$ in the antidiagonal of $n$ is equal to the product of $f$ evaluated at the original pairs $(i, j)$ over the same antidiagonal. That is, \[ \prod_{(i,j) \in \text{antidiagonal}(n)} f(j, i) = \prod_{(i,j) \in \text{antidiagonal}(n)} f(i, j). \]

Finset.Nat.prod_antidiagonal_succ' theorem

 {n : ℕ} {f : ℕ × ℕ → M} : (∏ p ∈ antidiagonal (n + 1), f p) = f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Full source

theorem prod_antidiagonal_succ' {n : ℕ} {f : ℕℕ × ℕ → M} : (∏ p ∈ antidiagonal (n + 1), f p) =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1) := by
  rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap]
  rfl

Product over Antidiagonal Recursion: $\prod_{\text{antidiagonal}(n+1)} f = f(n+1,0) \cdot \prod_{\text{antidiagonal}(n)} f(i,j+1)$

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \times \mathbb{N} \to M$ be a function. For any natural number $n$, the product of $f$ over the antidiagonal set of $n+1$ satisfies: \[ \prod_{(i,j) \in \text{antidiagonal}(n+1)} f(i,j) = f(n+1, 0) \cdot \prod_{(i,j) \in \text{antidiagonal}(n)} f(i, j+1), \] where $\text{antidiagonal}(k)$ denotes the finite set of pairs $(i,j)$ of natural numbers such that $i + j = k$.

Finset.Nat.sum_antidiagonal_succ' theorem

 {n : ℕ} {f : ℕ × ℕ → N} : (∑ p ∈ antidiagonal (n + 1), f p) = f (n + 1, 0) + ∑ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Full source

theorem sum_antidiagonal_succ' {n : ℕ} {f : ℕℕ × ℕ → N} :
    (∑ p ∈ antidiagonal (n + 1), f p) = f (n + 1, 0) + ∑ p ∈ antidiagonal n, f (p.1, p.2 + 1) :=
  @prod_antidiagonal_succ' (Multiplicative N) _ _ _

Sum over Antidiagonal Recursion: $\sum_{\text{antidiagonal}(n+1)} f = f(n+1,0) + \sum_{\text{antidiagonal}(n)} f(i,j+1)$

Informal description

For any natural number $n$ and any function $f : \mathbb{N} \times \mathbb{N} \to N$ where $N$ is an additive commutative monoid, the sum of $f$ over the antidiagonal set of $n+1$ satisfies: \[ \sum_{(i,j) \in \text{antidiagonal}(n+1)} f(i,j) = f(n+1, 0) + \sum_{(i,j) \in \text{antidiagonal}(n)} f(i, j+1), \] where $\text{antidiagonal}(k)$ denotes the finite set of pairs $(i,j)$ of natural numbers such that $i + j = k$.

Finset.Nat.prod_antidiagonal_subst theorem

{n : ℕ} {f : ℕ × ℕ → ℕ → M} : ∏ p ∈ antidiagonal n, f p n = ∏ p ∈ antidiagonal n, f p (p.1 + p.2)

Full source

@[to_additive]
theorem prod_antidiagonal_subst {n : ℕ} {f : ℕℕ × ℕ → ℕ → M} :
    ∏ p ∈ antidiagonal n, f p n = ∏ p ∈ antidiagonal n, f p (p.1 + p.2) :=
  prod_congr rfl fun p hp ↦ by rw [mem_antidiagonal.mp hp]

Product over Antidiagonal with Substituted Argument: $\prod_{i+j=n} f(i,j)(n) = \prod_{i+j=n} f(i,j)(i+j)$

Informal description

Let $n$ be a natural number and $f : \mathbb{N} \times \mathbb{N} \to \mathbb{N} \to M$ be a function where $M$ is a commutative monoid. Then the product of $f(p)(n)$ over all pairs $p = (i,j)$ in the antidiagonal of $n$ (i.e., pairs where $i + j = n$) is equal to the product of $f(p)(i + j)$ over the same pairs $p$.

Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk theorem

 {M : Type*} [CommMonoid M] (f : ℕ × ℕ → M) (n : ℕ) : ∏ ij ∈ antidiagonal n, f ij = ∏ k ∈ range n.succ, f (k, n - k)

Full source

@[to_additive]
theorem prod_antidiagonal_eq_prod_range_succ_mk {M : Type*} [CommMonoid M] (f : ℕℕ × ℕ → M)
    (n : ℕ) : ∏ ij ∈ antidiagonal n, f ij = ∏ k ∈ range n.succ, f (k, n - k) :=
  Finset.prod_map (range n.succ) ⟨fun i ↦ (i, n - i), fun _ _ h ↦ (Prod.mk.inj h).1⟩ f

Product over Antidiagonal Equals Product over Range

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \times \mathbb{N} \to M$ be a function. For any natural number $n$, the product of $f$ over the antidiagonal of $n$ is equal to the product of $f(k, n - k)$ over $k$ in the range $\{0, \ldots, n\}$. That is, \[ \prod_{(i,j) \in \text{antidiagonal}(n)} f(i,j) = \prod_{k=0}^n f(k, n - k). \]

Finset.Nat.prod_antidiagonal_eq_prod_range_succ theorem

 {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) :
  ∏ ij ∈ antidiagonal n, f ij.1 ij.2 = ∏ k ∈ range n.succ, f k (n - k)

Full source

/-- This lemma matches more generally than `Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk` when
using `rw ← `. -/
@[to_additive "This lemma matches more generally than
`Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk` when using `rw ← `."]
theorem prod_antidiagonal_eq_prod_range_succ {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) :
    ∏ ij ∈ antidiagonal n, f ij.1 ij.2 = ∏ k ∈ range n.succ, f k (n - k) :=
  prod_antidiagonal_eq_prod_range_succ_mk _ _

Product over Antidiagonal as Iterated Product over Range

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \to \mathbb{N} \to M$ be a function. For any natural number $n$, the product of $f$ over the antidiagonal of $n$ is equal to the product of $f(k)(n - k)$ over $k$ in the range $\{0, \ldots, n\}$. That is, \[ \prod_{(i,j) \in \text{antidiagonal}(n)} f(i)(j) = \prod_{k=0}^n f(k)(n - k). \]