English
Let M be a seminormed ring acting on a normed additively commutative group F. If a function f: R → F is absolutely continuous on [a,b], then for every α in M the function x ↦ α · f(x) is absolutely continuous on [a,b].
Русский
Пусть M — Семинормированное кольцо, действующее на нормированную абелеву группу F. Если f: R → F абсолютно непрерывна на [a,b], то для каждого α ∈ M функция x ↦ α · f(x) абсолютно непрерывна на [a,b].
LaTeX
$$$\forall \alpha \in M\,\forall f: \mathbb{R} \to F\,\Big( \text{AbsolutelyContinuousOnInterval}(f,a,b) \Rightarrow \text{AbsolutelyContinuousOnInterval}(\lambda x.\alpha\cdot f(x),a,b) \Big)$$$
Lean4
theorem const_smul {M : Type*} [SeminormedRing M] [Module M F] [NormSMulClass M F] (α : M)
(hf : AbsolutelyContinuousOnInterval f a b) : AbsolutelyContinuousOnInterval (fun x ↦ α • f x) a b :=
by
apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf.const_mul ‖α‖)
· exact Finset.sum_nonneg (fun i hi ↦ by positivity)
· rw [Finset.mul_sum]
gcongr
simp only [dist_smul₀]
rfl
