pdf_of_not_haveLebesgueDecomposition

English

If (map X ℙ).HaveLebesgueDecomposition μ does not hold, then pdf X ℙ μ = 0.

Русский

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

LaTeX

$$$(map X \\ℙ).HaveLebesgueDecomposition μ =\\text{ False } \\Rightarrow pdf X \\ℙ μ = 0$$$

Lean4

theorem pdf_of_not_haveLebesgueDecomposition {_ : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E}
    (h : ¬(map X ℙ).HaveLebesgueDecomposition μ) : pdf X ℙ μ = 0 :=
  rnDeriv_of_not_haveLebesgueDecomposition h

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