Theorems · Theorem · probability

ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real

∀ {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} [inst : MeasureTheory.IsFiniteMeasure ρ]
  (κ : ProbabilityTheory.Kernel α ℝ) [ProbabilityTheory.IsFiniteKernel κ],
  ρ = ρ.fst.compProd κ → ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x

Auxiliary lemma for eq_condKernel_of_measure_eq_compProd. Uniqueness of the disintegration kernel on ℝ.

Defined in

Mathlib.Probability.Kernel.Disintegration.Unique

Cited by

1 results in Mathlib

Foundations

Depth 280 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasureProbabilityTheory.IsFiniteKernel