English
If T is a continuous linear map and f is a μ-a.e. 2-Lp function, then condExpL2 commutes with T on the measurable space, i.e., condExpL2 of T ∘ f equals T ∘ condExpL2 of f almost everywhere.
Русский
Если T — непрерывное линейное отображение и f удовлетворяет условию 2-Lp, то condExpL2 commute с T: кондExpL2 (T ∘ f) = T ∘ кондExpL2 (f) почти всюду.
LaTeX
$$$\big(\operatorname{condExpL2} E'' 𝕜' hm (T \cdot_{Lp} f) \big) =^{μ}_{a.e.} T \cdot_{Lp} (\operatorname{condExpL2} E 𝕜 hm f)$$$
Lean4
theorem condExpL2_comp_continuousLinearMap (hm : m ≤ m0) (T : E' →L[ℝ] E'') (f : α →₂[μ] E') :
(condExpL2 E'' 𝕜' hm (T.compLp f) : α →₂[μ] E'') =ᵐ[μ] T.compLp (condExpL2 E' 𝕜 hm f : α →₂[μ] E') :=
by
refine
Lp.ae_eq_of_forall_setIntegral_eq' 𝕜' hm _ _ two_ne_zero ENNReal.coe_ne_top
(fun s _ hμs => integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _)
(fun s _ hμs => integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne) ?_ ?_ ?_
· intro s hs hμs
rw [T.setIntegral_compLp _ (hm s hs),
T.integral_comp_comm (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne),
integral_condExpL2_eq hm f hs hμs.ne, integral_condExpL2_eq hm (T.compLp f) hs hμs.ne,
T.setIntegral_compLp _ (hm s hs),
T.integral_comp_comm (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs.ne)]
· exact lpMeas.aestronglyMeasurable _
· have h_coe := T.coeFn_compLp (condExpL2 E' 𝕜 hm f : α →₂[μ] E')
rw [← EventuallyEq] at h_coe
refine AEStronglyMeasurable.congr ?_ h_coe.symm
exact T.continuous.comp_aestronglyMeasurable (lpMeas.aestronglyMeasurable (condExpL2 E' 𝕜 hm f))
