sum_comm — Mathlib

English

For Countable ι, κ: ι → ι → Kernel α β, kernels commute under double sum: sum_n (sum_k (κ n k)) = sum_m (sum_n (κ n m)).

Русский

Для счётного ι сумма по двум индексам обходится в любом порядке: сумма по n затем по m равна сумме по m затем по n.

LaTeX

$$$[Countable \\\\iota] \\\\forall κ : \\\\iota \\\\rightarrow \\\\iota \\\\rightarrow Kernel(\\\\alpha, \\\\beta), \\\\text{Eq }(Kernel.sum (fun n => Kernel.sum (κ n))) (Kernel.sum (fun m => Kernel.sum (fun n => κ n m)))$$$

Lean4

theorem sum_comm [Countable ι] (κ : ι → ι → Kernel α β) :
    (Kernel.sum fun n => Kernel.sum (κ n)) = Kernel.sum fun m => Kernel.sum fun n => κ n m := by ext a s;
  simp_rw [sum_apply]; rw [Measure.sum_comm]

Похожие утверждения