measurableSet_mutuallySingular — Mathlib

English

The set of points a where κ a is mutually singular 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_mutuallySingular (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    MeasurableSet {a | κ a ⟂ₘ η a} :=
  by
  simp_rw [← withDensity_rnDeriv_eq_zero_iff_mutuallySingular, withDensity_rnDeriv_eq_zero_iff_measure_eq_zero]
  exact measurable_kernel_prodMk_left (measurableSet_mutuallySingularSet κ η).compl (measurableSet_singleton 0)

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