English
Let μ and ν be finite measures on α × β × γ. If μ and ν agree on all measurable products s × t × u (with s ⊆ α, t ⊆ β, u ⊆ γ measurable), then μ = ν.
Русский
Пусть μ и ν — конечные меры на α × β × γ. Если они совпадают на всех измеримых произведениях s × t × u (с измеримыми s ⊆ α, t ⊆ β, u ⊆ γ), то μ = ν.
LaTeX
$$$\\forall s,t,u,\\; \\text{MeasurableSet}(s) \\to \\text{MeasurableSet}(t) \\to \\text{MeasurableSet}(u) \\to μ(s ×ˢ t ×ˢ u) = ν(s ×ˢ t ×ˢ u) \\Rightarrow μ = ν$$$
Lean4
/-- Two finite measures on a product `α × β × γ` that are equal on products of sets are equal.
See `ext_prod₃'` for the same statement for `(α × β) × γ`. -/
theorem ext_prod₃ {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
{μ ν : Measure (α × β × γ)} [IsFiniteMeasure μ]
(h :
∀ {s : Set α} {t : Set β} {u : Set γ},
MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)) :
μ = ν := by
ext s hs
have h_univ : μ univ = ν univ := by
simp_rw [← univ_prod_univ]
exact h .univ .univ .univ
have : IsFiniteMeasure ν := ⟨by simp [← h_univ]⟩
let C₂ := image2 (· ×ˢ ·) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
let C := image2 (· ×ˢ ·) {s : Set α | MeasurableSet s} C₂
refine MeasurableSpace.induction_on_inter (s := C) ?_ ?_ (by simp) ?_ ?_ ?_ s hs
· refine
(generateFrom_eq_prod (C := {s : Set α | MeasurableSet s}) (D := C₂) (by simp) generateFrom_prod
isCountablySpanning_measurableSet ?_).symm
exact isCountablySpanning_measurableSet.prod isCountablySpanning_measurableSet
· exact MeasurableSpace.isPiSystem_measurableSet.prod isPiSystem_prod
· rintro - ⟨s, hs, -, ⟨t, ht, u, hu, rfl⟩, rfl⟩
exact h hs ht hu
· 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]
