LemmaStatement: Literature-sourcedProof: 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.

Feature energy is W2-continuous on a common cutoff

Statement

Assume the feature-energy hypotheses on a closed convex set $Q_{r} \subseteq Ω$ , and let $μ_{n}, μ \in P_{2} (R^{d})$ be concentrated on $Q_{r}$ , with finite feature energy and $W_{2} (μ_{n}, μ) \to 0$ . Then $F (μ_{n}) \to F (μ)$ .

Statement references

Feature-measure energy and its regularity assumptions

The Euclidean quadratic Wasserstein space

Bounded linear maps commute with Bochner integration

Chizat and Bach, Lemma A.1

Ambrosio, Gigli, and Savaré, Chapter 8

Facts & Assumptions

Given: The measures and cutoff in the Statement.

[F1]

On $Q_{r}$ , $d Φ$ is Lipschitz and uniformly bounded by the stated linear growth bound. At every $x \in Q_{r}$ there is also a supporting vector $ξ_{x} \in \partial_{λ_{V}} V (x)$ with $∣ ξ_{x} ∣ \leq C_{1} + C_{2} r$ ; the definition requires this bounded selection rather than a bound on the full relative-domain subdifferential. Feature-measure energy and its regularity assumptions

[F2]

$W_{2} (μ_{n}, μ)^{2}$ is the infimum of $\int ∣ x - y ∣^{2} d π$ over all Borel couplings $π$ of $μ_{n}, μ$ . The Euclidean quadratic Wasserstein space

[F3]

The coupling marginals are the pushforwards of $π$ under its coordinate projections, so the scalar integral identity holds first for simple functions and then by approximation. For the Bochner feature moments, apply each bounded linear functional, use its commutation with Bochner integration, and use equality of all evaluations to identify the vectors. The Euclidean quadratic Wasserstein space Bounded linear maps commute with Bochner integration

Proof

Given: The data in the Statement.

1.1F1givenalgebra

For $x, y \in Q_{r}$ , the segment between them lies in $Q_{r}$ . The bound on $d Φ$ and the fundamental theorem of calculus on this segment give $∥ Φ (x) - Φ (y) ∥ \leq L_{Φ} ∣ x - y ∣$ . For $V$ , divide the segment into $N$ equal pieces. The two $λ_{V}$ -support inequalities at consecutive endpoints and the uniform bound $M_{V}$ on subgradients yield $∣ V (x_{j + 1}) - V (x_{j}) ∣ \leq M_{V} ∣ x - y ∣ / N + ∣ λ_{V} ∣ ∣ x - y ∣^{2} / (2 N^{2})$ . Summing and letting $N \to \infty$ gives $∣ V (x) - V (y) ∣ \leq M_{V} ∣ x - y ∣$ .

2.1F1F2F3step 1.1algebra∎

For any coupling $π \in Γ (μ_{n}, μ)$ , [F3] and [F1] give $∥ \int Φ d μ_{n} - \int Φ d μ ∥ \leq L_{Φ} \int ∣ x - y ∣ d π \leq L_{Φ} (\int ∣ x - y ∣^{2} d π)^{1 / 2}$ . The same coupling gives $∣ \int V d μ_{n} - \int V d μ ∣ \leq M_{V} (\int ∣ x - y ∣^{2} d π)^{1 / 2}$ . Taking the infimum over couplings and using [F2] makes both differences tend to zero. Continuity of $R$ then gives $F (μ_{n}) \to F (μ)$ .

Depends on

Used by

Particle number and training time limits interchange qualitatively Theorem

Dependency tree · two levels

17 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 (standard reference, not scraped)
Luigi Ambrosio, Nicola Gigli, and Giuseppe Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures (standard reference, not scraped)