TheoremStatement: 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 Lagrange multiplier rule for one regular constraint in Hilbert space

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $H$ be a real Hilbert space (Hilbert space), let $U \subseteq H$ be open, let $I : U \to R$ be Fréchet differentiable at $u \in U$ , and let $G : U \to R$ be of class $C^{1}$ with $D G (u) \neq 0$ (Fréchet derivative between Banach spaces). If $u$ is a local minimiser or a local maximiser of $I$ on the level set ${G = G (u)}$ , then there is a unique $λ \in R$ with $D I (u) = λ D G (u) .$

Facts & Assumptions

Given: A real Hilbert space $H$ , open $U \subseteq H$ , a functional $I$ Fréchet differentiable at $u$ , a $C^{1}$ function $G$ with $D G (u) \neq 0$ , and the assumption that $u$ is a local minimiser or local maximiser of $I$ on the level set ${G = G (u)}$ .

[F1]

The differential annihilates the tangent kernel at a constrained extremum: under these hypotheses $D I (u) h = 0$ for every $h \in \ker D G (u)$ , and the same conclusion is obtained from the constrained-extremum lemma applied with the single constraint $G$ (the level set and $C^{1}$ hypotheses are exactly those of that lemma with $m = 1$ , whose derivative $D G (u) \neq 0$ is surjective onto $R$ ).

[F2]

Functionals vanishing on a common kernel are combinations of an independent family: if $ψ \neq 0$ is a bounded linear functional on $H$ with $\ker ψ \subseteq \ker φ$ for some bounded linear functional $φ$ , then $φ = λ ψ$ for a unique $λ \in R$ ; this is the $m = 1$ clause of that lemma.

[F3]

Fréchet derivative between Banach spaces, Hilbert space: $D I (u)$ and $D G (u)$ are bounded linear functionals on $H$ (the derivative of a $C^{1}$ function into $R$ ), and $D G (u) \neq 0$ means that $D G (u)$ is not the zero functional.

[A1]

The Axiom of Choice: recorded as in the statement and consumed only through [F1].

Proof

technique · direct

Given: The hypotheses above, including the local extremum at $u$ and $D G (u) \neq 0$ .

1.1givenA1F1F3

Since $D G (u) : H \to R$ is a nonzero bounded linear functional, it is surjective, so the constrained-extremum lemma [F1] applies with the single constraint $G$ : the differential $D I (u)$ vanishes on $\ker D G (u)$ .

2.1step 1.1F2F3

The functionals $ψ : = D G (u) \neq 0$ and $φ : = D I (u)$ satisfy $\ker ψ = \ker D G (u) \subseteq \ker D I (u) = \ker φ$ by step 1.1, so the $m = 1$ clause of [F2] gives a unique $λ \in R$ with $D I (u) = λ D G (u)$ .

3.1step 2.1A1∎

This is the asserted multiplier identity with its uniqueness clause; the Hilbert structure is used only through the standing conventions of the page, the argument being valid in any real Banach space [A1].

Depends on

Used by

Dependency tree · two levels

26 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)