English
If T is a continuous linear map, then condExpL2 commutes with T on Lp via composition.
Русский
Если T — непрерывное линейное отображение, то CondExpL2 коммутирует с T через композицию на пространстве Lp.
LaTeX
$$$(\operatorname{condExpL2} E'' 𝕜' hm (T \cdot_{Lp} f) : α \to_{ μ} E'') =^{μ}_{a.e.} T \cdot_{Lp} (\operatorname{condExpL2} E' 𝕜 hm f : α \to_{ μ} E')$$$
Lean4
theorem setIntegral_condExpL2_indicator (hs : MeasurableSet[m] s) (ht : MeasurableSet t) (hμs : μ s ≠ ∞)
(hμt : μ t ≠ ∞) : ∫ x in s, (condExpL2 ℝ ℝ hm (indicatorConstLp 2 ht hμt 1) : α → ℝ) x ∂μ = μ.real (t ∩ s) :=
calc
∫ x in s, (condExpL2 ℝ ℝ hm (indicatorConstLp 2 ht hμt 1) : α → ℝ) x ∂μ =
∫ x in s, indicatorConstLp 2 ht hμt (1 : ℝ) x ∂μ :=
@integral_condExpL2_eq α _ ℝ _ _ _ _ _ _ _ _ _ hm (indicatorConstLp 2 ht hμt (1 : ℝ)) hs hμs
_ = μ.real (t ∩ s) • (1 : ℝ) := (setIntegral_indicatorConstLp (hm s hs) ht hμt 1)
_ = μ.real (t ∩ s) := by rw [smul_eq_mul, mul_one]
