piecewise — Mathlib

English

If κ and η are IsSFiniteKernel, then the piecewise hs κ η is IsSFiniteKernel.

Русский

Если κ и η — IsSFiniteKernel, то piecewise hs κ η — IsSFiniteKernel.

LaTeX

$$$\\text{IsSFiniteKernel}(\\text{piecewise}(hs,\\kappa,\\eta))$$$

Lean4

protected instance piecewise [IsSFiniteKernel κ] [IsSFiniteKernel η] : IsSFiniteKernel (piecewise hs κ η) :=
  by
  refine ⟨⟨fun n => piecewise hs (seq κ n) (seq η n), inferInstance, ?_⟩⟩
  ext1 a
  simp_rw [sum_apply, Kernel.piecewise_apply]
  split_ifs <;> exact (measure_sum_seq _ a).symm

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