LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Quadratic path energy is lower semicontinuous

Statement

Assume AC. Let $T > 0$ and give $C ([0, T]; R^{d})$ the uniform topology. Define $E (γ) = {\begin{cases} \int_{0}^{T} ∣ \dot{γ} (t) ∣^{2} d t, & γ is absolutely continuous with \dot{γ} \in L^{2} (0, T; R^{d}), \\ + \infty, & otherwise. \end{cases}$ Then $E$ is lower semicontinuous. More precisely, $E (γ) = \sup_{0 = t_{0} < \dots < t_{N} = T} \sum_{i = 0}^{N - 1} \frac{∣ γ (t_{i + 1}) - γ (t_{i}) ∣^{2}}{t_{i + 1} - t_{i}},$ where the supremum is over all finite partitions of $[0, T]$ .

Statement references

The Axiom of Choice

AC implies DC implies countable choice

The Axiom of Countable Choice ( ${A C}_{ω}$ )

The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain

C_c(X) is dense in L^p(mu) for a Radon measure

Radon measure on an LCH space

Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$

Riesz representation for Hilbert spaces

The indefinite integral of an $L^{1}$ function is differentiable almost everywhere

Minkowski's integral inequality

Ambrosio, Gigli, and Savaré, Gradient Flows, Chapter 8, §8.2

Santambrogio, Optimal Transport for Applied Mathematicians, Chapter 5, §5.3

Facts & Assumptions

Given: AC, $T > 0$ , and a continuous path $γ : [0, T] \to R^{d}$ .

[F1]

Under DC, continuous compactly supported functions are dense in $L^{2} (0, T)$ for Lebesgue measure; uniform continuity approximates each continuous function uniformly by interval-step functions. C_c(X) is dense in L^p(mu) for a Radon measure Radon measure on an LCH space The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain

[F2]

The real Hilbert space $L^{2} (0, T; R^{d})$ is complete and bounded linear functionals on it have unique Riesz representatives under Countable Choice. Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$ Riesz representation for Hilbert spaces The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F3]

AC supplies Countable and Dependent Choice for [F1]–[F2] and the scalar Lebesgue FTC. The Axiom of Choice AC implies DC implies countable choice The Axiom of Countable Choice ( ${A C}_{ω}$ ) The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain The indefinite integral of an $L^{1}$ function is differentiable almost everywhere

[F4]

Cauchy--Schwarz holds for finite sums. Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs

Proof

1.1givenF4algebra

For a partition $P = (t_{i})_{i = 0}^{N}$ , write $Q_{P} (γ) = \sum_{i} ∣ γ (t_{i + 1}) - γ (t_{i}) ∣^{2} / (t_{i + 1} - t_{i})$ and set $C = \sup_{P} Q_{P} (γ)$ . If $γ$ is absolutely continuous with square-integrable derivative, Cauchy--Schwarz [F4] on each interval gives $Q_{P} (γ) \leq \int_{0}^{T} ∣ \dot{γ} ∣^{2} d t$ .

2.1F1givenstep 1.1

Suppose $C < \infty$ . On interval-step functions $f (t) = c_{i}$ for $t_{i} < t < t_{i + 1}$ define $Λ (f) = \sum_{i} c_{i} \cdot (γ (t_{i + 1}) - γ (t_{i}))$ . Refinement leaves this value unchanged, so the functional is well-defined. Cauchy--Schwarz for the finite sums gives $∣ Λ (f) ∣ \leq {(\sum_{i} ∣ c_{i} ∣^{2} Δ t_{i})}^{1 / 2} Q_{P} (γ)^{1 / 2} \leq \sqrt{C} ∥ f ∥_{L^{2}} .$ By [F1], interval-step functions are dense in $L^{2}$ , so $Λ$ extends uniquely to a bounded linear functional on the real Hilbert space $L^{2} (0, T; R^{d})$ .

3.1F2F3step 2.1

By [F2]–[F3], Riesz represents $Λ$ by some $u \in L^{2} (0, T; R^{d})$ . Taking the step function equal to a fixed vector c on $(s, t)$ and zero elsewhere gives $c \cdot (γ (t) - γ (s)) = \int_{s}^{t} c \cdot u (r) d r$ for every $c$ and every interval. Hence $γ (t) - γ (s) = \int_{s}^{t} u (r) d r$ . The scalar FTC [F3] coordinatewise shows that $γ$ is absolutely continuous and $\dot{γ} = u$ almost everywhere. Thus $E (γ) < \infty$ .

4.1F1step 1.1step 2.1step 3.1∎

For this absolutely continuous path, the functional $Λ$ is integration against $\dot{γ}$ on interval-step functions. Since those functions are dense, its norm is $∥ \dot{γ} ∥_{L^{2}}$ ; for each fixed partition the squared norm of the restriction of $Λ$ to step functions constant on its intervals is exactly $Q_{P} (γ)$ . Taking the supremum over partitions therefore gives $C = ∥ \dot{γ} ∥_{L^{2}}^{2} = E (γ)$ . Conversely, steps 2.1–3.1 prove that finite C forces finite energy, so if $E (γ) = + \infty$ then C is also infinite. Each $Q_{P}$ is continuous in the uniform topology because it uses finitely many point evaluations; their supremum is lower semicontinuous.

Depends on

Used by

Superposition for finite-action Euclidean continuity equations Theorem

Dependency tree · two levels

57 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, Chapter 8, §8.2 (standard reference, not scraped)
Filippo Santambrogio, Optimal Transport for Applied Mathematicians, Chapter 5, §5.3 (standard reference, not scraped)