English
For any real scalar c, the L1-transform is homogeneous with respect to scalar multiplication: setToL1(hT.smul c) f = c · setToL1(hT) f for f ∈ L1(μ; E).
Русский
Для любого вещественного скаляра c отображение SetToL1 является однородным по умножению на скаляр: setToL1(hT.smul c) f = c · setToL1(hT) f для f ∈ L1(μ; E).
LaTeX
$$$setToL1\, (h_T\text{.smul } c)\; f = c \cdot setToL1\, h_T\, f,$$$
Lean4
theorem setToL1_smul_left (hT : DominatedFinMeasAdditive μ T C) (c : ℝ) (f : α →₁[μ] E) :
setToL1 (hT.smul c) f = c • setToL1 hT f :=
by
suffices setToL1 (hT.smul c) = c • setToL1 hT by rw [this, ContinuousLinearMap.smul_apply]
refine ContinuousLinearMap.extend_unique (setToL1SCLM α E μ (hT.smul c)) _ _ _ _ ?_
ext1 f
suffices c • setToL1 hT f = setToL1SCLM α E μ (hT.smul c) f by rw [← this]; simp [coeToLp]
rw [setToL1_eq_setToL1SCLM, setToL1SCLM_smul_left c hT]
