ExampleConstruction: Literature-sourcedVerification: 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.

Mixture convexity does not imply displacement convexity

Example

Assume AC. Let $Ω = R$ , $H = R$ , $R (z) = z^{2}$ , $Φ (x) = \sin x$ , and $V (x) = 0$ , so $F (μ) = (\int \sin x d μ (x))^{2}$ for every finite nonnegative Borel measure. For each $r > 0$ , take $Q_{r} = [- r, r]$ and $C_{1} = C_{2} = 1$ ; the cutoff, boundedness, Lipschitz, and linear-growth assumptions hold. This energy is convex under linear mixtures of measures, but it is not displacement convex along $W_{2}$ geodesics: along the geodesic from $δ_{0}$ to $δ_{π}$ , its endpoint values are zero and its midpoint value is one.

Example references

Feature-measure energy and its regularity assumptions

Generalized W2 geodesics and strong Wasserstein subgradients

The Axiom of Choice

Chizat and Bach, Appendix B.2.1 and Theorem 2.6

Ambrosio, Gigli, and Savaré, Chapter 9

Facts & Assumptions

Given: The feature-energy data in the Example.

[F2]

The unique coupling of two Dirac probability measures is concentrated on their support-point pair, so their $W_{2}$ geodesic is the linear interpolation of those points. Generalized W2 geodesics and strong Wasserstein subgradients

Proof

Given: $F$ , $μ_{0}, μ_{1}$ , and AC as in the Example.

1.1givenalgebra

For $a, b \in R$ and $0 \leq t \leq 1$ , expansion gives $(1 - t) a^{2} + t b^{2} - ((1 - t) a + t b)^{2} = t (1 - t) (a - b)^{2} \geq 0$ . Thus the real square obeys the convexity inequality, including $t = 0, 1$ and $a = b$ , by core algebra alone.

2.1step 1.1algebra

For finite nonnegative measures $μ_{0}, μ_{1}$ , write $a = \int \sin x d μ_{0}$ and $b = \int \sin x d μ_{1}$ . Linearity of integration gives $F ((1 - t) μ_{0} + t μ_{1}) = ((1 - t) a + t b)^{2} \leq (1 - t) a^{2} + t b^{2} = (1 - t) F (μ_{0}) + t F (μ_{1})$ by step 1.1. Thus $F$ is mixture-convex.

3.1F2step 2.1given∎

For $μ_{0} = δ_{0}$ and $μ_{1} = δ_{π}$ , [F2] gives the geodesic $μ_{t} = δ_{π t}$ . Then $F (μ_{0}) = F (μ_{1}) = 0$ , whereas $F (μ_{1 / 2}) = \sin^{2} (π / 2) = 1$ . The convexity inequality at $t = 1 / 2$ would require $1 \leq 0$ , which is false. Hence mixture convexity does not imply displacement convexity.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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