Kolmogorov's 0-1 law #
Let s : ι → MeasurableSpace Ω be an independent sequence of sub-σ-algebras. Then any set which
is measurable with respect to the tail σ-algebra limsup s atTop has probability 0 or 1.
Main statements #
measure_zero_or_one_of_measurableSet_limsup_atTop: Kolmogorov's 0-1 law. Any set which is measurable with respect to the tail σ-algebralimsup s atTopof an independent sequence of σ-algebrasshas probability 0 or 1.
theorem
ProbabilityTheory.Kernel.measure_eq_zero_or_one_or_top_of_indepSet_self
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
{t : Set Ω}
(h_indep : IndepSet t t κ μα)
:
theorem
ProbabilityTheory.measure_eq_zero_or_one_or_top_of_indepSet_self
{Ω : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{t : Set Ω}
(h_indep : IndepSet t t μ)
:
theorem
ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self'
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
(h : ∀ᵐ (a : α) ∂μα, MeasureTheory.IsFiniteMeasure (κ a))
{t : Set Ω}
(h_indep : IndepSet t t κ μα)
:
theorem
ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
[h : ∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)]
{t : Set Ω}
(h_indep : IndepSet t t κ μα)
:
theorem
ProbabilityTheory.measure_eq_zero_or_one_of_indepSet_self
{Ω : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{t : Set Ω}
(h_indep : IndepSet t t μ)
:
theorem
ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self
{Ω : Type u_2}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[hμ : MeasureTheory.IsFiniteMeasure μ]
{t : Set Ω}
(ht : MeasurableSet t)
(h_indep : CondIndepSet m hm t t μ)
:
@[deprecated ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self (since := "2025-01-21")]
theorem
ProbabilityTheory.condexp_eq_zero_or_one_of_condIndepSet_self
{Ω : Type u_2}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[hμ : MeasureTheory.IsFiniteMeasure μ]
{t : Set Ω}
(ht : MeasurableSet t)
(h_indep : CondIndepSet m hm t t μ)
:
Alias of ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self.
theorem
ProbabilityTheory.Kernel.indep_biSup_compl
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
(t : Set ι)
:
theorem
ProbabilityTheory.indep_biSup_compl
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
(t : Set ι)
:
theorem
ProbabilityTheory.condIndep_biSup_compl
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
(t : Set ι)
:
We prove a version of Kolmogorov's 0-1 law for the σ-algebra limsup s f where f is a filter
for which we can define the following two functions:
p : Set ι → Propsuch that for a sett,p t → tᶜ ∈ f,ns : α → Set ιa directed sequence of sets which all verifypand such that⋃ a, ns a = Set.univ.
For the example of f = atTop, we can take
p = bddAbove and ns : ι → Set ι := fun i => Set.Iic i.
theorem
ProbabilityTheory.Kernel.indep_biSup_limsup
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
{p : Set ι → Prop}
{f : Filter ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
{t : Set ι}
(ht : p t)
:
Indep (⨆ n ∈ t, s n) (Filter.limsup s f) κ μα
theorem
ProbabilityTheory.indep_biSup_limsup
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{p : Set ι → Prop}
{f : Filter ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
{t : Set ι}
(ht : p t)
:
Indep (⨆ n ∈ t, s n) (Filter.limsup s f) μ
theorem
ProbabilityTheory.condIndep_biSup_limsup
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{p : Set ι → Prop}
{f : Filter ι}
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
{t : Set ι}
(ht : p t)
:
CondIndep m (⨆ n ∈ t, s n) (Filter.limsup s f) hm μ
theorem
ProbabilityTheory.Kernel.indep_iSup_directed_limsup
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
:
Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (Filter.limsup s f) κ μα
theorem
ProbabilityTheory.indep_iSup_directed_limsup
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
:
Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (Filter.limsup s f) μ
theorem
ProbabilityTheory.condIndep_iSup_directed_limsup
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
:
CondIndep m (⨆ (a : β), ⨆ n ∈ ns a, s n) (Filter.limsup s f) hm μ
theorem
ProbabilityTheory.Kernel.indep_iSup_limsup
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
:
Indep (⨆ (n : ι), s n) (Filter.limsup s f) κ μα
theorem
ProbabilityTheory.indep_iSup_limsup
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
:
Indep (⨆ (n : ι), s n) (Filter.limsup s f) μ
theorem
ProbabilityTheory.condIndep_iSup_limsup
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
:
CondIndep m (⨆ (n : ι), s n) (Filter.limsup s f) hm μ
theorem
ProbabilityTheory.Kernel.indep_limsup_self
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
:
Indep (Filter.limsup s f) (Filter.limsup s f) κ μα
theorem
ProbabilityTheory.indep_limsup_self
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
:
Indep (Filter.limsup s f) (Filter.limsup s f) μ
theorem
ProbabilityTheory.condIndep_limsup_self
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
:
CondIndep m (Filter.limsup s f) (Filter.limsup s f) hm μ
theorem
ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
theorem
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
theorem
ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
@[deprecated ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup (since := "2025-01-21")]
theorem
ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{β : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : β → Set ι}
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x1 x2 : Set ι) => x1 ≤ x2) ns)
(hnsp : ∀ (a : β), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
Alias of ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup.
theorem
ProbabilityTheory.Kernel.indep_limsup_atTop_self
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
:
Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) κ μα
theorem
ProbabilityTheory.indep_limsup_atTop_self
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
:
Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) μ
theorem
ProbabilityTheory.condIndep_limsup_atTop_self
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
:
CondIndep m (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) hm μ
theorem
ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
theorem
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
Kolmogorov's 0-1 law : any event in the tail σ-algebra of an independent sequence of
sub-σ-algebras has probability 0 or 1.
The tail σ-algebra limsup s atTop is the same as ⋂ n, ⋃ i ≥ n, s i.
theorem
ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atTop
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
@[deprecated ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atTop (since := "2025-01-21")]
theorem
ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atTop
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
Alias of ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atTop.
theorem
ProbabilityTheory.Kernel.indep_limsup_atBot_self
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
:
Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) κ μα
theorem
ProbabilityTheory.indep_limsup_atBot_self
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
:
Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) μ
theorem
ProbabilityTheory.condIndep_limsup_atBot_self
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
:
CondIndep m (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) hm μ
theorem
ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{κ : Kernel α Ω}
{μα : MeasureTheory.Measure α}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s κ μα)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
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
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iIndep s μ)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
Kolmogorov's 0-1 law : any event in the tail σ-algebra of an independent sequence of sub-σ-algebras has probability 0 or 1.
theorem
ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
Kolmogorov's 0-1 law, conditional version: any event in the tail σ-algebra of a conditionally independent sequence of sub-σ-algebras has conditional probability 0 or 1.
@[deprecated ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot (since := "2025-01-21")]
theorem
ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atBot
{Ω : Type u_2}
{ι : Type u_3}
{s : ι → MeasurableSpace Ω}
{m m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : iCondIndep m hm s μ)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
Alias of ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot.
Kolmogorov's 0-1 law, conditional version: any event in the tail σ-algebra of a conditionally independent sequence of sub-σ-algebras has conditional probability 0 or 1.