2.8 极限与导数的定义 · 从直觉到证明

一步一步建立直观

先预测，再点“演示本步”核对右图。每一步都重设到指定情形，随后可以自由修改参数。

先观察非零步长下的割线。极限问题不是要求在 $h=0$ 计算差商，而是问：当 $h$ 从允许的非零值靠近零时，差商能否被逼近到某个固定数。右图保留两个点，让“接近”与“已经重合”在操作上分开。

平方函数的差商与 $2a$ 相差恰好 $h$ 。因此只要要求 $|h|$ 小于给定误差，就能确保读数达到目标精度。这比观察小数位看起来稳定更强：它说明对任意要求的精度，都有一个明确的输入范围保证结果。

改变步长的正负，从观察点两侧接近。两侧趋向同一值，才得到通常的双侧导数；若函数只在一侧有定义，应声明研究的是单侧极限。窗口提供的其他函数也有自己的定义域，尤其不能在实对数的非正输入处假装得到函数值。

把 $(x^2-1)/(x-1)$ 的输入逐渐靠近一，会发现输出靠近二。原表达式在一处无定义，但这不妨碍附近的趋势稳定。极限问的是：输入足够接近时，输出能否被迫足够接近某个目标，而不是问在那个点代入后得到什么。

对 $x\ne1$ ，因式分解允许约去 $x-1$ ，表达式等于 $x+1$ 。这说明邻近行为与一个简单连续函数相同。即使人为把原函数在一处的值设成七，极限仍是二；只有把该点值补成二，它才连续。

算几个小步长只能提示候选极限，不能证明所有更小步长都满足要求。一个函数可能在你没取到的点强烈振荡。证明需要把“足够近”写成一种对整片邻域有效的保证，下一节将把这个保证拆成输入和输出两种误差。

左右也必须分别检查。一个跳跃函数从左边靠近与从右边靠近可能指向不同值；单侧趋势各自稳定，不代表双侧极限存在。导数的差商同样需要这项检查，绝对值函数的尖角就是一个例子。

最后区分三个问题：函数在一点有没有值，附近有没有极限，极限是否等于点值。连续性把后二者连接，可导性再要求差商具有极限。把这些问题逐个问清，比笼统地说“函数很平滑”更精确。

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

极限描述输入接近某处时输出是否能被控制到任意精度，并不要求函数在该点已有定义。

连续性是 $\lim_{x\to a}f(x)=f(a)$ ；导数是另一函数“差商”的去心极限。多项式连续，所以 $\lim_{x\to a}x^2=a^2$ 。

例 2.8.1 把概念用于具体计算

$(x^2-1)/(x-1)$ 在 $x=1$ 未定义，但对 $x\ne1$ 等于 $x+1$ ，因此极限为 $2$ ，可用补值修复连续性。

把上例在 $x=1$ 处定义成 $7$ ，极限变了吗？

展开解答与检查

没有，仍为 $2$ ，但不连续。

Lean 对照 2.8.1 命题、证明与适用边界

完整验证平方函数的双侧极限；使用邻域过滤器表达“趋近”。

Calculus.square_limit

theorem square_limit (a : ℝ) :
    Tendsto (fun x : ℝ => x^2) (𝓝 a) (𝓝 (a^2)) :=
  (continuous_pow 2).continuousAt.tendsto

原课对照观课问题、视频与图示

区分函数在点上的值与附近的趋势，检查左右靠近是否得到同一结果。

点击后连接 YouTube；播放器不可用时可通过上方原链接观看。