posterior_boolKernel_apply_true — Mathlib

English

Analogous to the false case, the true value posterior for the boolKernel corresponds to the product of π(true) and the RN-derivative with respect to the posterior kernel.

Русский

Аналогично случаю false, постериор для true в boolKernel равен произведению π(true) на RN-дериватив по постериорному ядру.

LaTeX

$$$$ ∀ x, ((\text{boolKernel } μ ν)†π) x \{\text{true}\} = π\{\text{true}\} \cdot ν rnDeriv (π \bind (Kernel.const 𝓧 μ)) x.$$$$

Lean4

theorem posterior_boolKernel_apply_true (μ ν : Measure 𝓧) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (π : Measure Bool)
    [IsFiniteMeasure π] :
    ∀ᵐ x ∂Kernel.boolKernel μ ν ∘ₘ π,
      ((Kernel.boolKernel μ ν)†π) x { true } = π { true } * ν.rnDeriv (Kernel.boolKernel μ ν ∘ₘ π) x :=
  by
  filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx
  rw [hx]
  simp

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