measurable_singularPart — Mathlib

English

If κ = η.withDensity f + ξ and f is measurable, then ξ a equals the singularPart of κ a with respect to η a for all a, given mutual singularity conditions.

Русский

Если κ = η.withDensity f + ξ и f измеримо, то ξ a равняется сингулярной части κ a по η a при условии взаимной сингулярности.

LaTeX

$$ξ a = (κ a).singularPart (η a)$$

Lean4

/-- For two kernels `κ, η`, the singular part of `κ a` with respect to `η a` is a measurable
function of `a`. -/
theorem measurable_singularPart (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    Measurable (fun a ↦ (κ a).singularPart (η a)) :=
  by
  refine Measure.measurable_of_measurable_coe _ (fun s hs ↦ ?_)
  simp_rw [← κ.singularPart_eq_singularPart_measure, κ.singularPart_def η]
  exact Kernel.measurable_coe _ hs

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