pi_map_eval — Mathlib

English

If maps f_i are measurable, then the map induced on the product measure equals the product of pushforwards.

Русский

Если карты f_i измеримы, то отображение на произведение мер равняется произведению сумм-переходов.

LaTeX

$$$(\mathrm{pi\,map}\ μ) = \mathrm{pi}(μ_i\ map f_i)$$

Lean4

theorem pi_map_eval [DecidableEq ι] (i : ι) :
    (Measure.pi μ).map (Function.eval i) = (∏ j ∈ Finset.univ.erase i, μ j Set.univ) • (μ i) :=
  by
  ext s hs
  classical
  rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi, Measure.smul_apply,
    smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]
  congrm ?_ * ?_
  swap; · simp
  refine Finset.prod_congr rfl fun j hj ↦ ?_
  simp [Function.update, Finset.ne_of_mem_erase hj]

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