rnDeriv_pos — Mathlib

English

Under Lebesgue decomposition, if μ ≪ ν, then μ-almost everywhere the RN-derivative is strictly positive.

Русский

При разложении Лебеса, если μ ≪ ν, то радоновская производная положительна μ-пк почти везде.

LaTeX

$$$$ \\forall^{a.e.}_{x \\in \\mu} \\; 0 < \\mathrm{rnDeriv}(\\nu, \\mu)(x). $$$$

Lean4

theorem rnDeriv_pos [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) : ∀ᵐ x ∂μ, 0 < μ.rnDeriv ν x :=
  by
  rw [← Measure.withDensity_rnDeriv_eq _ _ hμν, ae_withDensity_iff (Measure.measurable_rnDeriv _ _),
    Measure.withDensity_rnDeriv_eq _ _ hμν]
  exact ae_of_all _ (fun x hx ↦ lt_of_le_of_ne (zero_le _) hx.symm)

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