Alphabeta Math
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.

Mini-element H1 velocity and L2 pressure error estimate

Statement

Assume Countable Choice. Let D be a bounded connected Lipschitz polygonal/polyhedral domain in dimension d=2 or 3, with a conforming shape-regular simplicial mesh family of mesh size h. Put V=H01(D;Rd) and Q=L02(D). For ν>0 and F∈V′, suppose (u,p)∈V×Q satisfies 2ν∫Dε(u):ε(v)−∫Dp div⁡v=F(v),−∫Dq div⁡u=0 for every v∈V,q∈Q, with u∈H2(D;Rd) and p∈H1(D). Let (uh,ph)∈Vh×Qh solve the same equations for every vh∈Vh,qh∈Qh, where Vh,Qh are the P1-bubble/P1 mini spaces. Then ∥u−uh∥H1(D)+∥p−ph∥L2(D)≤Ch(∥u∥H2(D)+∥p∥H1(D)). The constant is independent of h and depends on d, D, shape regularity, ν, Cdiv(D), and the Poincare constant. The mixed error formula retains Ma=2ν, Mb=d, discrete-kernel coercivity α∗=ν, and βh≥(CFCdiv(D))−1 explicitly.

Facts & Assumptions

Given: Countable Choice; the continuous Stokes solution with the stated regularity, the mini-element spaces, a conforming shape-regular mesh, and positive viscosity ν.

[A1]

Countable Choice is inherited through the Sobolev Hilbert and interpolation inputs. (The Axiom of Countable Choice (ACω))

[F1]

The mini pair is Vh=[Sh,01]d⊕∑KbKRd, Qh=Sh1∩L02, with continuous piecewise P1 pressures. (The conforming P1-bubble/P1 mini element)

[F2]

The face-average map is defined on all of H1(D) with values in continuous piecewise P1, has the H1-to-L2 and H2-to-H1 estimates, and maps H01(D) into the zero-boundary subspace. (Boundary-preserving face-average P1 interpolation)

[F3]

The mini Fortin map gives βh≥(CFCdiv(D))−1, and the mixed Galerkin theorem gives the explicit velocity/pressure bounds Uh,Ph. (Uniform Fortin stability of the mini element, Mixed Galerkin error bound retaining beta_h)

[F4]

The Stokes conventions are aν(u,v)=2ν∫ε(u):ε(v), b(v,q)=−∫qdiv⁡v, and the velocity gradient norm; the zero-boundary Poincare inequality controls the full H1 norm. (Stokes velocity and pressure spaces and weak forms, A bounded-domain Poincare inequality for H1-zero fields)

[F5]

The homogeneous Korn identity gives 2∥ε(v)∥22=∥∇v∥22+∥div⁡v∥22. (The homogeneous Dirichlet strain identity)

[F6]

Holder bounds the mean of an L2 error by ∣D∣1/2 times its L2 norm. (Holder's inequality for integrals, including the endpoint cases)

[F7]

The L2 Cauchy--Schwarz inequality gives ∫∣fg∣≤∥f∥2∥g∥2. (Cauchy-Schwarz inequality for L2)

Proof

1.1A1F1F2F6given

Set wh=Ihu. By [F2], wh∈Vh and δu:=∥u−wh∥V≤CIh∥u∥H2. Define p~h=Ihp and subtract its mean, rh=p~h−∣D∣−1∫Dp~h. Then rh∈Qh. Since p has zero mean, ∣D∣1/2∣D∣−1∣∫D(p~h−p)∣≤∥p~h−p∥2, and [F2] gives δp:=∥p−rh∥2≤2CIh∥p∥H1.

2.1A1F3F4F5F7step 1.1

The strain bound ∣ε(v)∣≤∣∇v∣F and Cauchy–Schwarz give Ma≤2ν; ∣div⁡v∣≤d∣∇v∣F gives Mb≤d. By [F5], aν(v,v)=2ν∥ε(v)∥22≥ν∥∇v∥22 for every v∈Vh, so α∗=ν. The uniform Fortin theorem in [F3] supplies the stated βh bound.

3.1A1F2F3step 1.1step 2.1

Apply [F3] with the approximants of step 1.1 and these constants. The explicit quantities Rh,Uh,Ph are linear combinations of δu,δp with coefficients depending only on ν,d,βh; the lower bound on βh makes those coefficients uniform in h. Thus ∥u−uh∥V+∥p−ph∥2≤Ch(∥u∥H2+∥p∥H1).

4.1A1F4step 3.1∎

Since u−uh∈H01(D)d, [F4] gives ∥u−uh∥H1≤(1+CP(D)2)1/2∥u−uh∥V. Absorb this fixed domain factor into C; it is independent of h. This proves the asserted full H1 velocity estimate without asserting additional regularity of the Stokes solution.

Depends on

Used by

Dependency tree · two levels

45 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