TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

Backward Euler MINI step existence and discrete energy bound

Statement

Assume Countable Choice, the mini-element hypotheses of The mixed mini-element backward Euler Navier–Stokes scheme, $f \in L^{2} (0, T; L^{2} (D)^{d})$ , and an initial value $u_{h}^{0} \in Z_{h}$ . On every finite positive time partition there is at least one mixed solution $(u_{h}^{n}, p_{h}^{n})_{n = 1}^{N}$ of the backward Euler scheme. Every such solution satisfies, for $0 \leq m \leq N$ , the work-form inequality $\frac{1}{2} ∥ u_{h}^{m} ∥_{2}^{2} + \frac{1}{2} \sum_{n = 1}^{m} ∥ u_{h}^{n} - u_{h}^{n - 1} ∥_{2}^{2} + ν \sum_{n = 1}^{m} τ_{n} ∥ \nabla u_{h}^{n} ∥_{2}^{2} \leq \frac{1}{2} ∥ u_{h}^{0} ∥_{2}^{2} + \sum_{n = 1}^{m} τ_{n} (f_{h}^{n}, u_{h}^{n})_{L^{2}} .$ Consequently it satisfies the mesh-independent estimate $\frac{1}{2} ∥ u_{h}^{m} ∥_{2}^{2} + \frac{1}{2} \sum_{n = 1}^{m} ∥ u_{h}^{n} - u_{h}^{n - 1} ∥_{2}^{2} + \frac{ν}{2} \sum_{n = 1}^{m} τ_{n} ∥ \nabla u_{h}^{n} ∥_{2}^{2} \leq \frac{1}{2} ∥ u_{h}^{0} ∥_{2}^{2} + \frac{C_{P} (D)^{2}}{2 ν} ∥ f ∥_{L^{2} (0, T; L^{2})}^{2} .$ The constant is independent of mesh size and time-step sizes.

Facts & Assumptions

Given: Countable Choice, the MINI spaces, $ν > 0$ , a finite partition, $f \in L^{2} (0, T; L^{2})$ , and $u_{h}^{0} \in Z_{h}$ .

[A1]

Countable Choice is inherited from the MINI/Stokes stability supplier; no arbitrary-index choice is used inside a single finite partition. (The Axiom of Countable Choice ( ${A C}_{ω}$ ), Uniform Fortin stability of the mini element)

[F1]

The velocity mass form is real Hilbert; $a_{ν} (z, z) = 2 ν ∥ ε (z) ∥_{2}^{2} \geq ν ∥ \nabla z ∥_{2}^{2}$ on $H_{0}^{1}$ . (Stokes velocity and pressure spaces and weak forms, The homogeneous Dirichlet strain identity)

[F2]

$c (z; z, z) = 0$ for every $z \in V$ , and $c$ is continuous on the finite-dimensional MINI space. (The skew convective form for incompressible flow, Continuity, energy cancellation, and Sobolev bounds for skew convection)

[F3]

A continuous finite-dimensional map with positive outward radial pairing on a sphere has a zero in the ball. (An outward-pointing finite-dimensional map has a zero)

[F4]

The stable MINI pair has a positive discrete inf-sup constant, so the pressure map is injective and the velocity constraint map is onto. (Uniform Fortin stability of the mini element, Weak and pointwise divergence-free discrete velocities)

[F5]

The identity $2 (x - y, x) = ∥ x ∥^{2} - ∥ y ∥^{2} + ∥ x - y ∥^{2}$ holds in $L^{2}$ , and Poincare gives $∥ z ∥_{2} \leq C_{P} (D) ∥ \nabla z ∥_{2}$ . (The Hilbert-space discrete energy identity, The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction)

[F6]

Holder and Young absorb $∥ f_{h}^{n} ∥_{2} ∥ u_{h}^{n} ∥_{2}$ into $ν ∥ \nabla u_{h}^{n} ∥_{2}^{2} / 2$ with remainder $C_{P} (D)^{2} ∥ f_{h}^{n} ∥_{2}^{2} / (2 ν)$ . (Holder's inequality for integrals, including the endpoint cases, Young's inequality for conjugate real exponents)

[F7]

The norm of a Bochner integral is at most the integral of the norm. (Bochner integral norm inequality)

Proof

1.1A1F2givenconstruct

