English
If hT' is a scaled version of hT by a scalar c, then for any f in L1, setToL1(hT') f = c · setToL1(hT) f.
Русский
Если hT' получено как масштабированием hT на скаляр c, то для любого f в L1 выполняется setToL1(hT') f = c · setToL1(hT) f.
LaTeX
$$$setToL1\, h_T'\, f = c \cdot setToL1\, h_T\, f,$$$
Lean4
theorem setToL1_smul_left' (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') (c : ℝ)
(h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) (f : α →₁[μ] E) : setToL1 hT' f = c • setToL1 hT f :=
by
suffices setToL1 hT' = c • setToL1 hT by rw [this, ContinuousLinearMap.smul_apply]
refine ContinuousLinearMap.extend_unique (setToL1SCLM α E μ hT') _ _ _ _ ?_
ext1 f
suffices c • setToL1 hT f = setToL1SCLM α E μ hT' f by rw [← this]; simp [coeToLp]
rw [setToL1_eq_setToL1SCLM, setToL1SCLM_smul_left' c hT hT' h_smul]
