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

The isotropic contact elasticity form is well defined and bounded

Statement

In the setting of Small-strain elasticity with a frictionless contact gap, the form $a$ is well defined, symmetric, and satisfies $∣ a (u, v) ∣ \leq (2 μ + 2 λ) ∥ u ∥_{H^{1} (Ω)} ∥ v ∥_{H^{1} (Ω)} (u, v \in V) .$

Facts & Assumptions

Given: The bounded polygon $Ω$ , $u, v \in V \subset H^{1} (Ω; R^{2})$ , constants $μ > 0$ , $λ \geq 0$ , and the form in Small-strain elasticity with a frictionless contact gap.

[F1]

The strain and form are $ε (u) = (\nabla u + (\nabla u)^{T}) / 2$ and $a (u, v) = \int_{Ω} 2 μ ε (u) : ε (v) + λ div u div v d x$ . (Small-strain elasticity with a frictionless contact gap)

[F2]

For $L^{2}$ matrix or scalar fields, the integral pairing is bounded by the product of the $L^{2}$ norms. (Cauchy-Schwarz inequality for $L^{2}$ )

[F3]

The $H^{1}$ norm contains the $L^{2}$ norm of the full weak gradient, and the entries of that gradient are in $L^{2}$ . (Integer-order Sobolev spaces and their norms)

Proof

technique · direct

Given: The setting above and the real isotropic elasticity form $a$ .

1.1F1F3givenalgebra

The symmetric-part map is an orthogonal projection in the Frobenius inner product, so $∣ ε (w) ∣_{F} \leq ∣ \nabla w ∣_{F}$ . Also $∣ div w ∣ = ∣ tr \nabla w ∣ \leq \sqrt{2} ∣ \nabla w ∣_{F}$ by Cauchy–Schwarz on the two diagonal entries. Thus both $ε (w)$ and $div w$ are in $L^{2}$ by [F3], so each integral defining $a (u, v)$ is finite.

2.1F1F2F3step 1.1algebra∎

Applying [F2] to the two terms of [F1] and then the bounds of step 1.1 gives $∣ a (u, v) ∣ \leq 2 μ ∥ \nabla u ∥_{2} ∥ \nabla v ∥_{2} + 2 λ ∥ \nabla u ∥_{2} ∥ \nabla v ∥_{2} \leq (2 μ + 2 λ) ∥ u ∥_{H^{1}} ∥ v ∥_{H^{1}}$ . The integrand is symmetric in $u, v$ , so $a (u, v) = a (v, u)$ .

Depends on

Used by

Cited to discharge well-definedness by Small-strain elasticity with a frictionless contact gap.

Dependency tree · two levels

15 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 53: Stokes equations: Basic ideas (standard reference, not scraped)
Walter Zulehner, Numerical Methods for Continuum Mechanics 1, complete 80-page lecture notes (standard reference, not scraped)