measurableSet_absolutelyContinuous

English

The set of points a in α for which κ a is absolutely continuous with respect to η a is a measurable subset of α.

Русский

Множество точек a ∈ α, для которых κ a абсолютно непрерывна по отношению к η a, является измеримым подмножеством α.

LaTeX

$$MeasurableSet { a | κ a ≪ η a }$$

Lean4

/-- The set of points `a : α` such that `κ a ≪ η a` is measurable. -/
@[measurability]
theorem measurableSet_absolutelyContinuous (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    MeasurableSet {a | κ a ≪ η a} :=
  by
  simp_rw [← singularPart_eq_zero_iff_absolutelyContinuous, singularPart_eq_zero_iff_measure_eq_zero]
  exact measurable_kernel_prodMk_left (measurableSet_mutuallySingularSet κ η) (measurableSet_singleton 0)

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