eq_withDensity_rnDeriv₀ — Mathlib

English

Same as above, but allowing f to be only a.e. with respect to ν; the equality ν.withDensity f = ν.withDensity(μ.rnDer ν) holds a.e.

Русский

То же самое, но допускаем f лишь до эквивалентности по ν; равенство ν.withDensity f = ν.withDensity(μ.rnDer ν) держится почти наверху по ν.

LaTeX

$$$ μ = s + ν.withDensity f \\Rightarrow ν.withDensity f = ν.withDensity(μ.rnDer ν) \\text{ (a.e.)}$$$

Lean4

theorem eq_withDensity_rnDeriv₀ {s : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f ν) (hs : s ⟂ₘ ν)
    (hadd : μ = s + ν.withDensity f) : ν.withDensity f = ν.withDensity (μ.rnDeriv ν) :=
  by
  rw [withDensity_congr_ae hf.ae_eq_mk] at hadd ⊢
  exact eq_withDensity_rnDeriv hf.measurable_mk hs hadd

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