English
A refinement of rnDeriv_posterior asserting the a.e. equality of dual rnDeriv expressions in the product measure μ × (μ ∘ₘ κ).
Русский
Уточнение rnDeriv_posterior: a.e. равенство двойственных rnDeriv в произведении μ × (μ ∘ₘ κ).
LaTeX
$$$$\text{ae equality: } (κ†μ) rnDeriv (Kernel.const_μ) p.2 p.1 = κ rnDeriv (Kernel.const_(κ ∘ₘ μ)) p.1 p.2 \text{ a.e. } (μ.prod (μ ∘ₘ κ)).$$$$
Lean4
theorem posterior_eq_withDensity_of_countable {Ω : Type*} [Countable Ω] [MeasurableSpace Ω] [Nonempty Ω]
[StandardBorelSpace Ω] (κ : Kernel Ω 𝓧) [IsFiniteKernel κ] (μ : Measure Ω) [IsFiniteMeasure μ] :
∀ᵐ x ∂(κ ∘ₘ μ), (κ†μ) x = μ.withDensity (fun ω ↦ (κ ω).rnDeriv (κ ∘ₘ μ) x) :=
by
have h_rnDeriv ω := Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := Kernel.const Ω (κ ∘ₘ μ)) (a := ω)
simp only [Filter.EventuallyEq, Kernel.const_apply] at h_rnDeriv
rw [← ae_all_iff] at h_rnDeriv
filter_upwards [posterior_eq_withDensity Measure.absolutelyContinuous_comp_of_countable, h_rnDeriv] with x hx hx_all
simp_rw [hx, hx_all]
