ProbabilityTheory.eq_condKernel_of_measure_eq_compProd
theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd :
∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
[inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ]
(κ : ↥(ProbabilityTheory.kernel α Ω)) [inst_4 : ProbabilityTheory.IsFiniteKernel κ],
ρ = ρ.fst.compProd κ → ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x
This theorem states that for every measure space `α` and `Ω`, given a finite measure `ρ` on the product space `α × Ω`, and a finite kernel `κ` from `α` to `Ω`, if `ρ` is equal to the composition of the first marginal of `ρ` and `κ` (denoted by `ρ.fst.compProd κ`), then `κ` is almost everywhere equal to the conditional kernel of `ρ` with respect to `α`. Here, the "almost everywhere" condition is with respect to the measure given by the first marginal of `ρ` (denoted by `ρ.fst`). This result is in the context of probability theory and it connects the concepts of measure theory, product space, and the disintegration of measures.
More concisely: If a finite measure ρ on the product space α × Ω equals the composition of the first marginal of ρ and kernel κ, then κ is almost everywhere equal to the conditional kernel of ρ with respect to α.
|
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd'
theorem ProbabilityTheory.eq_condKernel_of_measure_eq_compProd' :
∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
[inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ]
(κ : ↥(ProbabilityTheory.kernel α Ω)) [inst_4 : ProbabilityTheory.IsSFiniteKernel κ],
ρ = ρ.fst.compProd κ → ∀ {s : Set Ω}, MeasurableSet s → ∀ᵐ (x : α) ∂ρ.fst, ↑↑(κ x) s = ↑↑(ρ.condKernel x) s
The theorem `ProbabilityTheory.eq_condKernel_of_measure_eq_compProd'` states that for any types `α` and `Ω` with respective measurable spaces `mα` and `Ω`, where `Ω` is also a standard Borel space and is nonempty, any measure `ρ` on the product of `α` and `Ω` which is a finite measure, and any `κ` which is a member of the set of kernels from `α` to `Ω` that is s-finite, if `ρ` is equal to the composition of `ρ.fst` and `κ`, then for any set `s` of `Ω` that is measurable, almost everywhere with respect to the measure `ρ.fst`, the value of `κ` at `x` applied to `s` is equal to the value of the conditional kernel of `ρ` at `x` applied to `s`. In simpler terms, it says that if a measure is composed of a first component and a s-finite kernel, then the kernel is almost everywhere equal to the disintegration kernel of the measure when evaluated on a measurable set. This is a weaker statement than another theorem `eq_condKernel_of_measure_eq_compProd` which says that the kernels are equal almost everywhere, not just on a measurable set.
More concisely: For any finite measure ρ on the product of types α and Ω (where Ω is a standard Borel space), if ρ is equal to the composition of the projection measure and an s-finite kernel κ, then the value of κ applied to a measurable set s almost everywhere with respect to ρ.fst is equal to the conditional kernel of ρ at any point x applied to s.
|