pdf_eq_zero_of_measure_eq_zero_or_top

English

If μ(s)=0 or μ(s)=∞, then the density pdf X ℙ μ is zero almost everywhere.

Русский

Если μ(s)=0 или μ(s)=∞, то плотность pdf(X,ℙ,μ) равна нулю почти surely.

LaTeX

$$$\\text{pdf}(X,\\mathbb{P},\\mu)=^a_e 0$ как функция по μ, если $\\mu(s)=0$ или $\\mu(s)=\\infty$$$

Lean4

theorem pdf_eq_zero_of_measure_eq_zero_or_top {X : Ω → E} {s : Set E} (hu : IsUniform X s ℙ μ)
    (hμs : μ s = 0 ∨ μ s = ∞) : pdf X ℙ μ =ᵐ[μ] 0 :=
  by
  rcases hμs with H | H
  · simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_zero, restrict_eq_zero.mpr H, smul_zero] at hu
    simp [pdf, hu]
  · simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_top, zero_smul] at hu
    simp [pdf, hu]

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