Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck 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.

P1 PSPG Stokes form is coercive in its stabilization norm

Statement

Let d≥2, let Ω⊂Rd be a bounded connected polyhedral open set, and let a finite conforming nondegenerate simplicial mesh have connected cell adjacency. Let Vh be continuous vector-valued P1 functions vanishing on the boundary, and let Qh be continuous scalar P1 functions with zero mean. Let f∈L2(Ω;Rd), ν>0, τK>0, and γ≥0. For the stationary Stokes specialization of Residual PSPG and grad-div terms for equal-order flow spaces, define Bh((uh,ph),(vh,qh)):=ν(∇uh,∇vh)Ω−(ph,∇⋅vh)Ω+(qh,∇⋅uh)Ω+γ(∇⋅uh,∇⋅vh)Ω+∑KτK(∇qh,−νΔKuh+∇ph)K. For the residual load, set Fh(vh,qh):=(f,vh)Ω+∑KτK(∇qh,f)K. Define ∥(vh,qh)∥h2:=ν∥∇vh∥22+γ∥∇⋅vh∥22+∑KτK∥∇qh∥0,K2. Then this is a norm, Bh(zh,zh)=∥zh∥h2, and the discrete problem Bh(zh,⋅)=Fh(⋅) has a unique solution satisfying ∥zh∥h≤∥Fh∥h,∗, where ∥Fh∥h,∗:=sup⁡yh≠0∣Fh(yh)∣/∥yh∥h. The estimate controls pressure in the mesh-dependent gradient stabilization norm; it does not assert a mesh-uniform L2 pressure bound or convergence.

Facts & Assumptions

Given: A connected domain and connected conforming cell adjacency, continuous equal-order P1 velocity and pressure spaces, zero velocity boundary values, mean-zero pressure, ν>0, τK>0, γ≥0, and the Stokes residual form.

[F1]

Residual PSPG and grad-div terms for equal-order flow spaces: PSPG adds the element momentum residual tested against ∇qh, while grad-div adds γ(∇⋅uh,∇⋅vh); both are definitions and supply no stability claim by themselves.

[A1]

On each cell, uh is affine, so ΔKuh=0. The cell mesh is connected, the pressure is continuous, and its mean is zero.

Proof

1.1F1A1givenalgebra

Setting (vh,qh)=(uh,ph) in the displayed form cancels the mixed terms −(ph,∇⋅uh)+(ph,∇⋅uh). By [A1], the PSPG residual term becomes ∑KτK∥∇ph∥0,K2. The remaining terms are exactly ν∥∇uh∥22+γ∥∇⋅uh∥22, so Bh((uh,ph),(uh,ph))=∥(uh,ph)∥h2.

2.1A1step 1.1algebra

If this norm is zero, ∇uh=0 on each cell; continuity and zero boundary values force uh=0. Also ∇ph=0 on each cell, so ph is constant on each cell. Continuity across shared facets and connected cell adjacency force one global constant; its zero mean forces ph=0. Thus the norm vanishes only at zero.

3.1step 1.1step 2.1givenalgebra∎

If zh is in the kernel of the bilinear map, then step 1.1 gives ∥zh∥h2=Bh(zh,zh)=0, and step 2.1 forces zh=0. Thus the linear map from Vh×Qh to its dual is injective and, by equal finite dimensions, bijective; the discrete problem has a unique solution. Testing that solution equation with itself gives ∥zh∥h2=Fh(zh)≤∥Fh∥h,∗∥zh∥h. If zh=0 the estimate is immediate; otherwise division proves ∥zh∥h≤∥Fh∥h,∗.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · one level

1 result within one dependency step 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