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.

Weak Stokes solvability on bounded connected Lipschitz domains

Statement

Assume Countable Choice. Let $D \subset R^{d}$ be nonempty, bounded, connected and Lipschitz, $d = 2$ or $3$ , and let $ν > 0$ . For every bounded linear functional $F$ on $V = H_{0}^{1} (D; R^{d})$ equipped with $∥ v ∥_{V} = ∥ \nabla v ∥_{2}$ , there is a unique $(u, p) \in V \times Q$ , $Q = L_{0}^{2} (D)$ , satisfying $2 ν \int_{D} ε (u) : ε (v) - \int_{D} p div v = F (v), - \int_{D} q div u = 0$ for every $v \in V, q \in Q$ . The pressure is normalized to have mean zero. One stability bound is $∥ u ∥_{V} \leq ν^{- 1} ∥ F ∥_{V^{'}}$ and $∥ p ∥_{2} \leq 3 C_{d i v} (D) ∥ F ∥_{V^{'}}$ .

Facts & Assumptions

Given: Countable Choice; a bounded connected Lipschitz $D$ ; the real Sobolev spaces; $ν > 0$ and $F \in V^{'}$ .

[A1]

Countable Choice is assumed by the Hilbert-space completeness and Lax–Milgram branch used below; no full Axiom of Choice is used by the local Korn or Poincare arguments. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

$H^{1} (D)$ is Hilbert under Countable Choice, $H_{0}^{1} (D)$ is its closed subspace, and bounded-domain Poincare makes the gradient norm equivalent to the H1 norm. (The Sobolev space $H^{1}$ is a Hilbert space, Zero-boundary Sobolev space as a norm closure, A bounded-domain Poincare inequality for H1-zero fields, The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F2]

Real $L^{2} (D)$ is Hilbert under Countable Choice, and the integral functional is bounded by $∣ D ∣^{1 / 2} ∥ q ∥_{2}$ , so its zero-mean kernel $Q$ is closed and Hilbert. ( $L^{2}$ with the integral pairing is a Hilbert space, Holder's inequality for integrals, including the endpoint cases, The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F3]

$2 ∥ ε (v) ∥_{2}^{2} = ∥ \nabla v ∥_{2}^{2} + ∥ div v ∥_{2}^{2}$ for every zero-boundary field. (The homogeneous Dirichlet strain identity)

[F4]

The divergence form is bounded and has continuous inf-sup constant at least $C_{d i v} (D)^{- 1}$ . (Continuous Stokes divergence inf-sup on a Lipschitz domain)

[F5]

On real Hilbert spaces, bounded $a, b$ , coercivity on the constraint kernel and positive inf-sup imply unique mixed solvability with the stated norm bounds. (Babuska-Brezzi solvability by kernel coercivity and inf-sup)

[F6]

Every zero-boundary velocity has zero-mean divergence. (Zero mean of the divergence of a zero-boundary field)

[F7]

The L2 Cauchy--Schwarz inequality gives $\int ∣ f g ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ . (Cauchy-Schwarz inequality for $L^{2}$ )

Proof

1.1A1F1F2

By [F1], $V$ is complete in the H1 norm. If $(v_{n})$ is Cauchy in $∥ \nabla \cdot ∥_{2}$ , [F1] and Poincare make it Cauchy in H1; its H1 limit is in the closed subspace $H_{0}^{1}$ and its gradients converge. Thus $V$ is Hilbert in the gradient norm. By [F2], $Q$ is Hilbert.

2.1F3F7step 1.1

Cauchy–Schwarz and $∣ ε (v) ∣ \leq ∣ \nabla v ∣_{F}$ give $∣ a_{ν} (u, v) ∣ \leq 2 ν ∥ u ∥_{V} ∥ v ∥_{V}$ . By [F3], $a_{ν} (v, v) = 2 ν ∥ ε (v) ∥_{2}^{2} \geq ν ∥ v ∥_{V}^{2}$ on all of $V$ , hence on $\ker B$ ; take $M_{a} = 2 ν$ and $α = ν$ .

3.1A1F4F5step 1.1step 2.1

The form $b$ has $M_{b} \leq \sqrt{d}$ and inf-sup $β \geq C_{d i v} (D)^{- 1}$ by [F4]. Apply [F5] with $G = 0$ . It yields a unique velocity and a unique mean-zero pressure satisfying the two displayed equations. The bound on velocity is $∥ u ∥_{V} \leq α^{- 1} ∥ F ∥ = ν^{- 1} ∥ F ∥$ .

4.1A1F4F5F6step 3.1∎

By [F6], $div u \in Q$ . The constraint equation tested with $q = div u$ therefore gives $∥ div u ∥_{2}^{2} = 0$ , so the weak constraint is exact incompressibility. Also [F5] gives $∥ p ∥_{2} \leq β^{- 1} (∥ F ∥ + M_{a} ∥ u ∥_{V})$ . Use $β^{- 1} \leq C_{d i v} (D)$ , $M_{a} = 2 ν$ and the velocity estimate of step 3.1 to obtain $∥ p ∥_{2} \leq 3 C_{d i v} (D) ∥ F ∥$ . Mean-zero gauge is part of $Q$ , so the pressure is unique in that normalization.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 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

Jean-Luc Guermond, MATH 661 Fall 2025, Chapters 49–54 (complete course notes) (standard reference, not scraped)
Daniele Boffi, Franco Brezzi, Michel Fortin, Mixed Finite Element Methods and Applications (complete textbook) (standard reference, not scraped)