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.

Well-definedness of the finite-dimensional mini backward Euler equations

Statement

Assume Countable Choice. For each fixed finite mesh and time partition in The mixed mini-element backward Euler Navier–Stokes scheme, every term of its velocity equation is a continuous finite-dimensional functional of the trial and test vectors, the pressure constraints are linear, and the forcing averages exist.

Facts & Assumptions

Given: Countable Choice, a bounded Lipschitz domain, a finite matching mesh, its mini spaces, a finite partition, $f \in L^{2} (0, T; L^{2})$ , and $u_{h}^{n - 1} \in Z_{h}$ .

[F1]

The MINI spaces are finite-dimensional subspaces of $H_{0}^{1} (D)^{d}$ and the weak kernel $Z_{h}$ is a finite-dimensional linear subspace. (The conforming P1-bubble/P1 mini element, Weak and pointwise divergence-free discrete velocities)

[F2]

The skew convective form is continuous on $V^{3}$ . (The skew convective form for incompressible flow, Continuity, energy cancellation, and Sobolev bounds for skew convection)

[A1]

Countable Choice is inherited from the MINI/Stokes space conventions; the Bochner criterion itself only uses the asserted strong measurability and integrable norm. (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The conforming P1-bubble/P1 mini element, Bochner integrability criterion)

[F3]

A strongly measurable $L^{2} (0, T; L^{2})$ function is Bochner integrable on the finite interval, since Holder makes its norm integrable. (Bochner-integrable function, Bochner integrability criterion, Holder's inequality for integrals, including the endpoint cases)

Proof

1.1F1givenalgebra

Every finite-dimensional subspace inherits the continuous inclusions and bilinear forms from $V$ and $H$ ; thus $(u_{h}^{n} - u_{h}^{n - 1}, v_{h})_{H}$ , $a_{ν} (u_{h}^{n}, v_{h})$ , and $b (v_{h}, p_{h}^{n})$ are continuous in their coordinates.

2.1A1F1F2F3step 1.1∎

The nonlinear term is continuous by [F2], and the force average is a finite vector in $L^{2} (D)^{d}$ by [F3] because each interval has $τ_{n} > 0$ . The divergence constraint is a finite set of linear equations in $V_{h}$ and $Q_{h}$ . These facts make the scheme a well-defined finite-dimensional system.

Depends on

Used by

Backward Euler MINI step existence and discrete energy bound Theorem

Cited to discharge well-definedness by The mixed mini-element backward Euler Navier–Stokes scheme.

Dependency tree · two levels

38 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)