eq_infinitePi — Mathlib

English

Reindexing with an equivalence e preserves the infinite product measure: infinitePi μ equals the pushforward of infinitePi (μ ∘ e).

Русский

Переиндексация посредством эквивиалентности e сохраняет произведение: infinitePi μ равно образу infinitePi (μ ∘ e).

LaTeX

$$$$\mathrm{infinitePi}_{i}(μ_i) = \bigl(\mathrm{equivLeft}\;e\bigr)_*(\mathrm{infinitePi}_{i}(μ_{e(i)})).$$$$

Lean4

/-- To prove that a measure is equal to the product measure it is enough to check that it
it gives the same measure to measurable boxes. -/
theorem eq_infinitePi {ν : Measure (Π i, X i)}
    (hν :
      ∀ s : Finset ι, ∀ t : (i : ι) → Set (X i), (∀ i ∈ s, MeasurableSet (t i)) → ν (Set.pi s t) = ∏ i ∈ s, μ i (t i)) :
    ν = infinitePi μ := by
  refine (isProjectiveLimit_infinitePi μ).unique ?_ |>.symm
  refine fun s ↦ (pi_eq fun t ht ↦ ?_).symm
  classical
  rw [Measure.map_apply, restrict_preimage, hν, ← prod_attach, univ_eq_attach]
  · congr with i
    rw [dif_pos i.2]
  any_goals fun_prop
  · exact fun i hi ↦ dif_pos hi ▸ ht ⟨i, hi⟩
  · exact .univ_pi ht

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