English
If g grows polynomially and f =Θ_atTop g, then f grows polynomially (assuming f is eventually nonnegative).
Русский
Если g растёт полиномиально и f = Θ_atTop g, то f растёт полиномиально (при условии, что f неотсрочно неотрицательна).
LaTeX
$$$\\text{GrowsPolynomially}(g) \\to (f =_ {atTop} Θ g) \\to (\\forall^\\infty x, 0 \\le f(x)) \\Rightarrow \\text{GrowsPolynomially}(f)$$$
Lean4
theorem of_isTheta {f g : ℝ → ℝ} (hg : GrowsPolynomially g) (hf : f =Θ[atTop] g) (hf' : ∀ᶠ x in atTop, 0 ≤ f x) :
GrowsPolynomially f := by
intro b hb
have hb_pos := hb.1
have hf_lb := isBigO_iff''.mp hf.isBigO_symm
have hf_ub := isBigO_iff'.mp hf.isBigO
obtain ⟨c₁, hc₁_pos : 0 < c₁, hf_lb⟩ := hf_lb
obtain ⟨c₂, hc₂_pos : 0 < c₂, hf_ub⟩ := hf_ub
have hg := hg.norm b hb
obtain ⟨c₃, hc₃_pos : 0 < c₃, hg⟩ := hg
obtain ⟨c₄, hc₄_pos : 0 < c₄, hg⟩ := hg
have h_lb_pos : 0 < c₁ * c₂⁻¹ * c₃ := by positivity
have h_ub_pos : 0 < c₂ * c₄ * c₁⁻¹ := by positivity
refine ⟨c₁ * c₂⁻¹ * c₃, h_lb_pos, ?_⟩
refine ⟨c₂ * c₄ * c₁⁻¹, h_ub_pos, ?_⟩
have c₂_cancel : c₂⁻¹ * c₂ = 1 := inv_mul_cancel₀ (by positivity)
have c₁_cancel : c₁⁻¹ * c₁ = 1 := inv_mul_cancel₀ (by positivity)
filter_upwards [(tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf',
(tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf_lb,
(tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf_ub,
(tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hg, eventually_ge_atTop 0] with x hf_pos h_lb h_ub
hg_bound 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 rw [one_mul]
have hg_bound := hg_bound x hbx
refine ⟨?lb, ?ub⟩
case lb =>
calc
c₁ * c₂⁻¹ * c₃ * f x ≤ c₁ * c₂⁻¹ * c₃ * (c₂ * ‖g x‖) := by rw [← Real.norm_of_nonneg (hf_pos x hbx)]; gcongr;
exact h_ub x hbx
_ = (c₂⁻¹ * c₂) * c₁ * (c₃ * ‖g x‖) := by ring
_ = c₁ * (c₃ * ‖g x‖) := by simp [c₂_cancel]
_ ≤ c₁ * ‖g u‖ := by gcongr; exact (hg_bound u hu).1
_ ≤ f u := by
rw [← Real.norm_of_nonneg (hf_pos u hu.1)]
exact h_lb u hu.1
case ub =>
calc
f u ≤ c₂ * ‖g u‖ := by rw [← Real.norm_of_nonneg (hf_pos u hu.1)]; exact h_ub u hu.1
_ ≤ c₂ * (c₄ * ‖g x‖) := by gcongr; exact (hg_bound u hu).2
_ = c₂ * c₄ * (c₁⁻¹ * c₁) * ‖g x‖ := by simp [c₁_cancel]; ring
_ = c₂ * c₄ * c₁⁻¹ * (c₁ * ‖g x‖) := by ring
_ ≤ c₂ * c₄ * c₁⁻¹ * f x := by
gcongr
rw [← Real.norm_of_nonneg (hf_pos x hbx)]
exact h_lb x hbx
