English
A product measure equals a measure μν if they agree on a generating family of rectangles.
Русский
Произведение меры равно мере μν, если они совпадают на порождающей системе прямоугольников.
LaTeX
$$pi μ = μν if μν agrees on rectangles$$
Lean4
/-- A measure on a finite product space equals the product measure if they are equal on rectangles
with as sides sets that generate the corresponding σ-algebras. -/
theorem pi_eq_generateFrom {C : ∀ i, Set (Set (α i))} (hC : ∀ i, generateFrom (C i) = by apply_assumption)
(h2C : ∀ i, IsPiSystem (C i)) (h3C : ∀ i, (μ i).FiniteSpanningSetsIn (C i)) {μν : Measure (∀ i, α i)}
(h₁ : ∀ s : ∀ i, Set (α i), (∀ i, s i ∈ C i) → μν (pi univ s) = ∏ i, μ i (s i)) : Measure.pi μ = μν :=
by
have h4C : ∀ (i) (s : Set (α i)), s ∈ C i → MeasurableSet s := by intro i s hs; rw [← hC];
exact measurableSet_generateFrom hs
refine
(FiniteSpanningSetsIn.pi h3C).ext (generateFrom_eq_pi hC fun i => (h3C i).isCountablySpanning).symm
(IsPiSystem.pi h2C) ?_
rintro _ ⟨s, hs, rfl⟩
rw [mem_univ_pi] at hs
haveI := fun i => (h3C i).sigmaFinite
simp_rw [h₁ s hs, pi_pi_aux μ s fun i => h4C i _ (hs i)]
