Alphabeta Math
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 Cameron–Martin unit ball is compact in the Banach norm

Statement

Assume AC. Let μ be a centered tight Borel Gaussian law on a real separable Banach space B, and let H⊂B be its covariance RKHS. The closed Hilbert unit ball H1={h∈H:∥h∥H≤1} is compact in the Banach norm.

Facts & Assumptions

[A1]

AC is inherited from the Gaussian translation and tightness suppliers. Under AC, the ultrafilter lemma follows from The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter, and DC and countable choice follow from AC implies DC implies countable choice.

[A2]

Under AC, the real dominated-extension theorem supplies the Hahn–Banach principle HB used by the dual-norming interface (Hahn-Banach dominated extension theorem for real vector spaces, The real dominated-extension principle as an additional hypothesis over ZF).

[F1]

For h∈H, the translated law has density Dh=exp⁡(zh−∥h∥H2/2), where zh is centered normal of variance ∥h∥H2 (Cameron–Martin translation formula for a separable Banach Gaussian, Standard normal and normal laws).

[F2]

A Borel probability on the separable Banach space is tight (Every borel probability on a polish space is tight, Prokhorov tightness theorem on polish spaces).

[F3]

Under the ultrafilter lemma, DC and HB, a Banach space is reflexive exactly when every bounded sequence has a weakly convergent subsequence; under countable choice, a Hilbert space is reflexive (Reflexivity is equivalent to weak subsequential compactness of bounded sequences, Hilbert spaces are reflexive by Riesz representation). The needed choice hypotheses follow from [A1] and [A2].

[F4]

The canonical embedding satisfies ℓ(ih)=⟨h,[ℓ]⟩H, and continuous linear functionals separate points (Covariance operator and reproducing-kernel Hilbert space of a Banach Gaussian, Relative dual norming, point separation, and recovery of the norm).

[F5]

Cauchy–Schwarz applies to the square-integrable density and event indicator (Cauchy-Schwarz for random variables).

Proof

Given: AC and a centered tight Borel Gaussian law μ on B, its covariance RKHS H, and H1.

1.1A1F1F2F5givenalgebra

If h∈H1, write v=∥h∥H2≤1. If v=0, then zh=0 almost surely and Dh=1. If v>0, completing the square in the normal density of zh gives Ee2zh=e2v. In both cases [F1] yields ∫Dh2 dμ=ev≤e. Choose compact K⊂B with μ(Kc)<1/(16e) using [F2]. Cauchy–Schwarz [F5] then gives μh(Kc)=∫KcDh dμ<1/4, uniformly for all h∈H1, while μ(K)>3/4. Hence μ(K∩(K−h))≥μ(K)+μh(K)−1>0. For each h∈H1 there is x∈K with x+h∈K, so h∈K−K. The difference K−K is compact; therefore H1 is relatively compact in B.

2.1A1A2F3F4step 1.1algebra∎

Let (hn) be any sequence in H1. By [F3], pass to a subsequence weakly converging in H to some h∈H1. Relative compactness from step 1.1 gives a further subsequence with ihn→y in B. For every ℓ∈B∗, [F4] gives ℓ(y)=lim⁡n⟨hn,[ℓ]⟩H=⟨h,[ℓ]⟩H=ℓ(ih). By [F4], y=ih. Thus every sequence in H1 has a norm-convergent subsequence whose limit lies in H1; in the metric space B, this is compactness.

Depends on

Used by

Dependency tree · two levels

80 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