TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 weak Euler-Lagrange equation for integral functionals with fixed trace

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $Ω \subseteq R^{n}$ , $n \geq 2$ , be a bounded $C^{1}$ domain, $1 < p < \infty$ , let $f$ and $I$ satisfy the hypotheses of Differentiation of an integral functional under growth domination, and let $g \in W^{1 - 1 / p, p} (\partial Ω)$ lie in the trace range of $T : W^{1, p} (Ω) \to W^{1 - 1 / p, p} (\partial Ω)$ (The sharp trace theorem: boundedness and range in the fractional space, The fractional Sobolev space on a compact $C^{1}$ boundary, The $L^{p}$ trace operator on a bounded $C^{1}$ domain). Let $u \in W^{1, p} (Ω)$ with $T u = g$ be a local minimiser of $I$ among the functions with trace $g$ : $I (u) \leq I (w)$ for all $w \in W^{1, p} (Ω)$ with $T w = g$ and $∥ w - u ∥_{W^{1, p}}$ small. Then $\int_{Ω} (f_{ξ} (x, u, D u) \cdot D φ + f_{s} (x, u, D u) φ) d x = 0$ for every $φ \in W_{0}^{1, p} (Ω)$ (Zero-boundary Sobolev space as a norm closure); equivalently, for every $φ \in C_{c}^{\infty} (Ω)$ (Test function space d of an open set).

Facts & Assumptions

Given: The Axiom of Choice; a bounded $C^{1}$ domain $Ω \subseteq R^{n}$ , $1 < p < \infty$ , an integrand $f$ and functional $I (u) = \int_{Ω} f (x, u, D u) d x$ satisfying the hypotheses of Differentiation of an integral functional under growth domination, and $g \in W^{1 - 1 / p, p} (\partial Ω)$ in the trace range of $T$ ; a local minimiser $u \in W^{1, p} (Ω)$ of $I$ among the functions of trace $g$ . The Sobolev and trace framework is set up under the Axiom of Choice, used through Countable Choice (The Axiom of Choice), and $W^{1, p} (Ω)$ is a Banach space (Integer-order Sobolev spaces are Banach).

[F1]

$T : W^{1, p} (Ω) \to W^{1 - 1 / p, p} (\partial Ω)$ is linear and $\ker T = W_{0}^{1, p} (Ω)$ , the $W^{1, p}$ -closure of $C_{c}^{\infty} (Ω)$ (The kernel of the trace is the closure of the test functions, Zero-boundary Sobolev space as a norm closure, The $L^{p}$ trace operator on a bounded $C^{1}$ domain).

[F2]

Affine form of the first-variation theorem: if $F : U \to R$ on the open $U \subseteq X$ is Gateaux differentiable at $u$ and $F (u) \leq F (w)$ for all $w \in (u + V) \cap U$ with $∥ w - u ∥$ small, $V \subseteq X$ a linear subspace of the Banach space $X$ , then $δ F (u; v) = 0$ for every $v \in V$ (The first variation vanishes at an interior minimiser, Integer-order Sobolev spaces are Banach).

[F3]

The differentiation lemma: $I$ is Gateaux differentiable at $u$ with $δ I (u; v) = \int_{Ω} (f_{s} (x, u, D u) v + f_{ξ} (x, u, D u) \cdot D v) d x$ for every $v \in W^{1, p} (Ω)$ (Differentiation of an integral functional under growth domination).

[F4]

$C_{c}^{\infty} (Ω) \subseteq W_{0}^{1, p} (Ω)$ because $W_{0}^{1, p} (Ω)$ is defined as the closure of $C_{c}^{\infty} (Ω)$ in $W^{1, p} (Ω)$ (Zero-boundary Sobolev space as a norm closure, Test function space d of an open set).

Proof

technique · direct, by testing the affine first-variation theorem against the kernel of the trace

1.1F1given

Variations preserving the trace. Fix $φ \in W_{0}^{1, p} (Ω)$ . Then $T φ = 0$ by [F1], and linearity of $T$ gives $T (u + ε φ) = T u + ε T φ = g$ for every $ε \in R$ ; thus every point of the affine line $u + R φ$ has trace $g$ .

2.1givenstep 1.1

Local minimality along the line. For $ε$ with $∣ ε ∣$ small, the point $u + ε φ$ lies in the local admissible neighbourhood of $u$ among the functions of trace $g$ and has norm distance $∣ ε ∣ ∥ φ ∥_{W^{1, p}}$ from $u$ ; hence $I (u) \leq I (u + ε φ)$ . Therefore $u$ is a local minimiser of $I$ on the affine set $(u + W_{0}^{1, p} (Ω)) \cap W^{1, p} (Ω)$ .

3.1F2step 2.1

The first variation vanishes. By [F2] applied with $X = W^{1, p} (Ω)$ , $V = W_{0}^{1, p} (Ω)$ and the local minimality of step 2.1, $δ I (u; φ) = 0$ .

4.1F1F3F4step 3.1∎

Computing the derivative. By [F3] the Gateaux derivative is $δ I (u; φ) = \int_{Ω} (f_{s} (x, u, D u) φ + f_{ξ} (x, u, D u) \cdot D φ) d x$ ; together with step 3.1 this gives the displayed identity for the arbitrary element $φ \in W_{0}^{1, p} (Ω)$ . Finally, if $φ \in C_{c}^{\infty} (Ω)$ then $φ \in W_{0}^{1, p} (Ω)$ by [F4], so the identity holds in particular for every such test function. Conversely, the derivative in [F3] is bounded on $W^{1, p}$ , and every $φ \in W_{0}^{1, p}$ is a norm limit of compactly supported smooth functions by [F1]; continuity passes the identity from those tests to $φ$ .

Depends on

Used by

Dependency tree · two levels

57 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

Riccardo Cristoferi, Calculus of Variations: Lecture Notes, Carnegie Mellon University 2016 (complete 133-page notes) (standard reference, not scraped)
Francesco Paolo Maiale (course by Giovanni Alberti), Lecture Notes Calculus of Variations A, University of Pisa (last update 21 August 2019; complete 149-page notes) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)