densityProcess_def — Mathlib

English

The densityProcess is defined by the ratio of κ and ν on the corresponding partition sets, converted to a real number.

Русский

DensityProcess задаётся как отношение плотностей κ и ν на соответствующих частичных множествах разбиения, приведённое к вещественному числу.

LaTeX

$$$\text{densityProcess}(\kappa,\nu,n,a,x,s) = \left( \dfrac{\kappa a(\text{countablePartitionSet} n x \times^s s)}{\nu a(\text{countablePartitionSet} n x)} \right)^{\mathrm{toReal}}$$$

Lean4

theorem densityProcess_def (κ : Kernel α (γ × β)) (ν : Kernel α γ) (n : ℕ) (a : α) (s : Set β) :
    (fun t ↦ densityProcess κ ν n a t s) = fun t ↦
      (κ a (countablePartitionSet n t ×ˢ s) / ν a (countablePartitionSet n t)).toReal :=
  rfl

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