condExpIndSMul_add — Mathlib

English

Conditional expectation in L2 commutes with scalar multiplication by a scalar c: condExpIndSMul(hm, hs, hμs, c·x) = c·condExpIndSMul(hm, hs, hμs, x).

Русский

Условное ожидание в L2 сохраняет скаляры: condExpIndSMul(hm, hs, hμs, c·x) = c·condExpIndSMul(hm, hs, hμs, x).

LaTeX

$$$\operatorname{condExpIndSMul}(hm, hs, hμs, c \cdot x) = c \cdot \operatorname{condExpIndSMul}(hm, hs, hμs, x).$$$

Lean4

theorem condExpIndSMul_add (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x y : G) :
    condExpIndSMul hm hs hμs (x + y) = condExpIndSMul hm hs hμs x + condExpIndSMul hm hs hμs y := by
  simp_rw [condExpIndSMul]; rw [toSpanSingleton_add, add_compLpL, add_apply]

Похожие утверждения