singularPart_eq_self — Mathlib

English

In general, μ.singularPart ν = μ if and only if μ is mutually singular to ν.

Русский

В общем случае μ.singularPart ν = μ эквивалентно μ ⟂ ν.

LaTeX

$$$$ μ.singularPart ν = μ \iff μ ⟂_{m} ν $$$$

Lean4

theorem singularPart_eq_self : μ.singularPart ν = μ ↔ μ ⟂ₘ ν :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← h]
    exact mutuallySingular_singularPart _ _
  · have := h.haveLebesgueDecomposition
    conv_rhs => rw [← singularPart_add_rnDeriv μ ν]
    rw [(withDensity_rnDeriv_eq_zero _ _).mpr h, add_zero]

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