Measurable.lintegral_kernel_prod_right
theorem Measurable.lintegral_kernel_prod_right :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)} [inst : ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → ENNReal},
Measurable (Function.uncurry f) → Measurable fun a => ∫⁻ (b : β), f a b ∂κ a
The theorem `Measurable.lintegral_kernel_prod_right` states that for an s-finite kernel `κ` and a function `f` from `α` to `β` that maps to the extended nonnegative real numbers, if `f` is measurable when viewed as a function from the product space `α × β` (that is, the function `f` uncurried is measurable), then the function that maps each `a` to the lebesgue integral of `f a b` with respect to `κ a` over `b` is also measurable. Here, the s-finite kernel `κ` is a measure on the space `α` and `β`, and the function `f` is effectively a function of two variables from `α` and `β`. The measurability indicates that the pre-image of any measurable set under these functions is also measurable.
More concisely: If `κ` is an s-finite kernel and `f: α → ℝ∞²` is a measurable function on the product space `α × β`, then the function that maps each `a ∈ α` to the Lebesgue integral of `f a b` with respect to `κ a` over `β` is measurable.
|
ProbabilityTheory.kernel.measurable_kernel_prod_mk_left_of_finite
theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_left_of_finite :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)} {t : Set (α × β)},
MeasurableSet t →
(∀ (a : α), MeasureTheory.IsFiniteMeasure (κ a)) → Measurable fun a => ↑↑(κ a) (Prod.mk a ⁻¹' t)
This theorem, `ProbabilityTheory.kernel.measurable_kernel_prod_mk_left_of_finite`, is a helper lemma for `measurable_kernel_prod_mk_left`. It is stated for any types `α` and `β`, equipped with measurable spaces `mα` and `mβ` respectively. The theorem is concerned with a measurable kernel `κ` from `α` to `β` and a measurable set `t` in the product space of `α` and `β`. The theorem asserts that if every `κ a` is a finite measure for all `a` in `α`, then the function that takes an `a` in `α` and returns the measure of the preimage of `t` under the function `Prod.mk a` (which pairs `a` with an element in `β`), is measurable. In other words, it confirms the measurability of a function constructed from a measurable kernel under certain conditions.
More concisely: Given measurable spaces `(α, mα)` and `(β, mβ)`, a measurable kernel `κ` from `α` to `β`, and a measurable set `t` in the product space of `α × β`, if every `κ a` is a finite measure for all `a` in `α`, then the function that maps `a` to the measure of the preimage of `t` under `Prod.mk a` is measurable.
|
ProbabilityTheory.kernel.measurable_lintegral_indicator_const
theorem ProbabilityTheory.kernel.measurable_lintegral_indicator_const :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)} [inst : ProbabilityTheory.IsSFiniteKernel κ] {t : Set (α × β)},
MeasurableSet t →
∀ (c : ENNReal), Measurable fun a => ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂κ a
This theorem, named `ProbabilityTheory.kernel.measurable_lintegral_indicator_const`, states that for any measurable space `α` and `β`, any kernel `κ` from `α` to `β`, any measurable set `t` in the product space of `α` and `β`, and any extended nonnegative real number `c`, the function from `α` to the integral over `β` of the indicator function of `t` at `(a,b)` times the constant function `c` with respect to the measure induced by the kernel `κ` on `α` is measurable. This function essentially computes the expectation of the constant `c` with respect to the measure induced by `κ` on the set `t`, for each point in `α`. The condition that the kernel `κ` is s-finite is also required.
More concisely: For any s-finite kernel κ from measurable spaces α to β, the function mapping each a in α to the constant c integrated against the measure of κ(a) over the measurable set t in α × β is measurable.
|
MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'
theorem MeasureTheory.StronglyMeasurable.integral_kernel_prod_right' :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)} {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : ProbabilityTheory.IsSFiniteKernel κ] ⦃f : α × β → E⦄,
MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂κ x
The theorem `MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'` states that for any types `α`, `β`, `E`, given the measurable spaces `mα` and `mβ` on `α` and `β` respectively, a probability kernel `κ` from `α` to `β`, and a function `f` from the product space `α × β` to `E` (where `E` is a complete normed additive commutative group and also a normed space over the real numbers), if `f` is strongly measurable (i.e., it is the limit of simple functions), then the function that maps each element `x` of `α` to the integral over `β` of `f` applied to the pair `(x, y)`, with respect to the measure `κ x`, is also strongly measurable. A kernel `κ` is said to be `ProbabilityTheory.IsSFiniteKernel` if it is sigma-finite, which means that the space can be partitioned into a countable union of measurable sets with finite measure.
More concisely: If `α`, `β`, `E` are types, `mα` and `mβ` are measurable spaces, `κ` is a probability kernel from `α` to `β`, `f : α × β → E` is a strongly measurable function, and `κ` is sigma-finite, then the function `x ↦ ∫ₐβ f(x, y) d(κ x)` is strongly measurable.
|
ProbabilityTheory.kernel.measurable_kernel_prod_mk_left
theorem ProbabilityTheory.kernel.measurable_kernel_prod_mk_left :
∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
{κ : ↥(ProbabilityTheory.kernel α β)} [inst : ProbabilityTheory.IsSFiniteKernel κ] {t : Set (α × β)},
MeasurableSet t → Measurable fun a => ↑↑(κ a) (Prod.mk a ⁻¹' t)
The theorem `ProbabilityTheory.kernel.measurable_kernel_prod_mk_left` states that for any types `α` and `β`, given the measurable spaces `mα` and `mβ` respectively, a kernel `κ` from `α` to `β`, an instance proving that `κ` is a sigma-finite kernel, and a set `t` of ordered pairs of `α` and `β` that is measurable, the function that maps each element of `α` to the measure of the preimage of `t` under the function that pairs each element of `α` with that element (i.e., the function `(a => ↑↑(κ a) (Prod.mk a ⁻¹' t))`) is a measurable function. In other words, this theorem asserts the measurability of a certain function constructed from a probability kernel and a measurable set in the product space.
More concisely: Given measurable spaces `mα` and `mβ`, a sigma-finite kernel `κ` from `α` to `β`, and a measurable set `t` in the product space `α × β`, the function mapping each `α` element to the measure of the preimage of `t` under the pairing function is measurable.
|