fun_add — Mathlib

English

If f and g are absolutely continuous on [a,b], then their sum is absolutely continuous on [a,b].

Русский

Если функции f и g абсолютно непрерывны на [a,b], то их сумма тоже абсолютно непрерывна на [a,b].

LaTeX

$$$ \text{AbsolutelyContinuousOnInterval}(f,a,b) \wedge \text{AbsolutelyContinuousOnInterval}(g,a,b) \Rightarrow \text{AbsolutelyContinuousOnInterval}(f+g,a,b) $$$

Lean4

theorem fun_add (hf : AbsolutelyContinuousOnInterval f a b) (hg : AbsolutelyContinuousOnInterval g a b) :
    AbsolutelyContinuousOnInterval (fun x ↦ f x + g x) a b :=
  by
  apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using hf.add hg)
  · exact Finset.sum_nonneg (fun i hi ↦ by positivity)
  · rw [← Finset.sum_add_distrib]
    gcongr
    exact dist_add_add_le _ _ _ _

Похожие утверждения