English
Let μ and ν be finite measures on the product space α × β. If μ and ν assign the same measure to every measurable rectangle s × t (with s ⊆ α and t ⊆ β measurable), then μ = ν.
Русский
Пусть μ и ν — конечные меры на произведение α × β. Если они дают одинаковые значения мерам для каждой измеримой прямоугольной области s × t (где s ⊆ α и t ⊆ β измеримы), то μ = ν.
LaTeX
$$$\\displaystyle \\Big( \\forall\, s:\\mathcal{P}(\\alpha), t:\\mathcal{P}(\\beta),\\; \\text{MeasurableSet}(s) \\to \\text{MeasurableSet}(t) \\to μ(s \\times\\!\\, t) = ν(s \\times\\!\\, t) \\Big) \\Rightarrow μ = ν$$$
Lean4
/-- Two finite measures on a product that are equal on products of sets are equal. -/
theorem ext_prod {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : Measure (α × β)}
[IsFiniteMeasure μ] (h : ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)) :
μ = ν := by
ext s hs
have h_univ : μ univ = ν univ := by
rw [← univ_prod_univ]
exact h .univ .univ
have : IsFiniteMeasure ν := ⟨by simp [← h_univ]⟩
refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod (by simp) ?_ ?_ ?_ s hs
· rintro - ⟨s, hs, t, ht, rfl⟩
exact h hs ht
· intro t ht h
simp_rw [measure_compl ht (measure_ne_top _ _), h, h_univ]
· intro f h_disj hf h_eq
simp_rw [measure_iUnion h_disj hf, h_eq]
