absolutelyContinuous_posterior_iff

English

The posterior is absolutely continuous w.r.t. the joint measure iff the pointwise posterior is absolutely continuous w.r.t. the posterior of κ applied to μ, i.e., equivalence between pointwise and almost everywhere conditions for absolute continuity in the Bayes setting.

Русский

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

LaTeX

$$$$\\Big[ \\forall^{\\,\\text{ae}}\, b\\partial(κ\\circ_m μ): (κ^{†}μ) b ≪ μ \\Big] \\iff \\Big[ \\forall^{\\,\\text{ae}}\, ω\\partial μ: κ ω ≪ κ\\circ_m μ \\Big].$$$$

Lean4

theorem absolutelyContinuous_posterior_iff : (∀ᵐ b ∂(κ ∘ₘ μ), (κ†μ) b ≪ μ) ↔ ∀ᵐ ω ∂μ, κ ω ≪ κ ∘ₘ μ :=
  ⟨absolutelyContinuous_of_posterior, absolutelyContinuous_posterior⟩

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