haveLebesgueDecomposition — Mathlib

English

If X has a PDF, then the pushforward map (map X ℙ) has a Lebesgue decomposition with respect to μ.

Русский

Если у X есть плотность, то образующая мера map X ℙ имеет разложение по Лебегу относительно μ.

LaTeX

$$$(map X \\ℙ).HaveLebesgueDecomposition μ$$$

Lean4

instance haveLebesgueDecomposition [HasPDF X ℙ μ] : (map X ℙ).HaveLebesgueDecomposition μ :=
  HasPDF.haveLebesgueDecomposition'

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