measurePreserving_eval — Mathlib

English

For each i, eval_i is measure-preserving from the product measure to μ_i.

Русский

Для каждого i eval_i сохраняет меру при переходе от произведения π μ к μ_i.

LaTeX

$$measurePreserving_eval$$

Lean4

theorem _root_.MeasureTheory.measurePreserving_eval [∀ i, IsProbabilityMeasure (μ i)] (i : ι) :
    MeasurePreserving (Function.eval i) (Measure.pi μ) (μ i) :=
  by
  refine ⟨measurable_pi_apply i, ?_⟩
  classical
  rw [Measure.pi_map_eval, Finset.prod_eq_one, one_smul]
  exact fun _ _ ↦ measure_univ

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