quasiMeasurePreserving_snd — Mathlib

English

The projection to the second coordinate is measurable and the pushforward of μ × ν along snd is ν.

Русский

Вторая проекция измерима, и образ меры по snd равен ν.

LaTeX

$$$\text{QuasiMeasurePreserving}(\text{snd}, (\mu \otimes ν), ν)$$$

Lean4

@[fun_prop]
theorem quasiMeasurePreserving_snd : QuasiMeasurePreserving Prod.snd (μ.prod ν) ν :=
  by
  refine ⟨measurable_snd, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
  rw [map_apply measurable_snd hs, ← univ_prod, ← nonpos_iff_eq_zero]
  refine (prod_prod_le _ _).trans_eq ?_
  rw [h2s, mul_zero]

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