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.

Sobolev traces and Gauss–Green formula on physical simplices

Statement

Assume Countable Choice. Let $d \geq 2$ , let ${\hat{S}}_{d}$ be the reference simplex, and let $F_{K} (\hat{x}) = b + B \hat{x}$ map $\overline{{\hat{S}}_{d}}$ affinely onto a nondegenerate closed simplex $K$ , with $\det B > 0$ . Sobolev spaces on $K$ mean spaces on its open interior. For every scalar $u \in W^{1, 2} (K)$ and vector field $G \in W^{1, 2} (K; R^{d})$ , each physical facet has bounded $L^{2}$ traces $γ_{F} u$ and $γ_{F} G$ , obtained by affine transfer from the reference trace maps. These traces are independent of the chosen orientation-preserving reference map, and they satisfy $\int_{K} u div G + \nabla u \cdot G d x = \sum_{F \subset \partial K} \int_{F} (γ_{F} u) (γ_{F} G) \cdot n_{K, F} d S,$ where $n_{K, F}$ is the outward unit normal.

Facts & Assumptions

Given: Countable Choice, the reference simplex, an orientation-preserving affine map onto a nondegenerate simplex, $u \in W^{1, 2} (K)$ , and $G \in W^{1, 2} (K; R^{d})$ .

[F1]

Matching affine simplicial meshes and shape regularity: every physical cell is the image of the reference simplex by an affine bijection; its vertex order is chosen so the map has positive determinant.

[F2]

Affine pullback of weak derivatives and Sobolev seminorms: affine pullbacks of $W^{1, 2}$ functions lie in $W^{1, 2}$ and satisfy $\nabla_{\hat{x}} (v \circ F) = B^{T} (\nabla_{x} v) \circ F$ .

[F3]

Sobolev face traces and Gauss–Green on a reference simplex: scalar and componentwise vector traces from $W^{1, 2} ({\hat{S}}_{d})$ to $L^{2} (\hat{F})$ exist on every reference facet and obey the reference Gauss–Green identity.

[F4]

Gauss–Green formula on an affine simplex: the oriented face area element transforms as $n_{K, F} d S = \det (B) B^{- T} {\hat{n}}_{\hat{F}} d \hat{S}$ .

[F5]

Smooth functions are dense in finite-order Sobolev spaces on a reference simplex: restrictions of smooth functions on a neighborhood of the closed reference simplex are dense in $W^{1, 2} ({\hat{S}}_{d})$ .

[F6]

A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: under the affine map, volume integrals transform with the constant Jacobian $\det (B) > 0$ .

[F7]

Holder's inequality for integrals, including the endpoint cases: products of two $L^{2}$ functions on a measure space are integrable and their integrals satisfy the $L^{2}$ Cauchy–Schwarz bound.

[F8]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): Countable Choice is the declared hypothesis of the affine pullback, density, change-of-variables, and reference trace suppliers [F2]–[F3], [F5]–[F6].

Proof

1.1F1F2F3F4F5F8given

Put $\hat{u} = u \circ F_{K}$ and $\hat{G} = \det (B) B^{- 1} (G \circ F_{K})$ . By [F2], both belong to $W^{1, 2} ({\hat{S}}_{d})$ . Define the physical traces by $γ_{F} u (F_{K} (\hat{x})) = γ_{\hat{F}} \hat{u} (\hat{x})$ and $γ_{F} G (F_{K} (\hat{x})) = (\det B)^{- 1} B γ_{\hat{F}} \hat{G} (\hat{x})$ . The reference traces in [F3] are in $L^{2} (\hat{F})$ ; the constant affine surface Jacobian $\det (B) ∣ B^{- T} {\hat{n}}_{\hat{F}} ∣ > 0$ from [F4] and the fixed matrix factor show these definitions give bounded $L^{2} (F)$ traces. For a fixed map, [F5] supplies smooth approximants to $\hat{u}$ and each component of $G \circ F_{K}$ ; the reverse estimate in [F2] maps them to smooth approximants on $K$ . Thus smooth functions on $K$ are dense in $W^{1, 2} (K)$ , and any two bounded affine-transfer trace maps agree on this dense smooth class, so they agree on all of $W^{1, 2} (K)$ .

2.1F2F3F4F6F7F8step 1.1algebra∎

Applying the componentwise weak chain rule [F2] and the identity $\sum_{j} B_{ℓ j} (B^{- 1})_{j i} = δ_{ℓ i}$ gives ${div}_{\hat{x}} \hat{G} = \det (B) ({div}_{x} G) \circ F_{K}$ . Also $\nabla_{\hat{x}} \hat{u} \cdot \hat{G} = ((B^{T} \nabla_{x} u) \circ F_{K}) \cdot (\det (B) B^{- 1} (G \circ F_{K})) = \det (B) (\nabla_{x} u \cdot G) \circ F_{K}$ . The volume products are integrable by [F7], so [F6] applied to their positive and negative parts identifies the reference volume integral in [F3] with the physical volume integral in the claim. The reference boundary products are integrable by [F3] and [F7]. By the trace definition in step 1.1, $γ_{\hat{F}} \hat{G} = \det (B) B^{- 1} (γ_{F} G) \circ F_{K}$ ; hence its normal pairing is $\det (B) (γ_{F} G) \cdot B^{- T} {\hat{n}}_{\hat{F}} d \hat{S} = (γ_{F} G) \cdot n_{K, F} d S$ by [F4], while the scalar trace is the pullback of $γ_{F} u$ . Applying [F3] and summing over the finitely many facets proves the identity.

Depends on

Used by

Dependency tree · two levels

39 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 VIII, Chapter 38: Discontinuous Galerkin (standard reference, not scraped)
Douglas N. Arnold, Franco Brezzi, Bernardo Cockburn, and L. Donatella Marini, Unified Analysis of Discontinuous Galerkin Methods for Elliptic Problems, SIAM Journal on Numerical Analysis 39(5) (2002) (standard reference, not scraped)