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.

First variation and optimality over nonnegative measures

Statement

Let $H$ be a real Hilbert space, let $Ω$ be the feature domain, and let $F (μ) = R (\int_{Ω} Φ d μ) + \int_{Ω} V d μ$ be finite on a finite nonnegative Borel measure $μ$ , with $R$ differentiable and convex. Define $G_{μ} (u) = d R_{m_{μ}} [Φ (u)] + V (u)$ , where $m_{μ} = \int_{Ω} Φ d μ$ . Then $μ$ minimizes $F$ over all finite nonnegative Borel measures if and only if $G_{μ} (u) \geq 0$ for every $u \in Ω$ and $G_{μ} (u) = 0$ for $μ$ -almost every $u$ .

Statement references

Feature-measure energy and its regularity assumptions

Bounded linear maps commute with Bochner integration

The Dirac set function at a point

Chizat and Bach, Proposition 3.1 and Appendix C.1

Ambrosio, Gigli, and Savaré, Chapter 10

Facts & Assumptions

Given: The feature-measure energy, a finite nonnegative measure $μ$ , and a differentiable convex risk $R$ . For the necessity direction assume $μ$ is a minimizer; for sufficiency assume $G_{μ} \geq 0$ everywhere and $G_{μ} = 0$ $μ$ -almost everywhere.

[F1]

For a finite nonnegative Borel measure $μ$ on $R^{d}$ , set $F (μ) = R (\int_{Ω} Φ (u) d μ (u)) + \int_{Ω} V (u) d μ (u)$ when $μ$ is concentrated on $Ω$ , the Bochner integral exists, and the scalar integral is finite; set $F (μ) = + \infty$ otherwise. Feature-measure energy and its regularity assumptions

[F2]

A bounded linear map commutes with Bochner integration on every measurable set: $T (\int_{E} f d μ) = \int_{E} T f d μ$ . Bounded linear maps commute with Bochner integration

[F3]

For $u \in Ω$ , the Dirac measure $δ_{u}$ is the Borel probability with $δ_{u} (A) = 1$ if $u \in A$ and $0$ otherwise. The Dirac set function at a point A Dirac set function is a probability measure

Proof

Given: $μ, R, Φ, V$ as in the Statement.

1.1givenF1F3choose

Fix $u \in Ω$ . For $t \geq 0$ , the measure $μ + t δ_{u}$ from [F3] is nonnegative and $F (μ + t δ_{u})$ is finite for sufficiently small $t$ . Its right derivative at $t = 0$ is $d R_{m_{μ}} [Φ (u)] + V (u) = G_{μ} (u)$ . If $μ$ minimizes $F$ , this derivative is nonnegative. Since $u$ was arbitrary, $G_{μ} \geq 0$ everywhere.

1.2givenF1F2algebra

For $t$ in a neighborhood of $0$ with $1 + t > 0$ , the measure $(1 + t) μ$ is admissible. Differentiating $F ((1 + t) μ)$ at $0$ gives $d R_{m_{μ}} [m_{μ}] + \int V d μ = \int G_{μ} d μ$ by [F2]. A minimum at the interior parameter $t = 0$ forces this derivative to be zero. Since $G_{μ}$ is nonnegative and integrable, $\int G_{μ} d μ = 0$ implies $G_{μ} = 0$ $μ$ -almost everywhere.

2.1givenF1F2algebra∎

For any finite-energy nonnegative $ν$ , convexity of $R$ gives $R (m_{ν}) \geq R (m_{μ}) + d R_{m_{μ}} [m_{ν} - m_{μ}]$ . By [F2], after adding the $V$ terms this is $F (ν) - F (μ) \geq \int G_{μ} d ν - \int G_{μ} d μ \geq 0$ , using the assumed nonnegativity and $μ$ -almost-everywhere vanishing of $G_{μ}$ . Infinite-energy competitors cannot lower $F$ , so $μ$ is a global minimizer.

Depends on

Used by

Dependency tree · two levels

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