ProbabilityTheory.kernel.withDensity_apply
theorem ProbabilityTheory.kernel.withDensity_apply :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
(κ : ↥(ProbabilityTheory.kernel α β)) [inst : ProbabilityTheory.IsSFiniteKernel κ],
Measurable (Function.uncurry f) →
∀ (a : α), (ProbabilityTheory.kernel.withDensity κ f) a = (κ a).withDensity (f a)
The theorem `ProbabilityTheory.kernel.withDensity_apply` states that for any types `α` and `β` with measurable spaces `mα` and `mβ`, and for any function `f` from `α` and `β` to the extended nonnegative real numbers (`ENNReal`), if `κ` is a probability kernel from `α` to `β` which is also `s-finite`, and the uncurried version of `f` is measurable, then for any `α`, the density of `κ` with respect to `f` at `α` is equal to the density of `κ` at `α` with respect to the function `f` at `α`.
In simpler terms, this theorem expresses the relationship between a probability kernel and a probability density. If the density function is measurable, then the density of the kernel with respect to that measurable function does not change when evaluated at any point in the domain.
More concisely: For an s-finite probability kernel κ from measurable spaces (α, mα) to (β, mβ) and a measurable function f : α × β → ENNReal, the density of κ with respect to f equals the density of κ with respect to f's uncurried version, where f' is the function defined by f'(α) = ∫β f(α, β) d(κ α)(β).
|
ProbabilityTheory.kernel.isFiniteKernel_withDensity_of_bounded
theorem ProbabilityTheory.kernel.isFiniteKernel_withDensity_of_bounded :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
(κ : ↥(ProbabilityTheory.kernel α β)) [inst : ProbabilityTheory.IsFiniteKernel κ] {B : ENNReal},
B ≠ ⊤ →
(∀ (a : α) (b : β), f a b ≤ B) → ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.kernel.withDensity κ f)
This theorem states that given a finite kernel `κ` and a function `f` that maps from type `α` and `β` to the extended nonnegative real numbers (`ENNReal`), which is bounded by a value `B` that is not infinity, the kernel `κ` with density `f` is also finite. More precisely, for every element of types `α` and `β`, the function `f` does not exceed `B`. In the context of probability theory, a kernel is a function of two variables that specifies the way one variable depends on the other. Here, `withDensity` is a function that modifies a kernel by incorporating a function of one variable, in this case, `f`.
More concisely: Given a finite kernel κ and a function f : α × β -> ENNReal bounded by a finite value B, the kernel κ with density f is also finite, i.e., for all a : α and b : β, f a b ≤ B.
|
ProbabilityTheory.kernel.IsSFiniteKernel.withDensity
theorem ProbabilityTheory.kernel.IsSFiniteKernel.withDensity :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
(κ : ↥(ProbabilityTheory.kernel α β)) [inst : ProbabilityTheory.IsSFiniteKernel κ],
(∀ (a : α) (b : β), f a b ≠ ⊤) → ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.withDensity κ f)
This theorem states that, for a sigma-finite kernel `κ` and a function `f` from `α` to `β` which maps to the extended non-negative real numbers (denoted as `[0, ∞]` and referred to as `ENNReal`), and is everywhere finite (i.e., `f a b` is not `∞` for any `a` from `α` and `b` from `β`), the 'density' of `κ` with respect to `f` (denoted as `withDensity κ f`) is sigma-finite. Here, `α` and `β` are arbitrary types, and `mα` and `mβ` are their respective measurable spaces.
More concisely: Given a sigma-finite kernel κ and a finite-valued function f from α to [0, ∞], the measure κ with respect to f is also sigma-finite.
|
ProbabilityTheory.kernel.isSFiniteKernel_withDensity_of_isFiniteKernel
theorem ProbabilityTheory.kernel.isSFiniteKernel_withDensity_of_isFiniteKernel :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
(κ : ↥(ProbabilityTheory.kernel α β)) [inst : ProbabilityTheory.IsFiniteKernel κ],
(∀ (a : α) (b : β), f a b ≠ ⊤) → ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.kernel.withDensity κ f)
The theorem `ProbabilityTheory.kernel.isSFiniteKernel_withDensity_of_isFiniteKernel` states that for any types `α` and `β`, with measurable spaces `mα` and `mβ` respectively, and any function `f` from type `α` to type `β` that takes on values in the extended nonnegative real numbers (`ENNReal`), if a kernel `κ` from `α` to `β` is finite (i.e., it is an instance of `ProbabilityTheory.IsFiniteKernel`), and if the function `f` never assigns `∞` to any pair of elements from `α` and `β`, then the kernel obtained from `κ` by adding a density `f` (denoted as `ProbabilityTheory.kernel.withDensity κ f`) is s-finite, meaning it is an instance of `ProbabilityTheory.IsSFiniteKernel`. This theorem is a supporting result used in the demonstration of the `IsSFiniteKernel.withDensity` property in probability theory.
More concisely: If `κ` is a finite kernel from measurable spaces `α` to `β` and the function `f` from `α` to extended nonnegative real numbers never assigns `∞` to any pair, then the kernel `κ.withDensity f` is s-finite.
|