English
If IsFiniteMeasure μ, then the constant value x is carried by setToFun to T univ x: setToFun μ T hT fun _ => x = T univ x.
Русский
Если мера μ конечна, то константная функция x попадает в setToFun как T(универсум) x: setToFun μ T hT (fun _ => x) = T univ x.
LaTeX
$$$\text{If } IsFiniteMeasure(\mu)\text{, then } \mathrm{setToFun}(\mu, T)\,h_T\, (\lambda\_, x) = T(\text{univ})\,x$$$
Lean4
theorem setToFun_smul [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [Module 𝕜 F] [NormSMulClass 𝕜 F]
(hT : DominatedFinMeasAdditive μ T C) (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) (c : 𝕜) (f : α → E) :
setToFun μ T hT (c • f) = c • setToFun μ T hT f :=
by
by_cases hf : Integrable f μ
· rw [setToFun_eq hT hf, setToFun_eq hT (hf.smul c), Integrable.toL1_smul' f hf, L1.setToL1_smul hT h_smul c]
· by_cases hr : c = 0
· rw [hr]; simp
· have hf' : ¬Integrable (c • f) μ := by rwa [integrable_smul_iff hr f]
rw [setToFun_undef hT hf, setToFun_undef hT hf', smul_zero]
