English
If f,g are absolutely continuous on uIcc a b, then the pointwise product f(x) · g(x) is absolutely continuous on uIcc a b (real-valued case).
Русский
Если f и g абсолютно непрерывны на uIcc(a,b), то произведение f(x)g(x) абсолютно непрерывно на uIcc(a,b) (для вещественных функций).
LaTeX
$$$\forall a,b\in\mathbb{R},\; \forall f,g: \mathbb{R}\to \mathbb{R},\; (\text{AbsolutelyContinuousOnInterval}(f,a,b) \land \text{AbsolutelyContinuousOnInterval}(g,a,b)) \Rightarrow \text{AbsolutelyContinuousOnInterval}(x\mapsto f(x)\,g(x), a,b)$$$
Lean4
/-- If `f` and `g` are absolutely continuous on `uIcc a b`, then `f * g` is absolutely continuous
on `uIcc a b`. -/
theorem fun_mul {f g : ℝ → ℝ} (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) :
AbsolutelyContinuousOnInterval (fun x ↦ f x * g x) a b :=
hf.fun_smul hg
