English
The left-hand side and right-hand side of the set L-integral equality for condDistrib with respect to measurable X and Y coincide.
Русский
Левая и правая части равенства линтейнера по множеству совпадают для condDistrib с измеримыми X и Y.
LaTeX
$$$$(\\text{setLIntegral}_{\n μ}^{X,t} s) = (\\text{setLIntegral}_{\n μ}^{X,t} s).$$$$
Lean4
/-- The conditional expectation of a function `f` of the product `(X, Y)` is almost everywhere equal
to the integral of `y ↦ f(X, y)` against the `condDistrib` kernel. -/
theorem condExp_prod_ae_eq_integral_condDistrib' [NormedSpace ℝ F] [CompleteSpace F] (hX : Measurable X)
(hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
μ[fun a => f (X a, Y a)|mβ.comap X] =ᵐ[μ] fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a) :=
by
have hf_int' : Integrable (fun a => f (X a, Y a)) μ :=
(integrable_map_measure hf_int.1 (hX.aemeasurable.prodMk hY)).mp hf_int
refine (ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le hf_int' (fun s _ _ => ?_) ?_ ?_).symm
· exact (hf_int.integral_condDistrib hX.aemeasurable hY).integrableOn
· rintro s ⟨t, ht, rfl⟩ _
change
∫ a in X ⁻¹' t, ((fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x') ∘ X) a ∂μ = ∫ a in X ⁻¹' t, f (X a, Y a) ∂μ
simp only [Function.comp_apply]
rw [← integral_map hX.aemeasurable (f := fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x')]
swap
· rw [← Measure.restrict_map hX ht]
exact (hf_int.1.integral_condDistrib_map hY).restrict
rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prodMk₀ hY, condDistrib,
Measure.setIntegral_condKernel_univ_right ht hf_int.integrableOn,
setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prodMk hY), mk_preimage_prod,
preimage_univ, inter_univ]
· exact aestronglyMeasurable_integral_condDistrib hX.aemeasurable hY hf_int.1
