English
Let c be a scalar and T a family of continuous linear maps. Then for any f, scaling the outputs by c inside T yields the same as scaling the result of setToFun by c: setToFun μ (fun s => c • T(s)) (hT.smul c) f = c • setToFun μ T hT f.
Русский
Пусть скаляр c задаёт масштабирование в каждом T(s). Тогда результат эквивалентен умножению результата setToFun на c: setToFun μ (fun s => c • T(s)) (hT.smul c) f = c • setToFun μ T hT f.
LaTeX
$$$\forall c\in\mathbb{R},\; \mathrm{setToFun}(\mu, \lambda s. c\cdot T(s))\,(h_T.smul\,c)\,f = c\cdot \mathrm{setToFun}(\mu, T)\,h_T\,f$$$
Lean4
theorem setToFun_smul_left (hT : DominatedFinMeasAdditive μ T C) (c : ℝ) (f : α → E) :
setToFun μ (fun s => c • T s) (hT.smul c) f = c • setToFun μ T hT f :=
by
by_cases hf : Integrable f μ
· simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left hT c]
· simp_rw [setToFun_undef _ hf, smul_zero]
