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.
Primal compactness and selection of a minimum-TV limit
Statement
Assume Countable Choice. Let and let be real Hilbert spaces. Let be bounded and real-linear, let , and assume is an exact solution minimizing a proper, convex, lower semicontinuous, positively one-homogeneous TV functional with a source certificate , so . Use full-space if ; for a nonempty bounded connected Lipschitz , use either Neumann or Dirichlet for the zero extension , assigning outside the respective finite-variation domain. A bounded connected Lipschitz domain here is a nonempty bounded open set with a finite Lipschitz graph cover of its boundary, with the domain on one side of each graph, and with no separation into two disjoint nonempty relatively open sets.
Let tend to zero, let , and suppose for some finite . For each , suppose a supplied global minimizer minimizes In the Neumann case, if , take after subtracting its mean ; this leaves unchanged. Then a subsequence converges weakly in and, in addition, strongly in when is bounded or strongly in on every bounded ball when . Its limit is an exact solution minimizing among exact solutions, and .
Statement references
Facts & Assumptions
Given: The objects and hypotheses in the Statement, including supplied global minimizers of .
Countable Choice supplies the countable diagonal selections in the compactness and weak-subsequence arguments. (The Axiom of Countable Choice ())
Dual source certificates for TV regularization: , is minimal over exact solutions, and ; the Hilbert adjoint satisfies .
Dual attainment and convergence of TV source certificates: every supplied global minimizer has , the exact-data fields remain bounded as , and .
Compactness and lower semicontinuity for bounded-domain BV: bounded-domain BV sequences with bounded norm and variation have an -convergent subsequence, and TV is lower semicontinuous under convergence.
BV Sobolev inequality in full space: in two dimensions, for .
Full-space BV Sobolev inequality for L² distributional TV: the same estimate holds for with finite extended variation: .
A zero distributional gradient is constant on a connected domain: a locally integrable function with zero distributional gradient on a connected open domain is a.e. constant.
Full-space, Dirichlet, and Neumann TV conventions: Neumann TV is unchanged by adding constants; Dirichlet TV is the full-space TV of the zero extension and dominates the interior variation.
Test-field formula and L1 lower semicontinuity of spatial TV: spatial TV is lower semicontinuous in and finite whenever the extended test-field variation is finite under Countable Choice.
Finite L² distributional variation has a finite Radon derivative: finite gives a finite vector Radon derivative measure, whose restriction to bounded balls has variation at most .
Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence: bounded scalar real sequences have convergent subsequences.
Riesz representation for Hilbert spaces: bounded linear functionals on a real Hilbert space are inner products with vectors in that space.
Locally integrable functions embed in distributions: two locally integrable functions that define the same distribution are equal almost everywhere.
BV Sobolev–Poincaré inequality for Neumann TV: on a bounded connected Lipschitz domain, for a fixed finite .
Proof
If , the adjoint identity implies and . Since is exact, minimality gives . The data term of is then constant, so every global minimizer has . In the full-space case [F6] makes constant and forces it to be zero; in the Dirichlet case apply [F6] to its zero extension, which vanishes outside bounded , and again obtain zero; in the Neumann case [F6] makes it constant and the prescribed zero-mean choice makes it zero. Thus is an exact minimum-TV solution. Since and , , so and the assertion holds. For the remainder assume .
Put . By [F2], and is bounded. The noise hypothesis gives , hence [F2] makes bounded and . The identity therefore gives strongly in . Comparing the objective at and gives so . In particular the variations are bounded and .
In the Neumann branch on bounded connected , write and . The Poincaré inequality [F14] gives , which is uniformly bounded by step 1.2.
If , subtracting leaves both and Neumann TV unchanged, so we use the zero-mean minimizer specified in the Statement, which is uniformly bounded in by step 2.1. If , then [F1] and step 1.2 give bounded and so the means, and therefore , are bounded. In the full-space case [F5] gives . In the Dirichlet case [F4] applied to gives . Thus in every branch the selected sequence is bounded in .
If is bounded, the bound gives an bound by [F11]; the interior variation is bounded by in both boundary conventions [F7]. [F3] therefore supplies a subsequence converging strongly in . If , restrict to each ball : the norms are bounded by , and [F9] bounds the variation there. Applying [F3] on each ball and taking a countable diagonal subsequence using [A1] gives convergence in on every bounded ball.
The resulting sequence is still bounded in the Hilbert space . Its closed linear span is separable, since rational finite linear combinations of its terms are dense. Gram–Schmidt gives a finite or countable orthonormal family with dense span. Each coordinate sequence is bounded by [F11]; repeated use of [F10] and [A1] yields a subsubsequence on which every coordinate converges. Pythagoras applied to each finite orthogonal projection bounds the sums of squared limiting coordinates by the common squared norm bound, so these coordinates define a vector in the closed span. Approximation by finite linear combinations proves convergence of inner products against every vector in the span. For any , [F12] represents restricted to that span by a vector in the span, so the convergence is weak in all of . Testing against compactly supported smooth functions shows that this weak limit and the strong or local- limit from step 4.1 define the same distribution; injectivity [F13] makes them equal almost everywhere.
Weak convergence and boundedness of imply , while step 1.2 gives strongly; hence . In the full-space case, for every admissible test field , local convergence gives ; taking the supremum gives . In the Neumann case the same lower semicontinuity follows from [F8] and strong convergence. In the Dirichlet case the zero extensions converge strongly in , so [F8] gives the same inequality for their full-space TV. Thus . Exactness and the minimum property of force equality, so is a minimum-TV exact solution.
Let . Since , the adjoint identity in [F1] gives . For every , the subgradient inequality at therefore gives This is exactly , as required.
Depends on
- Dual source certificates for TV regularization
- Spatial BV and distributional total variation
- Full-space, Dirichlet, and Neumann TV conventions
- Distributional TV as an extended functional on L²
- Dual attainment and convergence of TV source certificates
- Compactness and lower semicontinuity for bounded-domain BV
- BV Sobolev inequality in full space
- Test-field formula and L1 lower semicontinuity of spatial TV
- A zero distributional gradient is constant on a connected domain
- BV Sobolev–Poincaré inequality for Neumann TV
- Finite L² distributional variation has a finite Radon derivative
- Full-space BV Sobolev inequality for L² distributional TV
- Bolzano-Weierstrass: every bounded real sequence has a convergent subsequence
- Cauchy–Schwarz: $|\langle x,y\rangle|\le\|x\|\,\|y\|$, with equality exactly for dependent pairs
- Riesz representation for Hilbert spaces
- Locally integrable functions embed in distributions
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Dependency tree · two levels
79 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
- José A. Iglesias, Gwenael Mercier, and Otmar Scherzer, A note on convergence of solutions of total variation regularized linear inverse problems, Lemma 1 and proof (standard reference, not scraped)
- Gláucio Terra, Introduction to Geometric Measure Theory — Lecture Notes, version 1.6 (standard reference, not scraped)