absolutelyContinuous_posterior — Mathlib

English

Posterior relative to swap is absolutely continuous with respect to μ once more, under the same hypotheses.

Русский

Постериор, связанный со swap, снова абсолюто непрерывно относительно μ при тех же предпосылках.

LaTeX

$$$\\forall ν, ((κ ∘ μ) ⊗ ν) ≪ μ \\Rightarrow (κ†μ) \\text{ абсл. непрерывно по } μ$$$

Lean4

theorem absolutelyContinuous_posterior {ν : Measure 𝓧} [SFinite ν] (h_ac : ∀ᵐ ω ∂μ, κ ω ≪ ν) :
    ∀ᵐ b ∂(κ ∘ₘ μ), (κ†μ) b ≪ μ :=
  by
  suffices (κ ∘ₘ μ) ⊗ₘ (κ†μ) ≪ ν.prod μ by
    rw [← Measure.compProd_const] at this
    simpa using this.kernel_of_compProd
  suffices μ ⊗ₘ κ ≪ μ.prod ν by
    rw [compProd_posterior_eq_map_swap, ← Measure.prod_swap]
    exact this.map measurable_swap
  rw [← Measure.compProd_const]
  refine Measure.AbsolutelyContinuous.compProd_right ?_
  simpa

Похожие утверждения