measure_zero_or_one_of_measurableSet_limsup_atTop

English

For kernel κ with iIndep s κ μα and ht_tail measurable, for any tail set t, κ a t ∈ {0,1} for μα-a.e. a.

Русский

Для ядра κ с iIndep s κ μα и хвостовым множеством t, почти наверняка a, κ a t ∈ {0,1}.

LaTeX

$$$\forall t\; (t\in\text{Tail}(s, atTop))\; (κ(a,t)\in\{0,1\})$ для a.e. a$$

Lean4

theorem measure_zero_or_one_of_measurableSet_limsup_atTop (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα) {t : Set Ω}
    (ht_tail : MeasurableSet[limsup s atTop] t) : ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1 :=
  by
  apply
    measure_eq_zero_or_one_of_indepSet_self' ?_
      ((indep_limsup_atTop_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)
  filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

Похожие утверждения