withDensity_rnDeriv_eq_zero — Mathlib

English

The density-measured zero condition: ν.withDensity(μ.rnDer ν) = 0 iff μ ⟂ ν.

Русский

Условие нулевой меры по плотности: ν.withDensity(μ.rnDer ν) = 0 тогда и только тогда, когда μ ⟂ ν.

LaTeX

$$$$ ν.withDensity(μ.rnDer ν) = 0 \iff μ ⟂_{m} ν $$$$

Lean4

@[simp]
theorem withDensity_rnDeriv_eq_zero (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] :
    ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν :=
  by
  have h_dec := haveLebesgueDecomposition_add μ ν
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [h, add_zero] at h_dec
    rw [h_dec]
    exact mutuallySingular_singularPart μ ν
  · rw [← MutuallySingular.self_iff]
    rw [h_dec, MutuallySingular.add_left_iff] at h
    refine MutuallySingular.mono_ac h.2 AbsolutelyContinuous.rfl ?_
    exact withDensity_absolutelyContinuous _ _

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