English
The order of conditioning in the posterior can be swapped, yielding the same RN-derivative relations, i.e., symmetry of the rnDeriv expressions with respect to ω and x when measuring posterior kernels.
Русский
Обмен условностей в постериоре приводит к той же RN-деривативной зависимости, т.е. симметрия rnDeriv в отношении переменных ω и x.
LaTeX
$$$$\forall^{\,\text{ae}} ω\partial μ: \forall x, \text{rnDeriv relations are symmetric: } (κ†μ) rnDeriv κ μ (x, ω) = κ rnDeriv κ (κ ∘ μ) (ω, x).$$$$
Lean4
theorem rnDeriv_posterior_symm (h_ac : ∀ᵐ ω ∂μ, κ ω ≪ κ ∘ₘ μ) :
∀ᵐ x ∂(κ ∘ₘ μ), ∀ᵐ ω ∂μ, (κ†μ).rnDeriv (Kernel.const _ μ) x ω = κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) ω x :=
by
rw [Measure.ae_ae_comm]
· exact rnDeriv_posterior h_ac
· exact measurableSet_eq_fun' (by fun_prop) (by fun_prop)
