TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)verified 2026-10-22 (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.

Existence of a global nonlinear Tikhonov minimizer

Statement

Assume the ultrafilter lemma, dependent choice, and the real Hahn–Banach dominated-extension principle. Let $X, Y$ be real Hilbert spaces, let $D \subseteq X$ be nonempty and weakly closed, and let $F : D \to Y$ be a map such that for every sequence $(x_{n})$ in $D$ and every $x \in X, z \in Y$ , $x_{n} ⇀ x$ and $F (x_{n}) ⇀ z$ imply $x \in D$ and $F (x) = z$ . Here $D$ is closed in the coarsest topology making every bounded real-linear functional continuous, and weak convergence means convergence under every such functional. For any $α > 0$ , $x_{0} \in X$ , and $y \in Y$ , the nonlinear Tikhonov functional

J_{α, y, x_{0}} (x) = \frac{1}{2} ∥ F (x) - y ∥_{Y}^{2} + \frac{α}{2} ∥ x - x_{0} ∥_{X}^{2} (x \in D)

attains a global minimum on $D$ ; that is, there exists $x_{α} \in D$ such that $J_{α, y, x_{0}} (x_{α}) \leq J_{α, y, x_{0}} (x)$ for every $x \in D$ . No exact solution of $F (x) = y$ is required.

Statement references

Weakly closed domains and sequential weak-to-weak graph closure

The Tikhonov functional and global minimizer

Christian Clason, Regularization of Inverse Problems, Theorem 10.1

Benedikt Wirth, Inverse Problems, Theorem 85(a)

Facts & Assumptions

Given: The ultrafilter lemma, dependent choice, and HB; real Hilbert spaces $X, Y$ ; a nonempty weakly closed domain $D \subseteq X$ ; a map $F : D \to Y$ with sequentially weak-to-weak closed graph; $α > 0$ , $x_{0} \in X$ , and $y \in Y$ .

[A1]

The ultrafilter lemma says every filter on a set extends to an ultrafilter (The ultrafilter extension principle (UL/BPI)).

[A2]

Dependent choice supplies an infinite sequence following any everywhere-extendible relation (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[A3]

HB is the real dominated-extension principle for linear functionals (The real dominated-extension principle as an additional hypothesis over ZF).

[F1]

DC implies countable choice, the principle that every countable family of nonempty sets admits a choice function (Dependent choice implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

Under countable choice, every complete real inner-product space is reflexive (Hilbert spaces are reflexive by Riesz representation).

[F3]

Under the ultrafilter lemma, DC, and HB, every bounded sequence in a real reflexive Banach space has a weakly convergent subsequence (A bounded sequence in a reflexive Banach space has a weakly convergent subsequence).

[F4]

Under HB, weak convergence implies lower semicontinuity of the norm (Weak convergence implies lower semicontinuity of the norm).

[F5]

Every nonempty real set bounded below has an infimum, and if $m = \inf S$ , then for every $ε > 0$ some $s \in S$ satisfies $s < m + ε$ (Greatest lower bound (infimum), Every nonempty set bounded below has an infimum, Epsilon characterisation of the infimum).

[F6]

The objective is the finite nonnegative sum $J_{α, y, x_{0}} (x) = \frac{1}{2} ∥ F (x) - y ∥_{Y}^{2} + \frac{α}{2} ∥ x - x_{0} ∥_{X}^{2}$ on $D$ (The nonlinear Tikhonov functional).

[F7]

Sequential graph closure identifies a joint weak limit: if $x_{n} \in D$ , $x_{n} ⇀ x$ , and $F (x_{n}) ⇀ z$ , then $x \in D$ and $F (x) = z$ (Weakly closed nonlinear forward maps on Hilbert spaces).

Proof

1.1givenF5

Let $m : = \inf {J_{α, y, x_{0}} (x) : x \in D}$ . The set of objective values is nonempty because $D \neq \emptyset$ , is bounded below by $0$ , and contains a finite value. Thus $m$ is a finite real number by [F5].

2.1A2F1F5step 1.1choose

For each $n \geq 1$ , [F5] gives $x_{n} \in D$ with $m \leq J_{α, y, x_{0}} (x_{n}) < m + 1 / n$ . Since DC implies countable choice by [F1], choose these points as a sequence; then $J_{α, y, x_{0}} (x_{n}) \to m$ .

3.1givenF6step 2.1algebra

The sequence of objective values is bounded above, say by $M > 0$ . Nonnegativity of both summands in [F6] and $α > 0$ give $∥ F (x_{n}) - y ∥_{Y}^{2} \leq 2 M$ and $∥ x_{n} - x_{0} ∥_{X}^{2} \leq 2 M / α$ . The triangle inequality then bounds $(x_{n})$ , and the first estimate together with fixed $y$ bounds $(F (x_{n}))$ .

4.1A1A2A3F1F2F3step 3.1construct

By [F2], $X$ and $Y$ are real reflexive Banach spaces: they are complete inner-product spaces, and DC supplies the countable choice assumed in [F2] by [F1]. Apply [F3] to the bounded sequence $(x_{n})$ to obtain a subsequence $x_{n_{k}} ⇀ x$ ; apply [F3] in $Y$ to the bounded sequence $(F (x_{n_{k}}))$ and pass to a further subsequence so that $F (x_{n_{k}}) ⇀ z$ . The further subsequence still has $x_{n_{k}} ⇀ x$ .

5.1F7step 4.1

By [F7], $x \in D$ and $F (x) = z$ . Subtracting the fixed vector $y$ preserves weak convergence, so $F (x_{n_{k}}) - y ⇀ F (x) - y$ , while $x_{n_{k}} - x_{0} ⇀ x - x_{0}$ .

6.1A3F4F5F6step 2.1step 5.1algebra∎

Apply [F4] to the two weakly convergent sequences in step 5.1. The maps $r \mapsto r^{2} / 2$ and $r \mapsto α r^{2} / 2$ are increasing and continuous on $[0, \infty)$ , so each squared-norm term is lower semicontinuous. If their limit values are $a : = \frac{1}{2} ∥ F (x) - y ∥_{Y}^{2}$ and $b : = \frac{α}{2} ∥ x - x_{0} ∥_{X}^{2}$ , then for every $ε > 0$ each sequence term is eventually at least its limit value minus $ε / 2$ ; taking the larger of the two eventual indices gives $J_{α, y, x_{0}} (x_{n_{k}}) \geq a + b - ε$ . Thus $J_{α, y, x_{0}} (x) \leq {lim inf}_{k} J_{α, y, x_{0}} (x_{n_{k}}) = m$ . Since $x \in D$ , the definition of $m$ gives $m \leq J_{α, y, x_{0}} (x)$ , so equality holds and $x$ is a global minimizer.

Remarks

The theorem guarantees global minimizers, not uniqueness. The sequential weak-to-weak graph condition is needed to identify the weak limit of the data sequence; weak-to-strong closedness alone would not identify a merely weak data limit. The direct method makes no claim that a numerical algorithm finds a global minimizer; nonlinear objectives may also have local minima.

Depends on

Used by

Dependency tree · two levels

57 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

Christian Clason, Regularization of Inverse Problems, Theorem 10.1 (standard reference, not scraped)
Benedikt Wirth, Inverse Problems, Theorem 85(a) (standard reference, not scraped)