singularPart — Mathlib

English

If f is almost everywhere measurable with respect to μ, then it remains almost everywhere measurable with respect to the singular part of μ with respect to ν, for any ν.

Русский

Если f почти всюду измерима относительно μ, то она остается почти всюду измеримой относительно части μ, которая является отделимой от ν, для любого ν.

LaTeX

$$$$ AEMeasurable\ f\ \mu \Rightarrow AEMeasurable\ f\ (\mu.singularPart\ \nu) $$$$

Lean4

theorem _root_.AEMeasurable.singularPart {β : Type*} {_ : MeasurableSpace β} {f : α → β} (hf : AEMeasurable f μ)
    (ν : Measure α) : AEMeasurable f (μ.singularPart ν) :=
  AEMeasurable.mono_measure hf (Measure.singularPart_le _ _)

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