English
Double product symmetry across a diagonal: product over range n of a two-argument function equals product over another diagonal with swapped arguments.
Русский
Двойное произведение по диагонали имеет симметрию.
LaTeX
$$$$ \\displaystyle \\prod_{m\\in \\mathrm{range}(n)} \\prod_{k\\in \\mathrm{range}(m+1)} f(k,m-k) = \\prod_{m\\in \\mathrm{range}(n)} \\prod_{k\\in \\mathrm{range}(n-m)} f(m,k). $$$$
Lean4
@[to_additive]
theorem prod_range_diag_flip (n : ℕ) (f : ℕ → ℕ → M) :
(∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k)) = ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k :=
by
rw [prod_sigma', prod_sigma']
refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_ <;>
simp +contextual only [mem_sigma, mem_range, lt_tsub_iff_left, Nat.lt_succ_iff, le_add_iff_nonneg_right,
Nat.zero_le, and_true, and_imp, implies_true, Sigma.forall, add_tsub_cancel_of_le, add_tsub_cancel_left]
exact fun a b han hba ↦ lt_of_le_of_lt hba han
