LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

A partial signed projection limit has convergent penalty and energy

Statement

Assume AC and the full partially homogeneous hypotheses of the stationarity lemma: a separable real Hilbert space $H$ ; the feature-energy hypotheses with convex differentiable $R : H \to [0, \infty)$ whose differential is locally Lipschitz on bounded subsets and bounded on sublevels; $d \geq 2$ ; bounded continuously differentiable maps $φ : Θ \to H$ and $\tilde{V} : Θ \to [0, \infty)$ with Lipschitz differentials; $Φ (w, θ) = w φ (θ)$ and the semiconvex potential $V (w, θ) = ∣ w ∣ \tilde{V} (θ)$ ; and the nested cutoff and derivative-growth conditions of the feature-energy definition. For every $f \in H$ , require dense regular values for $G_{f} (θ) = ⟨ f, φ (θ) ⟩ + \tilde{V} (θ)$ . Retain either (i) $Θ$ is the closure of a nonempty bounded connected open convex set with $C^{1}$ boundary and $d G_{f} (θ) [n_{θ}] = 0$ on $\partial Θ$ for every $f \in H$ , or (ii) $Θ = R^{d - 1}$ and, for every $f \in H$ , $G_{f} (r \cdot)$ converges uniformly in $C^{1} (S^{d - 2})$ as $r \to \infty$ to a function with dense regular values.

Let $μ_{t}$ be a Wasserstein gradient flow in $P_{2} (R \times Θ)$ with finite initial energy. Suppose the finite signed projections $σ_{t} = h^{1} (μ_{t})$ converge narrowly to a finite signed measure $ν$ , meaning convergence of integrals against every bounded continuous real test function on $Θ$ . Put $m_{ν} = \int φ d ν$ , with the intrinsic signed Bochner-integral convention, and $J (ν) = R (m_{ν}) + \int \tilde{V} d ∣ ν ∣$ . Then $\lim_{t \to \infty} \int ∣ w ∣ \tilde{V} (θ) d μ_{t} (w, θ) = \int \tilde{V} d ∣ ν ∣, \lim_{t \to \infty} F (μ_{t}) = J (ν) .$ No separation condition on the initial support is required.

Statement references

The Axiom of Choice

Feature-measure energy and its regularity assumptions

Wasserstein gradient flow for a feature-measure energy

Partially one-homogeneous signed measure projection

Relaxed objective for a partially one-homogeneous projection

Signed narrow convergence controls variation tails and Bochner moments

Partial feature flows have exact energy and weight-moment identities

Stationarity of a partially homogeneous signed projection limit

Chizat and Bach, Appendix C.4.2

Facts & Assumptions

Given: AC, the full partial hypotheses, the flow $μ_{t}$ , and narrow signed-projection convergence in the Statement.

[F1]

The intrinsic signed projection factors the feature moment: $m_{t} : = \int w φ (θ) d μ_{t} = \int φ d σ_{t}$ . The relaxed-objective inequality gives $P_{t} : = \int ∣ w ∣ \tilde{V} (θ) d μ_{t} \geq \int \tilde{V} d ∣ σ_{t} ∣$ . Partially one-homogeneous signed measure projection Relaxed objective for a partially one-homogeneous projection

[F2]

Narrow convergence of finite signed measures on a closed Euclidean domain gives norm convergence of their integrals against bounded norm-continuous Hilbert-valued maps. For bounded nonnegative continuous $W$ , it also gives $\int W d ∣ ν ∣ \leq {lim inf}_{t \to \infty} \int W d ∣ σ_{t} ∣$ . Signed narrow convergence controls variation tails and Bochner moments

[F3]

The energy is nonnegative and nonincreasing. With $f_{t} = \nabla R (m_{t})$ and $S (t) = \int w^{2} d μ_{t} \geq 0$ , the exact identity $S (t) - S (s) = - 2 \int_{s}^{t} (⟨ f_{q}, m_{q} ⟩ + P_{q}) d q$ holds for every finite $0 \leq s \leq t$ . Partial feature flows have exact energy and weight-moment identities

