English
If two cylinders match after a subset projection, the corresponding projected measures agree.
Русский
Если цилиндры совпадают после проекции подмножества, соответствующие проекции мер равны.
LaTeX
$$$\forall hP:\ IsProjectiveMeasureFamily P,\ \forall {S},{T},\ MeasurableSet S\ \&\ MeasurableSet T,\ cylinder I S = cylinder J T \Rightarrow P I S = P J T.$$$
Lean4
theorem congr_cylinder_of_subset (hP : IsProjectiveMeasureFamily P) {S : Set (∀ i : I, α i)} {T : Set (∀ i : J, α i)}
(hT : MeasurableSet T) (h_eq : cylinder I S = cylinder J T) (hJI : J ⊆ I) : P I S = P J T := by
cases isEmpty_or_nonempty (∀ i, α i) with
| inl
h =>
suffices ∀ I, P I univ = 0 by
simp only [Measure.measure_univ_eq_zero] at this
simp [this]
intro I
simp only [isEmpty_pi] at h
obtain ⟨i, hi_empty⟩ := h
rw [measure_univ_eq hP I { i }]
have : (univ : Set ((j : { x // x ∈ ({ i } : Finset ι) }) → α j)) = ∅ := by simp [hi_empty]
simp [this]
| inr h =>
have : S = Finset.restrict₂ hJI ⁻¹' T := eq_of_cylinder_eq_of_subset h_eq hJI
rw [hP I J hJI, Measure.map_apply _ hT, this]
exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)
