ProbabilityTheory.kernel.measure_le_bound
theorem ProbabilityTheory.kernel.measure_le_bound :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsFiniteKernel κ] (a : α) (s : Set β),
↑↑(κ a) s ≤ ProbabilityTheory.IsFiniteKernel.bound κ
This theorem from the field of probability theory, named "kernel.measure_le_bound", states that for any types `α` and `β`, given measurable spaces `mα` and `mβ` respectively, for any kernel `κ` from `α` to `β`, and assuming that `κ` is a finite kernel (as indicated by `h`), for any element `a` of type `α` and any set `s` of type `β`, the measure of `s` under `κ a` is always less than or equal to the bound of the finite kernel `κ`. In essence, it ensures that measures produced by a finite kernel never exceed its upper bound.
More concisely: Given measurable spaces `mα` and `mβ`, a finite kernel `κ` from `α` to `β`, and for any `a ∈ α` and `s ∈ β`, the measure of `s` under `κ a` is less than or equal to the bound of `κ`.
|
ProbabilityTheory.kernel.comapRight_apply'
theorem ProbabilityTheory.kernel.comapRight_apply' :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
{mγ : MeasurableSpace γ} {f : γ → β} (κ : ↥(ProbabilityTheory.kernel α β)) (hf : MeasurableEmbedding f) (a : α)
{t : Set γ}, MeasurableSet t → ↑↑((ProbabilityTheory.kernel.comapRight κ hf) a) t = ↑↑(κ a) (f '' t)
The theorem `ProbabilityTheory.kernel.comapRight_apply'` states that for any types `α`, `β`, and `γ`, given measurable spaces over these types, a function `f` from `γ` to `β`, a kernel `κ` from `α` to `β`, and a measurable embedding `hf` of `f`, for any element `a` of type `α` and any measurable set `t` of type `γ`, the measure of `t` under the measure obtained by comapping the kernel `κ` through `f` at `a` is equal to the measure of the image of `t` under `f` under the measure defined by `κ` at `a`. In mathematical terms, given $\kappa : \alpha \to \beta$, $f : \gamma \to \beta$, and $t \subset \gamma$ such that $t$ is measurable, we have $(\kappa \circ f^{-1})(t) = \kappa(f(t))$.
More concisely: Given measurable spaces over types `α`, `β`, and `γ`, a measurable embedding `hf` of a function `f` from `γ` to `β`, and a kernel `κ` from `α` to `β`, for any measurable set `t` of type `γ`, the measure of `t` under the comapped kernel `κ ∘ f` at any point `a` of type `α` equals the measure of `f(t)` under `κ` at `a`.
|
ProbabilityTheory.kernel.restrict_apply
theorem ProbabilityTheory.kernel.restrict_apply :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {s : Set β}
(κ : ↥(ProbabilityTheory.kernel α β)) (hs : MeasurableSet s) (a : α),
(ProbabilityTheory.kernel.restrict κ hs) a = (κ a).restrict s
The theorem `ProbabilityTheory.kernel.restrict_apply` states that for any types `α` and `β`, measurable spaces `mα` and `mβ`, a set `s` of type `β`, a probability kernel `κ` from `α` to `β`, a proof `hs` that `s` is a measurable set, and an element `a` of type `α`, the application of the restricted probability kernel `(ProbabilityTheory.kernel.restrict κ hs)` at `a` is equal to the restriction of the measure `(κ a)` to the set `s`. In essence, this theorem asserts the correctness of the `restrict` operation in the context of probability theory, ensuring that restricting a probability kernel to a measurable set behaves as expected.
More concisely: For any measurable spaces `mα` and `mβ`, type `α` element `a`, measurable set `s` in `β`, probability kernel `κ` from `α` to `β`, and proof `hs` of `s` being measurable, `(ProbabilityTheory.kernel.restrict κ hs) a = κ a | s`.
|
ProbabilityTheory.kernel.const_apply
theorem ProbabilityTheory.kernel.const_apply :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μβ : MeasureTheory.Measure β)
(a : α), (ProbabilityTheory.kernel.const α μβ) a = μβ
This theorem states that for any types `α` and `β`, given measurable spaces `mα` and `mβ` over these types and a measure `μβ` on `β`, the constant kernel (which always returns the same measure regardless of its input) when applied to any element of type `α` will always return the measure `μβ`. This essentially implies that the constant kernel is independent of the specific element in the measurable space `α` and only depends on the measure `μβ`.
More concisely: For any measurable spaces `mα` and `mβ` over types `α` and `β`, and any measure `μβ` on `β`, the constant kernel function maps every element of `α` to the measure `μβ`.
|
ProbabilityTheory.kernel.measurable
theorem ProbabilityTheory.kernel.measurable :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β)), Measurable ⇑κ
This theorem states that for any types `α` and `β` and any measurable spaces `mα` and `mβ` over these types, if `κ` is an element of the probability theory kernel from `α` to `β`, then the function defined by `κ` is measurable. In other words, for all measurable sets in `β`, the preimage of the set under `κ` is a measurable set in `α`.
More concisely: Given measurable spaces `mα` and `mβ` over types `α` and `β`, and a kernel `κ` from `α` to `β`, the function `κ` is measurable, i.e., for every measurable set `A` in `mβ`, the preimage `κ⁻¹(A)` in `mα` is also measurable.
|
ProbabilityTheory.kernel.deterministic_apply
theorem ProbabilityTheory.kernel.deterministic_apply :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f)
(a : α), (ProbabilityTheory.kernel.deterministic f hf) a = MeasureTheory.Measure.dirac (f a)
This theorem states that for any measurable spaces `α` and `β`, and any measurable function `f` from `α` to `β`, the application of the deterministic kernel to a point `a` in `α` results in the Dirac measure at `f(a)`. In other words, the deterministic kernel associates each point in `α` with the Dirac measure at the corresponding point `f(a)` in `β`, acting as a Markov kernel in probability theory.
More concisely: For any measurable spaces `α` and `β` and measurable function `f:` `α` → `β`, the deterministic kernel `K_f` satisfies `K_f(a) = δ(f(a))`, where `δ` denotes the Dirac measure.
|
ProbabilityTheory.kernel.ext
theorem ProbabilityTheory.kernel.ext :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
{κ η : ↥(ProbabilityTheory.kernel α β)}, (∀ (a : α), κ a = η a) → κ = η
This theorem is a part of Probability Theory and states that for any two measurable spaces `α` and `β` (with their associated measurable spaces `mα` and `mβ`), if two probability kernels `κ` and `η` from `α` to `β` are such that for every element `a` in `α`, `κ a = η a`, then the two kernels `κ` and `η` are equal. In other words, if two probability kernels produce the same output for every input in the source space, those two kernels are identical.
More concisely: If two probability kernels from one measurable space to another have identical output for every input in the source space, then they are equal.
|
ProbabilityTheory.kernel.measurable_coe
theorem ProbabilityTheory.kernel.measurable_coe :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β)) {s : Set β}, MeasurableSet s → Measurable fun a => ↑↑(κ a) s
This theorem states that for any given types `α` and `β`, each associated with measurable spaces `mα` and `mβ` respectively, and a kernel `κ` from `α` to `β` in the probability theory context, if `s` is a measurable set of type `β`, then the function that maps each element `a` of type `α` to the measure of the set `s` under the distribution `κ a` is measurable. This means that for any measurable set in the codomain, its preimage under this function is a measurable set in the domain.
More concisely: For any measurable spaces `α` and `β`, kernel `κ` from `α` to `β` in probability theory, and measurable set `s` of type `β`, the function mapping each `α` to the measure of `s` under `κ a` is measurable.
|
ProbabilityTheory.kernel.kernel_sum_seq
theorem ProbabilityTheory.kernel.kernel_sum_seq :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsSFiniteKernel κ],
ProbabilityTheory.kernel.sum (ProbabilityTheory.kernel.seq κ) = κ
This theorem in Probability Theory asserts that for any kernel `κ` from a measurable space `α` to a measurable space `β`, if `κ` is a so-called "s-finite" kernel (meaning it can be broken down into a countably infinite sequence of finite kernels), then the sum of all kernels in this breakdown sequence (obtained by applying the function `ProbabilityTheory.kernel.seq` to `κ`) is equal to the original kernel `κ`. In other words, an s-finite kernel can be decomposed into a sequence of finite kernels, and when we sum up all these finite kernels, we recover the original kernel.
More concisely: If `κ` is an s-finite kernel from measurable space `α` to measurable space `β`, then the sum of the sequence of finite kernels obtained from its decomposition is equal to `κ`.
|
ProbabilityTheory.kernel.sum_apply'
theorem ProbabilityTheory.kernel.sum_apply' :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
[inst : Countable ι] (κ : ι → ↥(ProbabilityTheory.kernel α β)) (a : α) {s : Set β},
MeasurableSet s → ↑↑((ProbabilityTheory.kernel.sum κ) a) s = ∑' (n : ι), ↑↑((κ n) a) s
This theorem states that for all types `α`, `β`, and `ι`, where `α` and `β` are equipped with a measurable space structure `mα` and `mβ` respectively, and `ι` is countable, given a function `κ` which assigns each element of `ι` a kernel on the spaces `α` and `β`, for any element `a` of `α` and any measurable set `s` of `β`, the value of the measure of `s` under the summed kernel at `a` is equal to the series sum of the values of the measure of `s` under each individual kernel at `a`. In mathematical terms, the theorem says that for a countable index set, the measure of a set under the sum of kernels is the series sum of the measures under each individual kernel, i.e., $((\text{kernel.sum}\ \kappa)(a))(s) = \sum'_{n \in \iota} ((\kappa(n))(a))(s)$ for each `a` in `α` and measurable `s` in `β`.
More concisely: For any countable index set `ι`, given measurable spaces `(α, mα)` and `(β, mβ)`, and a countable family of kernels `{κ(n)}` on `α × β`, the summed kernel `(kernel.sum κ)` satisfies the property that for all `a` in `α` and measurable `s` in `β`, $((\text{kernel.sum}\ κ)(a))(s) = \sum'_{n \in \iota} ((\kappa(n))(a))(s)$.
|
ProbabilityTheory.IsFiniteKernel.bound_lt_top
theorem ProbabilityTheory.IsFiniteKernel.bound_lt_top :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
(κ : ↥(ProbabilityTheory.kernel α β)) [h : ProbabilityTheory.IsFiniteKernel κ],
ProbabilityTheory.IsFiniteKernel.bound κ < ⊤
This theorem states that for any probability kernel `κ` from a measurable space `α` to a measurable space `β`, if `κ` is a finite kernel, then the bound of `κ` is strictly less than infinity. A probability kernel is a function that describes the transition probabilities from one random variable to another in a stochastic process. In this context, the 'bound' of a kernel refers to an upper limit on this transition probability. Thus, this theorem is essentially saying that for any finite transition model, the transition probabilities must have an upper limit that is not infinite.
More concisely: For any finite probability kernel from a measurable space to another, the supreme value of its transition probabilities is strictly less than infinity.
|