rnDeriv_eq_zero

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.rnDeriv_eq_zero

← MathLib Explorer

English

μ.rnDer ν =ᵐ[ν] 0 if and only if μ ⟂ ν.

Русский

μ.rnDer ν =ᵐ[ν] 0 тогда и только тогда, когда μ ⟂ ν.

LaTeX

$$$$ μ.rnDer ν =ᵐ[ν] 0 \iff μ ⟂_{m} ν $$$$

Lean4

@[simp]
theorem rnDeriv_eq_zero (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] : μ.rnDeriv ν =ᵐ[ν] 0 ↔ μ ⟂ₘ ν := by
  rw [← withDensity_rnDeriv_eq_zero, withDensity_eq_zero_iff (measurable_rnDeriv _ _).aemeasurable]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru