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.

The localized lifted feature energy is semiconvex

Statement

Assume AC and the hypotheses of the feature-measure energy definition. Fix an arbitrary probability label space $(S, Σ, σ)$ , let $K = L^{2} (σ; R^{d})$ , and let $C_{r} = {X : X (s) \in Q_{r} for σ -almost every s}$ . Write $A_{r} = \sup_{Q_{r}} ∥ d Φ ∥$ , $B_{r} = {Lip}_{Q_{r}} (d Φ)$ , $M_{r} = \sup_{Q_{r}} ∥ \partial V ∥$ , and let $L_{r}$ and $N_{r}$ be, respectively, a Lipschitz constant and a norm bound for $d R$ on the closed convex hull of $Φ (Q_{r})$ . For all $X, Y \in C_{r}$ , the smooth part $G_{r} (X) = R (\int Φ (X) d σ)$ has the first-order expansion on $C_{r}$ with gradient $\nabla G_{r} (X) (s) = d Φ_{X (s)}^{*} \nabla R (\int Φ (X) d σ)$ , and this gradient is Lipschitz with constant $L_{r} A_{r}^{2} + N_{r} B_{r}$ . No separability of the label space is required for these estimates. Consequently $E_{r} (X) = G_{r} (X) + \int V (X) d σ + ι_{C_{r}} (X)$ is $(λ_{V} - L_{r} A_{r}^{2} - N_{r} B_{r})$ -semiconvex on $K$ .

Statement references

Feature-measure energy and its regularity assumptions

Localized Hilbert lift of the feature energy

Chizat and Bach, Appendix B.2.1

Facts & Assumptions

Given: AC, $σ, Q_{r}, Φ, R, V$ and the constants in the Statement.

[F1]

Bounded linear maps commute with Bochner integration, and Bochner integrability is characterized by strong measurability plus integrability of the norm. Bounded linear maps commute with Bochner integration Bochner integrability criterion Bochner-integrable function

[F2]

The differential of $R$ has a unique Hilbert gradient with the same norm. Riesz representation for Hilbert spaces

[F3]

The feature map is differentiable, $d Φ$ is bounded and Lipschitz on $Q_{r}$ , and $d R$ is Lipschitz on bounded sets; on the relevant bounded convex hull its norm has some finite bound. Feature-measure energy and its regularity assumptions

[F6]

On every segment in $Q_{r}$ , semiconvexity of $V$ means $V (u) - (λ_{V} / 2) ∣ u ∣^{2}$ is convex. Feature-measure energy and its regularity assumptions

[F4]

AC supplies Countable Choice for the Bochner approximation and Riesz branches. The Axiom of Choice AC implies DC implies countable choice The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F5]

Cauchy–Schwarz controls integrals and the $L^{2} (σ)$ norm. Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs

Proof

Given: AC and the data above.

1.1F1F3F4F5construct

For $X, Y \in C_{r}$ , the segment $X_{θ} = X + θ (Y - X)$ lies in $C_{r}$ by convexity of $Q_{r}$ . Pointwise Fréchet differentiability and the bound $A_{r}$ give $∥ Φ (Y) - Φ (X) ∥_{L^{2} (σ; H)} \leq A_{r} ∥ Y - X ∥_{K}$ ; moreover Lipschitz continuity of $d Φ$ gives the pointwise remainder bound $∥ Φ (Y) - Φ (X) - d Φ_{X} (Y - X) ∥_{H} \leq (B_{r} / 2) ∣ Y - X ∣^{2}$ . Integrating this bound and using [F1], [F4], and [F5] proves $m (Y) = m (X) + \int d Φ_{X} (Y - X) d σ + O (∥ Y - X ∥_{K}^{2})$ , the required first-order expansion on $C_{r}$ .

2.1F1F2F3step 1.1

Write $m (Y) - m (X) = D m (X) [Y - X] + O (∥ Y - X ∥_{K}^{2})$ as in step 1.1. Fréchet differentiability of $R$ at $m (X)$ gives $R (m (Y)) = R (m (X)) + d R_{m (X)} [m (Y) - m (X)] + o (∥ m (Y) - m (X) ∥_{H})$ . By [F2] represent $d R_{m (X)}$ by its Riesz vector $\nabla R (m (X))$ . The bounded-linear-map commutation in [F1] then gives $D G_{r} (X) [H] = ⟨ \nabla R (m (X)), D m (X) [H] ⟩_{H} = ⟨ d Φ_{X (\cdot)}^{*} \nabla R (m (X)), H ⟩_{K} .$ The pointwise gradient is measurable by continuity of $d Φ$ on $Q_{r}$ and has $K$ -norm at most $N_{r} A_{r}$ .

3.1F3F5step 2.1

For $X, Y \in C_{r}$ , [F3] and [F5] give $∥ m (X) - m (Y) ∥_{H} \leq A_{r} ∥ X - Y ∥_{K}$ . Add and subtract $d Φ_{X}^{*} \nabla R (m (Y))$ in the gradient difference. The operator norm bounds yield $∥ \nabla G_{r} (X) - \nabla G_{r} (Y) ∥_{K} \leq A_{r} L_{r} ∥ m (X) - m (Y) ∥ + N_{r} B_{r} ∥ X - Y ∥_{K} \leq (L_{r} A_{r}^{2} + N_{r} B_{r}) ∥ X - Y ∥_{K} .$ Every term is finite by [F1] and [F3].

4.1F3F6step 3.1∎

Integrating the gradient along $X_{θ}$ and using step 3.1 gives $G_{r} (Y) \geq G_{r} (X) + ⟨ \nabla G_{r} (X), Y - X ⟩_{K} - \frac{L_{r} A_{r}^{2} + N_{r} B_{r}}{2} ∥ Y - X ∥_{K}^{2} .$ The pointwise $λ_{V}$ -semiconvex inequality [F6], integrated against $σ$ , gives the same inequality for $X \mapsto \int V (X) d σ$ with coefficient $λ_{V}$ . Adding the two inequalities and restricting to the convex set $C_{r}$ proves the claimed semiconvexity of $E_{r}$ .

Depends on

Used by

Dependency tree · two levels

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