Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

Tightness from a uniform moment bound

Example

For a family A of probability laws on Rd with finite d≥1, if p>0 and sup⁡μ∈A∫∥x∥p dμ≤C<∞, then the family is tight.

Facts & Assumptions

[F1]

Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it: Let n∈N with n≥1. A von Neumann natural is the set of its predecessors, n={0,1,…,n−1} (def-natural-numbers), so it can be used directly as an index set. Define

Rn:={ x:x is a function n→R },

and write xk for x(k), k<n. Two elements of Rn are equal exactly when they agree at every k<n, functions being equal when they have the same values. For x,y∈Rn put

d1(x,y):=∑k<n∣xk−yk∣,d2(x,y):= ∑k<n(xk−yk)2 ,d∞(x,y):=max⁡{ ∣xk−yk∣:k<n }.

All three are well defined: the finite sums are those of def-finite-sum; the sum of squares is nonnegative (lem-finite-sum-laws, lem-of-square-positive) so it has a unique nonnegative square root (thm-of-square-roots); and {∣xk−yk∣:k<n} is a nonempty finite subset of R, because n≥1, so it has a maximum (lem-finite-set-has-max, def-max-min).

Then d1, d2 and d∞ are metrics on Rn (def-metric-space).

Why n≥1. For n=0 the set R0 has exactly one element, the empty function, and d1 and d2 are the empty sum 0 and its root; but d∞ would be the maximum of the empty set, which does not exist. The hypothesis n≥1 is therefore not decoration, and it is carried by every statement about d∞ in this library.

[F2]

Markov's inequality for random variables: If X:Ω→[0,+∞] is a nonnegative random variable on a probability space and a>0, then P(X≥a)≤E[X]a.

[F3]

The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents: For a,b>0 and r,s∈R, ar+s=aras,(ab)r=arbr,(a/b)r=ar/br,(ar)s=ars.

[F4]

Heine-Borel in Rn: with the Euclidean metric a subset of Rn is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: Let n∈N with n≥1, let Rn be the set of functions n→R and let d2 be the Euclidean metric on it (lem-metrics-on-rn). Then:

  1. Closed boxes are compact. For reals ak≤bk (k<n) the box Q={ x∈Rn:ak≤xk≤bk for every k<n } is a compact subset of (Rn,d2) (def-metric-compactness).
  2. Heine-Borel. A subset K⊆Rn is a compact subset of (Rn,d2) if and only if K is closed in Rn (def-metric-topology) and bounded (def-metric-bounded-diameter).
  3. The real line. A subset K⊆R is a compact subset of (R,dR), the usual metric dR(x,y)=∣x−y∣ (lem-real-line-is-a-metric-space), if and only if K is closed in R and bounded.

No choice principle is used. The bisection below halves one coordinate at a time and takes the left half whenever the left half still fails to be finitely covered, the right half otherwise: a rule with two outcomes, decided by a property of the box, not a selection. That is the whole reason the theorem is available in ZF, while the general "complete and totally bounded implies compact" (thm-complete-and-totally-bounded-implies-compact) is not.

The hypothesis n≥1 is inherited from lem-metrics-on-rn, which defines Rn and its metrics only there; the last remark below records what happens at n=0.

[F5]

Tight family of probability measures: A family A of Borel probabilities on a metric space S is tight if, for every ε>0, there is a compact K⊆S such that μ(S∖K)<ε for every μ∈A. One K must work for the whole family. Compactness is def-metric-compactness. The empty family is tight, witnessed by the empty compact set.

[F6]

Continuity and derivatives of positive-base real powers: For a>0, the function x↦ax is continuous on R and (ax)′=axlog⁡a. For α∈R, the function x↦xα is continuous and differentiable on (0,∞), with (xα)′=αxα−1.

Verification

Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.

1.1F1F2F6

The Euclidean norm is distance to zero for the metric in F1, hence is continuous by the triangle inequality. On positive arguments F6 gives continuity of tp. Thus its composition with the norm is continuous off the origin, and assigning zero at the closed singleton origin gives a Borel function. If t>R>0, tp/Rp=exp⁡(plog⁡(t/R))>1, so the power is increasing on positive arguments. F2 on (Rd,B,μ) gives μ({∥x∥>R})≤C/Rp for every R>0.

2.1F3F4F5∎

The empty family is tight using the empty compact set. For a nonempty family C≥0. Given ε>0 take R=((C+1)/ε)1/p>0; F3 yields C/Rp=Cε/(C+1)<ε. The ball K={∥x∥≤R} is closed and bounded and therefore compact by F4. Step 1.1 proves the uniform loss bound for this K, which is F5.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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