English
If κ ω ≪ κ ∘ₘ μ for μ-almost every ω, then for almost every x with respect to κ ∘ₘ μ, the posterior κ†μ at x equals μ restricted by density κ.rnDeriv (κ ∘ₘ μ) ω x.
Русский
Если для почти всех ω выполняется κ ω ≪ κ ∘ₘ μ, то для почти всех x по κ ∘ₘ μ постериор κ†μ (при x) равен μ с плотностью κ.rnDeriv (κ ∘ₘ μ) ω x.
LaTeX
$$$$ (κ†μ) x = μ.withDensity (\omega ↦ κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) ω x). $$$$
Lean4
/-- If `κ ω ≪ κ ∘ₘ μ` for `μ`-almost every `ω`, then for `κ ∘ₘ μ`-almost every `x`,
`κ†μ x = μ.withDensity (fun ω ↦ κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) ω x)`.
This is a form of **Bayes' theorem**.
The condition is true for example for countable `Ω`. -/
theorem posterior_eq_withDensity (h_ac : ∀ᵐ ω ∂μ, κ ω ≪ κ ∘ₘ μ) :
∀ᵐ x ∂(κ ∘ₘ μ), (κ†μ) x = μ.withDensity (fun ω ↦ κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) ω x) :=
by
filter_upwards [rnDeriv_posterior_symm h_ac, absolutelyContinuous_posterior h_ac] with x h h_ac'
ext s hs
rw [← Measure.setLIntegral_rnDeriv h_ac', withDensity_apply _ hs]
refine setLIntegral_congr_fun_ae hs ?_
filter_upwards [h, Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ†μ) (η := Kernel.const 𝓧 μ) (a := x)] with ω h h_eq hωs
rw [← h, h_eq, Kernel.const_apply]