Fix a time cell and the previous value $u_{h}^{n - 1} \in Z_{h}$ . On $Z_{h}$ , define $F_{n} (z) \in Z_{h}^{*}$ by $⟨ F_{n} (z), w_{h} ⟩ = τ_{n}^{- 1} (z - u_{h}^{n - 1}, w_{h})_{L^{2}} + a_{ν} (z, w_{h}) + c (z; z, w_{h}) - (f_{h}^{n}, w_{h})_{L^{2}} .$ The map is continuous by [F2] and finite dimensionality. If $Z_{h} = {0}$ its only velocity is zero; otherwise represent $F_{n}$ in coordinates of a gradient-orthonormal basis of $Z_{h}$ .

2.1F1F2F3givenstep 1.1algebra

By [F1]–[F2], $⟨ F_{n} (z), z ⟩ \geq ν ∥ \nabla z ∥_{2}^{2} - C_{P} (D) (τ_{n}^{- 1} ∥ u_{h}^{n - 1} ∥_{2} + ∥ f_{h}^{n} ∥_{2}) ∥ \nabla z ∥_{2} .$ Choose $R$ so the right side is strictly positive whenever $∥ \nabla z ∥_{2} = R$ . The outward-zero result [F3] supplies $u_{h}^{n} \in Z_{h}$ with $F_{n} (u_{h}^{n}) = 0$ .

3.1F4step 2.1algebra

Let $G_{n} (v_{h})$ be the velocity residual (time term plus viscosity and convection minus forcing). Step 2.1 gives $G_{n} = 0$ on $Z_{h} = \ker B$ , where $B v_{h} (q_{h}) = b (v_{h}, q_{h})$ . Since [F4] makes $B$ onto $Q_{h}^{*}$ , $B^{*}$ is injective and its range is contained in $(\ker B)^{\circ}$ . Rank-nullity gives both spaces dimension $\dim Q_{h}$ , so they are equal. Thus $- G_{n} = B^{*} p_{h}^{n}$ for a unique $p_{h}^{n} \in Q_{h}$ , which gives the stated mixed equation with the correct residual sign. Repeating the finite step for $n = 1, \dots, N$ gives a mixed solution.

4.1F1F2F5givenstep 3.1

Test the mixed equation with $u_{h}^{n}$ . Its pressure term is zero since $u_{h}^{n} \in Z_{h}$ , and its convective term is zero by [F2]. Apply [F5] to the time term and [F1] to the viscosity term, obtaining $\frac{1}{2} (∥ u_{h}^{n} ∥_{2}^{2} - ∥ u_{h}^{n - 1} ∥_{2}^{2} + ∥ u_{h}^{n} - u_{h}^{n - 1} ∥_{2}^{2}) + ν τ_{n} ∥ \nabla u_{h}^{n} ∥_{2}^{2} \leq τ_{n} (f_{h}^{n}, u_{h}^{n})_{L^{2}} .$ The right side is retained with its sign; it follows directly from the tested equation, skew cancellation, and the lower Korn bound.

5.1F5F6F7step 4.1algebra∎

Before applying Young, retain the actual work term in step 4.1 and sum over $n = 1, \dots, m$ ; telescoping gives the first displayed inequality. For the coarser estimate, Cauchy–Schwarz, Poincare and Young give $τ_{n} (f_{h}^{n}, u_{h}^{n}) \leq \frac{ν}{2} τ_{n} ∥ \nabla u_{h}^{n} ∥_{2}^{2} + \frac{C_{P} (D)^{2}}{2 ν} τ_{n} ∥ f_{h}^{n} ∥_{2}^{2} .$ For each interval, [F7] and Holder [F6] give $τ_{n} ∥ f_{h}^{n} ∥_{2}^{2} = τ_{n}^{- 1} {∥ \int_{t_{n - 1}}^{t_{n}} f (t) d t ∥}_{2}^{2} \leq τ_{n}^{- 1} {(\int_{t_{n - 1}}^{t_{n}} ∥ f (t) ∥_{2} d t)}^{2} \leq \int_{t_{n - 1}}^{t_{n}} ∥ f (t) ∥_{2}^{2} d t .$ Summing proves $\sum_{n} τ_{n} ∥ f_{h}^{n} ∥_{2}^{2} \leq ∥ f ∥_{L^{2} L^{2}}^{2}$ . Substitution into the work-form inequality proves the second displayed estimate.

Depends on

Used by

Dependency tree · two levels

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