English
If f grows polynomially and g = o_atTop(f), then f+g grows polynomially.
Русский
Если f растёт полиномиально, а g = o_atTop(f), то f+g растёт полиномиально.
LaTeX
$$$\\text{GrowsPolynomially}(f) \\land (g =o_{\\text{atTop}} f) \\Rightarrow \\text{GrowsPolynomially}(x \\mapsto f(x)+g(x))$$$
Lean4
theorem add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomially f) (hfg : g =o[atTop] f) :
GrowsPolynomially fun x => f x + g x := by
intro b hb
have hb_ub := hb.2
rw [isLittleO_iff] at hfg
cases hf.eventually_atTop_nonneg_or_nonpos with
| inl hf' => -- f is eventually non-negative
have hf := hf b hb
obtain ⟨c₁, hc₁_mem : 0 < c₁, c₂, hc₂_mem : 0 < c₂, hf⟩ := hf
specialize hfg (c := 1 / 2) (by norm_num)
refine ⟨c₁ / 3, by positivity, 3 * c₂, by positivity, ?_⟩
filter_upwards [hf, (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hfg,
(tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hf', eventually_ge_atTop 0] with x hf₁ hfg' hf₂
hx_nonneg
have hbx : b * x ≤ x := by nth_rewrite 2 [← one_mul x]; gcongr
have hfg₂ : ‖g x‖ ≤ 1 / 2 * f x := by
calc
‖g x‖ ≤ 1 / 2 * ‖f x‖ := hfg' x hbx
_ = 1 / 2 * f x := by congr; exact norm_of_nonneg (hf₂ _ hbx)
have hx_ub : f x + g x ≤ 3 / 2 * f x := by
calc
_ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
_ ≤ f x + 1 / 2 * f x := by gcongr
_ = 3 / 2 * f x := by ring
have hx_lb : 1 / 2 * f x ≤ f x + g x := by
calc
f x + g x ≥ f x - ‖g x‖ := by rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x)
_ ≥ f x - 1 / 2 * f x := by gcongr
_ = 1 / 2 * f x := by ring
intro u ⟨hu_lb, hu_ub⟩
have hfu_nonneg : 0 ≤ f u := hf₂ _ hu_lb
have hfg₃ : ‖g u‖ ≤ 1 / 2 * f u := by
calc
‖g u‖ ≤ 1 / 2 * ‖f u‖ := hfg' _ hu_lb
_ = 1 / 2 * f u := by congr; simp only [norm_eq_abs, abs_eq_self, hfu_nonneg]
refine ⟨?lb, ?ub⟩
case lb =>
calc
f u + g u ≥ f u - ‖g u‖ := by rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le _
_ ≥ f u - 1 / 2 * f u := by gcongr
_ = 1 / 2 * f u := by ring
_ ≥ 1 / 2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1
_ = c₁ / 3 * (3 / 2 * f x) := by ring
_ ≥ c₁ / 3 * (f x + g x) := by gcongr
case ub =>
calc
_ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
_ ≤ f u + 1 / 2 * f u := by gcongr
_ = 3 / 2 * f u := by ring
_ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
_ = 3 * c₂ * (1 / 2 * f x) := by ring
_ ≤ 3 * c₂ * (f x + g x) := by gcongr
| inr hf' => -- f is eventually nonpos
have hf := hf b hb
obtain ⟨c₁, hc₁_mem : 0 < c₁, c₂, hc₂_mem : 0 < c₂, hf⟩ := hf
specialize hfg (c := 1 / 2) (by norm_num)
refine ⟨3 * c₁, by positivity, c₂ / 3, by positivity, ?_⟩
filter_upwards [hf, (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hfg,
(tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hf', eventually_ge_atTop 0] with x hf₁ hfg' hf₂
hx_nonneg
have hbx : b * x ≤ x := by nth_rewrite 2 [← one_mul x]; gcongr
have hfg₂ : ‖g x‖ ≤ -1 / 2 * f x := by
calc
‖g x‖ ≤ 1 / 2 * ‖f x‖ := hfg' x hbx
_ = 1 / 2 * (-f x) := by congr; exact norm_of_nonpos (hf₂ x hbx)
_ = _ := by ring
have hx_ub : f x + g x ≤ 1 / 2 * f x := by
calc
_ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
_ ≤ f x + (-1 / 2 * f x) := by gcongr
_ = 1 / 2 * f x := by ring
have hx_lb : 3 / 2 * f x ≤ f x + g x := by
calc
f x + g x ≥ f x - ‖g x‖ := by rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le (g x)
_ ≥ f x + 1 / 2 * f x := by
rw [sub_eq_add_neg]
gcongr
refine le_of_neg_le_neg ?bc.a
rwa [neg_neg, ← neg_mul, ← neg_div]
_ = 3 / 2 * f x := by ring
intro u ⟨hu_lb, hu_ub⟩
have hfu_nonpos : f u ≤ 0 := hf₂ _ hu_lb
have hfg₃ : ‖g u‖ ≤ -1 / 2 * f u := by
calc
‖g u‖ ≤ 1 / 2 * ‖f u‖ := hfg' _ hu_lb
_ = 1 / 2 * (-f u) := by congr; exact norm_of_nonpos hfu_nonpos
_ = -1 / 2 * f u := by ring
refine ⟨?lb, ?ub⟩
case lb =>
calc
f u + g u ≥ f u - ‖g u‖ := by rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le _
_ ≥ f u + 1 / 2 * f u := by
rw [sub_eq_add_neg]
gcongr
refine le_of_neg_le_neg ?_
rwa [neg_neg, ← neg_mul, ← neg_div]
_ = 3 / 2 * f u := by ring
_ ≥ 3 / 2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1
_ = 3 * c₁ * (1 / 2 * f x) := by ring
_ ≥ 3 * c₁ * (f x + g x) := by gcongr
case ub =>
calc
_ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
_ ≤ f u - 1 / 2 * f u := by
rw [sub_eq_add_neg]
gcongr
rwa [← neg_mul, ← neg_div]
_ = 1 / 2 * f u := by ring
_ ≤ 1 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
_ = c₂ / 3 * (3 / 2 * f x) := by ring
_ ≤ c₂ / 3 * (f x + g x) := by gcongr
