snd_apply

Mathlib.MeasureTheory.Measure.Prod

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.snd_apply

English

The rule for the second marginal: ρ.snd(s) = ρ(Prod.snd^{-1}(s)) for measurable s.

Русский

Правило для второй маргинальной меры: ρ.snd(s) = ρ(Prod.snd^{-1}(s)) для измеримых s.

LaTeX

$$$$ \\rho.snd(s) = \\rho\\bigl(\\mathrm{Prod.snd}^{-1}(s)\\bigr) $$$$

Lean4

theorem snd_apply {s : Set β} (hs : MeasurableSet s) : ρ.snd s = ρ (Prod.snd ⁻¹' s) := by
  rw [snd, Measure.map_apply measurable_snd hs]

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

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

Разделы

Аффилиация

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