2.7 隐函数求导 · 从直觉到证明

一步一步建立直观

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

令右图保持单位半径。圆方程 $x^2+y^2=1$ 要求点的两个坐标协同变化：一个变大时，另一个必须做出补偿。沿圆运动的小位移 $(dx,dy)$ 在一阶上满足 $2x\,dx+2y\,dy=0$ ，这比先求出上下两个平方根分支更直接。

约束的梯度 $(2x,2y)$ 沿半径向外，切向位移与它垂直，所以一阶变化为零。转到圆的左端点，切线竖直；此时不能把附近的整段圆当成一个可微的 $y(x)$ 。隐式关系仍然有意义，某种坐标表达却可能失效。

从约束式得到 $dy/dx=-x/y$ 时，必须假设 $y\ne0$ 。回到圆顶，分母非零，斜率为零；回到左右端点，分母为零，提示应换用 $x(y)$ 或参数表示。公式里的限制并非技术障碍，而是图形姿态在坐标中的真实反映。

圆由 $x^2+y^2=1$ 描述，不必先把 $y$ 解成一个全局函数。沿圆移动时， $x$ 和 $y$ 不能自由独立变化，它们必须共同维持这个约束。若 $x$ 增加一点，另一个坐标要怎样配合，才能仍在曲线上？

对关系作一阶变化，得到 $2x\,dx+2y\,dy=0$ 。这里的 $dy$ 不是任意小量，而是曲线约束要求的响应。若 $y\ne0$ ，解出 $dy/dx=-x/y$ ，就得到局部斜率，无须展开平方根。

在 $(3/5,4/5)$ 处，斜率为 $-3/4$ 。向右走一点必须略向下，才能补偿横坐标平方的增加。切线给出这种补偿的一阶近似；有限移动后的点通常不在圆上，因为曲线还存在二阶弯曲。

来到 $(1,0)$ ，公式不能除以 $y$ 。这并非圆突然不光滑，而是此处不能用单值的 $y(x)$ 斜率描述垂直切线。改用 $x$ 作为 $y$ 的局部函数，就能恢复合适的坐标语言。一个几何对象是否规则，与某种表示是否方便，是两个问题。

一般关系 $F(x,y)=0$ 中，沿曲线总变化为零，得到 $F_x+F_y y'=0$ 。使用它时仍须核对相关可微性及局部函数存在条件。Lean 对照只验证微分约束后的代数解法；不要把这一点误认为已经证明任意隐式关系都能解成光滑函数。

与本图相连的定义与证明：5.4 · 乘以 i 保持长度并旋转直角。本节的具体条件与形式化范围见下文。

曲线由关系式定义，不必先显式解出 $y$ 。沿曲线移动时，定义关系的总变化必须为零。

若 $F(x,y(x))=0$ 且相关函数可微，则 $F_x+F_y y'=0$ 。对 $x^2+y^2=1$ ，当 $y\ne0$ 时 $y'=-x/y$ 。

例 2.7.1 把概念用于具体计算

在 $(3/5,4/5)$ 处，切线斜率为 $-3/4$ ，切线方程为 $3x+4y=5$ 。

在同一点沿切线有 $dx=0.04$ ，一阶估计 $dy$ 。

展开解答与检查

答案 $-0.03$ 。

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

从微分约束 $2x\,dx+2y\,dy=0$ 和 $y\ne0$ 推导 $dy=-x\,dx/y$ ；隐函数存在性定理未形式化。

Calculus.circle_tangent

theorem circle_tangent (x y dx dy : ℝ) (hy : y ≠ 0)
    (h : 2*x*dx+2*y*dy=0) : dy= -x*dx/y := by
  apply (eq_div_iff hy).2
  nlinarith

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

沿约束曲线移动，观察两个坐标必须如何互相补偿，并留意垂直切线。

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