LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Korn coercivity with a partial Dirichlet segment

Statement

Assume the geometry of Partial-trace displacement space on a polygon and let $V = {v \in H^{1} (Ω; R^{2}) : T_{D} v = 0}$ . Then there is $c_{K} > 0$ , depending on $Ω$ and $Γ_{D}$ , such that $∥ v ∥_{H^{1} (Ω)} \leq c_{K} ∥ ε (v) ∥_{L^{2} (Ω)} (v \in V) .$

Facts & Assumptions

Given: A nonempty bounded connected Lipschitz extension polygon $Ω \subset R^{2}$ , a straight Dirichlet segment $Γ_{D}$ of length $L > 0$ , and $V$ as above.

[A1]

Countable Choice is used by the bounded-Lipschitz divergence right inverse and the closure-defined $H_{0}^{1}$ approximation. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[A2]

The Axiom of Choice is used through the bounded C1 trace theorem and Poincare-Wirtinger on the bounded connected extension domain. (The Axiom of Choice, The $L^{p}$ trace operator on a bounded $C^{1}$ domain, Poincare-Wirtinger on bounded connected extension domains by Rellich compactness)

[F0]

A nonempty open bounded set has finite positive Lebesgue measure: it contains a ball and is contained in a ball. (Euclidean balls have positive finite Lebesgue measure)

[F1]

There is a bounded linear $B_{Ω} : L_{0}^{2} (Ω) \to H_{0}^{1} (Ω; R^{2})$ with $div B_{Ω} q = q$ and $∥ \nabla B_{Ω} q ∥_{2} \leq C_{d i v} (Ω) ∥ q ∥_{2}$ . (Divergence right inverse on bounded connected Lipschitz domains)

[F2]

For $z \in H^{1} (Ω)$ of zero mean, $∥ z ∥_{2} \leq C_{P} ∥ \nabla z ∥_{2}$ ; apply this componentwise. (Poincare-Wirtinger on bounded connected extension domains by Rellich compactness)

[F3]

$T_{D}$ is bounded and $V = \ker T_{D}$ ; in particular $T_{D} v = 0$ for $v \in V$ . (Partial-trace displacement space on a polygon, The partial-trace displacement space is a Hilbert space)

[F4]

Every planar rigid motion $r (x) = a + ω J x$ satisfies $∥ r ∥_{H^{1} (Ω)} \leq C_{D} ∥ T_{D} r ∥_{L^{2} (Γ_{D})}$ . (A planar rigid motion is controlled by its trace on a segment)

[F5]

$H_{0}^{1} (Ω)$ is the $H^{1}$ closure of $C_{c}^{\infty} (Ω)$ . (Zero-boundary Sobolev space as a norm closure)

[F6]

$ε (v) = (\nabla v + (\nabla v)^{T}) / 2$ , and $J = (\begin{array}{cc} 0 & - 1 \\ 1 & 0 \end{array})$ ; adding a rigid motion $a + ω J x$ does not change $ε (v)$ . (Small-strain elasticity with a frictionless contact gap, A planar rigid motion is controlled by its trace on a segment)

[F7]

For finite-measure $Ω$ , every $L^{2} (Ω)$ function is integrable and $∥ g ∥_{L^{1}} \leq ∣ Ω ∣^{1 / 2} ∥ g ∥_{L^{2}}$ . (Cauchy-Schwarz inequality for $L^{2}$ )

Proof

technique · direct

Given: The polygon, trace segment and space $V$ of the statement, with the Axiom of Choice and Countable Choice available through [A1]–[A2].

1.1A1givenF0F6F7constructalgebra

Since $Ω$ is nonempty, open and bounded, [F0] gives $0 < ∣ Ω ∣ < \infty$ . Hence $1 \in L^{2} (Ω)$ , and [F7] with the Cauchy–Schwarz inequality makes every $L^{2}$ component of $v$ and its weak gradient integrable; boundedness of $Ω$ also makes $x$ and $J x$ integrable. Thus the means in $ω = (2 ∣ Ω ∣)^{- 1} \int_{Ω} curl v$ and $a = ∣ Ω ∣^{- 1} \int_{Ω} (v - ω J x)$ exist. Put $r (x) = a + ω J x$ and $z = v - r$ . Then $\int_{Ω} z = 0$ , $\int_{Ω} curl z = 0$ , and $ε (z) = ε (v)$ by [F6].

