4.7 把微分方程变成代数方程

一步一步建立直观

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

01把一个初值问题看成待求的整条信号

选定初始状态后，局部速度规则产生整条未来轨迹。拉普拉斯方法将这条未知信号整体送到参数域，在那里把微分操作转成乘法，同时留下初始值项。右图的初值拖动可以提醒我们：初始条件改变，解就改变，变换计算不能把它丢掉。

02为什么导数变换带着边界项

对加权积分做分部积分，导数从未知信号转移到指数核上，因而出现乘以 $s$ 的项。下端点则贡献初始值，上端点需借助衰减条件消失。因此公式不是单纯的“把求导替换成乘法”；边界与收敛假设同样参与计算。

03代数解仍要回到原问题核对

改成增长轨迹，观察解的长期行为怎样变化。在参数域求出的分式必须在合适的收敛域内解释，再还原时间函数，最后检查微分方程与初值。右图不是拉普拉斯计算器，而是用于核对所得解的轨迹、初值与稳定性是否合理的模型。

4.7.1 求导为何变成乘法¶

从 $\int_0^\infty y'(t)\mathrm e^{-st}\,dt$ 出发，对乘积做分部积分。导数从 $y$ 移到指数核时带出 $s$ ，下端边界留下 $-y(0)$ ，无穷远边界在适当增长与收敛条件下消失。于是得到 $\mathcal L(y')=sY-y(0)$ 。

再做一次，就得到二阶导数的变换，除 $s^2Y$ 外，还必须保留初始位置和初始速度。初值并没有因换到变换域而消失，而是以边界项的形式编码进去。

4.7.2 把一条完整求解链走完¶

考虑 $y'+2y=0,y(0)=3$ 。变换后是 $sY-3+2Y=0$ ，解得 $Y=3/(s+2)$ ，再从已知指数变换识别 $y=3\mathrm e^{-2t}$ 。最后求导代回并检查零时刻值，完成闭环验证。

二阶受迫振子类似：先整理成 $(s^2+\omega^2)Y=F+sy_0+v_0$ ，再除以分母。每一项都有来源，若漏了初始值，得到的就会是另一个问题。分母中的根提示系统模态，但还需结合收敛域和约定理解。

变换法把困难移到了另一个表示中，并没有免除存在性和反演条件。Lean 在这里核验的是已经得到代数方程之后的求商步骤；积分分部与函数空间条件仍属于正文分析。读证明时要知道每一步解决了哪一部分，而不是把整个方法看成一条自动规则。

与本图相连的定义与证明：4.1 · 长度平方的增长只由径向项控制。本节的具体条件与形式化范围见下文。

数学表述 4.7.1¶

积分分部把求导转换为乘 $s$ ，同时保留初始值。于是线性常系数方程可以在变换域中求解。

在所需光滑、增长及收敛条件下， $\mathcal L(y')=sY-y(0)$ ， $\mathcal L(y'')=s^2Y-sy(0)-y'(0)$ 。若 $y''+\omega^2y=f$ ，则 $Y(s)=\frac{F(s)+sy_0+v_0}{s^2+\omega^2}.$

例 4.7.1 把概念用于具体计算

$f=0,y_0=0,v_0=1$ 给 $Y=1/(s^2+\omega^2)$ ，当 $\omega>0$ 时对应 $y(t)=\sin(\omega t)/\omega$ 。

练习 4.7.1¶

$y'+2y=0,y(0)=3$ 的变换与解？

展开解答与检查

$Y=3/(s+2)$ ， $y=3\mathrm{e}^{-2t}$ 。

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

从已得到的变换域等式及非零分母推导商公式。积分分部、拉普拉斯存在性和反演不在该形式命题中。

DifferentialEquations.transformed_oscillator

theorem transformed_oscillator (s ω Y F y₀ v₀ : ℝ)
    (h : s^2*Y-s*y₀-v₀+ω^2*Y=F) (hn : s^2+ω^2 ≠ 0) :
    Y=(F+s*y₀+v₀)/(s^2+ω^2) := by
  apply (eq_div_iff hn).2
  nlinarith

查看完整定义与上下文 ↗ · 全书证明范围

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

逐步记录分部积分产生的初值项，最后将反演结果代回原方程。

官方课程与图示 ↗ · 原视频 ↗

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