rnDeriv_self — Mathlib

English

Taking the singular part twice with respect to ν leaves the result unchanged: (μ.singularPart ν).singularPart ν = μ.singularPart ν.

Русский

Повторное взятие сингулярной части по ν не изменяет меру: (μ.singularPart ν).singularPart ν = μ.singularPart ν.

LaTeX

$$$$ (μ.singularPart ν).singularPart ν = μ.singularPart ν $$$$

Lean4

theorem rnDeriv_self (μ : Measure α) [SigmaFinite μ] : μ.rnDeriv μ =ᵐ[μ] fun _ ↦ 1 :=
  by
  have h := rnDeriv_add_singularPart μ μ
  rw [singularPart_self, add_zero] at h
  have h_one : μ = μ.withDensity 1 := by simp
  conv_rhs at h => rw [h_one]
  rwa [withDensity_eq_iff_of_sigmaFinite (measurable_rnDeriv _ _).aemeasurable] at h
  exact aemeasurable_const

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