absolutelyContinuous_comp_of_absolutelyContinuous

English

If κ is absolutely continuous with respect to ν for μ-almost every ω, then the kernel composition (κ ∘ η) inherits an absolute continuity relation from κ and η under finite-kernel hypotheses.

Русский

Если κ ≪ ν для μ-почти каждого ω, то композиция ядра (κ ∘ η) наследует отношение абсолютной непрерывности от κ и η при условии конечности ядер.

LaTeX

$$$$\forall^{\,\text{ae}} ω\partial μ: κ ω ≪ ν \quad \Rightarrow \quad κ ω ≪ κ ∘_m μ.$$$$

Lean4

theorem absolutelyContinuous_comp_of_absolutelyContinuous {ν : Measure 𝓧} [SFinite ν] (h_ac : ∀ᵐ ω ∂μ, κ ω ≪ ν) :
    ∀ᵐ ω ∂μ, κ ω ≪ κ ∘ₘ μ := by
  rw [← absolutelyContinuous_posterior_iff]
  exact absolutelyContinuous_posterior h_ac

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