English
Let f be an lp-measurable function with values in F'. The L1 conditional expectation operator, viewed as an operator on these functions, leaves f unchanged: condExpL1CLM F' hm μ (f) = f.
Русский
Пусть f является lp-измеримой функцией, принимающей значения в F'. Оператор условного ожидания в L1, применяемый к f, оставляет его неизменным: condExpL1CLM F' hm μ (f) = f.
LaTeX
$$$condExpL1CLM F' hm μ\, f = f$$$
Lean4
theorem condExpL1CLM_lpMeas (f : lpMeas F' ℝ m 1 μ) : condExpL1CLM F' hm μ (f : α →₁[μ] F') = ↑f :=
by
let g := lpMeasToLpTrimLie F' ℝ 1 μ hm f
have hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g := by simp only [g, LinearIsometryEquiv.symm_apply_apply]
rw [hfg]
refine
@Lp.induction α F' m _ 1 (μ.trim hm) _ ENNReal.coe_ne_top
(fun g : α →₁[μ.trim hm] F' =>
condExpL1CLM F' hm μ ((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g : α →₁[μ] F') =
↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g))
?_ ?_ ?_ g
· intro c s hs hμs
rw [@Lp.simpleFunc.coe_indicatorConst _ _ m, lpMeasToLpTrimLie_symm_indicator hs hμs.ne c,
condExpL1CLM_indicatorConstLp]
exact condExpInd_of_measurable hs ((le_trim hm).trans_lt hμs).ne c
· intro f g hf hg _ hf_eq hg_eq
rw [LinearIsometryEquiv.map_add]
push_cast
rw [map_add, hf_eq, hg_eq]
· refine isClosed_eq ?_ ?_
· refine (condExpL1CLM F' hm μ).continuous.comp (continuous_induced_dom.comp ?_)
exact LinearIsometryEquiv.continuous _
· refine continuous_induced_dom.comp ?_
exact LinearIsometryEquiv.continuous _
