English
The Radon-Nikodym derivative of the posterior with respect to the product measure μ × (μ ∘ κ) matches almost everywhere with the product structure (rectangular decomposition) on Ω × 𝓧, signifying a product formula for rn-derivatives.
Русский
Пределение радона никодя для постериора относительно произведения μ × (κ∘μ) совпадает почти всюду с соответствующей прямоугольной декомпозицией на Ω × 𝓧, т.е. есть формула произведения для rnDeriv.
LaTeX
$$$$ (κ^{†}μ)\; rnDeriv\; (Kernel.const\; μ) = κ \otimes (κ∘μ) \, a.e. $$$$
Lean4
theorem rnDeriv_posterior_ae_prod (h_ac : ∀ᵐ ω ∂μ, κ ω ≪ κ ∘ₘ μ) :
∀ᵐ p ∂(μ.prod (κ ∘ₘ μ)), (κ†μ).rnDeriv (Kernel.const _ μ) p.2 p.1 = κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) p.1 p.2 :=
by
-- We prove the a.e. equality by showing that integrals on the π-system of rectangles are equal.
-- First, the integral of the left-hand side on `s ×ˢ t` is `(μ ⊗ₘ κ) (s ×ˢ t)`, which we prove
-- by showing that it's equal to `((κ ∘ₘ μ) ⊗ κ†μ) (t ×ˢ s)` and using the main property of the
-- posterior.
have h1 {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t) :
∫⁻ x in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const _ μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t) :=
by
rw [setLIntegral_prod_symm _ (by fun_prop), ← swap_compProd_posterior, Measure.swap_comp,
Measure.map_apply measurable_swap (hs.prod ht), Set.preimage_swap_prod, Measure.compProd_apply_prod ht hs]
refine lintegral_congr_ae <| ae_restrict_of_ae ?_
filter_upwards [absolutelyContinuous_posterior h_ac] with x h_ac'
change ∫⁻ ω in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω ∂(Kernel.const 𝓧 μ x) = _
rw [Kernel.setLIntegral_rnDeriv h_ac' hs]
have h2 {s : Set Ω} {t : Set 𝓧} (hs : MeasurableSet s) (ht : MeasurableSet t) :
-- Second, the integral of the right-hand side on `s ×ˢ t` is `(μ ⊗ₘ κ) (s ×ˢ t)`.
∫⁻ x in s ×ˢ t, κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) x.1 x.2 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t) :=
by
rw [setLIntegral_prod _ (by fun_prop), Measure.compProd_apply_prod hs ht]
refine lintegral_congr_ae <| ae_restrict_of_ae ?_
filter_upwards [h_ac] with ω h_ac
change ∫⁻ x in t, κ.rnDeriv (Kernel.const Ω (κ ∘ₘ μ)) ω x ∂(Kernel.const Ω (κ ∘ₘ μ) ω) = _
rw [Kernel.setLIntegral_rnDeriv h_ac ht]
-- We extend from the π-system to the σ-algebra.
refine ae_eq_of_setLIntegral_prod_eq (by fun_prop) (by fun_prop) ?_ ?_
· refine ne_of_lt ?_
calc
∫⁻ x, (κ†μ).rnDeriv (Kernel.const _ μ) x.2 x.1 ∂μ.prod (κ ∘ₘ μ)
_ = (μ ⊗ₘ κ) Set.univ := by rw [← setLIntegral_univ, ← Set.univ_prod_univ, h1 .univ .univ]
_ < ⊤ := measure_lt_top _ _
· intro s hs t ht
rw [h1 hs ht, h2 hs ht]
