LemmaStatement: 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.

Differentiation of an integral functional under growth domination

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $Ω \subseteq R^{n}$ be a bounded $C^{1}$ domain (Bounded C^k domains and boundary charts), $1 < p < \infty$ , and let $f : Ω \times R \times R^{n} \to R$ be a Caratheodory integrand (A Caratheodory integrand composed with measurable functions is measurable) whose classical partial derivatives $f_{s}$ , $f_{ξ}$ exist and are continuous in $(s, ξ)$ for almost every $x$ , with a constant $C \geq 0$ and functions $G \in L^{1} (Ω)$ , $g \in L^{p^{'}} (Ω)$ , where $p^{'} = p / (p - 1)$ , such that for almost every $x$ and all $(s, ξ)$ $∣ f (x, s, ξ) ∣ \leq C (1 + ∣ s ∣^{p} + ∣ ξ ∣^{p}) + G (x), ∣ f_{s} (x, s, ξ) ∣ + ∣ f_{ξ} (x, s, ξ) ∣ \leq C (1 + ∣ s ∣^{p - 1} + ∣ ξ ∣^{p - 1}) + g (x) .$ Then $I (u) : = \int_{Ω} f (x, u (x), D u (x)) d x$ is well defined and finite on $W^{1, p} (Ω)$ (Integer-order Sobolev spaces and their norms), and for all $u, v \in W^{1, p} (Ω)$ $δ I (u; v) = \int_{Ω} (f_{s} (x, u, D u) v + f_{ξ} (x, u, D u) \cdot D v) d x .$ In particular $I$ is Gateaux differentiable at every $u$ , with bounded Gateaux derivative $δ I (u) \in W^{1, p} (Ω)^{*}$ (Gateaux and Frechet derivatives of a functional).

Facts & Assumptions

Given: Countable Choice; a bounded $C^{1}$ domain $Ω \subseteq R^{n}$ , $1 < p < \infty$ with Holder conjugate $p^{'} = p / (p - 1)$ , and a Caratheodory integrand $f : Ω \times R \times R^{n} \to R$ whose classical partials $f_{s}, f_{ξ}$ exist and are continuous in $(s, ξ)$ for almost every $x$ , with $C \geq 0$ , $G \in L^{1} (Ω)$ , $g \in L^{p^{'}} (Ω)$ and, for almost every $x$ and all $(s, ξ)$ , $∣ f (x, s, ξ) ∣ \leq C (1 + ∣ s ∣^{p} + ∣ ξ ∣^{p}) + G (x), ∣ f_{s} (x, s, ξ) ∣ + ∣ f_{ξ} (x, s, ξ) ∣ \leq C (1 + ∣ s ∣^{p - 1} + ∣ ξ ∣^{p - 1}) + g (x) .$

[F1]

For a Caratheodory integrand and 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]

The proof of Integer-order Sobolev spaces are Banach uses only Countable Choice after AC supplies it, so the Countable Choice assumed here supplies that same completeness argument and makes $W^{1, p}$ a Banach space. On a bounded domain, the class $u \in W^{1, p} (Ω)$ has $u, D u \in L^{p} (Ω)$ and finite norm $∥ u ∥_{W^{1, p} (Ω)}$ , with $∥ u ∥_{p} \leq ∥ u ∥_{W^{1, p}}$ and $∥ ∣ D u ∣ ∥_{p} \leq n ∥ u ∥_{W^{1, p}}$ , since $∣ D u ∣ \leq \sum_{i} ∣ D_{i} u ∣$ ; the constant $1$ lies in $L^{1} (Ω) \cap L^{p^{'}} (Ω)$ , $∣ G ∣ \in L^{1} (Ω)$ , and $∣ u ∣^{p - 1}, ∣ D u ∣^{p - 1}$ (and the analogous monomials in $v, D v$ ) lie in $L^{p^{'}} (Ω)$ (Integer-order Sobolev spaces and their norms, Bounded C^k domains and boundary charts).

[F3]

Holder's inequality: $\int ∣ h w ∣ \leq ∥ h ∥_{p^{'}} ∥ w ∥_{p}$ for $h \in L^{p^{'}} (Ω)$ and $w \in L^{p} (Ω)$ (Holder's inequality for integrals, including the endpoint cases).

[F4]

Dominated convergence: if measurable $q_{k} \to q$ almost everywhere and $∣ q_{k} ∣ \leq H$ almost everywhere for a single $H \in L^{1} (Ω)$ , then $\int q_{k} \to \int q$ (Dominated convergence).

[F5]

If the classical partial derivatives of $(s, ξ) \mapsto f (x, s, ξ)$ are continuous at a point, then that map is totally differentiable there (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative); the chain rule identifies the total derivative of $t \mapsto f (x, s + t v, ξ + t w)$ as $f_{s} (x, s + t v, ξ + t w) v + f_{ξ} (x, s + t v, ξ + t w) \cdot w$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ); the one-variable mean value theorem applies to $t \mapsto f (x, s + t v, ξ + t w)$ on a compact interval (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)$ ).

[F6]

$I$ is Gateaux differentiable at $u$ with Gâteaux derivative $δ I (u) \in W^{1, p} (Ω)^{*}$ precisely when the limits $δ I (u; v)$ exist for all $v$ and $v \mapsto δ I (u; v)$ is a bounded linear functional (Gateaux and Frechet derivatives of a functional).

Proof

technique · direct, by difference quotients, the mean value theorem, a uniform integrable dominator and dominated convergence

1.1F1F2given

