congr

Mathlib.Probability.Density

URI: https://scilib.ai/kg/mathlib#MeasureTheory.pdf.congr

English

If X and Y are almost everywhere equal, then pdf X ℙ μ equals pdf Y ℙ μ.

Русский

Если X и Y равны почти всюду, то pdf X ℙ μ равно pdf Y ℙ μ.

LaTeX

$$$(X =^{\\mathrm{a.e.}}_{\\ℙ} Y) \\Rightarrow pdf X \\ℙ μ = pdf Y \\ℙ μ$$$

Lean4

protected theorem congr {X Y : Ω → E} (hXY : X =ᵐ[ℙ] Y) : pdf X ℙ μ = pdf Y ℙ μ := by
  rw [pdf_def, pdf_def, map_congr hXY]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru