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.
Stratification and allocation
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Conditional Distributions and Regular Conditional Probability
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Estimators and Randomized Procedures
- Finite Counting, Factorials and Binomial Coefficients
- Finite populations and design probability
- Finite Probability Spaces and Random Variables
- Finite-Sample Point Estimation
- Fixed-design regression, estimability, and Gauss–Markov
- Foundations of the Real Numbers for Analysis
- HT variance and SRSWOR
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- limsup, liminf, and Subsequential Limits
- Loss, Risk and Decision Theory
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Probability Spaces Random Variables and Expectation
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Roots, Rational Powers, and Classical Inequalities
- Scientific model contracts and applicability
- Sequences and Limits
- Sigma Algebras and Borel Sets
- Simple Field Extensions and the Construction of the Complex Numbers
- Statistical Experiments, Models and Identifiability
- Suprema and Infima
- The Lebesgue Integral and the Convergence Theorems
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
2 · Summary
This page treats the population values as fixed and the sample selections as random under the design. A finite population is partitioned into nonempty strata; each stratum receives an independent SRSWOR sample, and its weighted sample mean contributes to the estimated total. The total is design-unbiased, and its variance is the sum of the within-stratum finite-population variance terms. A certainty stratum contributes zero without requiring its population variance. For continuous allocations with positive noncertainty variances, the fixed-size optimum is proportional to , while a fixed per-unit-cost budget gives weights . These formulas optimize uncapped continuous relaxations; integer rounding, capacity or minimum-sample constraints, and zero-variance strata require separate treatment. The probability notation follows probability-spaces-random-variables-and-expectation.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Stratified sampling designs and the stratified total estimator
Definition
Let be a finite population as in Finite populations and sampling designs, and let be a finite partition of into nonempty strata. Write and . Choose integers . In stratum , draw by SRSWOR of size as in Simple random sampling without replacement, independently across strata. Thus the joint probability of a tuple is and its sample in is . This is the stratified SRSWOR design. The union map is one-to-one because the strata are disjoint; the support has elements, so the displayed mass function sums to one.
The fixed mean in stratum is For a noncertainty stratum (), necessarily , and its finite- population variance is For every noncertainty stratum write for its nonnegative population standard deviation. For a realized sample, set The quantity is the stratified total estimator. When , the stratum is a certainty stratum and its contribution is the fixed total ; no is needed for that term. The population values remain fixed: only the sample selections are random.
Unbiasedness and variance of the stratified total estimator
Statement
Let be a finite population with a partition and stratified SRSWOR design as in Stratified sampling designs and the stratified total estimator. Under the design probability , the stratified total estimator satisfies Its design variance is Thus certainty strata contribute zero and require no within-stratum variance term.
Facts & Assumptions
Given: A fixed finite population , a finite partition , and independent within-stratum SRSWOR samples with .
Stratified sampling designs and the stratified total estimator: The joint design mass on stratum samples is the product of the uniform SRSWOR masses; ; and is defined for noncertainty strata.
Finite populations and sampling designs: Population values are fixed, the design is a finite probability mass function, the observed record contains selected labels and their values, and is the first-order inclusion probability.
The Horvitz–Thompson total and mean are design-unbiased under positive inclusion probabilities: If every , then is design-unbiased for .
SRSWOR inclusion covariance and sample-mean variance: For SRSWOR of from a fixed population of size , ; this includes and the census .
Moments, variance, and covariance on a probability space: Variance is the expectation of the squared centered variable and covariance is the expectation of the product of centered variables.
Variance of a finite sum as the sum of all variances and covariances: For a finite family of square-integrable variables on one probability space, the variance of their sum is the sum of all pairwise covariances, including diagonal terms.
Proof
For , counting the -subsets containing gives . On observed record , the recorded values are by [F2], so the Horvitz–Thompson total is ; [F3] gives .
Put . Each has finite support and is square-integrable. If , then and [F4] gives ; variance scaling from [F5] gives . If , is constant with variance zero.
For distinct strata , write . The product law in [F1] gives , since each remaining mass sum is one. Thus [F5] gives .
Since , [F6] and steps 1.2–1.3 give . Substituting step 1.2's noncertainty and certainty cases yields the stated variance, and step 1.1 gives unbiasedness.
Continuous fixed-size Neyman allocation minimizes stratified variance
Statement
Use the notation of Stratified sampling designs and the stratified total estimator and Unbiasedness and variance of the stratified total estimator. Let be a nonempty set of noncertainty strata whose allocations vary, and suppose for each , where is the positive population standard deviation. Hold all other stratum allocations fixed. For real with , consider the uncapped continuous relaxation of the variance expression where collects the fixed strata's variance terms. Its unique minimum over this positive simplex is attained at This is the continuous Neyman allocation. The relaxation imposes no integer, capacity, lower-bound, or minimum-sample constraints; if the displayed allocation violates a design constraint, it is not itself an admissible stratified SRSWOR design.
Facts & Assumptions
Given: A stratified SRSWOR finite-population design; a nonempty set of variable noncertainty strata with ; fixed allocations outside ; and a positive real budget for .
Stratified sampling designs and the stratified total estimator: For a noncertainty stratum, and .
Unbiasedness and variance of the stratified total estimator: A noncertainty stratum's variance contribution is ; certainty and fixed strata contribute terms that do not vary with .
Proof
Put . For , [F2]'s variable term with is . The subtracted term is constant, so the relaxed objective is minimized by minimizing subject to .
Set and . Expanding and grouping unordered pairs gives . Since and , we get , with equality exactly when is constant over .
Define . Positivity gives , and summing gives . This allocation satisfies step 2.1's equality condition and attains its lower bound; the equality condition uniquely fixes this normalization. By step 1.1 it uniquely minimizes the relaxed variance.
Continuous cost-optimal stratified allocation
Statement
Use the notation of Stratified sampling designs and the stratified total estimator and Unbiasedness and variance of the stratified total estimator. Let be a nonempty set of variable noncertainty strata with , and hold all other allocations fixed. Assign each a positive per-unit cost . For a fixed positive residual cost budget , the uncapped continuous relaxation of the stratified variance expression, minimized over positive real allocations for every subject to , has the unique minimizer Thus . As in the fixed-size result, this continuous formula does not enforce integer, capacity, lower-bound, or minimum-sample constraints.
Facts & Assumptions
Given: A finite stratified SRSWOR design, a nonempty set of variable noncertainty strata with , fixed allocations outside , per-unit costs , and a positive residual cost budget .
Stratified sampling designs and the stratified total estimator: For each noncertainty stratum, is the finite-population variance and denotes its nonnegative standard deviation. The hypothesis is imposed only for .
Unbiasedness and variance of the stratified total estimator: The variable variance term for stratum is ; contributions from fixed strata do not depend on the variable allocation.
Proof
Put . Replacing by in [F2] gives . The subtracted and fixed-stratum terms do not vary with , so it suffices to minimize subject to .
Set and . Expanding and grouping unordered pairs gives . Since and , the objective is at least , with equality exactly when is constant.
The allocation is positive and satisfies . It makes constant and attains step 2.1's bound; the equality condition uniquely determines it. By step 1.1 it uniquely minimizes the relaxed variance and gives the stated formula.
5 · Examples, counterexamples and false statements
None yet.
Sources
- Shalabh, Sampling Theory, MTH 417 lecture notes, Chapter 4: Stratified Sampling, Indian Institute of Technology Kanpur, complete 26-page chapter
- Robin Arnold, STAT392 Sample Surveys, Chapter 8: Stratified Sampling, Victoria University of Wellington
- Shalabh, Sampling Theory, MTH 417 lecture notes, Chapter 4: Stratified Sampling, PDF pp. 3–6, Indian Institute of Technology Kanpur
- Robin Arnold, STAT392 Sample Surveys, Chapter 8: Stratified Sampling, §§8.1–8.3
- Tommy Wright, A Simple Method of Exact Optimal Sample Allocation under Stratification with Any Mixed Constraint Patterns, U.S. Census Bureau, §2.1
- Shalabh, Sampling Theory, MTH 417 lecture notes, Chapter 4: Stratified Sampling, PDF pp. 8–9 and 12–14
- Robin Arnold, STAT392 Sample Surveys, Chapter 8: Stratified Sampling, §8.8
- Shalabh, Sampling Theory, MTH 417 lecture notes, Chapter 4: Stratified Sampling, PDF pp. 9–11
- Robin Arnold, STAT392 Sample Surveys, Chapter 8: Stratified Sampling, §8.8 and Example 8.8.1