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 Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μα : MeasureTheory.Measure α}
{t : Set Ω}
(h_indep : ProbabilityTheory.kernel.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 : ProbabilityTheory.IndepSet t t)
:
theorem
ProbabilityTheory.kernel.measure_eq_zero_or_one_of_indepSet_self
{α : Type u_1}
{Ω : Type u_2}
{_mα : MeasurableSpace α}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μα : MeasureTheory.Measure α}
[∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)]
{t : Set Ω}
(h_indep : ProbabilityTheory.kernel.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 : ProbabilityTheory.IndepSet t t)
:
theorem
ProbabilityTheory.condexp_eq_zero_or_one_of_condIndepSet_self
{Ω : Type u_2}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[hμ : MeasureTheory.IsFiniteMeasure μ]
{t : Set Ω}
(ht : MeasurableSet t)
(h_indep : ProbabilityTheory.CondIndepSet m hm t t)
:
∀ᵐ (ω : Ω) ∂μ,
MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 0 ∨ MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 1
theorem
ProbabilityTheory.kernel.indep_biSup_compl
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μα : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.iIndep s κ)
(t : Set ι)
:
ProbabilityTheory.kernel.Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) κ
theorem
ProbabilityTheory.indep_biSup_compl
{Ω : Type u_2}
{ι : Type u_3}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(t : Set ι)
:
ProbabilityTheory.Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n)
theorem
ProbabilityTheory.condIndep_biSup_compl
{Ω : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
(t : Set ι)
:
ProbabilityTheory.CondIndep m (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) hm
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 α}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μα : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
{p : Set ι → Prop}
{f : Filter ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.iIndep s κ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
{t : Set ι}
(ht : p t)
:
ProbabilityTheory.kernel.Indep (⨆ n ∈ t, s n) (Filter.limsup s f) κ
theorem
ProbabilityTheory.indep_biSup_limsup
{Ω : Type u_2}
{ι : Type u_3}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{p : Set ι → Prop}
{f : Filter ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
{t : Set ι}
(ht : p t)
:
ProbabilityTheory.Indep (⨆ n ∈ t, s n) (Filter.limsup s f)
theorem
ProbabilityTheory.condIndep_biSup_limsup
{Ω : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
{p : Set ι → Prop}
{f : Filter ι}
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
{t : Set ι}
(ht : p t)
:
ProbabilityTheory.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 α✝}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α✝ Ω)}
{μα : MeasureTheory.Measure α✝}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.iIndep s κ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
:
ProbabilityTheory.kernel.Indep (⨆ (a : α), ⨆ n ∈ ns a, s n) (Filter.limsup s f) κ
theorem
ProbabilityTheory.indep_iSup_directed_limsup
{Ω : Type u_2}
{ι : Type u_3}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
:
ProbabilityTheory.Indep (⨆ (a : α), ⨆ n ∈ ns a, s n) (Filter.limsup s f)
theorem
ProbabilityTheory.condIndep_iSup_directed_limsup
{Ω : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
:
ProbabilityTheory.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 α✝}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α✝ Ω)}
{μα : MeasureTheory.Measure α✝}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.iIndep s κ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a)
:
ProbabilityTheory.kernel.Indep (⨆ (n : ι), s n) (Filter.limsup s f) κ
theorem
ProbabilityTheory.indep_iSup_limsup
{Ω : Type u_2}
{ι : Type u_3}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a)
:
ProbabilityTheory.Indep (⨆ (n : ι), s n) (Filter.limsup s f)
theorem
ProbabilityTheory.condIndep_iSup_limsup
{Ω : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a)
:
ProbabilityTheory.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 α✝}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α✝ Ω)}
{μα : MeasureTheory.Measure α✝}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.iIndep s κ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a)
:
ProbabilityTheory.kernel.Indep (Filter.limsup s f) (Filter.limsup s f) κ
theorem
ProbabilityTheory.indep_limsup_self
{Ω : Type u_2}
{ι : Type u_3}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a)
:
ProbabilityTheory.Indep (Filter.limsup s f) (Filter.limsup s f)
theorem
ProbabilityTheory.condIndep_limsup_self
{Ω : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a)
:
ProbabilityTheory.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 α✝}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α✝ Ω)}
{μα : MeasureTheory.Measure α✝}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.iIndep s κ)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) 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}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) 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}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
{α : Type u_4}
{p : Set ι → Prop}
{f : Filter ι}
{ns : α → Set ι}
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
(hf : ∀ (t : Set ι), p t → tᶜ ∈ f)
(hns : Directed (fun (x x_1 : Set ι) => x ≤ x_1) ns)
(hnsp : ∀ (a : α), p (ns a))
(hns_univ : ∀ (n : ι), ∃ (a : α), n ∈ ns a)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
∀ᵐ (ω : Ω) ∂μ,
MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 0 ∨ MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 1
theorem
ProbabilityTheory.kernel.indep_limsup_atTop_self
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μα : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.iIndep s κ)
:
ProbabilityTheory.kernel.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) κ
theorem
ProbabilityTheory.indep_limsup_atTop_self
{Ω : Type u_2}
{ι : Type u_3}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
:
ProbabilityTheory.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop)
theorem
ProbabilityTheory.condIndep_limsup_atTop_self
{Ω : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
:
ProbabilityTheory.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 α}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μα : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.iIndep s κ)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
theorem
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop
{Ω : Type u_2}
{ι : Type u_3}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.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}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
[SemilatticeSup ι]
[NoMaxOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
∀ᵐ (ω : Ω) ∂μ,
MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 0 ∨ MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 1
theorem
ProbabilityTheory.kernel.indep_limsup_atBot_self
{α : Type u_1}
{Ω : Type u_2}
{ι : Type u_3}
{_mα : MeasurableSpace α}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μα : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.iIndep s κ)
:
ProbabilityTheory.kernel.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) κ
theorem
ProbabilityTheory.indep_limsup_atBot_self
{Ω : Type u_2}
{ι : Type u_3}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iIndep s)
:
ProbabilityTheory.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot)
theorem
ProbabilityTheory.condIndep_limsup_atBot_self
{Ω : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
:
ProbabilityTheory.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 α}
{m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)}
{μα : MeasureTheory.Measure α}
[ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.kernel.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}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{s : ι → MeasurableSpace Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.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}
{m : MeasurableSpace Ω}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{s : ι → MeasurableSpace Ω}
[SemilatticeInf ι]
[NoMinOrder ι]
[Nonempty ι]
[StandardBorelSpace Ω]
[Nonempty Ω]
(hm : m ≤ m0)
[MeasureTheory.IsFiniteMeasure μ]
(h_le : ∀ (n : ι), s n ≤ m0)
(h_indep : ProbabilityTheory.iCondIndep m hm s)
{t : Set Ω}
(ht_tail : MeasurableSet t)
:
∀ᵐ (ω : Ω) ∂μ,
MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 0 ∨ MeasureTheory.condexp m μ (Set.indicator t fun (ω : Ω) => 1) ω = 1
Kolmogorov's 0-1 law, conditional version: any event in the tail σ-algebra of a conditinoally independent sequence of sub-σ-algebras has conditional probability 0 or 1.