Well-definedness and finiteness. For $u \in W^{1, p} (Ω)$ the map $x \mapsto f (x, u (x), D u (x))$ is measurable by [F1], and the first bound of the hypothesis, together with $G \leq ∣ G ∣$ , gives $∣ f (x, u (x), D u (x)) ∣ \leq C (1 + ∣ u (x) ∣^{p} + ∣ D u (x) ∣^{p}) + ∣ G (x) ∣$ , whose integral is finite by [F2]. Hence $I (u) = \int_{Ω} f (x, u (x), D u (x)) d x$ is a well-defined real number for every $u \in W^{1, p} (Ω)$ .

1.2F5given

Difference quotients and their pointwise limit. Fix $u, v \in W^{1, p} (Ω)$ and put $q_{ε} (x) : = ε^{- 1} (f (x, u (x) + ε v (x), D u (x) + ε D v (x)) - f (x, u (x), D u (x)))$ for $ε \neq 0$ . For almost every $x$ the map $(s, ξ) \mapsto f (x, s, ξ)$ is $C^{1}$ , so [F5] applies to $g_{x} (t) : = f (x, u (x) + t v (x), D u (x) + t D v (x))$ : by the mean value theorem there is $θ = θ (x, ε) \in (0, 1)$ with $q_{ε} (x) = g_{x}^{'} (θ ε)$ , and $g_{x}^{'} (t) = f_{s} (x, u + t v, D u + t D v) v (x) + f_{ξ} (x, u + t v, D u + t D v) \cdot D v (x)$ . As $ε \to 0$ the arguments $(u (x) + θ ε v (x), D u (x) + θ ε D v (x))$ tend to $(u (x), D u (x))$ , so continuity of the partials gives the pointwise limit $q_{ε} (x) \to f_{s} (x, u (x), D u (x)) v (x) + f_{ξ} (x, u (x), D u (x)) \cdot D v (x)$ for almost every $x$ .

2.1F2F3step 1.2

A single integrable dominator. For almost every $x$ and every $0 < ∣ ε ∣ \leq 1$ , the representation of step 1.2 and the second bound of the hypothesis give, with $θ = θ (x, ε)$ and the elementary estimate $(a + b)^{p - 1} \leq 2^{p - 1} (a^{p - 1} + b^{p - 1})$ , $∣ q_{ε} (x) ∣ \leq h (x) (∣ v (x) ∣ + ∣ D v (x) ∣), h : = C^{'} (1 + ∣ u ∣^{p - 1} + ∣ v ∣^{p - 1} + ∣ D u ∣^{p - 1} + ∣ D v ∣^{p - 1}) + ∣ g ∣,$ for a constant $C^{'}$ depending only on $C$ and $p$ . Since $u, D u, v, D v \in L^{p} (Ω)$ , the monomials $∣ u ∣^{p - 1}, \dots, ∣ D v ∣^{p - 1}$ lie in $L^{p^{'}} (Ω)$ , and $∣ g ∣ \in L^{p^{'}} (Ω)$ , while the constant term is integrable on the bounded domain; hence $h \in L^{p^{'}} (Ω)$ , and Hölder's inequality [F3] gives $h (∣ v ∣ + ∣ D v ∣) \in L^{1} (Ω)$ , uniformly in $ε$ .

3.1F4step 2.1

Dominated convergence identifies the limit. Let $ε_{k} \to 0$ , $ε_{k} \neq 0$ , and choose $K$ such that $∣ ε_{k} ∣ \leq 1$ for every $k \geq K$ . By step 1.2 the functions $q_{ε_{k}}$ converge pointwise almost everywhere to $L (x) : = f_{s} (x, u, D u) v + f_{ξ} (x, u, D u) \cdot D v$ , and by step 2.1 the tail $(q_{ε_{k}})_{k \geq K}$ is dominated by the single $L^{1}$ function $h (∣ v ∣ + ∣ D v ∣)$ . Applying [F4] to this tail gives $\int_{Ω} q_{ε_{k}} \to \int_{Ω} L$ ; removing a finite prefix does not change the limit. Since the sequence $ε_{k} \to 0$ was arbitrary, $\lim_{ε \to 0} ε^{- 1} (I (u + ε v) - I (u)) = \int_{Ω} (f_{s} (x, u, D u) v + f_{ξ} (x, u, D u) \cdot D v) d x$ .

4.1F3F6step 3.1∎

Boundedness of the derivative, and conclusion. The map $v \mapsto δ I (u; v) : = \int_{Ω} (f_{s} (x, u, D u) v + f_{ξ} (x, u, D u) \cdot D v) d x$ is linear in $v$ by linearity of the integral, and the pointwise estimate $∣ f_{s} (x, u, D u) v + f_{ξ} (x, u, D u) \cdot D v ∣ \leq h_{u} (x) (∣ v ∣ + ∣ D v ∣)$ with $h_{u} : = C (1 + ∣ u ∣^{p - 1} + ∣ D u ∣^{p - 1}) + ∣ g ∣ \in L^{p^{'}} (Ω)$ gives, by [F3], $∣ δ I (u; v) ∣ \leq (1 + n) ∥ h_{u} ∥_{p^{'}} ∥ v ∥_{W^{1, p} (Ω)}$ ; hence $δ I (u) \in W^{1, p} (Ω)^{*}$ . By [F6] the functional $I$ is Gateaux differentiable at $u$ with derivative $δ I (u)$ and the displayed formula, as claimed.

Depends on

Used by

Dependency tree · two levels

68 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

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