ProbabilityTheory.integrable_compProd_iff
theorem ProbabilityTheory.integrable_compProd_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
{mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {κ : ↥(ProbabilityTheory.kernel α β)}
[inst_1 : ProbabilityTheory.IsSFiniteKernel κ] {η : ↥(ProbabilityTheory.kernel (α × β) γ)}
[inst_2 : ProbabilityTheory.IsSFiniteKernel η] {a : α} ⦃f : β × γ → E⦄,
MeasureTheory.AEStronglyMeasurable f ((ProbabilityTheory.kernel.compProd κ η) a) →
(MeasureTheory.Integrable f ((ProbabilityTheory.kernel.compProd κ η) a) ↔
(∀ᵐ (x : β) ∂κ a, MeasureTheory.Integrable (fun y => f (x, y)) (η (a, x))) ∧
MeasureTheory.Integrable (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a))
The theorem `ProbabilityTheory.integrable_compProd_iff` states that for any types `α`, `β`, `γ`, and `E`, measurable spaces `mα`, `mβ`, and `mγ`, a normed add commutative group `E`, a kernel `κ` from `α` to `β`, a kernel `η` from the product `α × β` to `γ`, and a function `f` from `β × γ` to `E` that is almost everywhere strongly measurable with respect to the measure derived from the product of kernels `κ` and `η` at a point `a` in `α`, the function `f` is integrable with respect to this measure if and only if two conditions hold:
1. The function `f`, when its first argument is fixed almost everywhere to a value `x` from `β` under the measure of `κ` at `a`, is integrable with respect to the measure of `η` at the pair `(a, x)`.
2. The function that takes a point `x` in `β` and maps it to the integral over `γ` of the norm of `f` at `(x, y)`, with respect to the measure of `η` at `(a, x)`, is integrable with respect to the measure of `κ` at `a`.
The theorem therefore provides a condition for integrability of a function in terms of the integrability of certain related functions.
More concisely: A function `f` from `β × γ` to a normed add commutative group `E`, almost everywhere strongly measurable with respect to the product of kernels `κ` from `α` to `β` and `η` from `α × β` to `γ`, is integrable with respect to the measure derived from `κ` and `η` if and only if, for almost every `x` in `β` under the measure of `κ` at a point `a` in `α`, `f(x, .)` is integrable with respect to `η` at `(a, x)`, and the function that maps `x` to the integral of the norm of `f(x, .)` with respect to `η` is integrable with respect to `κ` at `a`.
|