Conditioning kernel provider bridges

This module pushes the conditioning hardbone one honest step beyond indepFun_of_history_entry_measurable_of_indep: if a history parameter H is measurable and independent from a current step Z, then the conditional distribution of Z given H is the constant kernel law(Z), and conditional expectations of scalar functions F (H omega) (Z omega) reduce to frozen-parameter integrals against that law.

The conclusion is deliberately conditioned on MeasurableSpace.comap H. Lifting this reduction from the sigma-algebra generated by H to a larger history sigma-algebra remains an explicit separate task.

theorem HighDimProb.indepFun_of_measurable_of_indep_comap {Omega : Type u_1} {Alpha : Type u_2} {Beta : Type u_3} [MeasurableSpace Omega] [MeasurableSpace Alpha] [MeasurableSpace Beta] {P : MeasureTheory.Measure Omega} (mHist : MeasurableSpace Omega) (H : Omega → Alpha) (Z : Omega → Beta) (hH : Measurable H) (hIndep : ProbabilityTheory.Indep mHist (MeasurableSpace.comap Z inferInstance) P) : ProbabilityTheory.IndepFun H Z P

Convert independence from an explicit history sigma-algebra into function independence for a generic history parameter and current step.

noncomputable def HighDimProb.frozenParameterIntegral {Omega : Type u_1} {Alpha : Type u_2} {Beta : Type u_3} [MeasurableSpace Omega] [MeasurableSpace Alpha] [MeasurableSpace Beta] (P : MeasureTheory.Measure Omega) (H : Omega → Alpha) (Z : Omega → Beta) (F : Alpha → Beta → ℝ) : Omega → ℝ

Freeze the history parameter and integrate only over the law of the current step. This is the right-hand side produced by the kernel reduction.

noncomputable def HighDimProb.historyCondExp {Omega : Type u_1} {Alpha : Type u_2} {Beta : Type u_3} [MeasurableSpace Omega] [MeasurableSpace Alpha] [MeasurableSpace Beta] (P : MeasureTheory.Measure Omega) (H : Omega → Alpha) (Z : Omega → Beta) (F : Alpha → Beta → ℝ) : Omega → ℝ

Conditional expectation of omega ↦ F (H omega) (Z omega) with respect to the sigma-algebra generated by H.

theorem HighDimProb.condDistrib_ae_eq_const_of_indepFun {Omega : Type u_1} {Alpha : Type u_2} {Beta : Type u_3} [MeasurableSpace Omega] [MeasurableSpace Alpha] [MeasurableSpace Beta] [StandardBorelSpace Beta] [Nonempty Alpha] [Nonempty Beta] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure P] {H : Omega → Alpha} {Z : Omega → Beta} (hH : AEMeasurable H P) (hZ : AEMeasurable Z P) (hIndep : ProbabilityTheory.IndepFun H Z P) : (fun (a : Alpha) => (ProbabilityTheory.condDistrib Z H P) a) =ᵐ[MeasureTheory.Measure.map H P] fun (a : Alpha) => (ProbabilityTheory.Kernel.const Alpha (MeasureTheory.Measure.map Z P)) a

Under function independence, the conditional distribution of Z given H is almost everywhere the constant kernel law(Z).

theorem HighDimProb.historyCondExp_ae_eq_frozenParameterIntegral_of_indepFun {Omega : Type u_1} {Alpha : Type u_2} {Beta : Type u_3} [MeasurableSpace Omega] [MeasurableSpace Alpha] [MeasurableSpace Beta] [StandardBorelSpace Beta] [Nonempty Alpha] [Nonempty Beta] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure P] {H : Omega → Alpha} {Z : Omega → Beta} {F : Alpha → Beta → ℝ} (hH : Measurable H) (hZ : AEMeasurable Z P) (hIndep : ProbabilityTheory.IndepFun H Z P) (hInt : MeasureTheory.Integrable (fun (p : Alpha × Beta) => F p.1 p.2) (MeasureTheory.Measure.map (fun (omega : Omega) => (H omega, Z omega)) P)) : historyCondExp P H Z F =ᵐ[P] frozenParameterIntegral P H Z F

Kernel-form conditional expectation reduction for a measurable history parameter and an independent current step.

This theorem conditions only on MeasurableSpace.comap H; it does not claim a reduction for an arbitrary larger history sigma-algebra.

theorem HighDimProb.historyCondExp_le_of_indepFun_under_uniform_bound {Omega : Type u_1} {Alpha : Type u_2} {Beta : Type u_3} [MeasurableSpace Omega] [MeasurableSpace Alpha] [MeasurableSpace Beta] [StandardBorelSpace Beta] [Nonempty Alpha] [Nonempty Beta] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure P] {H : Omega → Alpha} {Z : Omega → Beta} {F : Alpha → Beta → ℝ} {B : Alpha → ℝ} (hH : Measurable H) (hZ : AEMeasurable Z P) (hIndep : ProbabilityTheory.IndepFun H Z P) (hInt : MeasureTheory.Integrable (fun (p : Alpha × Beta) => F p.1 p.2) (MeasureTheory.Measure.map (fun (omega : Omega) => (H omega, Z omega)) P)) (hBound : ∀ (a : Alpha), ∫ (z : Beta), F a z ∂MeasureTheory.Measure.map Z P ≤ B a) : historyCondExp P H Z F ≤ᵐ[P] fun (omega : Omega) => B (H omega)

If the frozen-parameter integrals have a deterministic bound B, then the conditional expectation along H is almost surely bounded by B (H omega).