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 direct method for convex integral functionals

Statement

Assume the ultrafilter lemma, DC and HB. Let $n \geq 2$ , $1 < p < \infty$ , let $Ω \subseteq R^{n}$ be a bounded $C^{1}$ domain, and let $u_{b} \in W^{1, p} (Ω)$ . Set $K : = u_{b} + W_{0}^{1, p} (Ω),$ where $W_{0}^{1, p} (Ω)$ is the closure of $C_{c}^{\infty} (Ω)$ in $W^{1, p} (Ω)$ (Zero-boundary Sobolev space as a norm closure). Let $f : Ω \times R \times R^{n} \to R$ be a Caratheodory integrand (A Caratheodory integrand composed with measurable functions is measurable) such that for almost every $x$ the map $(s, ξ) \mapsto f (x, s, ξ)$ is convex and lower semicontinuous (Convex and strictly convex functionals on a convex subset of a real vector space). Assume the upper growth bound $f (x, s, ξ) \leq C (1 + ∣ s ∣^{p} + ∣ ξ ∣^{p}) + G (x) for almost every x and all (s, ξ),$ where $G \in L^{1} (Ω)$ , together with the coercivity hypothesis: there are $ν > 0$ , $c \geq 0$ , $q \in [1, p]$ and $h \in L^{1} (Ω)$ , $h \geq 0$ , with $f (x, s, ξ) \geq ν ∣ ξ ∣^{p} - c ∣ s ∣^{q} - h (x)$ for almost every $x$ and all $(s, ξ)$ , where, in the case $q = p$ , the smallness condition $2^{p - 1} c C_{P}^{p} \leq ν 2^{- p}$ holds for a Poincare constant $C_{P}$ of $W_{0}^{1, p} (Ω)$ (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction). Then $I (u) = \int_{Ω} f (x, u (x), D u (x)) d x$ is finite on $W^{1, p} (Ω)$ and attains its infimum on $K$ . If in addition $f$ satisfies the hypotheses of Differentiation of an integral functional under growth domination, then every minimiser $u$ satisfies $\int_{Ω} (f_{s} (x, u, D u) v + f_{ξ} (x, u, D u) \cdot D v) d x = 0 (v \in W_{0}^{1, p} (Ω)),$ the weak Euler-Lagrange equation for zero-boundary variations. If $f (x, \cdot, \cdot)$ is strictly convex for almost every $x$ , the minimiser is unique.

Facts & Assumptions

Given: The ultrafilter lemma, DC (which implies Countable Choice by Dependent choice implies countable choice) and HB; a bounded $C^{1}$ domain $Ω \subseteq R^{n}$ , $n \geq 2$ , $1 < p < \infty$ ; a lift $u_{b} \in W^{1, p} (Ω)$ and the nonempty affine class $K = u_{b} + W_{0}^{1, p} (Ω)$ ; and a Caratheodory integrand $f : Ω \times R \times R^{n} \to R$ with $(s, ξ) \mapsto f (x, s, ξ)$ convex and lower semicontinuous for almost every $x$ , satisfying the upper growth bound $f (x, s, ξ) \leq C (1 + ∣ s ∣^{p} + ∣ ξ ∣^{p}) + G (x)$ with $G \in L^{1} (Ω)$ , and the coercivity bound $f (x, s, ξ) \geq ν ∣ ξ ∣^{p} - c ∣ s ∣^{q} - h (x)$ with $ν > 0$ , $c \geq 0$ , $q \in [1, p]$ , $0 \leq h \in L^{1} (Ω)$ , where $2^{p - 1} c C_{P}^{p} \leq ν 2^{- p}$ holds in the case $q = p$ for a Poincare constant $C_{P}$ of $W_{0}^{1, p} (Ω)$ (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction).

[F1]

For measurable $u, w$ the composition $x \mapsto f (x, u (x), w (x))$ is measurable (A Caratheodory integrand composed with measurable functions is measurable).

[F2]

