LemmaStatement: AI-adaptedProof: 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.

A topology-free bounded lifting of every ultraweak Poisson load

Statement

Assume Countable Choice and the real spaces and signs of Ultraweak Poisson DPG spaces and plan-consistent bilinear form. For every bounded connected Lipschitz polyhedron $Ω \subset R^{d}$ , $d \in {2, 3}$ , and every finite conforming shape-regular simplicial mesh, give $U$ the squared product norm from its two $L^{2}$ factors and two global trace lift-infimum norms, and give $V$ its full broken graph norm. Define $B : U \to V^{'}$ by $(B x) (y) = b (x, y)$ . There is a bounded linear map $R : V^{'} \to U$ such that $B R = I_{V^{'}}$ and $∥ R ∥ \leq C_{*}$ . Choose any $C_{P} > 0$ with $∥ w ∥_{2} \leq C_{P} ∥ \nabla w ∥_{2}$ for $w \in H_{0}^{1} (Ω)$ , put $a = (C_{P}^{2} + 2)^{1 / 2}$ , and set $C_{*}^{2} = (1 + a)^{2} + (1 + C_{P} a)^{2} + (1 + C_{P}^{2}) a^{2} + (\sqrt{2} + a)^{2} + 1.$ The constant is independent of the mesh. No simple-connectivity or connected-boundary hypothesis is imposed.

Facts & Assumptions

Given: Countable Choice, the stated domain and mesh, the real ultraweak spaces and bilinear form, a Poincaré constant $C_{P}$ , and an arbitrary $F \in V^{'}$ .

[A1]

Countable Choice is the stated axiom for the real Hilbert, Riesz, trace and Lax–Milgram interfaces. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

The formulation fixes the real product spaces, the global trace ranges with lift-infimum norms, and all five signs in $b$ . (Ultraweak Poisson DPG spaces and plan-consistent bilinear form, Ultraweak Poisson skeleton spaces are Hilbert trace quotients)

[F2]

The finite broken products of $H (div)$ and $H^{1}$ are real Hilbert spaces, and $H_{0}^{1} (Ω)$ is a real Hilbert space with its restricted $H^{1}$ inner product. (H(div) is Hilbert and H0(div) is closed, The Sobolev space $H^{1}$ is a Hilbert space)

[F3]

On a real Hilbert space, Riesz represents every bounded linear functional by a unique vector and preserves its norm. (Riesz representation for Hilbert spaces)

[F4]

A bounded coercive real bilinear form on a real Hilbert space has a unique solution for every bounded linear right-hand side under Countable Choice. (The Lax--Milgram theorem)

[F5]

For bounded open $Ω$ , homogeneous Dirichlet Poincaré gives $∥ w ∥_{2} \leq C_{P} ∥ \nabla w ∥_{2}$ on $H_{0}^{1} (Ω)$ ; a coordinate-slab width supplies such a constant. (A bounded-domain Poincare inequality for H1-zero fields)

[F6]

The weak normal trace of a global $H (div)$ field is defined by the cell Green functional, and an $L^{2}$ vector with $L^{2}$ distributional divergence belongs to $H (div)$ . (Weak normal trace by Green duality, The real H(div) space)

[F7]

The DPG form is bounded on the full trial and broken-test spaces by $∣ b (x, y) ∣ \leq 5 ∥ x ∥_{U} ∥ y ∥_{V}$ , so $B x = b (x, \cdot)$ is a well-defined bounded element of $V^{'}$ for every $x \in U$ . (The ultraweak Poisson DPG bilinear form is bounded)

Proof

1.1A1F2F3F7givenalgebra

By [F7], $B : U \to V^{'}$ given by $(B x) (y) = b (x, y)$ is well defined and bounded. By [F2] and [F3], there is a unique $(ρ, z) \in V$ such that $F (τ, v) = (ρ, τ) + ({div}_{h} ρ, {div}_{h} τ) + (z, v) + (\nabla_{h} z, \nabla_{h} v) .$ Set $g = ρ$ , $r = {div}_{h} ρ$ , $f = z$ , and $s = \nabla_{h} z$ , viewed as global $L^{2}$ classes by the finite mesh partition. If $D = ∥ F ∥_{V^{'}}$ , then $∥ g ∥_{2}^{2} + ∥ r ∥_{2}^{2} + ∥ f ∥_{2}^{2} + ∥ s ∥_{2}^{2} = D^{2}$ .

2.1A1F2F4F5step 1.1algebra

On $H_{0}^{1} (Ω)$ use the form $a (w, ϕ) = (\nabla w, \nabla ϕ)$ . It is bounded in the $H^{1}$ norm, and [F5] gives $a (w, w) \geq (1 + C_{P}^{2})^{- 1} ∥ w ∥_{H^{1}}^{2}$ . The functional $ϕ \mapsto (f, ϕ) + (g + s, \nabla ϕ)$ is bounded, since its absolute value is at most $(C_{P} ∥ f ∥_{2} + ∥ g ∥_{2} + ∥ s ∥_{2}) ∥ \nabla ϕ ∥_{2}$ . Thus [F4] gives a unique $w \in H_{0}^{1} (Ω)$ satisfying $(\nabla w, \nabla ϕ) = (f, ϕ) + (g + s, \nabla ϕ) (ϕ \in H_{0}^{1} (Ω)) .$ Testing with $w$ and using Cauchy–Schwarz yields $∥ \nabla w ∥_{2} \leq C_{P} ∥ f ∥_{2} + ∥ g ∥_{2} + ∥ s ∥_{2} \leq a D$ , including the case $\nabla w = 0$ ; hence $∥ w ∥_{2} \leq C_{P} a D$ .

3.1F1F6step 1.1step 2.1constructalgebra

Set $σ = g - \nabla w$ , $u = w - r$ , and $q = g + s - \nabla w$ . For every $ϕ \in C_{c}^{\infty} (Ω)$ , step 2.1 gives $(q, \nabla ϕ) = - (f, ϕ)$ , so $div q = f$ distributionally and $q \in H (div; Ω)$ . Set $\hat{u} = Γ_{0} w$ and ${\hat{σ}}_{n} = Γ_{n} q$ , using the elementwise scalar and weak normal traces. Since $w \in H_{0}^{1} (Ω)$ and $q$ is one global $H (div)$ field, these traces lie in the exact global ranges of [F1], with homogeneous scalar boundary trace and conservative normal trace. Define $R F = (σ, u, \hat{u}, {\hat{σ}}_{n}) \in U$ .

4.1F1F6step 1.1step 3.1algebra

Cell Green identities give $⟨ \hat{u}, τ \cdot n ⟩ = (\nabla w, τ) + (w, {div}_{h} τ)$ and $⟨ {\hat{σ}}_{n}, v ⟩ = (q, \nabla_{h} v) + (f, v)$ . Substitution into the five signed terms of the form gives $b (R F, (τ, v)) = (g - \nabla w, τ) - (w - r, {div}_{h} τ) + (\nabla w, τ) + (w, {div}_{h} τ) - (g - \nabla w, \nabla_{h} v) + (q, \nabla_{h} v) + (f, v) = (g, τ) + (r, {div}_{h} τ) + (s, \nabla_{h} v) + (f, v) = F (τ, v) .$ Therefore $B R = I_{V^{'}}$ .

5.1F1F3F4step 1.1step 2.1step 3.1step 4.1algebra∎

From steps 1.1–3.1, $∥ σ ∥_{2} \leq (1 + a) D$ , $∥ u ∥_{2} \leq (1 + C_{P} a) D$ , $∥ \hat{u} ∥_{\hat{U}} \leq ∥ w ∥_{H^{1}} \leq \sqrt{1 + C_{P}^{2}} a D$ , and $∥ {\hat{σ}}_{n} ∥_{{\hat{Q}}_{n}} \leq ∥ q ∥_{H (div)} \leq \sqrt{(\sqrt{2} + a)^{2} + 1} D$ , since $∥ g + s ∥_{2} \leq \sqrt{2} D$ and $div q = f$ . Adding the four squared product components gives $∥ R F ∥_{U} \leq C_{*} D$ . Riesz and the unique weak solve depend linearly on $F$ (a linear combination solves the combined variational equation, and uniqueness identifies it), and the remaining field and trace maps are linear; hence $R$ is linear. Only $C_{P}$ enters the bound, so it is mesh-independent.

Depends on

Used by

Adjoint graph inf-sup for ultraweak Poisson on connected Lipschitz polyhedra Theorem

Dependency tree · two levels

55 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

Jay Gopalakrishnan and Weifeng Qiu, An analysis of the practical DPG method (standard reference, not scraped)
Leszek Demkowicz and Jay Gopalakrishnan, Analysis of the DPG method for the Poisson equation (standard reference, not scraped)