LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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 fundamental lemma of the calculus of variations for continuous coefficients

Statement

Assume the Axiom of Countable Choice ( ${A C}_{ω}$ ). Let $n, m \geq 1$ , let $U \subseteq R^{n}$ be open, and let $g : U \to R^{m}$ be continuous. If $\int_{U} ⟨ g, h ⟩ d λ = 0$ for every $h \in C_{c}^{\infty} (U; R^{m})$ , then $g = 0$ on $U$ . Here $⟨ \cdot, \cdot ⟩$ is the Euclidean inner product and $\int_{U} ⟨ g, h ⟩ d λ$ is the finite sum $\sum_{i < m} \int_{U} g_{i} h_{i} d λ$ of integrals of continuous compactly supported functions (Integral over a measurable subset). The scalar case is $m = 1$ : a continuous $g$ with $\int_{U} g h d λ = 0$ for every $h \in C_{c}^{\infty} (U; R)$ vanishes on $U$ . The vector case is deduced from the scalar case componentwise, each component tested separately. The conclusion is pointwise on $U$ , and the hypothesis is the full family of compactly supported smooth test functions. The Axiom of Countable Choice is declared because the localization lemma Localization: vanishing integrals or fluxes force a continuous function to vanish and the measurability fact Continuous functions on Euclidean spaces are Borel measurable used in the recorded proof assume it; no other choice principle enters.

Conventions. $C_{c}^{\infty} (U; R^{m})$ is the space of smooth $R^{m}$ -valued functions with compact support in $U$ , defined componentwise in the sense of $C^{k}$ Euclidean maps and diffeomorphisms and Test function space d of an open set. Each product $g_{i} h_{i}$ is continuous on $U$ and vanishes outside a compact subset of $U$ , and $\int_{U} g_{i} h_{i} d λ$ denotes the Lebesgue integral of its zero extension to $R^{n}$ , where $λ = λ_{n}$ is $n$ -dimensional Lebesgue measure (Integrable real and complex functions, and their integrals); [F5] and [F6] below record that this is a finite real number and that for a nonnegative integrand it agrees with the nonnegative integral over the measurable set $U$ of Integral over a measurable subset.

Facts & Assumptions

Given: The Axiom of Countable Choice ${A C}_{ω}$ ; naturals $n, m \geq 1$ ; an open set $U \subseteq R^{n}$ ; a continuous $g : U \to R^{m}$ with $\int_{U} ⟨ g, h ⟩ d λ = 0$ for every $h \in C_{c}^{\infty} (U; R^{m})$ ; and, inside the contradiction argument below, a point $p \in U$ with $g (p) \neq 0$ .

[F1]

Cutoff lemma, in ZF: for a compact set $K \subseteq Ω$ with $Ω \subseteq R^{n}$ open there is $χ \in C_{c}^{\infty} (Ω)$ with $0 \leq χ \leq 1$ and $χ = 1$ on a neighborhood of $K$ (Test function cutoffs and euclidean localization).

[F2]

Localization, under ${A C}_{ω}$ : if $G : U \to R^{m}$ is continuous on an open set $U$ and $\int_{V} G d λ_{n} = 0$ for every ball $V$ compactly contained in $U$ , then $G = 0$ on $U$ (Localization: vanishing integrals or fluxes force a continuous function to vanish, where $\int_{V} G$ is the componentwise integral over the measurable set $V$ ). Below we use only its contrapositive form: if $G (q) \neq 0$ for some $q \in U$ , then some ball $V$ compactly contained in $U$ has $\int_{V} G d λ_{n} \neq 0$ .

[F3]

Order and scalar rules for the nonnegative integral (Monotonicity and nonnegative homogeneity of the nonnegative integral): for nonnegative measurable $f \leq h$ one has $\int f d λ \leq \int h d λ$ , and for $c > 0$ one has $\int c f d λ = c \int f d λ$ , while the zero function has integral $0$ ; the nonnegative integral over a measurable set of Integral over a measurable subset is an instance of this integral.

[F4]

Continuity of pairings: if $f, w : U \to R^{m}$ are continuous then $x \mapsto ⟨ f (x), w (x) ⟩$ is continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, clause 3); for $m = 1$ this is the ordinary product of two continuous real functions under The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ . In particular the components $g_{i}$ of $g$ are continuous, and for $ψ \in C_{c}^{\infty} (U; R)$ the function $ψ e_{i}$ lies in $C_{c}^{\infty} (U; R^{m})$ and has $⟨ g, ψ e_{i} ⟩ = g_{i} ψ$ .

[F5]

Signed integral (Integrable real and complex functions, and their integrals): for measurable real $F$ with at most one of $\int F^{+} d λ$ , $\int F^{-} d λ$ equal to $+ \infty$ , one sets $\int F d λ : = \int F^{+} d λ - \int F^{-} d λ$ ; $F$ is integrable when both parts are finite. If $F \geq 0$ then $F^{-} = 0$ and the signed integral of $F$ equals its nonnegative integral, which over a measurable set $E$ is the integral of $F χ_{E}$ (Integral over a measurable subset); and $\int (- F) d λ = - \int F d λ$ is definitional from $(- F)^{+} = F^{-}$ and $(- F)^{-} = F^{+}$ .

[F6]

