measure_zero_or_one_of_measurableSet_limsup_atBot

English

Another kernel-enabled version of limsup independence atTop_self with the standard hypotheses and the expected self-independence formula.

Русский

Еще одна версия независимости limsup atTop_self в рамках ядра.

LaTeX

$$$\Indep(\limsup s atTop, \limsup s atTop)\; κ\; μα$$$

Lean4

/-- **Kolmogorov's 0-1 law**, kernel version: any event in the tail σ-algebra of an independent
sequence of sub-σ-algebras has probability 0 or 1 almost surely. -/
theorem measure_zero_or_one_of_measurableSet_limsup_atBot (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα) {t : Set Ω}
    (ht_tail : MeasurableSet[limsup s atBot] t) : ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1 :=
  by
  apply
    measure_eq_zero_or_one_of_indepSet_self' ?_
      ((indep_limsup_atBot_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

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