2.1A1F1F5step 1.1

Let $q = curl z \in L_{0}^{2} (Ω)$ and choose $w = B_{Ω} q$ by [F1]. Define the matrix $R (w)$ rowwise by $R (w)_{i 1} = \partial_{2} w_{i}$ and $R (w)_{i 2} = - \partial_{1} w_{i}$ . For $w \in C_{c}^{\infty} (Ω; R^{2})$ each row of $R (w)$ has zero divergence, so distributional integration by parts gives $(\nabla z, R (w))_{L^{2}} = 0$ . Approximate the actual $w \in H_{0}^{1}$ by compactly supported smooth fields using [F5]; since $R (w_{m}) \to R (w)$ in $L^{2}$ , the same identity holds for $w$ .

3.1A1A2F1F2F6step 1.1step 2.1algebra

Set $G = \nabla z - R (w)$ . In two dimensions $J : G = G_{21} - G_{12} = curl z - div w = q - q = 0$ , so the off-diagonal entries of $G$ agree and $G$ is symmetric. Write $S = (\nabla z - (\nabla z)^{T}) / 2$ , which is skew-symmetric. Symmetric and skew-symmetric matrices are orthogonal in the Frobenius inner product, so $(S, G)_{L^{2}} = 0$ and $(\nabla z, G) = (ε (z), G)$ . By step 2.1, $(\nabla z, G) = ∥ \nabla z ∥_{2}^{2} - (\nabla z, R (w)) = ∥ \nabla z ∥_{2}^{2}$ . The entries of $R (w)$ are the entries of $\nabla w$ permuted and sign-changed, so $∥ R (w) ∥_{2} = ∥ \nabla w ∥_{2}$ . Also $∣ q ∣^{2} = ∣ \partial_{1} z_{2} - \partial_{2} z_{1} ∣^{2} \leq 2 (∣ \partial_{1} z_{2} ∣^{2} + ∣ \partial_{2} z_{1} ∣^{2}) \leq 2 ∣ \nabla z ∣_{F}^{2}$ almost everywhere; integration gives $∥ q ∥_{2} \leq \sqrt{2} ∥ \nabla z ∥_{2}$ . Thus [F1] and the triangle inequality imply $∥ G ∥_{2} \leq ∥ \nabla z ∥_{2} + ∥ \nabla w ∥_{2} \leq (1 + \sqrt{2} C_{d i v}) ∥ \nabla z ∥_{2}$ . Therefore $∥ \nabla z ∥_{2}^{2} \leq ∥ ε (z) ∥_{2} ∥ G ∥_{2} \leq (1 + \sqrt{2} C_{d i v}) ∥ ε (z) ∥_{2} ∥ \nabla z ∥_{2}$ . If $\nabla z = 0$ the gradient estimate is immediate; otherwise divide by $∥ \nabla z ∥_{2}$ . Then [F2] and $\int_{Ω} z = 0$ give $∥ z ∥_{2} \leq C_{P} ∥ \nabla z ∥_{2}$ , hence $∥ z ∥_{H^{1}} \leq \sqrt{1 + C_{P}^{2}} ∥ \nabla z ∥_{2} \leq C_{0} ∥ ε (v) ∥_{2}$ .

4.1A2F3F4step 3.1givenalgebra∎

For $v \in V$ , [F3] gives $T_{D} r = - T_{D} z$ . Apply [F4] and the trace bound [F3] to obtain $∥ r ∥_{H^{1}} \leq C_{D} ∥ T_{D} z ∥_{L^{2} (Γ_{D})} \leq C_{D} C_{T} ∥ z ∥_{H^{1}}$ . Since $v = z + r$ , step 3.1 yields $∥ v ∥_{H^{1}} \leq ∥ z ∥_{H^{1}} + ∥ r ∥_{H^{1}} \leq (1 + C_{D} C_{T}) C_{0} ∥ ε (v) ∥_{2}$ , proving the assertion.

Depends on

Used by

Dependency tree · two levels

51 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

Walter Zulehner, Numerical Methods for Continuum Mechanics 1, complete 80-page lecture notes (standard reference, not scraped)
Jean-Luc Guermond, MATH 661 Fall 2025, Part XI Chapter 53: Stokes equations: Basic ideas (standard reference, not scraped)