quasiMeasurePreserving_fst — Mathlib

English

The projection to the first coordinate is measurable and the pushforward of μ × ν along fst is μ (quasi-measure-preserving).

Русский

Проекция на первую координату измерима и образ меры μ × ν по fst равен μ (почти сохраняет меру).

LaTeX

$$$\text{QuasiMeasurePreserving}(\text{fst}, (\mu \otimes \nu), \mu)$$$

Lean4

@[fun_prop]
theorem quasiMeasurePreserving_fst : QuasiMeasurePreserving Prod.fst (μ.prod ν) μ :=
  by
  refine ⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
  rw [map_apply measurable_fst hs, ← prod_univ, ← nonpos_iff_eq_zero]
  refine (prod_prod_le _ _).trans_eq ?_
  rw [h2s, zero_mul]

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