English
For any real p, if f grows polynomially and is nonnegative eventually, then f^p grows polynomially.
Русский
Для любого действительного p, если f растёт полиномиально и неотрицательна в бесконечности, то f^p растёт полиномиально.
LaTeX
$$$\\text{GrowsPolynomially}(f) \\land (\\forall^\\infty x, 0 \\le f(x)) \\Rightarrow \\text{GrowsPolynomially}(x \\mapsto (f(x))^{p})$$$
Lean4
protected theorem rpow (p : ℝ) (hf : GrowsPolynomially f) (hf_nonneg : ∀ᶠ x in atTop, 0 ≤ f x) :
GrowsPolynomially fun x => (f x) ^ p := by
intro b hb
obtain ⟨c₁, (hc₁_mem : 0 < c₁), c₂, hc₂_mem, hfnew⟩ := hf b hb
have hc₁p : 0 < c₁ ^ p := Real.rpow_pos_of_pos hc₁_mem _
have hc₂p : 0 < c₂ ^ p := Real.rpow_pos_of_pos hc₂_mem _
cases le_or_gt 0 p with
| inl => -- 0 ≤ p
refine ⟨c₁ ^ p, hc₁p, ?_⟩
refine ⟨c₂ ^ p, hc₂p, ?_⟩
filter_upwards [eventually_gt_atTop 0, hfnew, hf_nonneg,
(tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hf_nonneg] with x _ hf₁ hf_nonneg hf_nonneg₂
intro u hu
have fu_nonneg : 0 ≤ f u := hf_nonneg₂ u hu.1
refine ⟨?lb, ?ub⟩
case lb =>
calc
c₁ ^ p * (f x) ^ p = (c₁ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₁_mem) hf_nonneg]
_ ≤ _ := by gcongr; exact (hf₁ u hu).1
case ub =>
calc
(f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
_ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]
| inr hp => -- p < 0
match hf.eventually_atTop_zero_or_pos_or_neg with
| .inl hzero => -- eventually zero
refine ⟨1, by norm_num, 1, by norm_num, ?_⟩
filter_upwards [hzero, hfnew] with x hx hx'
intro u hu
simp only [hx, zero_rpow (ne_of_lt hp), mul_zero, Set.Icc_self, Set.mem_singleton_iff]
simp only [hx, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx'
rw [hx' u hu, zero_rpow (ne_of_lt hp)]
| .inr (.inl hpos) => -- eventually positive
refine ⟨c₂ ^ p, hc₂p, ?_⟩
refine ⟨c₁ ^ p, hc₁p, ?_⟩
filter_upwards [eventually_gt_atTop 0, hfnew, hpos,
(tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hpos] with x _ hf₁ hf_pos hf_pos₂
intro u hu
refine ⟨?lb, ?ub⟩
case lb =>
calc
c₂ ^ p * (f x) ^ p = (c₂ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₂_mem) (le_of_lt hf_pos)]
_ ≤ _ := rpow_le_rpow_of_exponent_nonpos (hf_pos₂ u hu.1) (hf₁ u hu).2 (le_of_lt hp)
case ub =>
calc
(f u) ^ p ≤ (c₁ * f x) ^ p := by
exact rpow_le_rpow_of_exponent_nonpos (by positivity) (hf₁ u hu).1 (le_of_lt hp)
_ = _ := by rw [← mul_rpow (le_of_lt hc₁_mem) (le_of_lt hf_pos)]
| .inr (.inr hneg) => -- eventually negative (which is impossible)
have : ∀ᶠ (_ : ℝ) in atTop, False := by filter_upwards [hf_nonneg, hneg] with x hx hx'; linarith
rw [Filter.eventually_false_iff_eq_bot] at this
exact False.elim <| (atTop_neBot).ne this