Compactly supported continuous functions have finite integrals: let $F : R^{n} \to R$ be continuous with compact support $K$ . If $K = \emptyset$ then $F = 0$ and $\int F d λ = 0$ ; otherwise $K$ is a nonempty compact metric space, so $M : = \max_{K} ∣ F ∣$ is finite (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value), $K$ is bounded (A compact subset of a metric space is closed and bounded) hence contained in a closed box $Q$ with $λ (Q) < + \infty$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included), $F$ is Borel measurable (Continuous functions on Euclidean spaces are Borel measurable, under ${A C}_{ω}$ ), and $∣ F ∣ \leq M χ_{Q}$ , so $\int ∣ F ∣ d λ \leq \int M χ_{Q} d λ = M λ (Q) < + \infty$ by Monotonicity and nonnegative homogeneity of the nonnegative integral, The nonnegative integral agrees with the simple integral on simple functions and The integral of a nonnegative simple function; thus $F$ is integrable by [F5]. In particular each integrand $g_{i} h_{i}$ of the hypothesis has a continuous compactly supported zero extension by [F4], and each pairing in the hypothesis is a finite real number.

[F7]

Continuity in balls (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, Open ball, closed ball and sphere in a metric space): $u$ is continuous at $p$ when for every real $ε > 0$ there is $δ > 0$ with $u [B (p, δ)] \subseteq B (u (p), ε)$ ; and $B (p, δ) = {x : d (p, x) < δ}$ for $δ > 0$ .

Proof

technique · contradiction; assume a point where $g\ne0$, reduce to a scalar continuous function with a vanishing test pairing, and construct a nonnegative compactly supported product of that coefficient with an admissible smooth test function, whose integral is both $0$ and positive

1.1givenF4F5assume-contra

Suppose the conclusion fails: $g (p) \neq 0$ for some $p \in U$ . If $m = 1$ , put $u : = g$ ; then $u$ is continuous and the hypothesis reads $\int_{U} u ψ d λ = 0$ for every $ψ \in C_{c}^{\infty} (U; R)$ . If $m \geq 2$ , choose $i < m$ with $g_{i} (p) \neq 0$ and put $u : = g_{i}$ ; for every $ψ \in C_{c}^{\infty} (U; R)$ the function $ψ e_{i}$ lies in $C_{c}^{\infty} (U; R^{m})$ with $⟨ g, ψ e_{i} ⟩ = g_{i} ψ$ by [F4], so the hypothesis gives $\int_{U} u ψ d λ = 0$ . In both cases $u : U \to R$ is continuous with $u (p) \neq 0$ , and replacing $u$ by $- u$ preserves the vanishing pairing because $\int_{U} (- u) ψ d λ = - \int_{U} u ψ d λ$ by [F5]; hence we may assume $u (p) > 0$ .

2.1step 1.1F7algebra

Continuity of $u$ at $p$ with $u (p) > 0$ yields $δ > 0$ with $B (p, δ) \subseteq U$ and $u (x) \geq u (p) / 2$ for every $x \in B (p, δ)$ : taking $ε : = u (p) / 2 > 0$ in [F7] gives $δ_{0} > 0$ with $∣ u (x) - u (p) ∣ < u (p) / 2$ for $d (p, x) < δ_{0}$ , and since $U$ is open one may shrink $δ_{0}$ to a $δ > 0$ with $B (p, δ) \subseteq U$ , the bound remaining valid on the smaller ball.

3.1step 2.1F1

Apply [F1] with $Ω : = B (p, δ)$ and $K : = {p}$ : there is $χ \in C_{c}^{\infty} (B (p, δ))$ with $0 \leq χ \leq 1$ and $χ = 1$ on a neighborhood of $p$ . Extended by zero, $χ$ lies in $C_{c}^{\infty} (U; R)$ and satisfies $supp χ \subseteq B (p, δ)$ .

4.1step 2.1step 3.1F1F4algebra

Put $φ : = u χ$ , extended by zero to $R^{n}$ . Then $φ$ is continuous and compactly supported in $U$ by [F4] and [F1], satisfies $φ \geq 0$ on $U$ because $φ = 0$ where $χ = 0$ and $φ (x) = u (x) χ (x) \geq (u (p) / 2) χ (x) \geq 0$ for $x \in B (p, δ)$ by step 2.1, and has $φ (p) = u (p) > 0$ ; hence $φ$ is not the zero function.

5.1step 3.1step 4.1givenF5F6

The hypothesis at the admissible test function $χ$ gives $\int_{U} u χ d λ = 0$ , that is $\int_{U} φ d λ = 0$ : since $φ \geq 0$ , the signed integral equals the nonnegative integral of $φ$ over the measurable set $U$ by [F5], and that integral is a finite real number by [F6].

5.2step 4.1F2F3

By the contrapositive localization [F2] applied to the continuous function $φ$ with $φ (p) \neq 0$ , there is a ball $V$ compactly contained in $U$ with $\int_{V} φ d λ \neq 0$ ; as $φ \geq 0$ , monotonicity in [F3] applied to the zero function below $φ χ_{V}$ gives $\int_{V} φ d λ \geq 0$ , so this integral is strictly positive.

6.1step 5.1step 5.2F3discharge-contradiction∎

Since $V \subseteq U$ , the nonnegative measurable functions $φ χ_{V}$ and $φ χ_{U}$ satisfy $φ χ_{V} \leq φ χ_{U}$ pointwise, so monotonicity in [F3] gives $\int_{V} φ d λ \leq \int_{U} φ d λ = 0$ , contradicting step 5.2; therefore no point $p \in U$ with $g (p) \neq 0$ exists and $g = 0$ on $U$ .

Depends on

Dependency tree · 2 levels

Sources

J. Figueroa-O'Farrill, Brief Notes on the Calculus of Variations (University of Edinburgh), §4 Theorem 1, printed pp. 4–5; §12 Theorem 4, printed p. 19; §14 compact-support reformulation, printed p. 23