English
Two finite measures μ and ν on (α × β) × γ are equal iff they agree on products of the form (s × t) × u with s ⊆ α, t ⊆ β, u ⊆ γ measurable.
Русский
Две конечные меры μ и ν на (α × β) × γ равны тогда и только тогда, когда они совпадают на произведениях вида (s × t) × u с измеримыми s ⊆ α, t ⊆ β, u ⊆ γ.
LaTeX
$$$μ = ν \\iff \\forall s,t,u,\\; \\text{MeasurableSet}(s) \\to \\text{MeasurableSet}(t) \\to \\text{MeasurableSet}(u) \\to μ((s ×ˢ t) ×ˢ u) = ν((s ×ˢ t) ×ˢ u)$$$
Lean4
/-- Two finite measures on a product `(α × β) × γ` are equal iff they are equal on products of sets.
See `ext_prod₃_iff` for the same statement for `α × β × γ`. -/
theorem ext_prod₃_iff' {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
{μ ν : Measure ((α × β) × γ)} [IsFiniteMeasure μ] :
μ = ν ↔
(∀ {s : Set α} {t : Set β} {u : Set γ},
MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)) :=
by
rw [← MeasurableEquiv.prodAssoc.map_measurableEquiv_injective.eq_iff, ext_prod₃_iff]
have h_eq (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s)
(ht : MeasurableSet t) (hu : MeasurableSet u) :
ν.map MeasurableEquiv.prodAssoc (s ×ˢ (t ×ˢ u)) = ν ((s ×ˢ t) ×ˢ u) :=
by
rw [map_apply (by fun_prop) (hs.prod (ht.prod hu))]
congr 1 with x
simp [MeasurableEquiv.prodAssoc]
refine ⟨fun h s t u hs ht hu ↦ ?_, fun h s t u hs ht hu ↦ ?_⟩ <;> specialize h hs ht hu
· rwa [h_eq μ hs ht hu, h_eq ν hs ht hu] at h
· rwa [h_eq μ hs ht hu, h_eq ν hs ht hu]
