AI 中文总结
在Lean 4中形式化二维Navier--Stokes方程全局Leray--Hopf弱解的Galerkin构造，涵盖任意有界开域及矩形域，并推广到抽象Hilbert空间演化方程。
AI 中文摘要
我们在Lean 4中形式化了无外力二维Navier--Stokes方程在任意有界开域上具有无滑移边界条件的全局Leray--Hopf弱解的Galerkin构造。对于无散度L2速度空间中的每个初始数据，解具有弱连续的速度路径，在时间上局部满足弱方程，并在每个时刻满足能量不等式。对于矩形域，我们还形式化了在能量对偶空间中具有连续外力的有限时域解。该开发包括无散度图空间、紧致谱坐标、输运抵消、Ladyzhenskaya估计以及同时空间-时间紧致性。抽象的Hilbert空间结果适用于具有紧致能量到速度嵌入和斜三线性非线性的演化方程。
英文摘要
We formalize in Lean 4 the Galerkin construction of global Leray--Hopf weak solutions for the unforced two-dimensional Navier--Stokes equations on arbitrary bounded open domains with no-slip boundary conditions. For every initial datum in the solenoidal \(L^2\) velocity space, the solution has a weakly continuous velocity path, satisfies the weak equation locally in time, and obeys the energy inequality at every time. For rectangles, we also formalize finite-horizon solutions with continuous forcing in the dual energy space. The development includes divergence-free graph spaces, compact spectral coordinates, transport cancellation, Ladyzhenskaya estimates, and simultaneous space--time compactness. The abstract Hilbert-space results apply to evolution equations with a compact energy-to-velocity embedding and a skew trilinear nonlinearity.
