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.

A Euclidean probability label space gives a separable Hilbert L2 space

Statement

Assume the Axiom of Choice. Let $(S, Σ, σ)$ be any probability space and let $d \geq 1$ . Set $K = L^{2} (σ; R^{d})$ be the space of measurable vector fields modulo equality $σ$ -almost everywhere with finite squared norm. With $⟨ X, Y ⟩_{K} = \int_{S} X (s) \cdot Y (s) d σ (s), ∥ X ∥_{K}^{2} = \int_{S} ∣ X (s) ∣^{2} d σ (s),$ $K$ is a real Hilbert space. If $Σ$ is countably generated, then $K$ is separable. In particular this applies to every Borel probability on $S \subseteq R^{k}$ with its relative Borel sigma-algebra, for any $k \geq 1$ independent of the output dimension $d$ , and to every finite label space. No separability claim is made for an arbitrary probability sigma-algebra.

Statement references

The space $L^{p} (μ)$ as the quotient by null functions

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

Simple functions with finite-measure support are dense in $L^{p} (μ)$ for $1 \leq p < \infty$

A countable generator of a sigma-algebra yields a countable algebra of sets

Finite-measure sets are approximable in measure by sets from a countable generating algebra

Ambrosio, Gigli, and Savaré, Chapter 4

Chizat and Bach, Assumptions 2.1

Facts & Assumptions

Given: AC, the probability space $(S, Σ, σ)$ , and $d \geq 1$ .

[F1]

Scalar $L^{2} (σ)$ is the quotient of square-integrable measurable functions by equality almost everywhere, and its norm is complete by the Riesz–Fischer theorem. The space $L^{p} (μ)$ as the quotient by null functions Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$

[F2]

Finite-measure simple functions are dense in scalar $L^{2}$ . Simple functions with finite-measure support are dense in $L^{p} (μ)$ for $1 \leq p < \infty$

[F3]

AC implies Countable Choice. The Axiom of Choice AC implies DC implies countable choice The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F4]

Finite-measure sets in a sigma-finite countably generated space can be approximated in symmetric-difference measure by a countable generating algebra. A countable generator of a sigma-algebra yields a countable algebra of sets Finite-measure sets are approximable in measure by sets from a countable generating algebra

[F5]

Pointwise Euclidean Cauchy–Schwarz gives $∣ X (s) \cdot Y (s) ∣ \leq ∣ X (s) ∣ ∣ Y (s) ∣$ . The real inner-product axioms specify bilinearity, symmetry and positive definiteness. Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs Real and complex inner-product spaces and their induced length

Proof

Given: AC and $(S, Σ, σ)$ as in the Statement.

1.1givenF3F4

First assume that $Σ$ is countably generated. By [F3] and [F4], its countable generating family generates a countable algebra $A_{0}$ such that each $E \in Σ$ and each $ε > 0$ admit $A \in A_{0}$ with $σ (E △ A) < ε$ . Relative Borel spaces $S \subseteq R^{k}$ have countable generators obtained by intersecting $S$ with rational open boxes; every relative open set is a union of members of this countable base. Finite sigma-algebras are countably generated as well. These observations do not identify the label dimension $k$ with the output dimension $d$ .

2.1F2F4step 1.1choose

The functions $\sum_{j = 1}^{m} q_{j} 1_{A_{j}}$ , with $q_{j} \in Q$ and $A_{j} \in A_{0}$ , form a countable subset of scalar $L^{2} (σ)$ . It is dense: by [F2], approximate any $f$ by a finite-measure simple function $\sum_{j} c_{j} 1_{E_{j}}$ ; approximate each $E_{j}$ in measure using [F4], then approximate each coefficient by a rational. The error satisfies $∥ c 1_{E} - q 1_{A} ∥_{2} \leq ∣ c - q ∣ \sqrt{σ (E)} + ∣ q ∣ \sqrt{σ (E △ A)}$ , so the finitely many choices make the total error arbitrarily small.

3.1F1F5step 2.1∎

The vector space $K$ is the finite product of $d$ copies of scalar $L^{2} (σ)$ . By pointwise [F5], $2 ∣ X \cdot Y ∣ \leq ∣ X ∣^{2} + ∣ Y ∣^{2}$ , so its displayed pairing is integrable and independent of representatives. Linearity of the integral and the Euclidean dot product give bilinearity and symmetry. Its value on $(X, X)$ is $\int ∣ X ∣^{2} \geq 0$ , and equality forces $∣ X ∣ = 0$ almost everywhere, precisely the zero class. Thus it is an inner product, with the stated norm. A Cauchy sequence for that norm is Cauchy in each of the finitely many scalar coordinates; [F1] gives coordinate limits, and the sum of their squared errors tends to zero. This proves completeness for every probability space, without a countable-generation hypothesis. When $Σ$ is countably generated, the finite product of the countable dense scalar sets from step 2.1 is countable and dense in $K$ , proving separability.

Depends on

Used by

Localized Hilbert lift of the feature energy Definition
Finite-particle flows converge to the measure-valued flow in W2 Theorem

Dependency tree · two levels

68 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 (standard reference, not scraped)
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)