English
For a two-valued kernel boolKernel, the posterior at the false value equals the product of π(false) and the RN-derivative with respect to the resulting posterior measure.
Русский
Для двоичного ядра boolKernel постериор при значении false равен произведению π(false) на RN-дериватив по соответствующей постериорной мере.
LaTeX
$$$$ \forall x, ((\text{boolKernel } μ ν)†π) x \{\text{false}\} = π\{\text{false}\} \cdot μ rnDeriv (π \bind (Kernel.const 𝓧 μ)) x.$$$$
Lean4
theorem posterior_boolKernel_apply_false (μ ν : Measure 𝓧) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (π : Measure Bool)
[IsFiniteMeasure π] :
∀ᵐ x ∂Kernel.boolKernel μ ν ∘ₘ π,
((Kernel.boolKernel μ ν)†π) x { false } = π { false } * μ.rnDeriv (Kernel.boolKernel μ ν ∘ₘ π) x :=
by
filter_upwards [posterior_eq_withDensity_of_countable (Kernel.boolKernel μ ν) π] with x hx
rw [hx]
simp
