sum_comap_seq — Mathlib

English

If κ is IsSFiniteKernel and g is measurable, then the sum over n of comap (seq κ n) g hg equals comap κ g hg: sum_n comap(seq κ n) g hg = comap κ g hg.

Русский

Если κ—IsSFiniteKernel и g измеримо, то сумма по n от comap (seq κ n) g hg равна comap κ g hg.

LaTeX

$$$ \sum_n \bigl( \operatorname{comap}(\operatorname{seq} \kappa n) g hg \bigr) = \operatorname{comap} \kappa g hg $$$

Lean4

theorem sum_comap_seq (κ : Kernel α β) [IsSFiniteKernel κ] (hg : Measurable g) :
    (Kernel.sum fun n => comap (seq κ n) g hg) = comap κ g hg :=
  by
  ext a s hs
  rw [Kernel.sum_apply, comap_apply' κ hg a s, Measure.sum_apply _ hs, ← measure_sum_seq κ, Measure.sum_apply _ hs]
  simp_rw [comap_apply' _ hg _ s]

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