`BookProof.ChapterSelectingEvents.exists_regular_conditional_probability` [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace Data] (μ : Measure Ω) [IsFiniteMeasure μ] (X : Ω → Da
ProvedBookProof.ChapterSelectingEvents.exists_regular_conditional_probabilitytheoremstimepiece
Prove the following Lean 4 theorem from ChapterSelectingEvents.
BookProof.ChapterSelectingEvents.exists_regular_conditional_probability [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace Data] (μ : Measure Ω) [IsFiniteMeasure μ] (X : Ω → Data) : ∃ κ : Kernel Data Ω, IsMarkovKernel κ ∧ (μ.map X) ⊗ₘ κ = μ.map (fun ω => (X ω, ω))
Formalization note: Lean 4 identifier BookProof.ChapterSelectingEvents.exists_regular_conditional_probability.
Preamble
-- Generated from ChapterSelectingEvents.lean — theorem BookProof.ChapterSelectingEvents.exists_regular_conditional_probability
import Mathlib
import Definitions.Def_ChapterSelectingEvents
open BookProof.ChapterSelectingEvents
open scoped BigOperators
open MeasureTheory ProbabilityTheory
variable (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable {Ω Data : Type*} [MeasurableSpace Ω]Formal statement
theorem BookProof.ChapterSelectingEvents.exists_regular_conditional_probability
[StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace Data]
(μ : Measure Ω) [IsFiniteMeasure μ] (X : Ω → Data) :
∃ κ : Kernel Data Ω, IsMarkovKernel κ ∧
(μ.map X) ⊗ₘ κ = μ.map (fun ω => (X ω, ω)) := by sorry