Commit 2023-11-28 08:01 3f88a472

refactor(Probability/Density): define pdf using rnDeriv (#8544) Defines pdf in terms of rnDeriv. Main definition change:

/-- A random variable `X : Ω → E` is said to `HasPDF` with respect to the measure `ℙ` on `Ω` and
`μ` on `E` if the push-forward measure of `ℙ` along `X` is absolutely continuous with respect to
`μ` and they `HaveLebesgueDecomposition`. -/
class HasPDF {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
    (μ : Measure E := by volume_tac) : Prop where
  pdf' : Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
/-- If `X` is a random variable that `HasPDF X ℙ μ`, then `pdf X` is the Radon–Nikodym
derivative of the push-forward measure of `ℙ` along `X` with respect to `μ`. -/
def pdf {_ : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) :
    E → ℝ≥0∞ :=
  if HasPDF X ℙ μ then (map X ℙ).rnDeriv μ else 0

The law of the unconscious statistician is first generalized to rnDeriv on a general Banach space (∫ x, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ x, f x ∂μ), and then proven for PDFs. Zulip thread