English
If f has a simple root at x0 with positive derivative there, then near x0 the sign of f(x) matches the sign of x−x0.
Русский
Если у функции f есть простой корень в x0 и производная в окрестности x0 положительна, то знак f(x) близко к x0 совпадает со знаком x−x0.
LaTeX
$$$$\\text{If } f(x_0)=0,\\ f'(x_0)>0,\\text{ then } \\operatorname{sign}(f(x))=\\operatorname{sign}(x-x_0)\\text{ in a neighborhood of } x_0.$$$$
Lean4
/-- If the derivative of `f` is positive at a root `x₀` of `f`, then locally the sign of `f x`
matches `x - x₀`. -/
theorem eventually_nhdsWithin_sign_eq_of_deriv_pos (hf : deriv f x₀ > 0) (hx : f x₀ = 0) :
∀ᶠ x in 𝓝 x₀, sign (f x) = sign (x - x₀) :=
by
rw [← nhdsNE_sup_pure x₀, eventually_sup]
refine ⟨?_, by simpa⟩
have h_tendsto := hasDerivAt_iff_tendsto_slope.mp (differentiableAt_of_deriv_ne_zero <| ne_of_gt hf).hasDerivAt
filter_upwards [(h_tendsto.eventually <| eventually_gt_nhds hf), self_mem_nhdsWithin] with x hx₀ hx₁
rw [mem_compl_iff, mem_singleton_iff, ← Ne.eq_def] at hx₁
obtain (hx' | hx') := hx₁.lt_or_gt
· rw [sign_neg (neg_of_slope_pos hx' hx₀ hx), sign_neg (sub_neg.mpr hx')]
· rw [sign_pos (pos_of_slope_pos hx' hx₀ hx), sign_pos (sub_pos.mpr hx')]
