absolutelyContinuous_comp_of_countable

English

If α is countable with measurable singleton class, then for μ-a.e. ω, κ(ω) ≪ κ ∘ₘ μ.

Русский

Если α счётно и для каждого элемента существует измеримое синглтон-покрытие, то для μ-п почти всюду κ(ω) ≪ κ ∘ μ.

LaTeX

$$$[Countable(\\alpha)] [MeasurableSingletonClass(\\alpha)] : \\forall^{\\/} ω \\partial μ, \\; κ(ω) \\ll κ \\circ_{m} μ$$$

Lean4

theorem absolutelyContinuous_comp_of_countable [Countable α] [MeasurableSingletonClass α] : ∀ᵐ ω ∂μ, κ ω ≪ κ ∘ₘ μ :=
  by
  rw [Measure.comp_eq_sum_of_countable, ae_iff_of_countable]
  exact fun ω hμω ↦ Measure.absolutelyContinuous_sum_right ω (Measure.absolutelyContinuous_smul hμω)

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