English
If f grows polynomially, then its reciprocal f(x)^{-1} grows polynomially.
Русский
Если f растёт полиномиально, то 1/f растёт полиномиально.
LaTeX
$$$\\text{GrowsPolynomially}(f) \\Rightarrow \\text{GrowsPolynomially}(x \\mapsto (f(x))^{-1})$$$
Lean4
protected theorem inv {f : ℝ → ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially fun x => (f x)⁻¹ := by
cases hf.eventually_atTop_zero_or_pos_or_neg with
| inl hf' =>
refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩
have hb_pos := hb.1
filter_upwards [hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf'] with x hx hx'
intro u hu
simp only [hx, inv_zero, mul_zero, Set.Icc_self, Set.mem_singleton_iff, hx' u hu.1]
| inr
hf_pos_or_neg =>
suffices GrowsPolynomially fun x => |(f x)⁻¹| by
cases hf_pos_or_neg with
| inl
hf' =>
have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => |(f x)⁻¹| :=
by
filter_upwards [hf'] with x hx₁
rw [abs_of_nonneg (inv_nonneg_of_nonneg (le_of_lt hx₁))]
rwa [iff_eventuallyEq hmain]
| inr
hf' =>
have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹| :=
by
filter_upwards [hf'] with x hx₁
simp [abs_of_nonpos (inv_nonpos.mpr (le_of_lt hx₁))]
rw [iff_eventuallyEq hmain]
exact this.neg
have hf' : ∀ᶠ x in atTop, f x ≠ 0 := by
cases hf_pos_or_neg with
| inl H => filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm
| inr H => filter_upwards [H] with _ hx; exact (ne_of_gt hx).symm
simp only [abs_inv]
have hf := hf.abs
intro b hb
have hb_pos := hb.1
obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf b hb
refine ⟨c₂⁻¹, by change 0 < c₂⁻¹; positivity, ?_⟩
refine ⟨c₁⁻¹, by change 0 < c₁⁻¹; positivity, ?_⟩
filter_upwards [hf, hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf'] with x hx hx' hx''
intro u hu
have h₁ : 0 < |f u| := by rw [abs_pos]; exact hx'' u hu.1
refine ⟨?lb, ?ub⟩
case lb =>
rw [← mul_inv]
gcongr
exact (hx u hu).2
case ub =>
rw [← mul_inv]
gcongr
exact (hx u hu).1
