English
A measure on a product space equals the product measure if they are equal on rectangles and the generating systems are Pi-systems.
Русский
Мера на произведении пространства равна произведению мер, если они равны на прямоугольниках и учитываются Pi-системы.
LaTeX
$$prod_eq_generateFrom$$
Lean4
/-- A measure on a product space equals the product measure if they are equal on rectangles
with as sides sets that generate the corresponding σ-algebras. -/
theorem prod_eq_generateFrom {μ : Measure α} {ν : Measure β} {C : Set (Set α)} {D : Set (Set β)}
(hC : generateFrom C = ‹_›) (hD : generateFrom D = ‹_›) (h2C : IsPiSystem C) (h2D : IsPiSystem D)
(h3C : μ.FiniteSpanningSetsIn C) (h3D : ν.FiniteSpanningSetsIn D) {μν : Measure (α × β)}
(h₁ : ∀ s ∈ C, ∀ t ∈ D, μν (s ×ˢ t) = μ s * ν t) : μ.prod ν = μν :=
by
refine
(h3C.prod h3D).ext (generateFrom_eq_prod hC hD h3C.isCountablySpanning h3D.isCountablySpanning).symm (h2C.prod h2D)
?_
rintro _ ⟨s, hs, t, ht, rfl⟩
haveI := h3D.sigmaFinite
rw [h₁ s hs t ht, prod_prod]
/- Note that the next theorem is not true for s-finite measures: let `μ = ν = ∞ • Leb` on `[0,1]`
(they are s-finite as countable sums of the finite Lebesgue measure), and let `μν = μ.prod ν + λ`
where `λ` is Lebesgue measure on the diagonal. Then both measures give infinite mass to rectangles
`s × t` whose sides have positive Lebesgue measure, and `0` measure when one of the sides has zero
Lebesgue measure. And yet they do not coincide, as the first one gives zero mass to the diagonal,
and the second one gives mass one.
-/
