withDensity_rnDeriv — Mathlib

English

If f is AEM with respect to μ, then f is AEM with respect to ν.withDensity(μ.rnDer ν) for any ν.

Русский

Если f AEM относительно μ, то она AEM относительно ν.withDensity(μ.rnDer ν) для любой ν.

LaTeX

$$$$ AEMeasurable\ f\ \mu \Rightarrow AEMeasurable\ f\ (\nu.withDensity(\mu.rnDer \nu)) $$$$

Lean4

theorem _root_.AEMeasurable.withDensity_rnDeriv {β : Type*} {_ : MeasurableSpace β} {f : α → β} (hf : AEMeasurable f μ)
    (ν : Measure α) : AEMeasurable f (ν.withDensity (μ.rnDeriv ν)) :=
  AEMeasurable.mono_measure hf (Measure.withDensity_rnDeriv_le _ _)

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