seq — Mathlib

English

A sequence of finite kernels (κ_n) such that κ = Kernel.sum(seq κ).

Русский

Последовательность конечных ядер (κ_n) такова, что κ = Kernel.sum(seq κ).

LaTeX

$$Kernel.sum( (seq κ) ) = κ$$

Lean4

/-- A sequence of finite kernels such that `κ = ProbabilityTheory.Kernel.sum (seq κ)`. See
`ProbabilityTheory.Kernel.isFiniteKernel_seq` and `ProbabilityTheory.Kernel.kernel_sum_seq`. -/
noncomputable def seq (κ : Kernel α β) [h : IsSFiniteKernel κ] : ℕ → Kernel α β :=
  h.tsum_finite.choose

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