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.
Group-sequential alpha spending
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Areas of Elementary Plane Figures
- Binary Operations, Monoids, Groups and Subgroups
- Central Limit Theorems
- Characteristic Functions Inversion and Continuity
- Compactness
- Compactness in Metric Spaces
- Complete Metrizability, Čech-Completeness, and Baire Category
- Completeness, Completion, and Uniform Continuity
- Complex Lp Spaces and Test-Function Conventions
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Conditional Distributions and Regular Conditional Probability
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Cyclic Groups and Direct Products
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Estimators and Randomized Procedures
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Probability and the Probabilistic Method
- Foundations of the Real Numbers for Analysis
- Fourier Transform Convolution and Approximate Identities
- Fubini and Change of Variables
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hausdorff via the Diagonal
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper and Parameter-Dependent Multiple Integrals
- Improper Integrals
- Independence Borel Cantelli and Zero One Laws
- Infinite Product Measures and Kolmogorov Extension
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Loss, Risk and Decision Theory
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Partitions of Unity and Paracompactness
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Probability Spaces Random Variables and Expectation
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Radon Measures and the Riesz Markov Kakutani Theorem
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Splitting Fields
- Statistical Experiments, Models and Identifiability
- Subspaces, Products, and Quotients
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tests, Neyman–Pearson and Valid P-values
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Exponential Function
- The Fundamental Theorem of Algebra
- The Fundamental Theorem of Finite Abelian Groups
- The Galois Correspondence
- The Inverse and Implicit Function Theorems
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Radon Nikodym Theorem and Lebesgue Decomposition
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Urysohn's Lemma and the Tietze Extension Theorem
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Convergence Tightness and Representation
2 · Summary
This page defines a prescheduled group-sequential design under a stipulated canonical Gaussian simple-null law and proves the recursive boundaries exist uniquely. The cumulative rejection probability is calibrated to the chosen nondecreasing alpha-spending function at each planned information fraction. The proof treats one-sided upper boundaries and separately calibrated symmetric two-sided crossing events. Exactness depends on the specified joint law and planned looks; data-dependent timing, estimated variance, and composite-null guarantees require additional calibration arguments.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Canonical group-sequential alpha-spending design
Definition
Assume the Axiom of Choice (The Axiom of Choice). Fix a finite integer maximum , prescheduled information fractions (where is the fraction of total planned information available at look ), and a nominal level . An alpha-spending function is a nondecreasing map with and .
Under the stipulated simple null law , the standardized look vector is , where Here is the finite-dimensional multivariate normal law of Multivariate normal law, including singular covariance, whose projection characterization determines the law by Characteristic function of a multivariate normal law. The construction of this covariance matrix as a valid Gaussian covariance is proved in Group-sequential boundaries exist uniquely and spend alpha exactly ↗. The standardized coordinates are correlated; independence of the is not assumed.
For a one-sided upper-boundary design, look rejects when . For a symmetric two-sided design, look rejects when . In either case, the procedure stops at its first crossing. For each , its cumulative type-I probability is the probability under the stipulated null law of crossing at one of looks . The design is exactly calibrated to when this cumulative probability equals for every . If it is embedded in an experiment with a nonempty alternative and singleton null hypothesis, this null rejection probability is the test size in the sense of Test size and power.
The fractions and joint null law are assumptions of this definition. It does not derive a Gaussian model from an asymptotic central limit theorem, justify data-dependent look timing, justify estimated variance, or establish error control over an unspecified composite null. A two-sided design calibrates its two-sided crossing events separately; one-sided boundaries are not doubled to obtain two-sided boundaries.
Recursive group-sequential boundary calibration
Definition
Inputs: The Axiom of Choice (The Axiom of Choice) and a canonical design from Canonical group-sequential alpha-spending design and a mode, either one-sided upper-boundary or symmetric two-sided.
Output: The look boundaries for the selected mode.
Set , , and process in order. Let be the union of the crossing events already defined at the earlier looks.
- If , set the boundary at look to . Its crossing event is empty, so .
- If and the mode is one-sided, choose the real number satisfying and set .
- If and the mode is symmetric two-sided, choose satisfying and set .
The root-existence theorem Group-sequential boundaries exist uniquely and spend alpha exactly ↗ proves that every positive spending increment has a unique finite solution; the algorithm therefore makes no arbitrary boundary selection. The procedure specifies exact boundaries under the supplied joint null law. It does not prescribe a numerical integration package or tolerance.
Group-sequential boundaries exist uniquely and spend alpha exactly
Statement
Assume AC and the canonical group-sequential design of Canonical group-sequential alpha-spending design. The recursive boundary algorithm Recursive group-sequential boundary calibration is well-defined: every positive spending increment has a unique finite boundary, while a zero increment has boundary . For every , the probability under of a rejection by look is ; in particular the terminal simple-null rejection probability is . When embedded in an experiment with a nonempty alternative and a singleton null whose law is , the test size is therefore . The same cumulative-probability conclusion holds for separately calibrated symmetric two-sided crossing events. This exact statement is conditional on the specified joint Gaussian null law and prescheduled information fractions; it does not cover data-dependent timing, an estimated variance, or a composite null without an additional argument.
Facts & Assumptions
Given: AC, a finite , prescheduled fractions , , a nondecreasing spending function with and , and the specified canonical null vector . Prove the boundary algorithm is well-defined and gives cumulative null rejection probability at each planned look.
Canonical group-sequential alpha-spending design: The planned information fractions, spending-function conditions, canonical covariance for , and the one-sided or symmetric two-sided crossing events are as stated in the definition.
Multivariate normal law, including singular covariance: Under AC, for finite and symmetric positive semidefinite , the law exists and has a realization with independent standard-normal coordinates .
Characteristic function of a multivariate normal law: Under AC, the vector characteristic function of is and determines its Borel law uniquely, including for singular .
Standard normal and normal laws: Under AC, the standard normal law is the probability measure with density on Borel subsets of .
The standard normal density has total mass one: The standard normal density is positive and Borel measurable and has Lebesgue integral one.
Continuity from below for measures: For an increasing sequence of measurable sets , a measure satisfies .
Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on takes every value between and : A continuous real function on a closed bounded interval takes every value between its endpoint values.
Test size and power: For a statistical experiment and nonempty disjoint null and alternative hypotheses, the size of a test is the supremum of its rejection probability over the null; when the null is a singleton, size is its rejection probability under that one null law.
Recursive group-sequential boundary calibration: At a positive spending increment the one-sided mode solves and the symmetric two-sided mode solves ; at a flat increment the boundary is .
The Axiom of Choice: Assume the Axiom of Choice.
Proof
For , define a lower-triangular matrix by and, for , , with for . For , the entry of is Thus . Its diagonal entries in are and for , so is invertible and for every nonzero .
For every , the th coordinate has law by the projection clause in [F2]. It has no atoms, and for , Positivity follows from [F5]; the upper bound follows from . The same facts bound a two-sided strip by when .
By [F2] and [F3], the canonical law exists and is represented by for independent standard-normal coordinates . Since is positive definite by step 1.1, is invertible: if , then , forcing . The inverse image under this linear homeomorphism of any nonempty open subset of is nonempty and open, hence contains a product of nonempty open intervals. Each interval has positive standard-normal probability by [F4]–[F5], and independence makes the product probability positive. Therefore every nonempty open subset of has positive -probability.
For the induction step, fix . Assume that the boundaries through have been constructed with ; for this is the empty base case , . Any finite two-sided boundary already constructed is positive, as established when its root was obtained. Let . In the one-sided mode, is the intersection of the open conditions for earlier finite boundaries; in the symmetric two-sided mode, it is the intersection of for earlier finite boundaries. These conditions describe a nonempty open set: choose each constrained coordinate below its upper boundary, or inside its interval , and ignore infinite boundaries. Thus .
In the one-sided mode set for . If , then . Although , it restricts only coordinates , as described in step 3.1. Thus is nonempty and open: choose each earlier coordinate below its finite one-sided boundary (or arbitrarily when its boundary is ), choose , and choose the remaining coordinates arbitrarily. By step 2.1, ; the only part of omitted from lies on , which has probability zero by step 1.2. Also by step 1.2, so is continuous. Moreover as and as , since the omitted lower and upper normal tails tend to zero. For the symmetric two-sided mode set for . For , . Here again restricts only coordinates , so is nonempty and open: set every earlier coordinate to (which satisfies every finite earlier symmetric no-crossing condition because its boundary is positive), choose , and choose the remaining coordinates arbitrarily. Step 2.1 gives . The bound in step 1.2 makes continuous. Here and as . The tail limits in both modes follow from [F6] applied to increasing lower or central intervals of the standard-normal coordinate.
Since is nondecreasing, either or . In the flat case, [F9] assigns , whose crossing event is empty, so the previous cumulative probability is unchanged. In the increasing case, the target lies strictly between the endpoint limits of . The limits in step 4.1 give finite endpoints on which the continuous function takes values on opposite sides of ; [F7] gives a root. Strict decrease in step 4.1 makes that finite root unique. The induction therefore defines every boundary through the finite maximum . In the symmetric two-sided mode , so the root is strictly positive.
The induction step is complete: at an increasing look the selected root gives by [F9]; at a flat look the event union is unchanged and . Induction from proves the equality for every . Stopping at the first crossing makes exactly the event of rejection by look . At , and , so the terminal simple-null rejection probability is . For any embedding with a nonempty alternative and singleton null whose law is , the rejection indicator is a measurable test function because is a finite union of Borel threshold events; [F8] then makes its size . AC is used in the supplied Gaussian law and representation [F2] and [F4], not in the finite root selection: each root is unique and there are only finitely many looks.
5 · Examples, counterexamples and false statements
None yet.
Sources
- David L. DeMets and K. K. Gordon Lan, Interim Analysis: The Alpha Spending Function Approach, Statistics in Medicine 13 (1994), PDF pp. 2–3, 6–7
- Michael J. Grayling, James M. S. Wason, and Adrian P. Mander, Group Sequential Clinical Trial Designs for Normally Distributed Outcome Variables, The Stata Journal 18(2) (2018), PDF pp. 2–4
- Giorgos Minas, Multivariate Global Testing and Adaptive Designs, PhD thesis, Chapter 5 §§5.3–5.3.1, printed pp. 72–73