eq_singularPart — Mathlib

English

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

Русский

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

LaTeX

$$MeasurableSet {a | κ a \\ll η a}$$

Lean4

theorem eq_singularPart (h : κ = η.withDensity f + ξ) (hf : Measurable (Function.uncurry f)) (a : α) (hξ : ξ a ⟂ₘ η a) :
    ξ a = singularPart κ η a :=
  (eq_singularPart_measure h hf a hξ).trans singularPart_eq_singularPart_measure.symm

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