English
Let u, v, t, w be real-valued functions on a set with a filter l. If u is asymptotically equivalent to v and t is asymptotically equivalent to w with respect to l, and v and w are pointwise nonnegative, then u + t is asymptotically equivalent to v + w with respect to l.
Русский
Пусть u, v, t, w — функции из множества в ℝ, определённые на одном наборе с фильтром l. Если u эквивалентно v по отношению к l и t эквивалентно w по отношению к l, причём для всех аргументов v(p) ≥ 0 и w(p) ≥ 0, тогда u(p) + t(p) эквивалентно v(p) + w(p) по отношению к l.
LaTeX
$$$u \sim_l v \; \land \; t \sim_l w \; \land \; (\forall x, 0 \le v(x)) \; \land \; (\forall x, 0 \le w(x)) \Rightarrow (u+t) \sim_l (v+w)$$$
Lean4
theorem add_add_of_nonneg {α : Type*} {u v t w : α → ℝ} {l : Filter α} (hu : 0 ≤ v) (hw : 0 ≤ w) (htu : u ~[l] v)
(hvw : t ~[l] w) : u + t ~[l] v + w :=
by
simp only [IsEquivalent, add_sub_add_comm]
change (fun x ↦ (u - v) x + (t - w) x) =o[l] (fun x ↦ v x + w x)
conv => enter [3, x]; rw [← abs_eq_self.mpr (hu x), ← abs_eq_self.mpr (hw x)]
simpa [← Real.norm_eq_abs] using .add_add htu hvw
