condExpIndSMul_smul — Mathlib

English

The map x ↦ condExpIndSMul(hm, hs, hμs, x) is additive with respect to its argument in the Bochner sense, i.e., condExpIndSMul(hm, hs, hμs, x) + condExpIndSMul(hm, hs, hμs, y) equals condExpIndSMul(hm, hs, hμs, x+y).

Русский

Карта x ↦ condExpIndSMul(hm, hs, hμs, x) аддитивна по аргументу в смысле Боунхерна: condExpIndSMul(hm, hs, hμs, x) + condExpIndSMul(hm, hs, hμs, y) = condExpIndSMul(hm, hs, hμs, x+y).

LaTeX

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

Lean4

theorem condExpIndSMul_smul [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : 𝕜)
    (x : F) : condExpIndSMul hm hs hμs (c • x) = c • condExpIndSMul hm hs hμs x := by
  simp_rw [condExpIndSMul, toSpanSingleton_smul, smul_compLpL, smul_apply]

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