CorollaryStatement: 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 classical Euler-Lagrange equation under regularity

Statement

Let the hypotheses of The weak Euler-Lagrange equation for integral functionals with fixed trace hold, and assume in addition that $f \in C^{2} (\overline{Ω} \times R \times R^{n})$ and $u \in C^{2} (\overline{Ω})$ ( $C^{k}$ maps and multi-index derivative notation in Euclidean space). Then $w (x) : = f_{ξ} (x, u (x), D u (x)) \in C^{1} (Ω; R^{n})$ and $- div w + f_{s} (x, u (x), D u (x)) = 0 (x \in Ω),$ the classical Euler-Lagrange equation (Divergence and curl of a $C^{1}$ vector field), with the first variation supplied by Differentiation of an integral functional under growth domination.

Facts & Assumptions

Given: The hypotheses of The weak Euler-Lagrange equation for integral functionals with fixed trace (a bounded $C^{1}$ domain $Ω$ , $1 < p < \infty$ , the Caratheodory integrand $f$ with the stated growth bounds, a local minimiser $u \in W^{1, p} (Ω)$ of the integral functional among the functions of trace $g$ with $g$ in the trace range), together with $f \in C^{2} (\overline{Ω} \times R \times R^{n})$ and $u \in C^{2} (\overline{Ω})$ . The measure-theoretic background is the Axiom-of-Countable-Choice framework of the published surface and divergence theory (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

For every $φ \in W_{0}^{1, p} (Ω)$ , and in particular for every $φ \in C_{c}^{\infty} (Ω)$ , the weak Euler-Lagrange identity holds: $\int_{Ω} (f_{ξ} (x, u, D u) \cdot D φ + f_{s} (x, u, D u) φ) d x = 0$ (The weak Euler-Lagrange equation for integral functionals with fixed trace).

[F2]

Composites of $C^{k}$ Euclidean maps are $C^{k}$ ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition): since $f \in C^{2}$ gives $f_{s}, f_{ξ} \in C^{1}$ and $x \mapsto (x, u (x), D u (x))$ is $C^{1}$ for $u \in C^{2} (\overline{Ω})$ , the functions $x \mapsto f_{s} (x, u (x), D u (x))$ and $w (x) : = f_{ξ} (x, u (x), D u (x))$ are of class $C^{1}$ on $Ω$ ; consequently $div w$ is continuous and $f_{s} - div w$ is continuous on $Ω$ (Divergence and curl of a $C^{1}$ vector field, $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[F3]

Divergence theorem: for a bounded $C^{1}$ domain and $F \in C^{1} (\overline{Ω}; R^{n})$ , $\int_{Ω} div F d x = \int_{\partial Ω} F \cdot ν d σ$ (Divergence on a bounded C1 Euclidean domain); the first Green identity is the special case $F = v D u$ of this identity (First Green identity).

[F4]

Fundamental lemma: if $g \in L_{l o c}^{1} (Ω)$ satisfies $\int_{Ω} g φ = 0$ for every $φ \in C_{c}^{\infty} (Ω)$ , then $g = 0$ almost everywhere; a continuous such $g$ vanishes everywhere (The fundamental lemma of the calculus of variations).

Proof

technique · direct, by testing the weak equation with compactly supported functions and integrating by parts

1.1F2given

Regularity of the coefficients. By [F2] the vector field $w (x) = f_{ξ} (x, u (x), D u (x))$ is of class $C^{1}$ on the open set $Ω$ , and the function $x \mapsto f_{s} (x, u (x), D u (x))$ is continuous; hence $div w$ is continuous and so is $f_{s} - div w$ .

2.1F1step 1.1

The weak identity. Let $φ \in C_{c}^{\infty} (Ω)$ . Then $φ \in W_{0}^{1, p} (Ω)$ , so [F1] gives $\int_{Ω} (f_{ξ} (x, u, D u) \cdot D φ + f_{s} (x, u, D u) φ) d x = 0$ , that is $\int_{Ω} w \cdot D φ d x = - \int_{Ω} f_{s} φ d x$ .

2.2F3step 1.1

Integration by parts with compact support. The field $F : = φ w$ is $C^{1}$ and compactly supported in $Ω$ ; in particular $F$ extends by zero to a $C^{1}$ field on $\overline{Ω}$ , so [F3] may be applied to it. Since $φ = 0$ on $\partial Ω$ , the boundary term vanishes and $\int_{Ω} div (φ w) d x = 0$ . By the product rule $div (φ w) = D φ \cdot w + φ div w$ , hence $\int_{Ω} w \cdot D φ d x = - \int_{Ω} (div w) φ d x$ .

3.1step 2.1step 2.2

The combined identity. Substituting step 2.2 into step 2.1 gives $\int_{Ω} (f_{s} (x, u, D u) - div w) φ d x = 0$ for every $φ \in C_{c}^{\infty} (Ω)$ .

4.1F4step 3.1∎

The fundamental lemma. The function $g : = f_{s} (x, u (x), D u (x)) - div w (x)$ is continuous on $Ω$ by step 1.1 and is orthogonal to every test function by step 3.1; [F4] gives $g = 0$ almost everywhere, and continuity upgrades this to $g = 0$ everywhere on $Ω$ . Hence $- div w + f_{s} (x, u (x), D u (x)) = 0$ on $Ω$ , the classical Euler-Lagrange equation.

Depends on

Used by

Dependency tree · two levels

59 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)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)