Conditional expectation from restricted restart laws #
This file records a generic measure-theoretic bridge from an event-restricted future-law identity to a conditional-expectation identity. The restart hypothesis is required after restriction to every event in the conditioning measurable space. Its specialization to the whole space alone is only an unconditional distributional identity and is not enough for this conclusion.
No stochastic process, Markov property, or path-space construction is asserted here.
theorem
MarkovProcess.condExp_comp_ae_eq_integral_kernel_of_restrict_map
{Omega : Type u_1}
{beta : Type u_2}
{E : Type u_3}
{m mOmega : MeasurableSpace Omega}
{mBeta : MeasurableSpace beta}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(mu : MeasureTheory.Measure Omega)
[MeasureTheory.IsFiniteMeasure mu]
(kappa : ProbabilityTheory.Kernel Omega beta)
[ProbabilityTheory.IsMarkovKernel kappa]
(Y : Omega → beta)
(hY : Measurable Y)
(hm : m ≤ mOmega)
(hJoint :
∀ (A : Set Omega), MeasurableSet A → MeasureTheory.Measure.map Y (mu.restrict A) = (mu.restrict A).bind ⇑kappa)
(F : beta → E)
(hF : MeasureTheory.StronglyMeasurable F)
(hFm : MeasureTheory.StronglyMeasurable fun (omega : Omega) => ∫ (y : beta), F y ∂kappa omega)
(C : ℝ)
(hFC : ∀ (y : beta), ‖F y‖ ≤ C)
:
If the law of Y after restriction to every conditioning event is obtained by mixing
kappa, then integrating any bounded strongly measurable observable against kappa gives the
corresponding conditional expectation.