English
If κ ω is almost surely absolutely continuous with respect to κ ∘ₘ μ, then κ ω is almost surely absolutely continuous with respect to κ ∘ₘ μ as well in the joint sense, i.e., the posterior operation preserves absolute continuity under suitable finiteness assumptions.
Русский
Если почти наверняка для ω выполняется κ ω ≪ κ ∘ₘ μ, то совместно κ ω ≪ κ ∘ₘ μ сохраняется через постериорную операцию при подходящих ограничениях на конечность.
LaTeX
$$$$\text{If } (\forall^{\,\text{ae}}\,\omega\,\partial\mu)(κ(ω) \ll κ\circ_m μ) \Rightarrow (κ(ω) \ll κ\circ_m μ) \text{ a.e. w.r.t. } μ.$$$$
Lean4
theorem absolutelyContinuous_of_posterior (h_ac : ∀ᵐ b ∂(κ ∘ₘ μ), (κ†μ) b ≪ μ) : ∀ᵐ ω ∂μ, κ ω ≪ κ ∘ₘ μ :=
by
suffices μ ⊗ₘ κ ≪ μ.prod (κ ∘ₘ μ) by
rw [← Measure.compProd_const] at this
simpa using this.kernel_of_compProd
suffices (κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (κ ∘ₘ μ).prod μ
by
rw [← swap_compProd_posterior, ← Measure.prod_swap, Measure.swap_comp]
exact this.map measurable_swap
rw [← Measure.compProd_const]
refine Measure.AbsolutelyContinuous.compProd_right ?_
simpa
