English
If κ ω ≪ ν for almost every ω with ν a fixed measure, then (κ ∘ μ) ⊗ (κ†μ) ≪ ν × μ, and posterior kernel is absolutely continuous w.r.t. μ.
Русский
Если κ ω ≪ ν почти для каждого ω и ν фиксирована, то (κ ∘ μ) ⊗ (κ†μ) ≪ ν × μ и постериорный ядро абсолютноспринято относительно μ.
LaTeX
$$$ (κ ∘ μ) ⊗ (κ†μ) ≪ ν \\times μ \\Rightarrow (μ \\bind κ) \\circ κ†μ \\text{ абсолюто непрерывно относительно } μ$$$
Lean4
/-- For a deterministic kernel `κ`, `κ ∘ₖ κ†μ` is `μ.map f`-a.e. equal to the identity kernel. -/
theorem deterministic_comp_posterior [MeasurableSpace.CountablyGenerated 𝓧] {f : Ω → 𝓧} (hf : Measurable f) :
Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ =ᵐ[μ.map f] Kernel.id :=
by
refine Kernel.ae_eq_of_compProd_eq ?_
calc
μ.map f ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
_ = (Kernel.deterministic f hf ∘ₘ μ) ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) := by
rw [Measure.deterministic_comp_eq_map]
_ =
(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ
(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ Kernel.copy 𝓧 ∘ₘ Kernel.deterministic f hf ∘ₘ μ :=
by
rw [Measure.compProd_eq_parallelComp_comp_copy_comp, ← Kernel.parallelComp_id_left_comp_parallelComp, ←
Measure.comp_assoc]
_ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.deterministic f hf ∥ₖ Kernel.id) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
rw [parallelProd_posterior_comp_copy_comp]
_ = (Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]
_ = (Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ := by -- `deterministic` is used here
rw [Measure.comp_assoc, Kernel.deterministic_comp_copy]
_ = μ.map f ⊗ₘ Kernel.id := by
rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc, Measure.deterministic_comp_eq_map]