$W_{0}^{1, p} (Ω)$ is a closed linear subspace by its definition as the closure of $C_{c}^{\infty} (Ω)$ ; hence $K = u_{b} + W_{0}^{1, p} (Ω)$ is nonempty, convex and norm closed. Under HB, norm-closed convex sets are weakly closed (Zero-boundary Sobolev space as a norm closure, Norm closed convex iff weakly closed).

[F3]

On the bounded domain, $u \in W^{1, p} (Ω)$ has $u, D u \in L^{p} (Ω)$ , and $L^{p} (Ω) \subseteq L^{q} (Ω)$ for $q \leq p$ with $∥ w ∥_{q} \leq ∣ Ω ∣^{1 / q - 1 / p} ∥ w ∥_{p}$ ; for $q < p$ this follows by applying Holder to $∣ w ∣^{q}$ and $1$ with conjugate exponents $p / q$ and $p / (p - q)$ , while $q = p$ is equality (Holder's inequality for integrals, including the endpoint cases); the space $W^{1, p} (Ω)$ is a real Banach space and its classes are $L^{p}$ classes (Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions).

[F4]

Fatou's lemma for nonnegative measurable functions (Fatou's lemma).

[F5]

If a sequence converges in $L^{p}$ , $1 \leq p < \infty$ , then a subsequence converges almost everywhere (Assuming Countable Choice, $L^{p}$ -convergent sequences have almost-everywhere convergent subsequences).

[F6]

Under HB and Countable Choice, a convex functional that is sequentially lower semicontinuous in the norm topology on a nonempty convex set is weakly sequentially lower semicontinuous (A convex norm-lower-semicontinuous functional is weakly lower semicontinuous).

[F7]

$W^{1, p} (Ω)$ is a real reflexive Banach space under the ultrafilter lemma, DC and HB (W^{1,p}(Omega) is reflexive for 1<p<infinity, Reflexivity is surjectivity of the canonical map), and the direct method in a reflexive Banach space yields a minimiser (The direct method in a reflexive Banach space); a nonempty convex norm-closed set is admissible by Norm closed convex iff weakly closed.

[F8]

If $f$ satisfies the hypotheses of Differentiation of an integral functional under growth domination, then $I$ is Gateaux differentiable with the displayed integral derivative. A minimiser on $u_{b} + W_{0}^{1, p} (Ω)$ is a local minimiser along every direction in $W_{0}^{1, p} (Ω)$ , so the first-variation theorem gives vanishing derivative on that space (The first variation vanishes at an interior minimiser).

[F9]

A proper, strictly convex functional has at most one minimiser on a convex set (Strict convexity gives uniqueness of a minimiser, Convex and strictly convex functionals on a convex subset of a real vector space); in the application $I$ is finite on the nonempty class $K$ , hence proper.

Proof

technique · direct; finiteness, convexity and norm lower semicontinuity of $I$, then the coercivity estimate and the direct method

1.1F1F2F3given

Finiteness of $I$ . For $u \in W^{1, p} (Ω)$ the integrand $x \mapsto f (x, u (x), D u (x))$ is measurable by [F1]. Its positive part is bounded by $C (1 + ∣ u ∣^{p} + ∣ D u ∣^{p}) + ∣ G ∣$ because $G \leq ∣ G ∣$ , and this has finite integral because $Ω$ is bounded, $u, D u \in L^{p}$ and $∣ G ∣ \in L^{1}$ ; its negative part is bounded by $c ∣ u ∣^{q} + h$ , whose integral is finite because $q \leq p$ , $u \in L^{q}$ by [F3] and $h \in L^{1}$ . Hence $I (u) = \int_{Ω} f (x, u (x), D u (x)) d x$ is a well-defined real number, and $I$ is proper as $K \neq \emptyset$ .

2.1F3step 1.1algebra

