uniformPDF_ite — Mathlib

English

Under measurability of s and uniform X, pdf X equals the indicator of s scaled by (μ s)⁻¹ almost everywhere.

Русский

При измеримости s и равномерности X pdf X совпадает с индикатором s, масштабированным на (μ(s))⁻¹, почти наверняка.

LaTeX

$$$\\text{pdf}(X,\\mathbb{P},\\mu)=^a_e s\\,\\mathbf{1}_{s} (\\mu(s))^{-1}$$$

Lean4

/-- Alternative way of writing the uniformPDF. -/
theorem uniformPDF_ite {s : Set E} {x : E} : uniformPDF s x μ = if x ∈ s then (μ s)⁻¹ else 0 :=
  by
  unfold uniformPDF
  unfold Set.indicator
  simp only [Pi.smul_apply, Pi.one_apply, smul_eq_mul, mul_one]

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