English
If f and g grow polynomially and are nonnegative eventually, then f+g grows polynomially.
Русский
Если f и g растут полиномиально и в конечном счете неотрицательны, то f+g растёт полиномиально.
LaTeX
$$$\\text{GrowsPolynomially}(f) \\to \\text{GrowsPolynomially}(g) \\to (0 \\le^\\infty f) \\to (0 \\le^\\infty g) \\to \\text{GrowsPolynomially}(x \\mapsto f(x)+g(x))$$$
Lean4
protected theorem add {f g : ℝ → ℝ} (hf : GrowsPolynomially f) (hg : GrowsPolynomially g) (hf' : 0 ≤ᶠ[atTop] f)
(hg' : 0 ≤ᶠ[atTop] g) : GrowsPolynomially fun x => f x + g x :=
by
intro b hb
have hf := hf b hb
have hg := hg b hb
obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf
obtain ⟨c₃, hc₃_mem, c₄, _, hg⟩ := hg
refine ⟨min c₁ c₃, by change 0 < min c₁ c₃; positivity, ?_⟩
refine ⟨max c₂ c₄, by change 0 < max c₂ c₄; positivity, ?_⟩
filter_upwards [hf, hg, (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hf',
(tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hg', eventually_ge_atTop 0] with x hf hg hf' hg' hx_pos
intro u hu
have hbx : b * x ≤ x :=
calc
b * x ≤ 1 * x := by gcongr; exact le_of_lt hb.2
_ = x := by ring
have fx_nonneg : 0 ≤ f x := hf' x hbx
have gx_nonneg : 0 ≤ g x := hg' x hbx
refine ⟨?lb, ?ub⟩
case lb =>
calc
min c₁ c₃ * (f x + g x) = min c₁ c₃ * f x + min c₁ c₃ * g x := by simp only [mul_add]
_ ≤ c₁ * f x + c₃ * g x := by
gcongr
· exact min_le_left _ _
· exact min_le_right _ _
_ ≤ f u + g u := by
gcongr
· exact (hf u hu).1
· exact (hg u hu).1
case ub =>
calc
max c₂ c₄ * (f x + g x) = max c₂ c₄ * f x + max c₂ c₄ * g x := by simp only [mul_add]
_ ≥ c₂ * f x + c₄ * g x := by
gcongr
· exact le_max_left _ _
· exact le_max_right _ _
_ ≥ f u + g u := by
gcongr
· exact (hf u hu).2
· exact (hg u hu).2
