LemmaStatement: Literature-sourcedProof: 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 multiplier vector is unique when the constraint gradients are independent

Statement

Assume the Axiom of Choice (The Axiom of Choice). In the setting of The Lagrange multiplier rule for finitely many regular constraints — a real Banach space $X$ (Banach space), open $U \subseteq X$ , and a $C^{1}$ map $G = (G_{1}, \dots, G_{m}) : U \to R^{m}$ with $D G (u) : X \to R^{m}$ surjective — if $λ, λ^{'} \in R^{m}$ satisfy $\sum_{i = 1}^{m} λ_{i} D G_{i} (u) = \sum_{i = 1}^{m} λ_{i}^{'} D G_{i} (u)$ in $X^{*}$ , then $λ = λ^{'}$ . Equivalently, the transpose $D G (u)^{*} : R^{m} \to X^{*}$ (The transpose of a bounded operator, Fréchet derivative between Banach spaces) is injective.

Facts & Assumptions

Given: The setting of the multiplier rule: a real Banach space $X$ , open $U \subseteq X$ , a $C^{1}$ map $G$ with $D G (u)$ surjective, and vectors $λ, λ^{'} \in R^{m}$ as in the statement.

[F1]

The Lagrange multiplier rule for finitely many regular constraints: under these hypotheses $D G (u)$ has components $D G_{i} (u) \in X^{*}$ , surjectivity is available exactly as in the multiplier rule, and multiples and sums of the component functionals are formed pointwise.

[F2]

Every natural-number-indexed list of nonempty sets has a choice function on its family of values: a finite family of nonempty sets indexed by a natural number admits a choice function.

[F3]

The transpose of a bounded operator, Fréchet derivative between Banach spaces: for a bounded linear operator $T : X \to R^{m}$ the transpose $T^{*} : (R^{m})^{*} \to X^{*}$ is defined by $T^{*} g = g \circ T$ ; under the identification of $(R^{m})^{*}$ with $R^{m}$ by the standard basis, $(D G (u)^{*} μ) (x) = \sum_{i} μ_{i} D G_{i} (u) x$ , so $D G (u)^{*} μ = 0$ if and only if $\sum_{i} μ_{i} D G_{i} (u)$ is the zero functional.

Proof

technique · direct

Given: The setting above and $λ, λ^{'} \in R^{m}$ with equal associated functionals.

1.1givenF1F2choosealgebra

Put $μ : = λ - λ^{'} \in R^{m}$ . Subtracting the two equal functionals gives $\sum_{i = 1}^{m} μ_{i} D G_{i} (u) = 0$ in $X^{*}$ [F1]. Since $D G (u)$ is surjective, for each $i$ the preimage $D G (u)^{- 1} ({e_{i}})$ is nonempty, and finite choice [F2] selects $x_{1}, \dots, x_{m} \in X$ with $D G (u) x_{i} = e_{i}$ , that is $D G_{j} (u) x_{i} = δ_{i j}$ . Evaluating the vanishing functional at $x_{j}$ gives $0 = \sum_{i} μ_{i} D G_{i} (u) x_{j} = μ_{j}$ , and this holds for every $j$ ; hence $μ = 0$ and $λ = λ^{'}$ .

2.1step 1.1F3

For the equivalent formulation, [F3] identifies $D G (u)^{*} μ \in X^{*}$ with $x \mapsto \sum_{i} μ_{i} D G_{i} (u) x$ . Consequently $D G (u)^{*} μ = 0$ holds exactly when $\sum_{i} μ_{i} D G_{i} (u)$ is the zero functional, which by the evaluation argument of step 1.1 forces $μ = 0$ ; so $D G (u)^{*} : R^{m} \to X^{*}$ is injective.

3.1step 1.1step 2.1∎

Step 1.1 proves the uniqueness of the multiplier vector and step 2.1 the equivalent statement that the transpose of the surjective derivative is injective; this records the independence boundary case in which the surjectivity hypothesis of the multiplier rule cannot be dropped.

Depends on

Used by

Dependent equality constraints have nonunique multiplier vectors Counterexample

Dependency tree · two levels

24 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)
Riccardo Cristoferi, Calculus of Variations: Lecture Notes, Carnegie Mellon University 2016 (complete 133-page notes) (standard reference, not scraped)