English
Let S be a measurable subset and x an element of the Lp submodule G. Then the conditional expectation operator applied to c · x equals c times the operator applied to x, for any real scalar c. In other words, condExpIndL1 hm μ s is linear in the argument x.
Русский
Пусть S измеримо и x ∈ G. Тогда условное математическое ожидание в отношении x масштабируемо по скаляру: condExpIndL1 hm μ s (c · x) = c · condExpIndL1 hm μ s x для любого действительного числа c.
LaTeX
$$$ condExpIndL1\; hm\; \mu\; s\; (c \cdot x) = c \cdot condExpIndL1\; hm\; \mu\; s\; x, \quad c \in \mathbb{R},\ x \in G,$$
Lean4
theorem condExpIndL1_smul (c : ℝ) (x : G) : condExpIndL1 hm μ s (c • x) = c • condExpIndL1 hm μ s x :=
by
by_cases hs : MeasurableSet s
swap; · simp_rw [condExpIndL1_of_not_measurableSet hs]; rw [smul_zero]
by_cases hμs : μ s = ∞
· simp_rw [condExpIndL1_of_measure_eq_top hμs]; rw [smul_zero]
· simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]
exact condExpIndL1Fin_smul hs hμs c x
