English
For f ∈ L1, the conditional expectation condExpL1CLM F' hm μ f is AEStronglyMeasurable.
Русский
Для f ∈ L1 условное ожидание condExpL1CLM является AEStronglyMeasurable.
LaTeX
$$$ AEStronglyMeasurable\; m \; (condExpL1CLM\; F'\; hm\; μ\; f)\; μ,$$
Lean4
theorem aestronglyMeasurable_condExpL1CLM (f : α →₁[μ] F') : AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ :=
by
refine
@Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
(fun f : α →₁[μ] F' => AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ) ?_ ?_ ?_ f
· intro c s hs hμs
rw [condExpL1CLM_indicatorConst hs hμs.ne c]
exact aestronglyMeasurable_condExpInd hs hμs.ne c
· intro f g hf hg _ hfm hgm
rw [(condExpL1CLM F' hm μ).map_add]
exact (hfm.add hgm).congr (coeFn_add ..).symm
· have :
{f : Lp F' 1 μ | AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ} =
condExpL1CLM F' hm μ ⁻¹' {f | AEStronglyMeasurable[m] f μ} :=
rfl
rw [this]
refine IsClosed.preimage (condExpL1CLM F' hm μ).continuous ?_
exact isClosed_aestronglyMeasurable hm
