rnDeriv_gaussianReal — Mathlib

English

The Radon–Nikodym derivative of GaussianReal μ v with respect to volume is gaussianPDF μ v almost surely.

Русский

Пускай производная Радона–Никодима распределения гауссового вида по отношению к объёму равна плотности gaussianPDF μ v почти всюду.

LaTeX

$$$\frac{\partial}{\partial \mathrm{volume}} \mathrm{gaussianReal}(\mu, v) \\ =_{a.e.} \mathrm{gaussianPDF}(\mu, v)$$$

Lean4

theorem rnDeriv_gaussianReal (μ : ℝ) (v : ℝ≥0) : ∂(gaussianReal μ v)/∂volume =ₐₛ gaussianPDF μ v :=
  by
  by_cases hv : v = 0
  · simp only [hv, gaussianReal_zero_var, gaussianPDF_zero_var]
    refine (Measure.eq_rnDeriv measurable_zero (mutuallySingular_dirac μ volume) ?_).symm
    rw [withDensity_zero, add_zero]
  · rw [gaussianReal_of_var_ne_zero _ hv]
    exact Measure.rnDeriv_withDensity _ (measurable_gaussianPDF μ v)

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