English
Same as above: if hg is quasi-measure-preserving and the composition pushforward has Lebesgue decomposition, then HasPDF (g ∘ X) ℙ ν.
Русский
То же, что и выше: если hg квази-измеримо-представляющее, а образующая мера имеет разложение по Лебегу, то HasPDF (g ∘ X) ℙ ν.
LaTeX
$$$\\text{(hg : QuasiMeasurePreserving g μ ν)} \\land \\text{(hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν)} \\Rightarrow HasPDF (g \\circ X) ℙ ν$$$
Lean4
/-- A random variable that `HasPDF` transformed under a `QuasiMeasurePreserving`
map also `HasPDF` if `(map g (map X ℙ)).HaveLebesgueDecomposition μ`.
`quasiMeasurePreserving_hasPDF` is more useful in the case we are working with a
probability measure and a real-valued random variable. -/
theorem quasiMeasurePreserving_hasPDF (hg : QuasiMeasurePreserving g μ ν)
(hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν) : HasPDF (g ∘ X) ℙ ν :=
by
have hgm : AEMeasurable g (map X ℙ) := hg.aemeasurable.mono_ac HasPDF.absolutelyContinuous
rw [hasPDF_iff, ← AEMeasurable.map_map_of_aemeasurable hgm (HasPDF.aemeasurable X ℙ μ)]
refine ⟨hg.measurable.comp_aemeasurable (HasPDF.aemeasurable _ _ μ), hmap, ?_⟩
exact (HasPDF.absolutelyContinuous.map hg.1).trans hg.2
