English
When scalars come from the real numbers, the smul commutes with setToSimpleFunc in a straightforward way: setToSimpleFunc T (c • f) = c • setToSimpleFunc T f.
Русский
Для скалярного множителя из ℝ выполняется обычное умножение на множитель: setToSimpleFunc T (c • f) = c • setToSimpleFunc T f.
LaTeX
$$$ setToSimpleFunc T (c \cdot f) = c \cdot setToSimpleFunc T f $$$
Lean4
theorem setToSimpleFunc_smul_real (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) (c : ℝ) {f : α →ₛ E}
(hf : Integrable f μ) : setToSimpleFunc T (c • f) = c • setToSimpleFunc T f :=
calc
setToSimpleFunc T (c • f) = ∑ x ∈ f.range, T (f ⁻¹' { x }) (c • x) := by
rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]; dsimp only; rw [smul_zero]
_ = ∑ x ∈ f.range, c • T (f ⁻¹' { x }) x :=
(Finset.sum_congr rfl fun b _ => by rw [ContinuousLinearMap.map_smul (T (f ⁻¹' { b })) c b])
_ = c • setToSimpleFunc T f := by simp only [setToSimpleFunc, smul_sum]