Convexity of $I$ . For $u, v \in W^{1, p} (Ω)$ and $λ \in [0, 1]$ the pair $(λ u + (1 - λ) v, λ D u + (1 - λ) D v)$ equals $λ (u, D u) + (1 - λ) (v, D v)$ because the weak gradient is linear, and for almost every $x$ the convexity of $f (x, \cdot, \cdot)$ gives $f (x, λ u + (1 - λ) v, λ D u + (1 - λ) D v) \leq λ f (x, u, D u) + (1 - λ) f (x, v, D v)$ . All three functions are integrable by step 1.1, so integrating gives $I (λ u + (1 - λ) v) \leq λ I (u) + (1 - λ) I (v)$ : $I$ is convex on the real vector space $W^{1, p} (Ω)$ .

2.2F4F5step 1.1given

Norm lower semicontinuity of $I$ . Let $u_{j} \to u$ in $W^{1, p}$ . Suppose, for contradiction, that $I (u) > {lim inf}_{j} I (u_{j}) = : ℓ$ ; since $I$ is real-valued, choose a real $t$ with $ℓ < t < I (u)$ . Then $I (u_{j}) \leq t$ for infinitely many $j$ , so passing to that subsequence (and relabelling) we may assume $I (u_{j}) \leq t$ for all $j$ and still $u_{j} \to u$ in $W^{1, p}$ ; in particular $u_{j} \to u$ and $D u_{j} \to D u$ in $L^{p}$ . By [F5] pass to a further subsequence with $u_{j} \to u$ and $D u_{j} \to D u$ almost everywhere. Since $(s, ξ) \mapsto f (x, s, ξ)$ is lower semicontinuous at $(u (x), D u (x))$ for almost every $x$ , the pointwise limit inferior satisfies $f (x, u, D u) + c ∣ u ∣^{q} + h \leq {lim inf}_{j} (f (x, u_{j}, D u_{j}) + c ∣ u_{j} ∣^{q} + h)$ . The shifted integrands $φ_{j} : = f (x, u_{j}, D u_{j}) + c ∣ u_{j} ∣^{q} + h$ are nonnegative by the coercivity bound and measurable by [F1], so Fatou's lemma [F4] gives $\int_{Ω} (f (x, u, D u) + c ∣ u ∣^{q} + h) \leq {lim inf}_{j} \int_{Ω} φ_{j} = {lim inf}_{j} I (u_{j}) + c ∥ u ∥_{q}^{q} + ∥ h ∥_{1}$ , where $∥ u_{j} ∥_{q} \to ∥ u ∥_{q}$ because $u_{j} \to u$ in $L^{p}$ and $q \leq p$ . Cancelling the common finite terms yields $I (u) \leq {lim inf}_{j} I (u_{j}) \leq t$ , contradicting $t < I (u)$ . Hence $I$ is sequentially lower semicontinuous in the norm topology.

2.3F2F3step 1.1givenalgebra

