ProbabilityTheory.kernel.indepSets_piiUnionInter_of_disjoint
theorem ProbabilityTheory.kernel.indepSets_piiUnionInter_of_disjoint :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{s : ι → Set (Set Ω)} {S T : Set ι},
ProbabilityTheory.kernel.iIndepSets s κ μ →
Disjoint S T → ProbabilityTheory.kernel.IndepSets (piiUnionInter s S) (piiUnionInter s T) κ μ
This theorem, `ProbabilityTheory.kernel.indepSets_piiUnionInter_of_disjoint`, states that for any types `α`, `Ω`, and `ι`, measurable spaces `_mα` and `_mΩ`, a kernel `κ` of type `ProbabilityTheory.kernel α Ω`, a measure `μ` of type `MeasureTheory.Measure α`, a family of sets `s` of type `ι → Set (Set Ω)`, and two sets `S` and `T` of type `Set ι`, if the family of sets `s` is independent with respect to the kernel `κ` and the measure `μ`, and if the sets `S` and `T` are disjoint, then the sets formed by the union and intersection of `s` with `S` and `s` with `T` are independent with respect to the kernel `κ` and the measure `μ`. This theorem allows us to extend the concept of independence from a family of sets to more complex structures formed by unions and intersections, provided the original sets are disjoint.
More concisely: If `κ` is a kernel, `μ` is a measure, `s` is an independent family of sets, and `S` and `T` are disjoint sets, then the sets `s ∩ S`, `s ∩ T`, `(s ∩ S) ∪ (s ∩ T)`, and `s ∩ (S ∪ T)` are independent with respect to `κ` and `μ`.
|
ProbabilityTheory.kernel.Indep.symm
theorem ProbabilityTheory.kernel.Indep.symm :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ _mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α},
ProbabilityTheory.kernel.Indep m₁ m₂ κ μ → ProbabilityTheory.kernel.Indep m₂ m₁ κ μ
This theorem states that in probability theory, the independence of two measurable spaces with respect to a kernel and a measure is symmetric. Given two measurable spaces `m₁` and `m₂`, a measurable space `α` with its corresponding measure `μ`, and a kernel `κ` from `α` to `Ω` (the outcome space), if `m₁` and `m₂` are independent with respect to `κ` and `μ`, then `m₂` and `m₁` are also independent with respect to `κ` and `μ`.
More concisely: If measurable spaces `m₁` and `m₂` are independent with respect to a kernel `κ` and measure `μ`, then `m₂` and `m₁` are also independent with respect to `κ` and `μ`.
|
ProbabilityTheory.kernel.indep_of_indep_of_le_right
theorem ProbabilityTheory.kernel.indep_of_indep_of_le_right :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ m₃ _mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α},
ProbabilityTheory.kernel.Indep m₁ m₂ κ μ → m₃ ≤ m₂ → ProbabilityTheory.kernel.Indep m₁ m₃ κ μ
This theorem from Probability Theory states that for any types `α` and `Ω`, given measurable spaces `_mα`, `m₁`, `m₂`, `m₃`, and `_mΩ`, a kernel `κ` from `α` to `Ω`, and a measure `μ` on `α`, if the kernel `κ` is independent of the measurable space `m₂` with respect to measure `μ` and `m₁`, and if `m₃` is a sub-measurable space of `m₂` (i.e., `m₃ ≤ m₂`), then `κ` is also independent of `m₃` with respect to measure `μ` and `m₁`. In other words, the independence of a kernel of measurable spaces is preserved when the independent space is reduced to a sub-space.
More concisely: If a kernel is independent of a measurable space with respect to a measure, and the smaller measurable space is a sub-measurable space of the larger one, then the kernel is also independent of the smaller measurable space with respect to the same measure.
|
ProbabilityTheory.kernel.indepSet_empty_right
theorem ProbabilityTheory.kernel.indepSet_empty_right :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
(s : Set Ω), ProbabilityTheory.kernel.IndepSet s ∅ κ μ
This theorem states that for any given type `α` and `Ω` with their measurable spaces `_mα` and `_mΩ`, any member `κ` of the probability kernel from `α` to `Ω`, any measure `μ` on `α`, and any set `s` of type `Ω`, the set `s` is independent of the empty set under the probability kernel `κ` and the measure `μ`. This holds true when `κ` is a Markov kernel. In terms of probability theory, this means that the event represented by the set `s` is independent of no event (the empty set), under the given probability measure and Markov transition kernel.
More concisely: For any Markov kernel κ from type α to Ω, measure μ on α, and set s of type Ω, the empty set is independent of s under κ and μ, meaning μ(κ⁻¹(s) ∩ ∅) = 0.
|
ProbabilityTheory.kernel.iIndepFun.indepFun_sub_left
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_sub_left :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
[inst : Sub β] [inst_1 : MeasurableSub₂ β] {f : ι → Ω → β} [inst_2 : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ μ →
(∀ (i : ι), Measurable (f i)) →
∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.kernel.IndepFun (f i - f j) (f k) κ μ
This theorem, `ProbabilityTheory.kernel.iIndepFun.indepFun_sub_left`, states that in the context of probability theory, given a measurable space `α`, an underlying sample space `Ω`, an index type `ι`, a kernel `κ` of type `ProbabilityTheory.kernel α Ω`, a measure `μ` on `α`, and a type `β` equipped with a measurable space, a subtraction operation, and a measurable subtraction operation, if every function `f` from `ι` to `Ω` to `β` is measurable and `κ` is a Markov kernel, then if `f` is independent of the kernel `κ` under measure `μ` in the sense of `ProbabilityTheory.kernel.iIndepFun`, then for any three distinct indices `i`, `j`, and `k` from `ι`, the function `f i - f j` is independent of `f k` under the kernel `κ` and the measure `μ` in the sense of `ProbabilityTheory.kernel.IndepFun`.
In simpler terms, this theorem is about the preservation of independence in a certain sense under subtraction for a family of functions in the setting of probability theory involving Markov kernels.
More concisely: Given a measurable space, a kernel, a measure, and a type with measurable subtraction, if every measurable function from the index type to the type is independent of the kernel under measure and the kernel is Markov, then for any three distinct indices, the difference of the functions is independent of the third function under the kernel and the measure.
|
ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_le
theorem ProbabilityTheory.kernel.iIndepSet.indep_generateFrom_le :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} [inst : LinearOrder ι]
[inst_1 : ProbabilityTheory.IsMarkovKernel κ] {s : ι → Set Ω},
(∀ (n : ι), MeasurableSet (s n)) →
ProbabilityTheory.kernel.iIndepSet s κ μ →
∀ (i : ι) {k : ι},
i < k →
ProbabilityTheory.kernel.Indep (MeasurableSpace.generateFrom {s k})
(MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}) κ μ
This theorem states that for all types `α`, `Ω`, `ι` equipped with measurable spaces `_mα`, `_mΩ` respectively, and any kernel `κ` from a probability theory, measure `μ` from measure theory and a family of sets `s` indexed by `ι`, if for all `n` in `ι`, `s n` is a measurable set and the family of sets `s` is independent, then for any `i` in `ι` and any `k` in `ι` such that `i` is less than `k`, the independence holds between the measure space generated by `{s k}` and the measure space generated by the set of all `t` such that there exists `j` less than or equal to `i` for which `s j` equals `t`. Here, the independence is in the context of a probability theory kernel and a measure from measure theory. The independence of a family of sets is defined by the independence of the family of measurable space structures they generate.
More concisely: Given measurable spaces `αm`, `Ωm`, a probability kernel `κ`, a measure `μ`, and a family `s` of measurable sets indexed by `ι` that is independent and has each member `sn` measurable, for all `i < k` in `ι`, the measure spaces generated by `{sk}` and `{t | ∃j ≤ i. sj = t}` are independent.
|
ProbabilityTheory.kernel.iIndepFun.indepFun_finset_prod_of_not_mem
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_finset_prod_of_not_mem :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
[inst : CommMonoid β] [inst_1 : MeasurableMul₂ β] {f : ι → Ω → β} [inst_2 : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ μ →
(∀ (i : ι), Measurable (f i)) →
∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.kernel.IndepFun (s.prod fun j => f j) (f i) κ μ
The theorem `ProbabilityTheory.kernel.iIndepFun.indepFun_finset_prod_of_not_mem` states that, given a probability kernel `κ` on measurable spaces `α` and `Ω`, a measure `μ` on `α`, a measurable space `β` with a commutative monoid structure and a measurable multiplication, a function `f` from `ι` to `Ω` to `β`, and a finset `s` of `ι`, if `κ` is a Markov kernel, `f` is measurable for every `ι`, and `f` is independent for every `x` in the measure space, then for every `i` in `ι` not in `s`, the function `f` at `i` is independent from the product of `f` at elements of `s`. This implies that the process defined by `f` has independent increments.
More concisely: If `κ` is a Markov kernel on measurable spaces `α` and `Ω`, `μ` is a measure on `α`, `β` is a commutative monoid with measurable multiplication, `f` is a measurable function from `ι` to `Ω` to `β`, `s` is a finset of `ι` such that `f(i)` is independent of the product of `f(j)` for all `j` in `s` and `i` not in `s`, then `f(i)` is independent of the product of `f(j)` for all `i` not in `s` and every choice of `j` in `s`.
|
ProbabilityTheory.kernel.iIndepFun.indepFun_prod_mk
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_prod_mk :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} [inst : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.iIndepFun m f κ μ →
(∀ (i : ι), Measurable (f i)) →
∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.kernel.IndepFun (fun a => (f i a, f j a)) (f k) κ μ
The theorem `ProbabilityTheory.kernel.iIndepFun.indepFun_prod_mk` states that in the context of probability theory with a Markov kernel `κ`, a measure `μ` and measurable spaces `α` and `Ω`, if we have a set of functions `f` from `Ω` to a family of types `β` indexed by `ι`, such that each function `f i` is measurable and the functions are independent with respect to the Markov kernel `κ` and measure `μ`, then for any three distinct indices `i`, `j` and `k` in `ι`, the function that maps `a` to the pair `(f i a, f j a)` is independent of the function `f k` with respect to the same Markov kernel and measure.
More concisely: If `κ` is a Markov kernel, `μ` is a measure, `α` and `Ω` are measurable spaces, `f: ι → β -> Ω -> Sort _` is a family of measurable functions from `Ω` to `β` indexed by `ι`, and `f i` and `f j` are independent for all distinct `i` and `j` in `ι` with respect to `κ` and `μ`, then the functions `(λ a: Ω, (f i a, f j a))` and `f k` are independent for all `k` distinct from `i` and `j`.
|
ProbabilityTheory.kernel.iIndep.indep
theorem ProbabilityTheory.kernel.iIndep.indep :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
{_mΩ : MeasurableSpace Ω} {κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α},
ProbabilityTheory.kernel.iIndep m κ μ → ∀ {i j : ι}, i ≠ j → ProbabilityTheory.kernel.Indep (m i) (m j) κ μ
The theorem `ProbabilityTheory.kernel.iIndep.indep` states that for any types `α`, `Ω`, and `ι`, and for any measure space over `α`, any function `m` from `ι` to a measure space over `Ω`, any measure space over `Ω`, any kernel `κ` from a probability theory over types `α` and `Ω`, and any measure `μ` over `α`, if the family of measurable space structures is independent with respect to the kernel `κ` and the measure `μ`, then for any distinct `i` and `j` in `ι`, the measurable spaces `m i` and `m j` are also independent with respect to the kernel `κ` and the measure `μ`.
More concisely: If a family of measurable spaces is independent with respect to a kernel and a measure, then any pair of distinct measurable spaces in the family are also independent with respect to that kernel and measure.
|
ProbabilityTheory.kernel.IndepSets.indep
theorem ProbabilityTheory.kernel.IndepSets.indep :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m1 m2 m : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{p1 p2 : Set (Set Ω)},
m1 ≤ m →
m2 ≤ m →
IsPiSystem p1 →
IsPiSystem p2 →
m1 = MeasurableSpace.generateFrom p1 →
m2 = MeasurableSpace.generateFrom p2 →
ProbabilityTheory.kernel.IndepSets p1 p2 κ μ → ProbabilityTheory.kernel.Indep m1 m2 κ μ
This theorem states that if we have two subsets (`p1` and `p2`) of the power set of a set `Ω` that are π-systems (i.e., for any two sets in the collection, their non-empty intersection is also in the collection) and independent with respect to a Markov kernel `κ` and a measure `μ`, then the measurable space structures generated by these π-systems are also independent with respect to the same kernel and measure.
In other words, if `p1` and `p2` define independent structures under the Markov kernel `κ` and the measure `μ`, then the measurable spaces created from `p1` and `p2` also maintain this independence under the same kernel and measure. Here, independence of two sets of sets means that for any sets selected from each set of sets, the kernel of their intersection equals the product of their individual kernels almost everywhere with respect to the measure `μ`.
More concisely: If two π-systems `p1` and `p2` of a measurable space `(Ω, Σ, μ)` are independent with respect to a Markov kernel `κ`, then the σ-algebras they generate are independent under `κ` and `μ`.
|
ProbabilityTheory.kernel.Indep.indepSet_of_measurableSet
theorem ProbabilityTheory.kernel.Indep.indepSet_of_measurableSet :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ m0 : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α},
ProbabilityTheory.kernel.Indep m₁ m₂ κ μ →
∀ {s t : Set Ω}, MeasurableSet s → MeasurableSet t → ProbabilityTheory.kernel.IndepSet s t κ μ
This theorem states that for any two types `α` and `Ω`, given measure spaces on both `α` and `Ω`, a kernel from `α` to `Ω`, and a measure on `α`, if the two measure spaces on `Ω` are independent with respect to the kernel and the measure, then for any two measurable sets in `Ω`, these two sets are independent. In other words, if the measure spaces generated by two sets are independent, then the sets themselves are independent in the sense of probability theory.
More concisely: If two measure spaces on types `Ω` are independent with respect to a kernel and a measure on type `α`, then any two measurable sets in `Ω` are independent events.
|
ProbabilityTheory.kernel.IndepFun.comp
theorem ProbabilityTheory.kernel.IndepFun.comp :
∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {γ : Type u_6} {γ' : Type u_7}
{_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ↥(ProbabilityTheory.kernel α Ω)}
{μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
{mγ : MeasurableSpace γ} {mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'},
ProbabilityTheory.kernel.IndepFun f g κ μ →
Measurable φ → Measurable ψ → ProbabilityTheory.kernel.IndepFun (φ ∘ f) (ψ ∘ g) κ μ
The theorem `ProbabilityTheory.kernel.IndepFun.comp` states that for all types α, Ω, β, β', γ, γ', given an appropriate measurable space for each type, a kernel κ, a measure μ, two functions f and g from Ω to β and Ω to β' respectively, and two measurable functions φ and ψ from β to γ and β' to γ' respectively, if the functions f and g are independent with respect to the kernel κ and the measure μ, then the composition of φ and f, and ψ and g are also independent with respect to the same kernel κ and measure μ. In other words, if f and g are independent, then their measurable transformations φ and ψ maintain this independence.
More concisely: If functions f and g are independent with respect to kernel κ and measure μ, then the compositions φ∘f and ψ∘g are also independent with respect to kernel κ and measure μ.
|
ProbabilityTheory.kernel.iIndepFun.indepFun_prod_mk_prod_mk
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_prod_mk_prod_mk :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} [inst : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.iIndepFun m f κ μ →
(∀ (i : ι), Measurable (f i)) →
∀ (i j k l : ι),
i ≠ k →
i ≠ l →
j ≠ k →
j ≠ l → ProbabilityTheory.kernel.IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) κ μ
This theorem, `indepFun_prod_mk_prod_mk`, states that for any types `α`, `Ω`, and `ι`, given a measurable space over `α` and `Ω`, a measure `μ` on `α`, a `κ` kernel on the measurable space over `α` and `Ω`, and a family of functions `{f : (i : ι) → Ω → β i}` on an index type `ι` and outputting in some type `β` where each `β i` has a measurable space structure, under the condition that `κ` is a Markov kernel, and the function `f` is independent with respect to the kernel `κ` and the measure `μ`, if all functions `f i` are measurable, then for any distinct indices `i`, `j`, `k`, `l` in `ι`, the functions `(f i a, f j a)` and `(f k a, f l a)` are mutually independent with respect to the kernel `κ` and the measure `μ`.
In the context of probability theory, this theorem is stating a property about independence of functions under certain conditions. In particular, it says that if we have a set of measurable functions that are independent with respect to a Markov kernel and a measure, then certain pairs of these functions, specified by distinct indices, will also be independent.
More concisely: If `κ` is a Markov kernel, `μ` is a measure, `α`, `Ω`, and `ι` are types, `f : ι → Ω → β i` is a family of measurable functions, and `κ` and `f` are independent with respect to `μ`, then for any distinct indices `i`, `j` in `ι`, the functions `f i` and `f j` are independent with respect to `κ` and `μ`.
|
ProbabilityTheory.kernel.indep_iSup_of_disjoint
theorem ProbabilityTheory.kernel.indep_iSup_of_disjoint :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{m : ι → MeasurableSpace Ω},
(∀ (i : ι), m i ≤ _mΩ) →
ProbabilityTheory.kernel.iIndep m κ μ →
∀ {S T : Set ι}, Disjoint S T → ProbabilityTheory.kernel.Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
The theorem `ProbabilityTheory.kernel.indep_iSup_of_disjoint` states that for every type `α`, `Ω`, and `ι`, and given a measurable space on `α` and `Ω`, a kernel `κ` in the probability theory, a measure `μ` on `α`, and a Markov kernel, and a function `m` which assigns a measurable space to each `ι`, if each measurable space `m i` is a sub-measurable space of `_mΩ` and the measurable spaces are independent with respect to the kernel `κ` and the measure `μ`, then for any two disjoint sets `S` and `T` of `ι`, the supremum of measurable spaces `m i` over `i` in `S` is independent of the supremum of measurable spaces `m i` over `i` in `T` with respect to the kernel `κ` and the measure `μ`. This is a result related to the independence of sigma-algebras in probability theory.
More concisely: If `κ` is a probability kernel, `μ` is a measure, `m` is a Markov kernel assigning sub-measurable spaces to each index `ι`, and the measurable spaces `m i` are independent with respect to `κ` and `μ` for all `ι` in disjoint sets `S` and `T`, then the supremum of `m i` over `i` in `S` is independent of the supremum of `m i` over `i` in `T` with respect to `κ` and `μ`.
|
ProbabilityTheory.kernel.IndepSets.union
theorem ProbabilityTheory.kernel.IndepSets.union :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ s₂ s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α},
ProbabilityTheory.kernel.IndepSets s₁ s' κ μ →
ProbabilityTheory.kernel.IndepSets s₂ s' κ μ → ProbabilityTheory.kernel.IndepSets (s₁ ∪ s₂) s' κ μ
The theorem `ProbabilityTheory.kernel.IndepSets.union` in probability theory states that given measurable spaces `α` and `Ω` with `α` being the type of the random variables and `Ω` the sample space, two collections of sets `s₁` and `s₂`, and a third collection of sets `s'`. If `s₁` and `s'` are independent with respect to a kernel `κ` and a measure `μ`, and if `s₂` and `s'` are also independent with respect to the same kernel and measure, then the union of `s₁` and `s₂` is independent with `s'` with respect to the same kernel and measure. In mathematical terms, independence here means that for all `t₁` in `s₁` (or `s₂`) and `t₂` in `s'`, almost everywhere in `a` with respect to measure `μ`, the kernel of `a` applied to the intersection of `t₁` and `t₂` equals the product of the kernel of `a` applied to `t₁` and `t₂` separately.
More concisely: If measurable collections of sets `s₁` and `s₂` are independent of a collection `s'` with respect to a kernel `κ` and measure `μ`, then the union of `s₁` and `s₂` is independent of `s'` with respect to `κ` and `μ`, meaning their intersections almost everywhere have kernels equal to the product of their individual kernels.
|
ProbabilityTheory.kernel.indepSets_of_indepSets_of_le_left
theorem ProbabilityTheory.kernel.indepSets_of_indepSets_of_le_left :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ s₂ s₃ : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α},
ProbabilityTheory.kernel.IndepSets s₁ s₂ κ μ → s₃ ⊆ s₁ → ProbabilityTheory.kernel.IndepSets s₃ s₂ κ μ
The theorem `ProbabilityTheory.kernel.indepSets_of_indepSets_of_le_left` states that for any types `α` and `Ω`, given measurable spaces `_mα` and `_mΩ`, and three sets of sets `s₁`, `s₂`, and `s₃`, along with a kernel `κ` from `α` to `Ω` and a measure `μ` on `α`, if sets `s₁` and `s₂` are independent with respect to the kernel `κ` and measure `μ`, and if all elements of `s₃` are also elements of `s₁` (i.e., `s₃` is a subset of `s₁`), then `s₃` and `s₂` are also independent with respect to the kernel `κ` and measure `μ`. In other words, the independence of sets with respect to a kernel and a measure is preserved under taking subsets.
More concisely: If sets `s₁` and `s₂` are independent and `s₃ ⊆ s₁`, then `s₃` and `s₂` are independent in the measure `μ` with respect to the kernel `κ`.
|
ProbabilityTheory.kernel.indep_iSup_of_directed_le
theorem ProbabilityTheory.kernel.indep_iSup_of_directed_le :
∀ {α : Type u_1} {ι : Type u_3} {_mα : MeasurableSpace α} {Ω : Type u_4} {m : ι → MeasurableSpace Ω}
{m' m0 : MeasurableSpace Ω} {κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α}
[inst : ProbabilityTheory.IsMarkovKernel κ],
(∀ (i : ι), ProbabilityTheory.kernel.Indep (m i) m' κ μ) →
(∀ (i : ι), m i ≤ m0) →
m' ≤ m0 → Directed (fun x x_1 => x ≤ x_1) m → ProbabilityTheory.kernel.Indep (⨆ i, m i) m' κ μ
This theorem states that in a probability theory context, given a set `α` and an index set `ι`, along with measurable spaces over a set `Ω` defined by a function `m` indexed by `ι` and two other measurable spaces `m'` and `m0`. If we have a Markov kernel `κ` from `α` to `Ω` and a measure `μ` over `α`, we can show the following: If every `m i` is independent from `m'` with respect to `κ` and `μ`, if every `m i` is a sub-measurable space of `m0`, and if `m'` is a sub-measurable space of `m0`, and if the `m i`'s form a directed set with respect to the subset relation, then the supremum of the `m i`'s is also independent from `m'` with respect to `κ` and `μ`. In other words, the independence property is preserved when moving from any index `i` to the supremum over all indices in the context of directed sets and Markov kernels.
More concisely: Given a measurable space `(Ω, Σ)`, a set `α`, an index set `ι`, measurable spaces `(α, Σα)` and `(Ω, Σ′)` over `Ω`, a Markov kernel `κ : α -> Ω`, and a measure `μ` over `α`, if for all `i ∈ ι`, `m i` is a sub-measurable, independent sub-σ-algebra of `m0 = Σ′` with respect to `κ` and `μ`, then the supremum of the `m i`'s is also independent from `m' = Σ` with respect to `κ` and `μ`.
|
ProbabilityTheory.kernel.IndepSets.indep'
theorem ProbabilityTheory.kernel.IndepSets.indep' :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
{p1 p2 : Set (Set Ω)},
(∀ s ∈ p1, MeasurableSet s) →
(∀ s ∈ p2, MeasurableSet s) →
IsPiSystem p1 →
IsPiSystem p2 →
ProbabilityTheory.kernel.IndepSets p1 p2 κ μ →
ProbabilityTheory.kernel.Indep (MeasurableSpace.generateFrom p1) (MeasurableSpace.generateFrom p2) κ
μ
The theorem `ProbabilityTheory.kernel.IndepSets.indep'` states that for any two sets `p1` and `p2` of subsets of a measurable space `Ω`, which are both `π-systems` (i.e., collections of subsets closed under binary intersection), and every subset within each of these sets is measurable, if these two sets are independent with respect to a `Markov kernel` `κ` and a measure `μ`, then these two sets remain independent even when they are extended to generate the smallest measure space containing them.
More concisely: If two `π-systems` of measurable subsets `p1` and `p2` in a measurable space `Ω`, such that every subset in each is measurable and they are independent with respect to a Markov kernel `κ` and measure `μ`, then they remain independent when extended to generate the smallest measurable space containing them.
|
ProbabilityTheory.kernel.indep_of_indep_of_le_left
theorem ProbabilityTheory.kernel.indep_of_indep_of_le_left :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ m₃ _mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α},
ProbabilityTheory.kernel.Indep m₁ m₂ κ μ → m₃ ≤ m₁ → ProbabilityTheory.kernel.Indep m₃ m₂ κ μ
This theorem, in the field of Probability Theory, states that for any types `α` and `Ω`, given measurable spaces on `α` and `Ω`, a kernel from `α` to `Ω`, and a measure on `α`, if two measurable spaces `m₁` and `m₂` are independent with respect to the kernel and measure, then if a third measurable space `m₃` is a sub-space (or less than/equal to) `m₁`, `m₃` and `m₂` are also independent with respect to the same kernel and measure.
More concisely: If two measurable subspaces are independent with respect to a kernel and measure, then their intersection is also independent.
|
ProbabilityTheory.kernel.indepSet_iff_indepSets_singleton
theorem ProbabilityTheory.kernel.indepSet_iff_indepSets_singleton :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s t : Set Ω} {m0 : MeasurableSpace Ω},
MeasurableSet s →
MeasurableSet t →
∀ (κ : ↥(ProbabilityTheory.kernel α Ω)) (μ : MeasureTheory.Measure α)
[inst : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.IndepSet s t κ μ ↔ ProbabilityTheory.kernel.IndepSets {s} {t} κ μ
This theorem states that for any types `α` and `Ω`, given `α` and `Ω` are both measurable spaces, two sets `s` and `t` from `Ω` that are measurable, and any kernel `κ` from `α` to `Ω` and any measure `μ` on `α`, if `κ` is a Markov kernel then the two sets `s` and `t` are independent if and only if the singleton sets `{s}` and `{t}` are independent with respect to the kernel `κ` and the measure `μ`. In the context of probability theory, this means that the probability of the intersection of two events equals the product of their probabilities.
More concisely: Given measurable spaces `α` and `Ω`, measurable sets `s` and `t` in `Ω`, a Markov kernel `κ` from `α` to `Ω`, and a measure `μ` on `α`, sets `s` and `t` are independent if and only if `κ({s}) ⊤ {t} = κ({s}) ∘ κ({t})`, where `⊤` is the lifting of the measure `μ` to `Ω` and `∘` is functional composition.
|
ProbabilityTheory.kernel.Indep.indepSets
theorem ProbabilityTheory.kernel.Indep.indepSets :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {s1 s2 : Set (Set Ω)},
ProbabilityTheory.kernel.Indep (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) κ μ →
ProbabilityTheory.kernel.IndepSets s1 s2 κ μ
This theorem states that for any types `α` and `Ω`, given a measurable space on `α` and `Ω`, a kernel `κ` from `α` to `Ω`, a measure `μ` on `α`, and two sets of sets `s1` and `s2` in `Ω`, if the two measurable spaces generated from `s1` and `s2` are independent with respect to the kernel `κ` and the measure `μ`, then the sets of sets `s1` and `s2` are also independent with respect to the same kernel and measure. In other words, it shows that the independence of the generated measurable spaces implies the independence of the original sets of sets under the same conditions.
More concisely: If measurable spaces $(s_1, \mathcal{A}_1, \mu, \kappa)$ and $(s_2, \mathcal{A}_2, \mu, \kappa)$ generated from sets $s_1, s_2 \subseteq \Omega$ are independent with respect to kernel $\kappa$ and measure $\mu$, then $s_1$ and $s_2$ are independent sets in $\Omega$ with respect to kernel $\kappa$ and measure $\mu$.
|
ProbabilityTheory.kernel.iIndepFun.indepFun_div_left
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_div_left :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
[inst : Div β] [inst_1 : MeasurableDiv₂ β] {f : ι → Ω → β} [inst_2 : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ μ →
(∀ (i : ι), Measurable (f i)) →
∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.kernel.IndepFun (f i / f j) (f k) κ μ
The theorem, `ProbabilityTheory.kernel.iIndepFun.indepFun_div_left`, states that given a Markov kernel, `κ`, and a measure, `μ`, on a measurable space of type `α`, for any division-closed measurable space of type `β`, and a function `f` from type `ι` to `Ω → β` that is `i`-independent (`iIndepFun`) with respect to the measure `m`, if each instance of `f i` is measurable, then for any three distinct instances `i`, `j`, and `k` of `ι`, the functions `(f i / f j)` and `f k` are independent (`IndepFun`) under the kernel `κ` and the measure `μ`. This theorem thus provides a condition under which the division of two measurable functions is also measurable and independent of another function.
More concisely: Given a Markov kernel and measure, if a division-closed measurable function that is i-independent with respect to the measure is defined on a measurable space, then the quotient of any two instances of the function and a third function are independent under the kernel and measure.
|
ProbabilityTheory.kernel.iIndepFun.indepFun_mul_left
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_mul_left :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
[inst : Mul β] [inst_1 : MeasurableMul₂ β] {f : ι → Ω → β} [inst_2 : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ μ →
(∀ (i : ι), Measurable (f i)) →
∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.kernel.IndepFun (f i * f j) (f k) κ μ
This theorem states that for any types `α`, `Ω`, `ι`, and `β`, given measurable spaces `α` and `Ω`, a Markov kernel `κ`, a measure `μ`, a measurable space `m` for `β`, multiplication operation on `β`, the measurability of the binary multiplication operation, and a function `f` from `ι` to a function on `Ω` with output in `β`, if the function `f` is independent under `κ` and `μ` for any input `x` from `m`, and every `ι` indexed function `f i` is measurable, then for any three distinct indices `i`, `j` and `k` from `ι`, the product of the functions `f i` and `f j` is independent of the function `f k` under the kernel `κ` and measure `μ`. This theorem is a part of the mathematical field of Probability Theory.
More concisely: If `κ` is a Markov kernel, `μ` is a measure, `m` is a measurable space for `β` with a measurable binary multiplication operation, `α`, `Ω`, `ι`, and `β` are types, `f : ι → Ω → β` is a measurable function independent of itself under `κ` and `μ` for all `x ∈ m`, and each `f i` is measurable, then for all distinct `i`, `j`, and `k` in `ι`, the functions `f i` and `f j` are independent of `f k` under `κ` and `μ` for the product of their outputs.
|
ProbabilityTheory.kernel.IndepSets.iUnion
theorem ProbabilityTheory.kernel.IndepSets.iUnion :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → Set (Set Ω)} {s' : Set (Set Ω)}
{_mΩ : MeasurableSpace Ω} {κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α},
(∀ (n : ι), ProbabilityTheory.kernel.IndepSets (s n) s' κ μ) →
ProbabilityTheory.kernel.IndepSets (⋃ n, s n) s' κ μ
The theorem `ProbabilityTheory.kernel.IndepSets.iUnion` states that for any types `α`, `Ω`, and `ι`, given a measurable space `α`, a family of sets `s : ι → Set (Set Ω)`, a set `s' : Set (Set Ω)`, a measurable space `Ω`, a kernel `κ : ↥(ProbabilityTheory.kernel α Ω)` and a measure `μ : MeasureTheory.Measure α`, if every set `s n` in the family is independent with respect to the kernel `κ` and the measure `μ` for all `n` in `ι`, then the union of all these sets `⋃ n, s n` is also independent with respect to the kernel `κ` and the measure `μ`.
In other words, the independence of each set in a family of sets implies the independence of their union. Here, two sets of sets `s₁, s₂` are said to be independent with respect to a kernel `κ` and a measure `μ` if for any sets `t₁ ∈ s₁, t₂ ∈ s₂`, almost everywhere `a`, the kernel `κ` applied to the intersection of `t₁` and `t₂` equals the product of `κ` applied to `t₁` and `κ` applied to `t₂`.
More concisely: If each set in a measurable family is independent with respect to a kernel and measure, then their union is also independent under the same kernel and measure.
|
ProbabilityTheory.kernel.iIndepSets.iIndep
theorem ProbabilityTheory.kernel.iIndepSets.iIndep :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ]
(m : ι → MeasurableSpace Ω),
(∀ (i : ι), m i ≤ _mΩ) →
∀ (π : ι → Set (Set Ω)),
(∀ (n : ι), IsPiSystem (π n)) →
(∀ (i : ι), m i = MeasurableSpace.generateFrom (π i)) →
ProbabilityTheory.kernel.iIndepSets π κ μ → ProbabilityTheory.kernel.iIndep m κ μ
The theorem `ProbabilityTheory.kernel.iIndepSets.iIndep` states that given a measurable space structure `_mα` on a type `α`, another measurable space structure `_mΩ` on a type `Ω`, a kernel function `κ` of type `ProbabilityTheory.kernel α Ω`, a measure `μ` on `α`, and a family of measurable space structures `m` indexed by `ι` such that each `m i` is a sub-measurable space of `_mΩ`, if for each `ι`-index `i`, there exists a set `π i` which is a π-system and the `m i` is the smallest measurable space containing the set `π i`, and if these π-systems are independent with respect to `κ` and `μ`, then the measurable space structures `m` are also independent with respect to `κ` and `μ`. In other words, if the π-systems that generate the measurable spaces are independent, then the generated measurable spaces themselves are also independent.
More concisely: If for each index `i`, a π-system `π i` generates a sub-measurable space `m i` of a measurable space `_mΩ` such that `m i` is the smallest measurable space containing `π i` and the π-systems `π i` are independent, then the measurable spaces `m i` are independent with respect to a kernel function `κ` and a measure `μ`.
|
ProbabilityTheory.kernel.iIndepFun.indepFun_finset_sum_of_not_mem
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_finset_sum_of_not_mem :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
[inst : AddCommMonoid β] [inst_1 : MeasurableAdd₂ β] {f : ι → Ω → β}
[inst_2 : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ μ →
(∀ (i : ι), Measurable (f i)) →
∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.kernel.IndepFun (s.sum fun j => f j) (f i) κ μ
This theorem states that for any types `α`, `Ω`, `ι`, and `β`, given measurable spaces over `α` and `Ω`, a subset of the kernel of a probability theory in `α` and `Ω`, a measure over `α`, a measurable space over `β`, a function `f` from `ι` to `Ω` to `β`, and assuming that `β` is an additive commutative monoid and that the function is measurable under addition, if `κ` is a Markov kernel, then if the function `f` is independent of the kernel `κ` under the measure `μ`, and for all indices `i` in `ι`, the function `f` at `i` is measurable, then for any finite set `s` of indices in `ι`, and for any index `i` in `ι` not in the set `s`, the function `f` at `i` is independent of the sum over `s` of the function `f` at each index in `s`, under the kernel `κ` and measure `μ`. It's part of the formalization of the concept of independence in probability theory.
More concisely: Given measurable spaces `α`, `Ω`, measurable functions `f: ι -> Ω -> β` from a type `ι` to `Ω` to a commutative additive monoid `β`, a probability theory `κ` on `α × Ω`, a measure `μ` on `α`, and assuming `f` is measurable, independent of `κ` under `μ` for all indices in `ι`, and `f(i)` is measurable for all `i` in `ι`, then for any finite subset `s` of `ι` and any `i` not in `s`, `f(i)` is independent of the sum of `f` over `s` under `κ` and `μ`.
|
ProbabilityTheory.kernel.iIndepFun.indepFun_finset
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_finset :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
{m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i} [inst : ProbabilityTheory.IsMarkovKernel κ]
(S T : Finset ι),
Disjoint S T →
ProbabilityTheory.kernel.iIndepFun m f κ μ →
(∀ (i : ι), Measurable (f i)) →
ProbabilityTheory.kernel.IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
The theorem `ProbabilityTheory.kernel.iIndepFun.indepFun_finset` states that if we have a family of random variables `f` that are all mutually independent (denoted by `iIndepFun m f μ`), and if `S` and `T` are two disjoint finite index sets, then the tuple that is formed by the variables `f i` for each `i` in `S` is independent of the tuple formed by the variables `f i` for each `i` in `T`. This holds under the condition that each `f i` is measurable.
More concisely: If `f` is a family of mutually independent measurable random variables and `S` and `T` are disjoint finite index sets, then the sub-vectors of `f` indexed by `S` and `T` are independent.
|
ProbabilityTheory.kernel.iIndepSets.indepSets
theorem ProbabilityTheory.kernel.iIndepSets.indepSets :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → Set (Set Ω)}
{_mΩ : MeasurableSpace Ω} {κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α},
ProbabilityTheory.kernel.iIndepSets s κ μ →
∀ {i j : ι}, i ≠ j → ProbabilityTheory.kernel.IndepSets (s i) (s j) κ μ
The theorem `ProbabilityTheory.kernel.iIndepSets.indepSets` asserts that for any types `α`, `Ω`, and `ι`, any measurable spaces of types `α` and `Ω`, any function `s` from `ι` to a set of sets of `Ω`, any kernel `κ` from `α` to `Ω`, and any measure `μ` of `α`, if the function `s` is independent with respect to the kernel `κ` and the measure `μ` (as defined by `ProbabilityTheory.kernel.iIndepSets`), then for any distinct indices `i` and `j` of `ι`, the sets `s i` and `s j` are also independent with respect to the kernel `κ` and the measure `μ` (as defined by `ProbabilityTheory.kernel.IndepSets`).
In terms of probability theory, this theorem means that if a collection of sets is mutually independent (each set is independent of any intersection of other sets), then any pair of these sets is also independent. Independence here means that for almost all elements in the underlying space (with respect to the given measure), the value of the kernel for the intersection of the two sets equals the product of the kernel values for each set.
More concisely: If a collection of sets is mutually independent with respect to a kernel and measure, then any pair of sets in the collection is also independently in the same sense with respect to the same kernel and measure.
|
ProbabilityTheory.kernel.indep_bot_right
theorem ProbabilityTheory.kernel.indep_bot_right :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} (m' : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} [inst : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.Indep m' ⊥ κ μ
This theorem states that for any types `α` and `Ω`, given measurable spaces over `α` and `Ω`, a Markov kernel `κ` from `α` to `Ω`, and a measure `μ` over `α`, the kernel `κ` is independent of the trivial σ-algebra (denoted by `⊥`) with respect to the measure `μ`. In the context of Probability Theory, this implicates that no information from the trivial σ-algebra can influence the transition probabilities defined by the Markov kernel.
More concisely: For any measurable spaces `(α, Σα)`, `(Ω, ΣΩ)`, measure `μ` on `(α, Σα)`, and Markov kernel `κ : α → Ω`, the kernel `κ` is μ-independent of the trivial σ-algebra `⊥` on `(α, Σα)`, i.e., ∀A ∈ Σα, μ(κ(A)) = μ(A) ∘ κ.
|
ProbabilityTheory.kernel.IndepFun.symm
theorem ProbabilityTheory.kernel.IndepFun.symm :
∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'}
{x : MeasurableSpace β} {x_1 : MeasurableSpace β'},
ProbabilityTheory.kernel.IndepFun f g κ μ → ProbabilityTheory.kernel.IndepFun g f κ μ
The theorem `ProbabilityTheory.kernel.IndepFun.symm` states that for any given types `α`, `Ω`, `β`, and `β'`, measurable spaces over `α` and `Ω`, a probability kernel `κ` from `α` to `Ω`, a measure `μ` over `α`, and functions `f` and `g` from `Ω` to `β` and `β'` respectively, if the functions `f` and `g` are independent with respect to `κ` and `μ`, then `g` and `f` are also independent with respect to `κ` and `μ`. This means the property of being independent functions under a probability kernel and a measure is symmetric.
More concisely: If functions `f` and `g` are independent with respect to measure `μ` and probability kernel `κ` from type `α` to `Ω`, then `g` and `f` are also independent with respect to `μ` and `κ`.
|
ProbabilityTheory.kernel.iIndep.iIndepSets
theorem ProbabilityTheory.kernel.iIndep.iIndepSets :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {m : ι → MeasurableSpace Ω}
{s : ι → Set (Set Ω)},
(∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)) →
ProbabilityTheory.kernel.iIndep m κ μ → ProbabilityTheory.kernel.iIndepSets s κ μ
This theorem, `ProbabilityTheory.kernel.iIndep.iIndepSets`, states that for any types `α`, `Ω`, and `ι`, given measurable spaces `_mα` and `_mΩ`, a probability kernel `κ` from `α` to `Ω`, a measure `μ` on `α`, a function `m` that assigns a measurable space to each element in `ι`, and a function `s` that assigns a set of sets of `Ω` to each element in `ι`. If for every element `n` in `ι`, the measurable space `m n` equals the smallest measurable space containing all sets in `s n`, and if the family of measurable spaces defined by `m` is independent with respect to the kernel `κ` and the measure `μ`, then the family of sets of sets defined by `s` is also independent with respect to the kernel `κ` and the measure `μ`.
More concisely: If for every `n` in `ι`, the measurable spaces `m n` are the smallest containing the families `s n` and `κ(α)` is independent of `μ` and `m`, then the families `s n` are independent of `κ` and `μ`.
|
ProbabilityTheory.kernel.iIndepSet_iff_iIndepSets_singleton
theorem ProbabilityTheory.kernel.iIndepSet_iff_iIndepSets_singleton :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} [inst : ProbabilityTheory.IsMarkovKernel κ] {μ : MeasureTheory.Measure α}
{f : ι → Set Ω},
(∀ (i : ι), MeasurableSet (f i)) →
(ProbabilityTheory.kernel.iIndepSet f κ μ ↔ ProbabilityTheory.kernel.iIndepSets (fun i => {f i}) κ μ)
This theorem states that for any types `α`, `Ω`, and `ι`, given measurable spaces over `α` and `Ω`, a probability kernel from `α` to `Ω`, a measure over `α`, and a function `f` from `ι` to the set of `Ω`, if each set `f i` is measurable, then the family of sets `f` is independent with respect to the kernel and measure if and only if the family of singleton sets `{f i}` is independent with respect to the same kernel and measure. In simpler terms, it states that the independence of a family of sets regarding a probability kernel and a measure is equivalent to the independence of the corresponding singleton sets.
More concisely: For measurable spaces (α, Σ\_α) and (Ω, Σ\_Ω), a probability kernel P from α to Ω, a measure μ over α, and a function f : ι → Ω with measurable sets f i, the family {f i} is independent with respect to (P, μ) if and only if the family {fi} is independent with respect to (P, μ).
|
ProbabilityTheory.kernel.iIndepFun.indepFun_add_left
theorem ProbabilityTheory.kernel.iIndepFun.indepFun_add_left :
∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
[inst : Add β] [inst_1 : MeasurableAdd₂ β] {f : ι → Ω → β} [inst_2 : ProbabilityTheory.IsMarkovKernel κ],
ProbabilityTheory.kernel.iIndepFun (fun x => m) f κ μ →
(∀ (i : ι), Measurable (f i)) →
∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.kernel.IndepFun (f i + f j) (f k) κ μ
This theorem is about the independence of functions in the context of probability theory. Specifically, it states that for any types `α`, `Ω`, `ι`, and `β`, given a measurable space for `α` and `Ω`, a marked kernel `κ` from `α` to `Ω`, a measure `μ` on `α`, a measurable space `m` on `β`, an addition operation on `β`, a measurable binary addition on `β`, a function `f` from `ι` to a function from `Ω` to `β`, and assuming that `κ` is a Markov kernel, if the kernel of the function `m` and `f` with respect to `κ` and `μ` is independent, and every function `f(i)` for `i` in `ι` is measurable, then for any three distinct elements `i`, `j`, `k` of `ι`, the function `f(i) + f(j)` is independent of `f(k)` with respect to the kernel `κ` and the measure `μ`.
More concisely: Given measurable spaces `α`, `Ω`, `β`, a Markov kernel `κ` from `α` to `Ω`, a measure `μ` on `α`, a measurable space `m` on `β` with measurable binary addition, a function `f` from `ι` to `Ω -> β` such that `κ` is the kernel of `m` and `f` with respect to `κ` and `μ`, and `f(i)` measurable for all `i` in `ι`, if `f(i)`, `f(j)`, and `f(k)` are independent for any distinct `i`, `j`, `k` in `ι` with respect to `κ` and `μ`, then `f(i) + f(j)` is independent of `f(k)` with respect to `κ` and `μ`.
|
ProbabilityTheory.kernel.IndepSets.symm
theorem ProbabilityTheory.kernel.IndepSets.symm :
∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
{κ : ↥(ProbabilityTheory.kernel α Ω)} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set (Set Ω)},
ProbabilityTheory.kernel.IndepSets s₁ s₂ κ μ → ProbabilityTheory.kernel.IndepSets s₂ s₁ κ μ
The theorem `ProbabilityTheory.kernel.IndepSets.symm` states that for any types `α` and `Ω`, measurable spaces `_mα` and `_mΩ`, an instance `κ` of a probability kernel from `α` to `Ω`, a measure `μ` on `α`, and two sets of sets `s₁` and `s₂` in `Ω`, if the sets `s₁` and `s₂` are independent with respect to kernel `κ` and measure `μ`, then the sets `s₂` and `s₁` are also independent with respect to the same kernel and measure. This is a symmetry property of independent sets in the context of probability theory and measure spaces.
More concisely: If sets $S\_1$ and $S\_2$ are independent in the probability measure $\mu$ with respect to the kernel $\kappa$ from $\alpha$ to $\Omega$, then $S\_2$ and $S\_1$ are also independent in the same measure $\mu$ and kernel $\kappa$.
|