[F4]

Writing $a_{ν} (θ) = ⟨ \nabla R (m_{ν}), φ (θ) ⟩$ , signwise stationarity gives $a_{ν} + \tilde{V} = 0$ $ν^{+}$ -almost everywhere and $- a_{ν} + \tilde{V} = 0$ $ν^{-}$ -almost everywhere. Stationarity of a partially homogeneous signed projection limit

[A1]

The existing AC assumption supplies the choice hypotheses inherited from these suppliers. The Axiom of Choice

Proof

Given: The data in the Statement and [F1]–[F4].

1.1A1F1F2F3given

By [F1] and [F2], $m_{t} \to m_{ν}$ in Hilbert norm. Continuity of $R$ and local Lipschitz continuity of its differential imply $R (m_{t}) \to R (m_{ν})$ and $f_{t} \to f_{ν} : = \nabla R (m_{ν})$ in norm, hence $⟨ f_{t}, m_{t} ⟩ \to ⟨ f_{ν}, m_{ν} ⟩$ . By [F3], $F (μ_{t})$ decreases to a finite limit $E_{\infty} \geq 0$ . Since $F (μ_{t}) = R (m_{t}) + P_{t}$ , it follows that $P_{t} \to P_{\infty} : = E_{\infty} - R (m_{ν})$ .

2.1F1F2step 1.1

Put $P_{ν} = \int \tilde{V} d ∣ ν ∣$ . The static inequality [F1] and weighted-variation lower semicontinuity [F2], applied to the bounded nonnegative continuous function $\tilde{V}$ , give $P_{\infty} \geq {lim inf}_{t \to \infty} \int \tilde{V} d ∣ σ_{t} ∣ \geq P_{ν}$ . This does not require convergence of the separate raw sign measures or their Jordan parts.

3.1F1F4step 2.1

Integrate the two stationarity equalities [F4] against the respective finite Jordan parts. The intrinsic signed Bochner integral and $∣ ν ∣ = ν^{+} + ν^{-}$ give $⟨ f_{ν}, m_{ν} ⟩ = \int a_{ν} d ν^{+} - \int a_{ν} d ν^{-} = - \int \tilde{V} d ν^{+} - \int \tilde{V} d ν^{-} = - P_{ν}$ . All integrands are bounded, so these integrals are finite.

4.1F3step 1.1step 2.1step 3.1

If $P_{\infty} > P_{ν}$ , let $ϵ = (P_{\infty} - P_{ν}) / 2 > 0$ . Steps 1.1 and 3.1 imply that there is a finite $T$ such that $⟨ f_{q}, m_{q} ⟩ + P_{q} \geq ϵ$ for every $q \geq T$ . The all-endpoint moment identity [F3] then gives $S (t) \leq S (T) - 2 ϵ (t - T)$ for every finite $t \geq T$ . Choosing $t > T + S (T) / (2 ϵ)$ contradicts $S (t) \geq 0$ . Hence $P_{\infty} \leq P_{ν}$ , which together with step 2.1 yields $P_{\infty} = P_{ν}$ .

5.1F1step 1.1step 4.1∎

Therefore $P_{t} \to P_{ν}$ , and step 1.1 gives $F (μ_{t}) \to R (m_{ν}) + P_{ν} = J (ν)$ . These are the two asserted limits.

Source note

Appendix C.4.2 motivates the projected-limit energy claim. The convergence of the lifted penalty is proved here from signwise stationarity, signed norm-moment convergence and the exact weight-moment identity; continuity of the penalty as a function of the signed projection is not assumed.

Depends on

Used by

A partially homogeneous signed projection limit is a minimizer Theorem

Dependency tree · two levels

35 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

Lénaïc Chizat and Francis Bach, On the Global Convergence of Gradient Descent for Over-parameterized Models using Optimal Transport, Appendix C.4.2; local reconstruction of the penalty-convergence argument (standard reference, not scraped)