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.

Continuous mixed Darcy well-posedness with pressure gauge

Statement

Assume Countable Choice and the hypotheses in No-flow mixed Darcy problem and coefficient norms on a bounded connected Lipschitz domain in dimension two or three. For every $F \in V^{'}$ and $f \in Q$ , there is a unique $(u, p) \in V \times Q$ solving $a (u, v) + b (v, p) = F (v), b (u, q) = - \int_{D} f q$ for all $v \in V, q \in Q$ . The graph norm on the flux and zero-mean pressure norm make these equations well-posed; the mean-zero pressure convention fixes the Neumann gauge.

Facts & Assumptions

Given: Countable Choice, $D, K, V, Q, a, b, F, f$ as in the no-flow Darcy definition.

[A1]

Countable Choice is inherited from the right-inverse and Babuška–Brezzi suppliers. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

$V = H_{0} (div; D)$ and $Q = L_{0}^{2} (D)$ are real Hilbert spaces in their graph and integral norms. (H(div) is Hilbert and H0(div) is closed, The real zero-mean $L^{2}$ space is Hilbert)

[F2]

Every $v \in V$ has $\int_{D} div v = 0$ , hence $div v \in Q$ . (Zero mean of the divergence under zero normal trace)

[F3]

The divergence has a bounded right inverse $B_{D} : Q \to H_{0}^{1} (D; R^{d})$ with $div B_{D} q = q$ and $∥ \nabla B_{D} q ∥_{2} \leq C_{d i v} ∥ q ∥_{2}$ . (Divergence right inverse on bounded connected Lipschitz domains)

[F4]

For a bounded domain in a coordinate slab of width $L$ , $∥ w ∥_{2} \leq L ∥ \nabla w ∥_{2}$ for $w \in H_{0}^{1} (D)$ . (A bounded-domain Poincare inequality for H1-zero fields)

[F5]

Bounded forms with positive inf-sup and coercivity on the closed constraint kernel give a unique mixed solution under Countable Choice. (Babuska-Brezzi solvability by kernel coercivity and inf-sup)

[F6]

The real $L^{2}$ Cauchy–Schwarz inequality bounds the data functional and the bilinear form pairings. (Cauchy-Schwarz inequality for $L^{2}$ )

[F7]

Every H1-zero vector field belongs to the zero-normal H(div) space. (H1-zero fields have zero weak H(div) normal trace)

Proof

1.1givenF1algebra

The form bounds follow from the permeability eigenvalue bounds: $∣ a (u, v) ∣ \leq κ_{\min}^{} ∥ u ∥_{L^{2}} ∥ v ∥_{L^{2}} \leq κ_{\min}^{} ∥ u ∥_{V} ∥ v ∥_{V}$ , and $∣ b (v, q) ∣ \leq ∥ div v ∥_{2} ∥ q ∥_{2} \leq ∥ v ∥_{V} ∥ q ∥_{Q}$ . Thus $M_{a} \leq κ_{\min}^{}$ and $M_{b} \leq 1$ .

1.2A1F3F7construct

For $q \in Q$ , the right inverse [F3] gives $B_{D} q \in H_{0}^{1} (D; R^{d})$ , so [F7] places $B_{D} q$ in $V$ . Its graph norm is finite.

1.3F1F2givenalgebra

Define $B : V \to Q$ by $(B v, q)_{Q} = b (v, q)$ . Since $b (v, q) = - \int_{D} q div v$ and [F2] places the divergence in $Q$ , $B v = - div v$ . Hence $Z = \ker B = {v \in V : div v = 0}$ ; it is closed because divergence is continuous in the graph norm. For $v \in Z$ , the graph norm equals $∥ v ∥_{2}$ , and $a (v, v) \geq κ_{\max}^{} ∥ v ∥_{2}^{2} = κ_{\max}^{} ∥ v ∥_{V}^{2}$ .

2.1F3F4step 1.2algebra

For nonzero $q \in Q$ , choose $v = - B_{D} q$ . Then $b (v, q) = ∥ q ∥_{2}^{2}$ by [F3]. The Poincare bound [F4] gives $∥ B_{D} q ∥_{V}^{2} = ∥ B_{D} q ∥_{2}^{2} + ∥ q ∥_{2}^{2} \leq (1 + L^{2} C_{d i v}^{2}) ∥ q ∥_{2}^{2}$ . Therefore the inf-sup constant for $b$ on $V \times Q$ is at least $(1 + L^{2} C_{d i v}^{2})^{- 1 / 2} > 0$ .

3.1A1F1F2F3F5F6step 1.1step 1.2step 1.3step 2.1algebracases∎

If $Q = {0}$ , [F2] makes $Z = V$ , so the Countable Choice Lax–Milgram branch of [F5] applies using coercivity from step 1.3. If $Q \neq {0}$ , [F3] supplies a nonzero $q$ ; then $B_{D} q \in V$ by step 1.2 and is nonzero since its divergence is $q$ . The positive inf-sup from step 2.1 and the nonzero Hilbert spaces [F1] allow the mixed branch of [F5]. In both cases boundedness from step 1.1, closedness and coercivity from step 1.3, and data functionals $F$ and $G (q) = - \int_{D} f q$ satisfy [F5]; [F6] makes $G$ bounded. The theorem gives the asserted unique pair, and the pressure mean-zero condition removes the additive constant.

Depends on

Used by

RT0/P0 Darcy stability and flux/pressure error bound Theorem

Dependency tree · two levels

33 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, Part XI Chapter 49: Well-posedness for PDEs in mixed form (standard reference, not scraped)
Daniele Boffi, Franco Brezzi and Michel Fortin, Mixed Finite Element Methods and Applications (standard reference, not scraped)