ExampleConstruction: Literature-sourcedVerification: 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 one-dimensional Euler-Lagrange equation for an energy with a potential

Example

Example. Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $V \in C^{1} (R)$ , let $a < b$ be real numbers and let $I (u) = \int_{a}^{b} (\frac{1}{2} u^{'} (x)^{2} + V (u (x))) d x .$ On the admissible class $C^{2} ([a, b])$ with fixed endpoint values $u (a) = u_{0}$ , $u (b) = u_{1}$ , a local minimiser in the $C^{2}$ norm satisfies the boundary value problem $u^{''} = V^{'} (u) in (a, b), u (a) = u_{0}, u (b) = u_{1},$ the classical Euler-Lagrange equation of the Lagrangian $f (x, s, ξ) = \frac{1}{2} ξ^{2} + V (s)$ (The classical Euler-Lagrange equation under regularity). In the special case $V = 0$ this is the one-dimensional Laplace equation $u^{''} = 0$ with the affine solution $u (x) = u_{0} + \frac{u_{1} - u_{0}}{b - a} (x - a)$ ; for $V (s) = \frac{1}{2} ω^{2} s^{2}$ it is the equation of an inverted harmonic oscillator $u^{''} = ω^{2} u$ .

Facts & Assumptions

Given: Countable Choice; a function $V \in C^{1} (R)$ , a compact interval $[a, b] \subset R$ with $a < b$ , the functional $I (u) = \int_{a}^{b} (\frac{1}{2} u^{'} (x)^{2} + V (u (x))) d x$ on the admissible class of $u \in C^{2} ([a, b])$ with fixed endpoint values $u (a) = u_{0}$ , $u (b) = u_{1}$ , and the Lagrangian $f (x, s, ξ) = \frac{1}{2} ξ^{2} + V (s)$ .

[F1]

The conclusion has the shape of the classical Euler-Lagrange equation of The classical Euler-Lagrange equation under regularity for the Lagrangian $f (x, s, ξ) = \frac{1}{2} ξ^{2} + V (s)$ , whose partials are $f_{ξ} = ξ$ and $f_{s} = V^{'} (s)$ . That corollary also assumes $f \in C^{2}$ and the growth hypotheses of the weak Euler-Lagrange theorem (The weak Euler-Lagrange equation for integral functionals with fixed trace), which need not hold for a general $V \in C^{1}$ ; the verification below therefore computes the equation directly from the minimality of $u$ .

[F2]

One-variable mean value theorem and Fermat's interior-extremum theorem: a differentiable function on an interval with an interior local extremum has vanishing derivative there, and the mean value theorem identifies $(V (u + ε φ) - V (u)) / ε$ with $V^{'} (u + θ ε φ) φ$ for some $θ \in (0, 1)$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ , Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$ ).

[F3]

Integration by parts on a compactly supported test function: $\int_{a}^{b} u^{'} φ^{'} d x = - \int_{a}^{b} u^{''} φ d x$ for $φ \in C_{c}^{\infty} ((a, b))$ and $u \in C^{2} ([a, b])$ . This is Integration by parts for continuous factors with Riemann-integrable extensions of their interior derivatives with $F = u^{'}$ and $G = φ$ ; its continuous integrands have equal Riemann and Lebesgue integrals by A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral.

[F4]

Fundamental lemma: a continuous function on an open set orthogonal to every compactly supported smooth test function vanishes identically (The fundamental lemma of the calculus of variations).

[F5]

A $C^{2}$ function on $[a, b]$ with $u^{''} = 0$ on $(a, b)$ is affine, since $u^{'}$ has vanishing derivative and is therefore constant (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Verification

technique · direct, by testing the minimality of $u$ against compactly supported variations

1.1F1F2givenalgebra

The first variation. Let $φ \in C_{c}^{\infty} ((a, b))$ . Since $φ$ vanishes near the endpoints, $u + ε φ$ belongs to the admissible class for every $ε$ , and for $∣ ε ∣$ small it is close to $u$ in $C^{2} ([a, b])$ , so $Φ (ε) : = I (u + ε φ)$ has a local minimum at $ε = 0$ . Computing the difference quotient, $ε^{- 1} (Φ (ε) - Φ (0)) = \int_{a}^{b} (u^{'} φ^{'} + \frac{ε}{2} φ^{' 2} + ε^{- 1} (V (u + ε φ) - V (u))) d x$ , and by the mean value theorem [F2] the last term equals $φ (x) V^{'} (u (x) + θ_{x} ε φ (x))$ with $θ_{x} \in (0, 1)$ ; as $ε \to 0$ this converges to $φ V^{'} (u)$ uniformly on $[a, b]$ , because $V^{'}$ is uniformly continuous by Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous on a compact interval containing the values $u (x) + θ_{x} ε φ (x)$ and $∣ u + θ ε φ - u ∣ \leq ∣ ε ∣ ∥ φ ∥_{\infty}$ . Hence $Φ$ is differentiable at $0$ with $Φ^{'} (0) = \int_{a}^{b} (u^{'} φ^{'} + V^{'} (u) φ) d x$ . This is the direct computation announced in [F1].

2.1F2step 1.1

Fermat's theorem. The point $0$ is an interior local minimum of the differentiable function $Φ$ , so [F2] gives $Φ^{'} (0) = 0$ , that is $\int_{a}^{b} (u^{'} φ^{'} + V^{'} (u) φ) d x = 0$ for every $φ \in C_{c}^{\infty} ((a, b))$ .

3.1F3F4step 2.1

The differential equation. For $φ \in C_{c}^{\infty} ((a, b))$ integration by parts [F3] gives $\int_{a}^{b} u^{'} φ^{'} d x = - \int_{a}^{b} u^{''} φ d x$ , so the identity of step 2.1 reads $\int_{a}^{b} (- u^{''} + V^{'} (u)) φ d x = 0$ for every such $φ$ . The function $- u^{''} + V^{'} (u)$ is continuous on $(a, b)$ , being a sum of continuous functions, so the fundamental lemma [F4] gives $- u^{''} + V^{'} (u) = 0$ on $(a, b)$ , that is $u^{''} = V^{'} (u)$ .

4.1F5step 3.1givenalgebra∎

Endpoint conditions and the two instances. The admissible class fixes $u (a) = u_{0}$ and $u (b) = u_{1}$ , so $u$ solves the boundary value problem of the statement. For $V = 0$ the equation is $u^{''} = 0$ , and [F5] makes $u$ affine, with values determined by the endpoints: $u (x) = u_{0} + \frac{u_{1} - u_{0}}{b - a} (x - a)$ . For $V (s) = \frac{1}{2} ω^{2} s^{2}$ one has $V^{'} (s) = ω^{2} s$ , so the equation reads $u^{''} = ω^{2} u$ , the equation of an inverted harmonic oscillator.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

73 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

Sung-Jin Oh, Lecture Notes for Math 222A, UC Berkeley, 19 March 2024 (complete 179-page author PDF) (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)