TheoremStatement: AI-adaptedProof: AI-adaptedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

First-order smooth pressure-primitive error for backward Euler MINI

Statement

Assume Countable Choice and every domain, mesh, time-partition, smooth-solution, initialization and time-step hypothesis of Smooth-branch velocity error for backward Euler MINI. Thus $D$ is a bounded connected Lipschitz polyhedral domain in dimension $d \in {2, 3}$ , the matching affine simplicial meshes are shape regular, $ν > 0$ , $f \in L^{2} (0, T; L^{2} (D)^{d})$ , and $(u, p)$ is a strong no-slip solution with $u \in W^{1, \infty} (0, T; H^{2} (D)^{d} \cap V_{σ}), p \in W^{1, \infty} (0, T; H^{1} (D) \cap Q), Q = L_{0}^{2} (D) .$ The point values of these classes mean their unique continuous representatives, constructed in the proof using Countable Choice. Set $M = 1 + ∥ u ∥_{W^{1, \infty} H^{2}} + ∥ p ∥_{W^{1, \infty} H^{1}}, M_{u} = ∥ u ∥_{L^{\infty} V}, M_{E} = ν^{- 1 / 2} ∥ u (0) ∥_{2} + C_{P} ν^{- 1} ∥ f ∥_{L^{2} L^{2}} .$ Let $C_{*}$ and $Λ$ be exactly the explicit viscosity-dependent constants in Smooth-branch velocity error for backward Euler MINI and impose its restriction $τ_{\max} Λ \leq 1 / 2$ . Use the same initialization $u_{h}^{0} = P_{Z_{h}} u (0)$ and any mixed backward Euler MINI solution. Define $e_{n} = u (t_{n}) - u_{h}^{n}, E_{0} = \max_{0 \leq n \leq N} ∥ e_{n} ∥_{2}, E_{1} = {(\sum_{n = 1}^{N} τ_{n} ∥ e_{n} ∥_{V}^{2})}^{1 / 2}, H = h M + τ_{\max} M^{2} .$ Let $β > 0$ be the uniform MINI inf-sup lower bound, $M_{b} = \sqrt{d}$ , and let $C_{I}$ be a mean-adjusted continuous P1 pressure interpolation constant satisfying $\inf_{q_{h} \in Q_{h}} ∥ q - q_{h} ∥_{2} \leq C_{I} h ∥ q ∥_{H^{1} (D)} (q \in H^{1} (D) \cap Q) .$ Choose $C_{c}$ with $∣ c (a; b, v) ∣ \leq C_{c} ∥ a ∥_{V} ∥ b ∥_{V} ∥ v ∥_{V}$ , put $P (t) = \int_{0}^{t} p (s) d s$ , $P_{h}^{0} = 0$ , $P_{h}^{m} = \sum_{n = 1}^{m} τ_{n} p_{h}^{n}$ , and let $P_{h}$ be the continuous piecewise-affine interpolant through $P_{h}^{m}$ . Then $\max_{0 \leq m \leq N} ∥ P (t_{m}) - P_{h}^{m} ∥_{2} \leq (1 + M_{b} / β) C_{I} T h M + β^{- 1} (2 C_{P} E_{0} + [2 ν \sqrt{T} + C_{c} (M_{E} + \sqrt{T} M_{u})] E_{1} + 2 ν T τ_{\max} M + 2 C_{c} T τ_{\max} M^{2}) .$ In particular, with $K = (1 + M_{b} / β) C_{I} T + β^{- 1} (2 C_{P} + [2 ν \sqrt{T} + C_{c} (M_{E} + \sqrt{T} M_{u})] ν^{- 1 / 2}) C_{*} + β^{- 1} (2 ν T + 2 C_{c} T),$ one has $\max_{m} ∥ P (t_{m}) - P_{h}^{m} ∥_{2} \leq K H, ∥ P - P_{h} ∥_{L^{\infty} (0, T; Q)} \leq (K + 1) H .$ For the right-constant pressure reconstruction ${\overline{p}}_{h} (t) = p_{h}^{n}$ on $(t_{n - 1}, t_{n}]$ , every $η \in C_{c}^{\infty} (0, T)$ also satisfies ${∥ \int_{0}^{T} (p (t) - {\overline{p}}_{h} (t)) η (t) d t ∥}_{2} \leq (K + 1) H ∥ η^{'} ∥_{L^{1} (0, T)} .$ The constants are independent of $h$ and the individual time steps; their viscosity dependence includes the displayed powers and the exponential contained in $C_{*}$ . No additional mesh/time relation is imposed. This estimate controls accumulated pressure and the stated negative time norm; it does not claim an instantaneous $L_{t}^{4 / 3} L_{x}^{2}$ pressure-error rate.

Facts & Assumptions

Given: Countable Choice, the smooth solution, MINI scheme solution, constants, initialization and partition in the Statement.

[A1]

Countable Choice is the only choice principle needed for the local representative argument below; it is also inherited by the smooth velocity, MINI stability and Bochner suppliers. No use of the Axiom of Choice or Dependent Choice is added here. (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Smooth-branch velocity error for backward Euler MINI)

[F1]

The strong solution satisfies the full time-tested mixed equation, with $b (v, q) = - (q, div v)$ and $∣ a_{ν} (v, w) ∣ \leq 2 ν ∥ v ∥_{V} ∥ w ∥_{V}$ ; every term is integrable. (Energy weak solutions of incompressible Navier–Stokes, Integrability of the energy weak Navier–Stokes formulation, Stokes velocity and pressure spaces and weak forms)

[F2]

The current smooth velocity theorem gives $E_{0} + \sqrt{ν} E_{1} \leq C_{*} H$ . The discrete energy theorem gives $\sum_{n} τ_{n} ∥ u_{h}^{n} ∥_{V}^{2} \leq M_{E}^{2}$ . (Smooth-branch velocity error for backward Euler MINI, Backward Euler MINI step existence and discrete energy bound)

[F3]

The MINI pressure space $Q_{h}$ from The conforming P1-bubble/P1 mini element is finite-dimensional and has inf-sup constant $β > 0$ . The face-average P1 interpolant in Boundary-preserving face-average P1 interpolation maps $H^{1} (D)$ to the continuous P1 space and has $L^{2}$ error at most $C h ∥ q ∥_{H^{1}}$ on the stated shape-regular meshes. Also $∣ b (v, q) ∣ \leq \sqrt{d} ∥ v ∥_{V} ∥ q ∥_{2}$ . (Uniform Fortin stability of the mini element, Boundary-preserving face-average P1 interpolation, The conforming P1-bubble/P1 mini element, Stokes velocity and pressure spaces and weak forms)

[F4]

The skew form is trilinear and satisfies the $V^{3}$ bound in the Statement under Countable Choice, as proved directly in the skew-form supplier. Poincare gives $∥ v ∥_{2} \leq C_{P} ∥ v ∥_{V}$ , and Holder gives the weighted time Cauchy–Schwarz estimates used below. (The skew convective form for incompressible flow, Continuity, energy cancellation, and Sobolev bounds for skew convection, The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction, Holder's inequality for integrals, including the endpoint cases)

[F5]

The Bochner norm inequality and bounded-linear-map interchange apply to interval averages and primitives. Scalar Fubini applies to the time integrals. (Bochner-integrable function, Strongly measurable Banach-valued function, Bochner integrability criterion, Bochner integral norm inequality, Bounded linear maps commute with Bochner integration, Fubini's theorem for L^1 functions on a sigma-finite product)

[F6]

$L^{2} (D)$ is a separable real Hilbert space, and every closed subspace has an orthogonal decomposition by Orthogonal decomposition by a closed subspace. $H^{1} (D)$ and $H^{2} (D)^{d}$ embed into finite products of $L^{2} (D)$ by listing their weak derivatives and are separable as subspaces under Countable Choice. A locally integrable scalar function defining the zero distribution vanishes almost everywhere, and countable unions of null sets are null. ( $L^{2}$ with the integral pairing is a Hilbert space, Rational box-step functions form a countable dense subset of $L^{p} (R^{n})$ for $1 \leq p < \infty$ , Separability: the existence of an at most countable dense subset, Locally integrable functions embed in distributions, A countable union of measure-zero sets has measure zero, by countable choice)

Proof

technique · direct

Given: The strong solution and all MINI scheme inputs in the Statement.

1.1A1F5F6givenconstruct

To justify pointwise time estimates without strengthening Countable Choice, let $X$ be either $H^{2} (D)^{d}$ or $H^{1} (D) \cap Q$ , let $w \in W^{1, \infty} (0, T; X)$ , and let $g = w^{'} \in L^{\infty} (0, T; X)$ be its weak Bochner derivative. The separability of $X$ is [F6]. Define $G (t) = \int_{0}^{t} g (s) d s$ . By [F5], $∥ G (t) - G (s) ∥_{X} \leq ∥ g ∥_{L^{\infty} X} ∣ t - s ∣$ . For $ξ \in X$ and $ϕ \in C_{c}^{\infty} (0, T)$ , scalar Fubini gives $- \int_{0}^{T} (G (t), ξ)_{X} ϕ^{'} (t) d t = - \int_{0}^{T} \int_{0}^{t} (g (s), ξ)_{X} d s ϕ^{'} (t) d t = \int_{0}^{T} (g (s), ξ)_{X} ϕ (s) d s .$ Thus $G^{'} = g$ in scalar distributions and $(w - G, ξ)$ has zero distributional derivative.

1.2F1givenalgebra

For $v \in V$ , Cauchy–Schwarz for the matrix trace gives $∣ div v ∣ = ∣ tr \nabla v ∣ \leq \sqrt{d} ∣ \nabla v ∣$ almost everywhere. Integrating and applying Cauchy–Schwarz yields $∥ b (v, q) ∥ \leq \sqrt{d} ∥ v ∥_{V} ∥ q ∥_{2} = M_{b} ∥ v ∥_{V} ∥ q ∥_{2}$ , as used in the Statement.

1.3F3F6givenconstructalgebra

For $q \in H^{1} (D) \cap Q$ , let $I_{h} q$ be the face-average P1 interpolant from [F3] and set $r_{h}^{0} q = I_{h} q - ∣ D ∣^{- 1} \int_{D} I_{h} q$ . This belongs to $Q_{h}$ . Since $q$ has mean zero, Cauchy–Schwarz gives $∣ D ∣^{1 / 2} ∣ ∣ D ∣^{- 1} \int_{D} I_{h} q ∣ \leq ∥ I_{h} q - q ∥_{2}$ , hence $∥ q - r_{h}^{0} q ∥_{2} \leq 2 ∥ q - I_{h} q ∥_{2} \leq 2 C h ∥ q ∥_{H^{1} (D)}$ . Thus some finite uniform best-approximation constant exists, as required by the Statement. Now let $r_{h}$ be the $L^{2}$ -orthogonal projection onto $Q_{h}$ . The finite-dimensional space $Q_{h}$ is closed in Hilbert $Q$ ; [F6] gives its unique orthogonal decomposition. Uniqueness makes $r_{h}$ linear, and Pythagoras gives $∥ r_{h} q ∥_{2} \leq ∥ q ∥_{2}$ , so it is bounded. The Statement's selected best-approximation constant therefore yields $∥ q - r_{h} q ∥_{2} = \inf_{q_{h} \in Q_{h}} ∥ q - q_{h} ∥_{2} \leq C_{I} h ∥ q ∥_{H^{1} (D)}$ .

2.1F6step 1.1algebra

A locally integrable scalar function with zero distributional derivative is constant almost everywhere. Indeed, fix $ρ \in C_{c}^{\infty} (0, T)$ with $\int ρ = 1$ . For any $ϕ \in C_{c}^{\infty} (0, T)$ , $ψ = ϕ - (\int ϕ) ρ$ has integral zero, so $θ (t) = \int_{0}^{t} ψ (s) d s$ belongs to $C_{c}^{\infty} (0, T)$ and $θ^{'} = ψ$ . The zero-derivative identity gives $\int (w - G, ξ) ψ = 0$ , hence $\int (w - G, ξ) ϕ = c_{ξ} \int ϕ$ with $c_{ξ} = \int (w - G, ξ) ρ$ . Injectivity of the locally integrable embedding into distributions [F6] yields $(w - G, ξ) = c_{ξ}$ almost everywhere.

3.1A1F6step 1.1step 2.1construct

Choose a countable dense set $(ξ_{k})$ in $X$ . By [F6], the scalar identities in step 2.1 hold outside one common null set. Choose $t_{0}$ outside that set where the Bochner representative of $w$ is defined, and put $c = w (t_{0}) - G (t_{0})$ . Density gives $w (t) - G (t) = c$ for almost every $t$ . Thus $w^{*} (t) = G (t) + c$ is the unique continuous representative and is Lipschitz with constant $∥ w^{'} ∥_{L^{\infty} X}$ . Apply this to $u$ and $p$ : for all $s, t$ , $∥ u (t) - u (s) ∥_{V} \leq M ∣ t - s ∣$ and $∥ p (t) - p (s) ∥_{H^{1}} \leq M ∣ t - s ∣$ . Continuity and their essential bounds then give $∥ u (t) ∥_{V} \leq M_{u}$ and $∥ p (t) ∥_{H^{1}} \leq M$ for every $t$ . Also $M \geq M_{u}$ , since the $H^{2}$ norm controls the $V$ norm. These representatives are the ones used for the nodal errors in the existing smooth velocity theorem.

4.1F1F5F6step 3.1givenalgebra

Write $u_{n} = u (t_{n})$ , ${\overline{u}}_{n} = τ_{n}^{- 1} \int_{t_{n - 1}}^{t_{n}} u (t) d t$ , and use bars similarly for exact pressure, forcing and convection. For each vector in a basis of the finite-dimensional $V_{h}$ , [F1] and step 3.1 imply that the full scalar momentum residual is the zero distribution. All residual terms are integrable, so [F6] identifies that residual with zero almost everywhere; integrating over each time cell and using $u (t_{n}) - u (t_{n - 1}) = \int_{t_{n - 1}}^{t_{n}} u_{t}$ from step 3.1 gives the exact interval equation. Subtract the mixed backward Euler equations and sum through $m$ . The identical forcing averages cancel and the time derivatives telescope, giving for every $v_{h} \in V_{h}$ $b (v_{h}, P (t_{m}) - P_{h}^{m}) = - (e_{m} - e_{0}, v_{h})_{2} - \sum_{n \leq m} τ_{n} a_{ν} ({\overline{u}}_{n} - u_{h}^{n}, v_{h}) - \sum_{n \leq m} τ_{n} ({\overline{c (u; u, v_{h})}}_{n} - c (u_{h}^{n}; u_{h}^{n}, v_{h})) .$ No projection onto the discrete kernel is used in this identity.

5.1F3F5step 1.2step 1.3step 4.1constructalgebra

Set $R_{h}^{m} = \int_{0}^{t_{m}} r_{h} p (t) d t \in Q_{h}$ , where $r_{h}$ is the $L^{2}$ -orthogonal pressure-space projection chosen in step 1.3. Its bounded linearity and [F5] give $∥ P (t_{m}) - R_{h}^{m} ∥_{2} \leq C_{I} \int_{0}^{t_{m}} h ∥ p (t) ∥_{H^{1}} d t \leq C_{I} T h M .$ Apply inf-sup to $R_{h}^{m} - P_{h}^{m}$ , and use $∣ b (v_{h}, R_{h}^{m} - P (t_{m})) ∣ \leq M_{b} ∥ v_{h} ∥_{V} ∥ R_{h}^{m} - P (t_{m}) ∥_{2}$ . The triangle inequality yields $∥ P (t_{m}) - P_{h}^{m} ∥_{2} \leq (1 + M_{b} / β) C_{I} T h M + β^{- 1} \sup_{v_{h} \neq 0} \frac{∣ b (v_{h}, P (t_{m}) - P_{h}^{m}) ∣}{∥ v_{h} ∥_{V}} .$

5.2F1F2F4step 3.1step 4.1algebra

Poincare bounds $∣ (e_{m} - e_{0}, v_{h})_{2} ∣ \leq 2 C_{P} E_{0} ∥ v_{h} ∥_{V}$ . Step 3.1 gives $∥ {\overline{u}}_{n} - u_{n} ∥_{V} \leq τ_{n} M$ , hence $\sum_{n \leq m} τ_{n} ∥ {\overline{u}}_{n} - u_{h}^{n} ∥_{V} \leq \sqrt{T} E_{1} + T τ_{\max} M .$ The viscosity contribution in step 4.1 is therefore at most $2 ν (\sqrt{T} E_{1} + T τ_{\max} M) ∥ v_{h} ∥_{V}$ .

5.3F2F4step 4.1algebra

Trilinearity gives $c (u_{n}; u_{n}, v_{h}) - c (u_{h}^{n}; u_{h}^{n}, v_{h}) = c (e_{n}; u_{n}, v_{h}) + c (u_{h}^{n}; e_{n}, v_{h}) .$ Its absolute value is at most $C_{c} (∥ u_{n} ∥_{V} + ∥ u_{h}^{n} ∥_{V}) ∥ e_{n} ∥_{V} ∥ v_{h} ∥_{V}$ . Weighted Cauchy–Schwarz, $∥ u_{n} ∥_{V} \leq M_{u}$ , and [F2] show that its summed contribution is at most $C_{c} (\sqrt{T} M_{u} + M_{E}) E_{1} ∥ v_{h} ∥_{V}$ .

6.1F4step 3.1step 4.1step 5.3algebra

For $t \in (t_{n - 1}, t_{n})$ , split $c (u (t); u (t), v_{h}) - c (u_{n}; u_{n}, v_{h}) = c (u (t) - u_{n}; u (t), v_{h}) + c (u_{n}; u (t) - u_{n}, v_{h}) .$ By step 3.1, $∥ u (t) - u_{n} ∥_{V} \leq τ_{n} M$ , and $M \geq M_{u}$ . The $V^{3}$ estimate bounds the integrand by $2 C_{c} τ_{n} M^{2} ∥ v_{h} ∥_{V}$ . Integrating over the cells through $m$ gives at most $2 C_{c} T τ_{\max} M^{2} ∥ v_{h} ∥_{V}$ , completing the convection bound in step 4.1.

7.1F2step 5.1step 5.2step 5.3step 6.1algebra

Insert the estimates in steps 5.2, 5.3, and 6.1 into step 5.1. This gives the first displayed pressure-primitive inequality, uniformly in $m$ . Substitute $E_{0} \leq C_{*} H$ and $E_{1} \leq ν^{- 1 / 2} C_{*} H$ from [F2]. Since $M \geq 1$ , both $h M$ and $τ_{\max} M$ are at most $H$ , and $τ_{\max} M^{2} \leq H$ . The resulting coefficient is exactly $K$ , so $\max_{m} ∥ P (t_{m}) - P_{h}^{m} ∥_{2} \leq K H$ .

8.1F5step 3.1step 7.1algebra

The exact primitive $P$ is Lipschitz in $Q$ with constant at most $∥ p ∥_{L^{\infty} Q} \leq M$ , by step 3.1. Let $\tilde{P}$ interpolate its exact endpoint values affinely on the partition. For $t \in [t_{n - 1}, t_{n}]$ and $α = (t - t_{n - 1}) / τ_{n}$ , $P (t) - \tilde{P} (t) = (1 - α) (P (t) - P (t_{n - 1})) + α (P (t) - P (t_{n})),$ so $∥ P (t) - \tilde{P} (t) ∥_{2} \leq 2 α (1 - α) τ_{n} M \leq τ_{\max} M$ . Convexity gives $∥ \tilde{P} - P_{h} ∥_{L^{\infty} Q} \leq \max_{m} ∥ P (t_{m}) - P_{h}^{m} ∥_{2}$ . Together with step 7.1 this proves $∥ P - P_{h} ∥_{L^{\infty} Q} \leq (K + 1) H$ , because $τ_{\max} M \leq H$ .

9.1F5step 8.1algebra∎

On each time cell, $P_{h}^{'} = {\overline{p}}_{h}$ . Scalar integration by parts against $η \in C_{c}^{\infty} (0, T)$ and cancellation of the node terms give the $Q$ -valued identity $\int_{0}^{T} (p - {\overline{p}}_{h}) η d t = - \int_{0}^{T} (P - P_{h}) η^{'} d t .$ Scalarization and [F5] justify the vector identity; its norm is at most $∥ P - P_{h} ∥_{L^{\infty} Q} ∥ η^{'} ∥_{L^{1}}$ . Step 8.1 proves the stated negative-time-norm estimate.

Remarks

This is an additive pressure estimate under the existing initialization and smooth-solution hypotheses. Differentiating a small primitive does not give a small instantaneous $L_{t}^{4 / 3} Q$ pressure error. The original unrestricted instantaneous pressure-rate clause is separately refuted by the smooth graded-mesh counterexample on the companion page; this does not change any hypothesis or conclusion here. The proof uses uniform inf-sup after time integration and neither assumes nor derives uniform $H^{1}$ stability of the mass-orthogonal projector onto $Z_{h}$ .

Depends on

Used by

PE06 instantaneous pressure refutations and retained primitive estimates Remark

Dependency tree · two levels

127 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jean-Luc Guermond, MATH 661 Fall 2025, Chapter 53: Stokes equations (standard reference, not scraped)
Daniele Boffi, Franco Brezzi, Michel Fortin, Mixed Finite Element Methods and Applications (standard reference, not scraped)
Endre Süli and Tabea Tscherpel, Fully discrete finite element approximation of unsteady flows of implicitly constituted incompressible fluids (standard reference, not scraped)
Xiaoming He, Introduction and Basic Implementation for Finite Element Methods, Chapter 9: Finite elements for 2D unsteady Navier–Stokes equations (standard reference, not scraped)