2.10 洛必达法则：比较消失速度

2.10.1 两个量都趋零，比例仍可能完全不同¶

$x/x$、$x^2/x$ 与 $x/x^2$ 的分子分母都趋零，比值却分别趋向一、零，或在零附近无界。零除以零不是一种答案，它只是提示直接代入没有揭示相对消失速度。需要进一步比较两个量的一阶或更高阶变化。

若 $f(a)=g(a)=0$，且两者可导、$g'(a)\ne0$，局部近似给出 $f(a+h)\approx f'(a)h$ 与 $g(a+h)\approx g'(a)h$，因此比例接近导数之比。这个简单版本提供了直觉，但一般洛必达法则可以处理更复杂的去心区间情况，需要明确的条件。

2.10.2 法则是有条件的工具¶

下面列出的条件要求相关区间可微、分母导数不为零，并且导数比值具有极限。使用时先判断原式的未定形式，再核对这些条件。仅仅看到一个分式，不意味着可以把分子分母各求一次导数。

例如 $(x+1)/(x+2)$ 在零附近没有未定性，直接连续代入得 $1/2$；随意求导反而得到一。又如 $(x^2-1)/(x-1)$ 在一处，可以因式分解直接求极限，没必要把简单结构藏到一般定理里。

如果一次求导后仍是未定式，再用一次也要重新核对条件。洛必达法则的假设不满足，并不能反推原极限不存在，只能说明这个工具暂时不给结论。解题时应先看能否约分、换元或利用已知局部近似，再考虑更一般的方法。

与本图相连的定义与证明：2.2 · 平方函数的差商与误差。本节的具体条件与形式化范围见下文。

theorem removable_limit :
    Tendsto (fun x : ℝ => (x^2-1)/(x-1)) (𝓝[≠] 1) (𝓝 2) := by
  have h : (fun x : ℝ => (x^2-1)/(x-1)) =ᶠ[𝓝[≠] 1] (fun x => x+1) := by
    filter_upwards [self_mem_nhdsWithin] with x hx
    have hn : x-1 ≠ 0 := sub_ne_zero.mpr hx
    field_simp
    ring
  apply Tendsto.congr' h.symm
  have hc : ContinuousAt (fun x : ℝ => x+1) 1 := by fun_prop
  have hlim : Tendsto (fun x : ℝ => x+1) (𝓝[≠] (1:ℝ)) (𝓝 ((1:ℝ)+1)) :=
    hc.tendsto.mono_left nhdsWithin_le_nhds
  norm_num at hlim
  exact hlim