Have you seen the updates from more recent work of the same Coq group you cite? To quote from their article this week:
Our long-term purpose is to formally prove the correctness of parts of a library implementing the Finite Element Method (FEM), which is used to compute approximated solutions of Partial Differential Equations (PDEs). We already formalized the Lax–Milgram theorem , one of the key ingredient to numerically solve PDEs, and we need to build suitable Hilbert functional spaces on which to apply it. The target candidates are the Sobolev spaces such as $H^1$, that represents square integrable functions with square integrable first derivatives. Of course, this will involve
the formalization of the $L^p$ Lebesgue spaces as complete normed vector spaces, and parts of the distribution theory.
In terms of your question,
verification of the numerical methods for PDEs
is very different from
the exposition of (any aspects of) the traditional PDE theory in proof assistants
I work in Lean and would say that mathlib is clearly heading toward the latter. For example, mathlib has $L^p$ spaces and the Lax-Milgram theorem, (soon) some theory on compact operators, and work in progress on distribution theory. The Sobolev inequalities are a big missing piece.
But there is nothing on numerics and the mathlib library is not particularly friendly to code generation.