English
Let s and t be measurable cylinders that are disjoint. Then the projective family is additive on their union: projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t.
Русский
Пусть s и t — измеримые цилиндры, взаимно простые. Тогда проектная семейная мера удовлетворяет аддитивности: projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t.
LaTeX
$$$\forall hP\, hs\, ht\, hst:\ Disjoint\ s\ t \Rightarrow \operatorname{projectiveFamilyFun} P (s \cup t) = \operatorname{projectiveFamilyFun} P s + \operatorname{projectiveFamilyFun} P t$$$
Lean4
theorem projectiveFamilyFun_union (hP : IsProjectiveMeasureFamily P) (hs : s ∈ measurableCylinders α)
(ht : t ∈ measurableCylinders α) (hst : Disjoint s t) :
projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t :=
by
obtain ⟨I, S, hS, hs_eq⟩ := (mem_measurableCylinders _).1 hs
obtain ⟨J, T, hT, ht_eq⟩ := (mem_measurableCylinders _).1 ht
classical
let S' := restrict₂ (subset_union_left (s₂ := J)) ⁻¹' S
let T' := restrict₂ (subset_union_right (s₁ := I)) ⁻¹' T
have hS' : MeasurableSet S' := measurable_restrict₂ _ hS
have hT' : MeasurableSet T' := measurable_restrict₂ _ hT
have h_eq1 : s = cylinder (I ∪ J) S' := by rw [hs_eq]; exact cylinder_eq_cylinder_union I S J
have h_eq2 : t = cylinder (I ∪ J) T' := by rw [ht_eq]; exact cylinder_eq_cylinder_union J T I
have h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T') := by rw [hs_eq, ht_eq]; exact union_cylinder _ _ _ _
rw [projectiveFamilyFun_congr hP hs h_eq1 hS', projectiveFamilyFun_congr hP ht h_eq2 hT',
projectiveFamilyFun_congr hP (union_mem_measurableCylinders hs ht) h_eq3 (hS'.union hT')]
cases isEmpty_or_nonempty (Π i, α i) with
| inl h => simp [hP.eq_zero_of_isEmpty]
| inr h =>
rw [measure_union _ hT']
rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst
