sum_map_seq — Mathlib

English

If κ is IsSFiniteKernel, then sum over n of map (seq κ n) f equals map κ f when f is measurable.

Русский

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

LaTeX

$$$$ \\sum_n (\\text{map} (\\text{seq } \\kappa n) f) = \\text{map } \\kappa f. $$$$

Lean4

theorem sum_map_seq (κ : Kernel α β) [IsSFiniteKernel κ] (f : β → γ) :
    (Kernel.sum fun n => map (seq κ n) f) = map κ f :=
  by
  by_cases hf : Measurable f
  · ext a s hs
    rw [Kernel.sum_apply, map_apply' κ hf a hs, Measure.sum_apply _ hs, ← measure_sum_seq κ,
      Measure.sum_apply _ (hf hs)]
    simp_rw [map_apply' _ hf _ hs]
  · simp [map_of_not_measurable _ hf]

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