condExpIndSMul_ae_eq_smul — Mathlib

English

If the scalar c acts on inputs in F, condExpIndSMul is compatible with scalar multiplication: condExpIndSMul(hm, hs, hμs, c·x) = c·condExpIndSMul(hm, hs, hμs, x).

Русский

Условное ожидание совместимо со скаляром: 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_ae_eq_smul (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
    condExpIndSMul hm hs hμs x =ᵐ[μ] fun a => (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) a • x :=
  (toSpanSingleton ℝ x).coeFn_compLpL _

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