English
If μ ≪ ν and both measures are σ-finite, then the reciprocal RN-derivative satisfies (μ.rnDeriv ν)^{-1} = μ.rnDeriv ν compared with ν.rnDeriv μ almost everywhere with respect to μ.
Русский
Если μ ≪ ν и обе меры σ-ограничены, то (dμ/dν)^{-1} = dν/dμ почти наверху μ.
LaTeX
$$$(μ.rnDeriv ν)^{-1} =_{μ}^{ae} ν.rnDeriv μ$$$
Lean4
theorem rnDeriv_eq_zero_of_mutuallySingular {ν' : Measure α} [HaveLebesgueDecomposition μ ν'] [SigmaFinite ν']
(h : μ ⟂ₘ ν) (hνν' : ν ≪ ν') : μ.rnDeriv ν' =ᵐ[ν] 0 :=
by
let t := h.nullSet
have ht : MeasurableSet t := h.measurableSet_nullSet
refine ae_of_ae_restrict_of_ae_restrict_compl t ?_ (by simp [t])
change μ.rnDeriv ν' =ᵐ[ν.restrict t] 0
have : μ.rnDeriv ν' =ᵐ[ν.restrict t] (μ.restrict t).rnDeriv ν' :=
by
have h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν') := hνν'.ae_le (rnDeriv_restrict μ ν' ht)
rw [Filter.EventuallyEq, ae_restrict_iff' ht]
filter_upwards [h] with x hx hxt
rw [hx, Set.indicator_of_mem hxt]
refine this.trans ?_
simp only [t, MutuallySingular.restrict_nullSet]
suffices (0 : Measure α).rnDeriv ν' =ᵐ[ν'] 0
by
have h_ac' : ν.restrict t ≪ ν' := restrict_le_self.absolutelyContinuous.trans hνν'
exact h_ac'.ae_le this
exact rnDeriv_zero _
