ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Fixed-trace and free-trace variations give different boundary equations

Example

Example. Assume the Axiom of Choice (The Axiom of Choice). Let $Ω \subseteq R^{n}$ , $n \geq 2$ , be a bounded $C^{1}$ domain, let $f \in L^{2} (Ω; R)$ , and put $I (u) = \frac{1}{2} \int_{Ω} ∣ D u ∣^{2} d x - \int_{Ω} f u d x .$ (a) Fixed trace: a local minimiser in the $H^{1}$ norm on the nonempty affine class $K_{g} = {v \in H^{1} (Ω) : T v = g}$ , with $g \in H^{1 / 2} (\partial Ω)$ , solves the weak Dirichlet problem $- Δ u = f$ , $T u = g$ (The Dirichlet principle for the Poisson equation, The affine Dirichlet trace class is nonempty, convex and weakly closed). (b) Free trace: if $u \in C^{2} (\overline{Ω})$ is a local minimiser in the $C^{2}$ norm on $C^{2} (\overline{Ω})$ , then $- Δ u = f$ almost everywhere in $Ω$ and $\partial_{ν} u = 0$ on $\partial Ω$ . Choosing the continuous representative $f = - Δ u$ makes the interior equation pointwise. This is the boundary condition suggested by The natural boundary condition for free boundary variations, proved directly here since a general $L^{2}$ forcing need not give a $C^{2}$ integrand.

The constant-shift identity is $I (u + c) = I (u) - c \int_{Ω} f$ . Thus $I$ is invariant under global constants exactly when $\int_{Ω} f = 0$ , and it is never coercive on all of $H^{1} (Ω)$ . If $\int_{Ω} f \neq 0$ , no free local minimiser exists. On a connected domain satisfying the extension-domain hypothesis of Weak Neumann solvability on the mean-zero subspace, zero-mean forcing gives a unique mean-zero weak Neumann solution; nonzero mean cannot be repaired merely by normalising the solution. On a disconnected domain compatibility is required on each component and the additive constants are independent on those components.

Facts & Assumptions

Given: The Axiom of Choice; the real domain and data above; local minimality in $H^{1}$ on $K_{g}$ in (a), or in $C^{2}$ on the whole $C^{2}$ space in (b).

[F1]

The fixed-trace class is a translate of $H_{0}^{1} (Ω)$ ; its admissible directions are exactly that subspace (The affine Dirichlet trace class is nonempty, convex and weakly closed). The weak Euler–Lagrange identity holds for these directions (The weak Euler-Lagrange equation for integral functionals with fixed trace).

[F2]

The Dirichlet principle identifies its energy minimiser with the unique weak Poisson solution (The Dirichlet principle for the Poisson equation).

[F3]

First Green identity holds for $u \in C^{2} (\overline{Ω})$ and smooth tests under Countable Choice, supplied by AC (First Green identity). A locally integrable function pairing to zero with all compactly supported tests is zero almost everywhere (The fundamental lemma of the calculus of variations). A continuous boundary flux pairing to zero with all ambient smooth tests vanishes on the boundary (The boundary fundamental lemma of the calculus of variations).

[F4]

The Neumann supplier requires a bounded connected extension domain and a bounded forcing functional $F$ with $F (1) = 0$ ; it gives a unique mean-zero solution and all other solutions differ by constants. It also records the componentwise compatibility needed in the disconnected case (Weak Neumann solvability on the mean-zero subspace).

[F5]

Holder makes $v \mapsto \int f v$ bounded on $H^{1}$ , and bounds all terms in the quadratic expansion below (Holder's inequality for integrals, including the endpoint cases). Fermat's theorem gives a zero derivative at a two-sided interior local minimum (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$ ).

Verification

1.1F1F2F5givenalgebra

Fixed trace. For every $φ \in H_{0}^{1} (Ω)$ , the curve $u + t φ$ stays in $K_{g}$ by [F1]. Its energy is exactly $I (u) + t \int (D u \cdot D φ - f φ) + \frac{1}{2} t^{2} \int ∣ D φ ∣^{2}$ . Local minimality and [F5] give $\int D u \cdot D φ = \int f φ$ , the weak Dirichlet equation. Moreover the same expansion at $t = 1$ shows $I (u + φ) - I (u) = \frac{1}{2} \int ∣ D φ ∣^{2} \geq 0$ , so this local minimiser is global and [F2] applies.

1.2F3F5given

Free trace. For every $φ \in C^{\infty} (\overline{Ω})$ , the curve $u + t φ$ is admissible and close to $u$ in the $C^{2}$ norm as $t \to 0$ . The same quadratic expansion and [F5] give $\int (D u \cdot D φ - f φ) = 0$ . For compactly supported tests, Green identity [F3] then yields $\int (- Δ u - f) φ = 0$ , so $- Δ u = f$ almost everywhere by the fundamental lemma. Returning to arbitrary smooth tests gives $\int_{\partial Ω} (\partial_{ν} u) φ = 0$ by Green identity; the continuous field $D u$ and the boundary fundamental lemma force $\partial_{ν} u = 0$ .

2.1F4F5step 1.2algebra∎

Constants and compatibility. Direct expansion gives $I (u + c) = I (u) - c \int f$ . If $\int f \neq 0$ , arbitrarily small constant shifts in the appropriate sign lower the energy, and large shifts make it tend to $- \infty$ ; if $\int f = 0$ , arbitrarily large shifts leave it fixed. In both cases coercivity on the full space fails. In case (b), testing the first variation with $1$ gives $\int f = 0$ . At each boundary point the one-sided $C^{1}$ graph convention gives a smaller connected subgraph neighbourhood meeting only one component; at interior points use a ball in the component. Thus a component indicator extends locally constantly to $\overline{Ω}$ and is a $C^{2}$ admissible direction, giving the componentwise condition. Under the connected extension-domain hypotheses of [F4], the functional $F (v) = \int f v$ is bounded by [F5] and satisfies $F (1) = 0$ precisely for zero-mean forcing, so [F4] supplies the normalised weak solution.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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