ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop
theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop :
∀ {Ω : Type u_2} {ι : Type u_3} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
[inst : MeasureTheory.IsProbabilityMeasure μ] {s : ι → MeasurableSpace Ω} [inst : SemilatticeSup ι]
[inst_1 : NoMaxOrder ι] [inst_2 : Nonempty ι],
(∀ (n : ι), s n ≤ m0) → ProbabilityTheory.iIndep s μ → ∀ {t : Set Ω}, MeasurableSet t → ↑↑μ t = 0 ∨ ↑↑μ t = 1
**Kolmogorov's 0-1 Law** - This theorem states that for any given set `Ω` of outcomes, a sequence `ι`, a measurable space `m0` on `Ω`, a measure `μ` on `Ω` that is a probability measure, a sequence `s` of measurable spaces on `Ω`, under the conditions that `ι` has a semilattice sup (least upper bound) structure, `ι` has no maximum element and `ι` is nonempty. If for all `n` in `ι`, `s n` is a subset of `m0`, and the sequence `s` is independent respect to the measure `μ`, then for any set `t` of outcomes that is a measurable set, the measure of `t` under `μ` is either 0 or 1. In other words, 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`.
More concisely: In a probability space with an independent sequence of sub-σ-algebras having no maximum element and no least upper bound, any event in the tail σ-algebra has a measure of either 0 or 1.
|
ProbabilityTheory.kernel.indep_limsup_atTop_self
theorem ProbabilityTheory.kernel.indep_limsup_atTop_self :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μα : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω} [inst : SemilatticeSup ι] [inst_1 : NoMaxOrder ι] [inst_2 : Nonempty ι],
(∀ (n : ι), s n ≤ m0) →
ProbabilityTheory.kernel.iIndep s κ μα →
ProbabilityTheory.kernel.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) κ μα
This theorem, `ProbabilityTheory.kernel.indep_limsup_atTop_self`, states that for any types `α`, `Ω`, and `ι`, with associated measurable spaces `_mα` and `m0`, and any probability kernel `κ` from `α` to `Ω`, and a measure `μα` on `α`, if `κ` is a Markov kernel, and `s` is a function from `ι` to the measurable space `Ω`, with `ι` being a semilattice sup (it has an associative, commutative, and idempotent binary operation) and having no maximum order, and also, `ι` is nonempty, if every `s n` is less than or equal to `m0`, and the family of measurable space structures `s` is independent with respect to `κ` and `μα`, then, the `limsup` of `s` as `ι` goes to infinity in both arguments of the `Indep` predicate (which states a certain form of independence) is also independent with respect to `κ` and `μα`. This theorem essentially shows that the independence of the family of measurable space structures `s` is preserved under the limit superior operation as `ι` goes to infinity.
More concisely: If `κ` is a Markov kernel from measurable spaces `α` to `Ω`, `μα` is a measure on `α`, `ι` is a semilattice sup without maximum, `s` is a family of measurable functions from `ι` to `Ω` with `s n ≤ m0` for all `n`, and `s` is independent of `κ` and `μα` for all `n`, then `limsup s` is independent of `κ` and `μα`.
|
ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atBot
theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atBot :
∀ {Ω : Type u_2} {ι : Type u_3} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → MeasurableSpace Ω}
[inst : SemilatticeInf ι] [inst_1 : NoMinOrder ι] [inst_2 : Nonempty ι] [inst_3 : StandardBorelSpace Ω]
[inst_4 : Nonempty Ω] (hm : m ≤ m0) [inst_5 : MeasureTheory.IsFiniteMeasure μ],
(∀ (n : ι), s n ≤ m0) →
ProbabilityTheory.iCondIndep m hm s μ →
∀ {t : Set Ω},
MeasurableSet t →
∀ᵐ (ω : Ω) ∂μ,
MeasureTheory.condexp m μ (t.indicator fun ω => 1) ω = 0 ∨
MeasureTheory.condexp m μ (t.indicator fun ω => 1) ω = 1
**Kolmogorov's 0-1 law, conditional version**: This theorem states that for any conditionally independent sequence of sub-sigma-algebras, any event in the tail sigma-algebra has a conditional probability of either 0 or 1. More precisely, given a set `Ω`, an index set `ι`, two measurable spaces `m` and `m0` with `m` being a sub-sigma-algebra of `m0`, a measure `μ`, and a sequence of measurable spaces `s` indexed by `ι`, if every measurable space `s(n)` is a sub-sigma-algebra of `m0` and the sequence `s` is conditionally independent, then for every measurable set `t` in `Ω`, it holds almost everywhere that the conditional expectation of `t` (with the indicator function applied) is either 0 or 1.
More concisely: If `Ω` is a probability space, `μ` is a probability measure, `m0` is a sub-σ-algebra of `μ`, `{s(n): n ∈ ι}` is a sequence of sub-σ-algebras of `m0` that are conditionally independent given `m`, then for any measurable set `t` in `Ω`, the conditional expectation of `t`'s indicator function with respect to `m0` is almost everywhere equal to either 0 or 1.
|
ProbabilityTheory.kernel.indep_limsup_atBot_self
theorem ProbabilityTheory.kernel.indep_limsup_atBot_self :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μα : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω} [inst : SemilatticeInf ι] [inst_1 : NoMinOrder ι] [inst_2 : Nonempty ι],
(∀ (n : ι), s n ≤ m0) →
ProbabilityTheory.kernel.iIndep s κ μα →
ProbabilityTheory.kernel.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) κ μα
This theorem states that for any types `α`, `Ω`, and `ι`, with `α` as a measurable space, `Ω` as a measurable space `m0`, and `κ` as an element of the kernel from `α` to `Ω`, and given a measure `μα` on `α`. If `κ` is a Markov kernel, and `s` is a function from `ι` to the measurable space `Ω`, where `ι` is a semilattice with the infimum operation and has no minimum element but is nonempty. If for all `n` in `ι`, `s n` is less than or equal to `m0`, and the family of measurable spaces `s` is independent with respect to the kernel `κ` and the measure `μα`, then the limsup of `s` at negative infinity is independent with respect to the kernel `κ` and the measure `μα`. Here, `limsup` of a function along a filter is the infimum of the `a` such that, eventually for the filter, `u x ≤ a` holds, and `atBot` is the filter representing the limit towards negative infinity.
More concisely: Given a measurable space `α`, a measurable space `Ω` with measure `m0`, a Markov kernel `κ` from `α` to `Ω`, a semilattice `ι` with no minimum element, a function `s: ι -> Ω`, measurable with respect to `κ` and `μα`, and `s(n) <= m0` for all `n` in `ι`, if `s` is independent under `κ` and `μα`, then the limsup of `s` with respect to the filter at negative infinity is independent of `κ` and `μα`.
|
Mathlib.Probability.Independence.ZeroOne._auxLemma.2
theorem Mathlib.Probability.Independence.ZeroOne._auxLemma.2 : ∀ {α : Type u} (s : Set α) (x : α), (x ∈ sᶜ) = (x ∉ s)
This theorem, named `Mathlib.Probability.Independence.ZeroOne._auxLemma.2`, states that for any type `α` and for any set `s` of type `α` and any element `x` of type `α`, `x` being a member of the complement of set `s` is equivalent to `x` not belonging to the set `s`. In mathematical notation, if `s` is a set and `x` is an element, then `x` being in the complement of `s` (denoted as `x ∈ sᶜ`) is the same as `x` not being in `s` (denoted as `x ∉ s`).
More concisely: The complement of a set is the set of all elements not in the original set. In Lean, this is formalized as `x ∈ sᶜ ↔ x ∉ s` for any type `α` and set `s` of type `α`.
|
ProbabilityTheory.kernel.measure_eq_zero_or_one_of_indepSet_self
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 α}
[inst : ∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)] {t : Set Ω},
ProbabilityTheory.kernel.IndepSet t t κ μα → ∀ᵐ (a : α) ∂μα, ↑↑(κ a) t = 0 ∨ ↑↑(κ a) t = 1
This theorem, `measure_eq_zero_or_one_of_indepSet_self` in `ProbabilityTheory.kernel`, asserts that for any given type `α` and `Ω` with their respective measurable spaces `_mα` and `m0`, any kernel `κ` which maps from `α` to `Ω`, any measure `μα` on `α` such that for every element `a` in `α` the measure `(κ a)` is finite, and any set `t` in `Ω`, if `t` is independent with itself under the kernel `κ` and the measure `μα`, then almost every `a` in `α` under measure `μα` has the property that the measure of `t` under `(κ a)` is either `0` or `1`. In other words, if a set is independent with itself in a probability space, then the probability of the event corresponding to that set must be either 0 or 1 for almost all outcomes.
More concisely: Given a measurable space `(α,_mα)`, a kernel `κ : α → Ω`, a finite measure `μα` on `α`, and a κ-independent and μα-measurable set `t` in `Ω`, almost every `a` in `α` has `μα` measure 0 or 1 for the measure of `t` under `κ(a)`.
|
ProbabilityTheory.kernel.indep_biSup_compl
theorem ProbabilityTheory.kernel.indep_biSup_compl :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μα : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω},
(∀ (n : ι), s n ≤ m0) →
ProbabilityTheory.kernel.iIndep s κ μα →
∀ (t : Set ι), ProbabilityTheory.kernel.Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) κ μα
This theorem, `ProbabilityTheory.kernel.indep_biSup_compl`, states that for any types `α`, `Ω`, and `ι`, a measurable space `_mα`, a measurable space `m0`, a kernel `κ` from the probability theory, a measure `μα`, a Markov kernel instance, and a function `s` mapping `ι` to `MeasurableSpace Ω` such that each `s n` is less than or equal to `m0`, if the family of measurable space structures is independent with respect to kernel `κ` and measure `μα`, then for any set `t` of type `ι`, the sup (supremum) of `s n` for each `n` in `t` is independent with the sup of `s n` for each `n` in the complement of `t` with respect to the kernel `κ` and measure `μα`. This is a theorem in the field of probability theory dealing with measure theory and Markov kernels.
More concisely: If `κ` is a probability kernel, `μα` is a measure, `s` maps `ι` to measurable spaces `Ω` with each `s n` less than or equal to `m0`, and the family of measurable spaces `{s n : n ∈ ι}` is independent with respect to `κ` and `μα`, then the supremum of `s n` for `n` in any subset `t` of `ι` is independent of the supremum of `s n` for `n` in the complement of `t` with respect to `κ` and `μα`.
|
ProbabilityTheory.kernel.measure_zero_or_one_of_measurableSet_limsup_atBot
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 α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω} [inst : SemilatticeInf ι] [inst_1 : NoMinOrder ι] [inst_2 : Nonempty ι],
(∀ (n : ι), s n ≤ m0) →
ProbabilityTheory.kernel.iIndep s κ μα →
∀ {t : Set Ω}, MeasurableSet t → ∀ᵐ (a : α) ∂μα, ↑↑(κ a) t = 0 ∨ ↑↑(κ a) t = 1
**Kolmogorov's 0-1 Law (Kernel Version)**: Given a measurable space `α` and a set of outcomes `Ω`, along with an indexing type `ι`, and a family of sub-σ-algebras `s` indexed by `ι`, this theorem states that for any sequence of these sub-σ-algebras that forms an independent family with respect to a Markov kernel `κ` and a measure `μα`, any event in the tail σ-algebra of this sequence has a probability of either 0 or 1 almost surely. This holds for any event `t` that is a measurable set under the measure `μα`. This version of the theorem is particularly apt for measure-theoretical probability and stochastic processes.
More concisely: Given a measurable space `α`, a set of outcomes `Ω`, an indexing type `ι`, a family of sub-σ-algebras `s` indexed by `ι`, a measure `μα`, and a Markov kernel `κ`: if `s` is independent under `κ` and `μα`, then any event in the tail σ-algebra has a probability of either 0 or 1 almost surely for all measurable sets under `μα`.
|
ProbabilityTheory.kernel.indep_iSup_directed_limsup
theorem ProbabilityTheory.kernel.indep_iSup_directed_limsup :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μα : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω} {α_1 : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : α_1 → Set ι},
(∀ (n : ι), s n ≤ m0) →
ProbabilityTheory.kernel.iIndep s κ μα →
(∀ (t : Set ι), p t → tᶜ ∈ f) →
Directed (fun x x_1 => x ≤ x_1) ns →
(∀ (a : α_1), p (ns a)) →
ProbabilityTheory.kernel.Indep (⨆ a, ⨆ n ∈ ns a, s n) (Filter.limsup s f) κ μα
This theorem establishes a condition for independence in the context of probability theory and measure theory. Specifically, it states that for any given types `α`, `Ω`, `ι`, and `α_1`, and given a measurable space structure on `α`, a specific measurable space `m0` on `Ω`, a kernel `κ`, a measure `μα` on `α`, a family of measurable spaces `s` indexed by `ι`, a property `p` on sets of `ι`, a filter `f` on `ι`, and a function `ns` mapping elements of `α_1` to sets of `ι`, if the following conditions are satisfied:
- Each measurable space `s n` is a subset of `m0`,
- The family `s` is independent with respect to the kernel `κ` and the measure `μα`,
- For every set `t` of `ι` satisfying property `p`, the complement of `t` belongs to the filter `f`,
- The function `ns` is directed with respect to the order relation `≤` on sets of `ι`, and
- For each element `a` of `α_1`, the set `ns a` satisfies property `p`,
then it follows that the family of measurable spaces generated by taking the suprema over all `a` and `n` in the set `ns a` of the spaces `s n`, is independent with respect to the kernel `κ` and the measure `μα`, where the measure is the limit superior of `s` along the filter `f`. This relates concepts from order theory, filter theory, and measure theory, establishing a relationship between directed sets, limit superior, independence, and suprema in the context of measurable spaces and probability kernels.
More concisely: Given measurable spaces `α`, `Ω`, `ι`, `α_1`, a measurable space structure on `α`, a measurable space `m0` on `Ω`, a kernel `κ`, a measure `μα` on `α`, a family `s` of measurable spaces indexed by `ι`, a property `p` on sets of `ι`, a filter `f` on `ι`, and a function `ns` mapping elements of `α_1` to sets of `ι`, if conditions 1-5 hold, then the family of measurable spaces generated by the suprema of `s n` over all `a` in `α_1` and `n` in `ns a` is independent with respect to `κ` and `μα`, and is the limit superior of `s` along `f`.
|
ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot
theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot :
∀ {Ω : Type u_2} {ι : Type u_3} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
[inst : MeasureTheory.IsProbabilityMeasure μ] {s : ι → MeasurableSpace Ω} [inst : SemilatticeInf ι]
[inst_1 : NoMinOrder ι] [inst_2 : Nonempty ι],
(∀ (n : ι), s n ≤ m0) → ProbabilityTheory.iIndep s μ → ∀ {t : Set Ω}, MeasurableSet t → ↑↑μ t = 0 ∨ ↑↑μ t = 1
The theorem, known as "Kolmogorov's 0-1 Law", states that for any given event in the tail σ-algebra of an independent sequence of sub-σ-algebras, the event's probability is either 0 or 1. This assertion holds under the conditions that the sequence of measurable spaces `s` is less than or equal to an initial measurable space `m0` for every index `n` in an index set `ι`, the measure `μ` is a probability measure, and the set `t` is measurable. This theorem is a fundamental result in probability theory, illustrating the extreme behavior of events that are 'far in the future' in the context of independent sequences of random variables or events.
More concisely: The probability of any event in the tail σ-algebra of an independent sequence of sub-σ-algebras, under the conditions that the sequence of measurable spaces is less than or equal to an initial measurable space for every index, the measure is a probability measure, and the set is measurable, is either 0 or 1.
|
ProbabilityTheory.kernel.indep_iSup_limsup
theorem ProbabilityTheory.kernel.indep_iSup_limsup :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μα : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω} {α_1 : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : α_1 → Set ι},
(∀ (n : ι), s n ≤ m0) →
ProbabilityTheory.kernel.iIndep s κ μα →
(∀ (t : Set ι), p t → tᶜ ∈ f) →
Directed (fun x x_1 => x ≤ x_1) ns →
(∀ (a : α_1), p (ns a)) →
(∀ (n : ι), ∃ a, n ∈ ns a) → ProbabilityTheory.kernel.Indep (⨆ n, s n) (Filter.limsup s f) κ μα
This theorem, `ProbabilityTheory.kernel.indep_iSup_limsup`, in the context of probability theory, states that given a measurable space `α`, a sample space `Ω`, an index set `ι`, a Markov kernel `κ` from `α` to `Ω`, a measure `μα` on `α`, a family of measurable spaces `s` indexed by `ι`, a certain property `p` on sets of `ι`, a filter `f` on `ι`, and a directed family of sets `ns` of `ι`: If for all index `n` the measurable space `s n` is a subset of some base measurable space `m0`, and the family of measurable spaces `s` is independent with respect to kernel `κ` and measure `μα`, and the complement of any set `t` satisfying property `p` belongs to the filter `f`, and all sets in `ns` satisfy property `p`, and for all index `n` there exists a set in `ns` that contains `n`, then the measurable space generated by the supremum of all `s n` and the limit superior (limsup) of `s` along the filter `f` are independent with respect to the kernel `κ` and the measure `μα`.
More concisely: Given a Markov kernel, measure, independent family of sub-σ-algebras, filter, and property, if the sub-σ-algebras are contained in a base measurable space, satisfy the property, and have the given intersection and limit superior properties, then they are independent with respect to the kernel and measure.
|
ProbabilityTheory.kernel.indep_biSup_limsup
theorem ProbabilityTheory.kernel.indep_biSup_limsup :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μα : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω} {p : Set ι → Prop} {f : Filter ι},
(∀ (n : ι), s n ≤ m0) →
ProbabilityTheory.kernel.iIndep s κ μα →
(∀ (t : Set ι), p t → tᶜ ∈ f) →
∀ {t : Set ι}, p t → ProbabilityTheory.kernel.Indep (⨆ n ∈ t, s n) (Filter.limsup s f) κ μα
This theorem is a statement in probability theory and measure theory, specifically relating to concepts of independent sets, limsup, and kernels. The theorem states that for all types `α`, `Ω`, and `ι`, given a measurable space `α`, another measurable space `m0` of type `Ω`, a kernel `κ` from the measurable space `α` to `Ω`, a measure `μα` on `α`, and the kernel `κ` being a Markov kernel, if you have a collection of measurable spaces `s` indexed by `ι`, a property `p` on sets of indices, and a filter `f` on `ι`, then under the conditions that each measurable space `s[n]` is a subspace of `m0`, the collection of measurable spaces `s` is independent with respect to the kernel and measure, and the complement of any set `t` satisfying property `p` belongs to the filter `f`, then for any such set `t`, the kernel independence of the superset of measurable spaces indexed by elements in `t` and the limsup of the sequence of measurable spaces along the filter `f` holds with respect to the kernel and measure.
More concisely: Given a measurable space `α`, a Markov kernel `κ` from `α` to another measurable space `m0`, a measure `μα` on `α`, a collection of subspaces `s[n]` of `m0` indexed by `ι`, a filter `f` on `ι`, and a property `p` on sets of indices, if each `s[n]` is independent of the limsup of `s` along `f` with respect to `κ` and `μα`, and the complement of any set `t` satisfying `p` belongs to `f`, then the same independence holds for the superset of `s[n]` indexed by elements in `t`.
|
ProbabilityTheory.kernel.indep_limsup_self
theorem ProbabilityTheory.kernel.indep_limsup_self :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μα : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{s : ι → MeasurableSpace Ω} {α_1 : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : α_1 → Set ι},
(∀ (n : ι), s n ≤ m0) →
ProbabilityTheory.kernel.iIndep s κ μα →
(∀ (t : Set ι), p t → tᶜ ∈ f) →
Directed (fun x x_1 => x ≤ x_1) ns →
(∀ (a : α_1), p (ns a)) →
(∀ (n : ι), ∃ a, n ∈ ns a) →
ProbabilityTheory.kernel.Indep (Filter.limsup s f) (Filter.limsup s f) κ μα
This theorem, `ProbabilityTheory.kernel.indep_limsup_self`, says that for all types `α`, `Ω`, and `ι`, and given a measurable space `α`, a measurable space `Ω`, a kernel `κ` belonging to the set of probability theory kernels between `α` and `Ω`, a measure `μα` on `α`, and a function `s` that maps `ι` to measurable spaces `Ω`, if every measurable space `s(n)` is a subset of `m0`, and the kernel is independent with respect to this family of measurable spaces `s`, and for another type `α_1`, a property `p` on sets of `ι`, a filter `f` on `ι`, and a function `ns` mapping `α_1` to sets of `ι`, if every complement of a set on which `p` holds belongs to the filter `f`, and the function `ns` is directed by the less than or equal to relation, and the property `p` holds for all sets `ns(a)`, and for every `n` in `ι` there exists an `a` such that `n` is an element of `ns(a)`, then the limit superior of the function `s` along the filter `f` is independent with respect to the kernel and the measure.
In other words, this theorem deals with the independence properties of limit superior of measurable spaces along a filter in the context of probability theory. Limit superior is a limit-like quantity that measures the "eventual" upper bound of a sequence of real numbers. The set of assumptions lays the groundwork for understanding how these measurable spaces, kernels, and measures interact under the conditions specified.
More concisely: Given a probability theory kernel, a measure, a family of measurable spaces, a filter on indices, and a function mapping indices to sets such that the property `p` holds for the sets and the limit superior exists, if the kernel is independent with respect to the family of measurable spaces and the filter satisfies certain conditions, then the limit superior is independent with respect to the kernel and the measure.
|