Coercivity of $I$ on $K$ . Write each $u \in K$ as $u = u_{b} + v$ with $v \in W_{0}^{1, p} (Ω)$ . The lower growth bound gives $I (u) \geq ν ∥ D u ∥_{p}^{p} - c ∥ u ∥_{q}^{q} - ∥ h ∥_{1}$ , while the triangle inequality and $(a + b)^{p} \leq 2^{p - 1} (a^{p} + b^{p})$ give $∥ D u ∥_{p}^{p} \geq 2^{1 - p} ∥ D v ∥_{p}^{p} - ∥ D u_{b} ∥_{p}^{p}$ . By Poincare, $∥ v ∥_{p} \leq C_{P} ∥ D v ∥_{p}$ , and with $C_{Ω} : = ∣ Ω ∣^{1 / q - 1 / p}$ (equal to $1$ when $q = p$ ), Holder and the triangle inequality imply $∥ u ∥_{q}^{q} \leq C_{Ω}^{q} 2^{q - 1} (∥ u_{b} ∥_{p}^{q} + C_{P}^{q} ∥ D v ∥_{p}^{q}) .$ If $q < p$ , these estimates yield $I (u) \geq ν 2^{1 - p} ∥ D v ∥_{p}^{p} - c^{'} ∥ D v ∥_{p}^{q} - C^{''}$ , which tends to $+ \infty$ as $∥ D v ∥_{p} \to \infty$ . If $q = p$ , they yield $I (u) \geq (ν 2^{1 - p} - c 2^{p - 1} C_{P}^{p}) ∥ D v ∥_{p}^{p} - C^{''} \geq ν 2^{- p} ∥ D v ∥_{p}^{p} - C^{''}$ by the smallness assumption. Finally, $u = u_{b} + v$ and Poincare give $∥ u ∥_{W^{1, p}} \leq C_{b} + C_{1} ∥ D v ∥_{p}$ for fixed finite constants $C_{b}, C_{1}$ , so $∥ u ∥_{W^{1, p}} \to \infty$ forces $∥ D v ∥_{p} \to \infty$ . Thus $I$ is coercive on $K$ .

3.1F6step 2.1step 2.2

Weak sequential lower semicontinuity on $K$ . By steps 2.1 and 2.2 the functional $I$ is convex and norm lower semicontinuous on the convex set $W^{1, p} (Ω)$ ; [F6] therefore makes $I$ weakly sequentially lower semicontinuous on $W^{1, p} (Ω)$ , hence on the subset $K$ .

4.1F2F7step 1.1step 2.3step 3.1

Existence of a minimiser. By [F7] the space $W^{1, p} (Ω)$ is a real reflexive Banach space under the present choice principles, and $K$ is nonempty, convex and weakly closed by [F2], in particular weakly sequentially closed. The functional $I$ is proper by step 1.1, coercive on $K$ by step 2.3 and weakly sequentially lower semicontinuous on $K$ by step 3.1, so the direct method [F7] provides $u_{0} \in K$ with $I (u_{0}) = \inf_{K} I$ .

5.1F8step 4.1

The Euler-Lagrange clause. Suppose in addition that $f$ satisfies the hypotheses of the differentiation lemma. Then [F8] gives the Gateaux derivative formula. Since $K = u_{b} + W_{0}^{1, p} (Ω)$ , a minimiser $u_{0}$ is a local minimiser along every direction in $W_{0}^{1, p} (Ω)$ ; applying the first-variation theorem with $V = W_{0}^{1, p} (Ω)$ yields $\int_{Ω} (f_{s} (x, u_{0}, D u_{0}) v + f_{ξ} (x, u_{0}, D u_{0}) \cdot D v) d x = 0 (v \in W_{0}^{1, p} (Ω)) .$ This is the weak Euler-Lagrange equation for the affine zero-boundary variation class.

6.1F9step 1.1step 4.1∎

Strict convexity and uniqueness. Assume finally that $f (x, \cdot, \cdot)$ is strictly convex for almost every $x$ . For distinct $u \neq v$ in $K$ the set $S : = {x : (u (x), D u (x)) \neq (v (x), D v (x))}$ has positive measure, because otherwise $u = v$ and $D u = D v$ almost everywhere, that is, $u = v$ as elements of $W^{1, p} (Ω)$ . For almost every $x \in S$ and every $λ \in (0, 1)$ the strict convexity of $f (x, \cdot, \cdot)$ gives $f (x, λ u + (1 - λ) v, λ D u + (1 - λ) D v) < λ f (x, u, D u) + (1 - λ) f (x, v, D v)$ , the values being finite by step 1.1; integrating over $S$ and using the convex inequality elsewhere gives $I (λ u + (1 - λ) v) < λ I (u) + (1 - λ) I (v)$ , so $I$ is strictly convex on the convex set $K$ . By [F9] the minimiser of step 4.1 is then unique.

Depends on

Used by

A nonconvex gradient energy can lose weak lower semicontinuity Counterexample
The Dirichlet principle for the Poisson equation Theorem

Dependency tree · two levels

91 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

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)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations, University of Illinois (complete 158-page graduate notes) (standard reference, not scraped)