English
For a random variable X, HasPDF X ℙ μ holds if and only if the pushforward map X ℙ has a Lebesgue decomposition with respect to μ and is absolutely continuous with respect to μ; equivalently, (map X ℙ).HaveLebesgueDecomposition μ and map X ℙ ≪ μ.
Русский
Для случайной величины X выражение HasPDF X ℙ μ эквивалентно тому, что образующая мера map X ℙ имеет разложение по Лебегу относительно μ и абсолютно непрерывна относительно μ; то есть (map X ℙ).HaveLebesgueDecomposition μ и map X ℙ ≪ μ.
LaTeX
$$$HasPDF X \\ℙ μ \\iff (map X \\ℙ).HaveLebesgueDecomposition μ \\land map X \\ℙ \\ll μ$$$
Lean4
theorem hasPDF_iff : HasPDF X ℙ μ ↔ AEMeasurable X ℙ ∧ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ :=
⟨fun ⟨h₁, h₂, h₃⟩ ↦ ⟨h₁, h₂, h₃⟩, fun ⟨h₁, h₂, h₃⟩ ↦ ⟨h₁, h₂, h₃⟩⟩
