2.9 把任意精度写清楚

2.9.1 把“再近一点”改成一场有规则的挑战¶

对方先指定输出误差 $\varepsilon>0$，你必须给出一个输入范围 $\delta>0$，保证之后任何落在范围内的输入都满足要求。关键是顺序：不能先挑一个有利的输入，再为它选择范围；也不能只展示几个成功的输入。

在线性函数 $f(x)=3x+2$ 中，输出误差恰为输入误差的三倍。要把输出误差压到 $\varepsilon$ 以下，取 $\delta=\varepsilon/3$ 即可。这个选择展示了完整逻辑：从目标精度反推输入限制，然后对所有满足限制的输入验证。

2.9.2 非线性时先给变化倍率一个上界¶

平方函数的误差是 $|x^2-a^2|=|x-a||x+a|$。第二个因子也随输入变化，不能当常数。先要求 $|x-a|<1$，就有 $|x+a|<2|a|+1$；再取 $$\delta=\min\!\left(1,\frac{\varepsilon}{2|a|+1}\right),$$ 两个要求就同时成立。这个额外的一并不是答案本身，而是先把局部倍率圈住的工具。

你可以选择更小的 $\delta$，定义不要求最佳范围。证明的目标是给出有效保证，而非求最大容许误差。这样的自由度常让推导简洁许多。

画一条包住目标值的水平细带，再找围绕输入点的竖直细带，使图像在竖带内都落进横带。图形解释了量词，但最终仍需不等式把所有点一起控制。这是从视觉直觉走向严格论证的一次完整练习。

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

theorem epsilon_delta_linear (a ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ x : ℝ, |x-a| < δ → |(3*x+2)-(3*a+2)| < ε := by
  refine ⟨ε/3, by positivity, ?_⟩
  intro x hx
  have heq : (3*x+2)-(3*a+2)=3*(x-a) := by ring
  rw [heq, abs_mul, abs_of_pos (by norm_num : (0:ℝ)<3)]
  linarith

-- A concrete removable-singularity limit, not the full general l'Hopital theorem.