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.
Translation of a Dirac mass
Example
Assume AC. Let be an integer, , and . The curve belongs to , has constant metric speed , and the Borel field solves the continuity equation. Its action is , equal to the minimum action among fields solving that equation for this curve.
Example references
The Euclidean quadratic Wasserstein space
The quadratic Wasserstein distance is a metric
Finite-action continuity equation in Euclidean space
AC2 curves admit a unique minimum-action velocity field
The Dirac set function at a point
The chain rule for total derivatives:
The second fundamental theorem: if is differentiable on with and is integrable, then
Ambrosio, Gigli, and Savaré, Gradient Flows, Theorem 8.3.1
Santambrogio, Optimal Transport for Applied Mathematicians, Chapter 5, §5.3
Facts & Assumptions
Given: AC, an integer , , and .
A coupling of two Dirac laws is forced to put all mass at the sole pair of support points, so the quadratic Wasserstein distance is . The Euclidean quadratic Wasserstein space The Dirac set function at a point
For a continuously differentiable scalar function, the total-derivative chain rule and fundamental theorem identify the integral of its derivative with its endpoint difference. The chain rule for total derivatives: The second fundamental theorem: if is differentiable on with and is integrable, then
The minimum-velocity theorem says the least action of any admissible velocity for an curve is the integral of its squared metric speed. AC2 curves admit a unique minimum-action velocity field
Proof
For , any coupling of and is concentrated at , hence [F1] gives . For every bounded continuous f, is continuous, so the curve is narrowly continuous. Thus it is with constant metric derivative (the endpoint difference quotient is exactly at every interior time).
For , the chain rule gives The left side integrates to zero over because the test vanishes near both time endpoints; this is exactly the weak continuity-equation identity for and . Its action is . By [F3] and step 1.1, this equals , the minimum action.
Depends on
- The Euclidean quadratic Wasserstein space
- The quadratic Wasserstein distance is a metric
- Finite-action continuity equation in Euclidean space
- AC2 curves admit a unique minimum-action velocity field
- The Dirac set function at a point
- The Axiom of Choice
- The chain rule for total derivatives: $D(g\circ f)(a)=Dg(f(a))\circ Df(a)$
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
58 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
- Luigi Ambrosio, Nicola Gigli, and Giuseppe Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, Theorem 8.3.1 (standard reference, not scraped)
- Filippo Santambrogio, Optimal Transport for Applied Mathematicians, Chapter 5, §5.3 (standard reference, not scraped)