hasLaw — Mathlib

English

If X has a PDF with respect to μ, then X has a law with respect to the measure μ.withDensity(pdf X P μ).

Русский

Если X имеет PDF по отношению к μ, то X имеет закон по мере μ.withDensity(pdf X P μ).

LaTeX

$$$$ \\text{HasPDF } X\\; P\\; \\mu \\Rightarrow \\text{HasLaw } X\\; (\\mu.withDensity(\\mathrm{pdf}\\; X\\; P\\; \\mu)) \\; P $$$$

Lean4

theorem hasLaw [h : HasPDF X P μ] : HasLaw X (μ.withDensity (pdf X P μ)) P
    where
  aemeasurable := h.aemeasurable
  map_eq := map_eq_withDensity_pdf X P μ

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