density — Mathlib

English

The density κ ν a x s equals almost surely the limitProcess value along the filtration: density κ ν a x s =limiting density.

Русский

Плотность κ ν a x s равна почти наверное пределу density по фильтрации: density κ ν a x s = limDensity.

LaTeX

$$(κ a x s) =ᵐ[ν a] (countableFiltration γ).limitProcess (fun n x ↦ densityProcess κ ν n a x s) (ν a) x$$

Lean4

/-- Density of the kernel `κ` with respect to `ν`. This is a function `α → γ → Set β → ℝ` which
is measurable on `α × γ` for all measurable sets `s : Set β` and satisfies that
`∫ x in A, density κ ν a x s ∂(ν a) = (κ a).real (A ×ˢ s)` for all measurable `A : Set γ`. -/
noncomputable def density (κ : Kernel α (γ × β)) (ν : Kernel α γ) (a : α) (x : γ) (s : Set β) : ℝ :=
  limsup (fun n ↦ densityProcess κ ν n a x s) atTop

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