English
Let Ω be a space with a family s of sub-sigma-algebras independent under μ, and let f be a tail-like filter with a directed ns, and hypotheses as in the theorem. Then the tail event limsup s f has probability 0 or 1: any tail event is a 0-1 event under μ.
Русский
Пусть имеется независимая под_sigma-алгебра s на Ω и хвостовая конструкция; тогда хвостовое событие limsup s f имеет вероятность либо 0, либо 1: хвостовые события — это события с вероятностью 0 или 1.
LaTeX
$$$\forall t\subseteq Ω\, (t \text{ tail for } s f) \Rightarrow μ(t) \in \{0,1\}$$$
Lean4
theorem measure_zero_or_one_of_measurableSet_limsup (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα)
(hf : ∀ t, p t → tᶜ ∈ f) (hns : Directed (· ≤ ·) ns) (hnsp : ∀ a, p (ns a)) (hns_univ : ∀ n, ∃ a, n ∈ ns a)
{t : Set Ω} (ht_tail : MeasurableSet[limsup s f] t) : ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1 :=
by
apply
measure_eq_zero_or_one_of_indepSet_self' ?_
((indep_limsup_self h_le h_indep hf hns hnsp hns_univ).indepSet_of_measurableSet ht_tail ht_tail)
filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance
