LemmaStatement: Literature-sourcedProof: 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.

Strong L2 compactness for weakly solenoidal MINI trajectories

Statement

Assume the Axiom of Choice. Let $D \subset R^{d}$ be bounded, connected and polyhedral, $d = 2$ or $3$ . Let $T_{j}$ be matching shape-regular meshes with $h_{j} \to 0$ , let $Z_{j}$ be the weak MINI divergence kernels, and let $0 = t_{0}^{j} < \dots < t_{N_{j}}^{j} = T$ have maximum step tending to zero. Suppose $U_{j}^{n} \in Z_{j}$ , their piecewise-constant reconstructions ${\overline{U}}_{j}$ satisfy $\sup_{j} (\max_{n} ∥ U_{j}^{n} ∥_{L^{2}} + ∥ {\overline{U}}_{j} ∥_{L^{2} (0, T; H_{0}^{1})}) < \infty,$ and the following coefficient condition holds: for every finite $L^{2}$ -orthonormal family $e_{1}, \dots, e_{m} \in V_{σ}$ , the $E$ -valued piecewise-constant functions $Y_{j} (t) = \sum_{i = 1}^{m} (U_{j}^{n}, Π_{j} e_{i})_{L^{2}} e_{i} (t \in (t_{n - 1}^{j}, t_{n}^{j}])$ have uniformly bounded $L^{2} (0, T; E)$ norms and their backward difference quotients are bounded in $L^{4 / 3} (0, T; E)$ ; here $Π_{j}$ is the MINI Fortin map and $E = span {e_{i}}$ . Then $({\overline{U}}_{j})$ is relatively compact in $L^{2} (0, T; L^{2} (D)^{d})$ .

Facts & Assumptions

Given: The shape-regular matching mesh family, $Z_{j}$ , the energy bounds, the coefficient condition, and the Axiom of Choice.

[F1]

Under the Axiom of Choice, $H_{0}^{1} (D)$ embeds compactly into $L^{2} (D)$ on bounded open $D$ ; applying the scalar result successively to the finitely many components gives the same compact embedding for $H_{0}^{1} (D)^{d}$ . (Compactness of $W_{0}^{1, p} (Ω) ↪ L^{p} (Ω)$ on bounded open sets)

[F2]

$\int_{D} div z = 0$ for $z \in H_{0}^{1} (D)^{d}$ , and $b (z, q_{h}) = 0$ for $z \in Z_{j}$ , $q_{h} \in Q_{j}$ . (Zero mean of the divergence of a zero-boundary field, Weak and pointwise divergence-free discrete velocities)

[F3]

For $q \in H^{1} (D)$ , the face-average interpolant approximates it in $L^{2}$ ; subtracting the mean gives a continuous piecewise-affine zero-mean pressure approximation. (Boundary-preserving face-average P1 interpolation, Stokes velocity and pressure spaces and weak forms)

[F4]

The MINI Fortin map satisfies $b (Π_{j} v, q_{h}) = b (v, q_{h})$ and $∥ v - Π_{j} v ∥_{2} \leq C h_{j} ∥ v ∥_{V}$ . (Uniform Fortin stability of the mini element, The mini-element Fortin map approximates in L2)

[F5]

The piecewise-constant discrete Aubin–Lions theorem gives compactness in $L^{2} (0, T; E)$ from a uniform $L^{2} (E)$ bound and an $L^{4 / 3} (E)$ difference-quotient bound when the time steps vanish. (Piecewise-constant discrete Aubin–Lions compactness)

[F6]

The scalar space $H_{0}^{1} (D)$ with its Sobolev norm is a separable real Hilbert space; its finite vector product is therefore also separable and Hilbert. (The zero-boundary Sobolev energy space is a separable Hilbert space)

[F7]

Poincare makes the gradient norm on $H_{0}^{1} (D)^{d}$ equivalent to its Sobolev norm, so a sequence bounded in $V$ is bounded in the separable Hilbert norm and weak convergence is the same for both norms. Every bounded sequence in a separable real Hilbert space has a weakly convergent subsequence. (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction, A bounded sequence in a separable Hilbert space has a weakly convergent subsequence)

[F8]

The Sobolev norm is weakly lower semicontinuous; the equivalent gradient norm on $V$ is also weakly lower semicontinuous. (Weak lower semicontinuity of the Sobolev norm, The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction)

[F9]

The Bochner space $L^{2} (0, T; L^{2} (D)^{d})$ is complete. (Bochner Lp is complete for a Banach value space)

[A1]

The compactness and subsequence extractions use the Axiom of Choice. (The Axiom of Choice)

Proof

1.1A1F1F2F3givenalgebra

Consider any sequence $z_{j} \in Z_{j}$ with $∥ z_{j} ∥_{V} \leq R$ and $h_{j} \to 0$ . By [F1], a subsequence converges strongly in $L^{2}$ and weakly in $H_{0}^{1}$ to some $z \in H_{0}^{1}$ . For any $q \in C_{c}^{\infty} (D)$ , put $q^{0} = q - ∣ D ∣^{- 1} \int_{D} q$ , interpolate $q^{0}$ by [F3], and subtract the interpolant's mean to obtain $q_{j} \in Q_{j}$ with $q_{j} \to q^{0}$ in $L^{2}$ . Since $b (z_{j}, q_{j}) = 0$ and $\int_{D} div z_{j} = 0$ by [F2], $\int_{D} q div z_{j} = \int_{D} (q^{0} - q_{j}) div z_{j} \to 0$ . Weak convergence of the gradients gives $div z = 0$ , hence $z \in V_{σ}$ .

1.2A1F4F5givenalgebra

For an $L^{2}$ -orthonormal basis $e_{1}, \dots, e_{m}$ of $E$ , [F4] and the uniform $L^{\infty} L^{2}$ bound imply $∥ P_{E} {\overline{U}}_{j} - Y_{j} ∥_{L^{\infty} (0, T; E)}^{2} = \sum_{i} ∣ (U_{j}^{n}, e_{i} - Π_{j} e_{i})_{L^{2}} ∣^{2} \leq C_{E} h_{j}^{2} .$ The coefficient condition and [F5], applied to the finite-dimensional evolution triple $E ↪ E ↪ E$ , make $(Y_{j})$ relatively compact in $L^{2} (0, T; E)$ .

2.1A1F1F6F7F8step 1.1choose

For each $R > 0$ , $K_{R} = {z \in V_{σ} : ∥ z ∥_{V} \leq R}$ is totally bounded in $L^{2}$ by [F1], so choose a finite $ϵ / 2$ -net with centers $e_{i} \in K_{R}$ and let $E$ be their span. If arbitrarily fine meshes had $z_{j} \in Z_{j}$ , $∥ z_{j} ∥_{V} \leq R$ , and distance at least $ϵ$ from $E$ , [A1, F1, F6, F7] would give a subsequence strongly convergent in $L^{2}$ and weakly in $H_{0}^{1}$ . Step 1.1 puts its limit in $K_{R}$ , and [F8] retains the norm bound; this contradicts the $ϵ / 2$ -net. Thus every such $z_{j}$ is within $ϵ$ of $E$ for all sufficiently large $j$ .

3.1givenstep 2.1algebra

Let $P_{E}$ be the $L^{2}$ -orthogonal projection. On times when $∥ {\overline{U}}_{j} (t) ∥_{V} \leq R$ , step 2.1 gives $∥ {\overline{U}}_{j} - P_{E} {\overline{U}}_{j} ∥_{2} \leq ϵ$ . The measure of the remaining times is at most $R^{- 2} ∥ {\overline{U}}_{j} ∥_{L^{2} V}^{2}$ , and there $∥ {\overline{U}}_{j} - P_{E} {\overline{U}}_{j} ∥_{2} \leq 2 \sup_{j, n} ∥ U_{j}^{n} ∥_{2}$ . First choose $R$ large, then $ϵ$ small; this makes the $L^{2} (0, T; L^{2})$ projection remainder uniformly small for sufficiently large $j$ .

4.1F5F9step 3.1step 1.2algebra∎

Given any tolerance, steps 3.1 and 1.2 approximate the tail of $({\overline{U}}_{j})$ within that tolerance by a relatively compact family $Y_{j}$ in $L^{2} (0, T; E)$ . Hence the tail is totally bounded in $L^{2} (0, T; L^{2})$ ; adjoining finitely many initial terms preserves total boundedness. Completeness [F9] gives relative compactness.

Depends on

Used by

MINI backward Euler converges subsequentially to a solenoidal energy weak velocity Theorem

Dependency tree · two levels

80 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

Endre Süli and Tabea Tscherpel, Fully discrete finite element approximation of unsteady flows of implicitly constituted incompressible fluids, arXiv:1804.02264v1 (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)