False Positives under Multiple Testing

Abstract

Independent repeated tests amplify false-positive risk, while every finite family obeys the union bound.

Theorem 1.1 (At least one false positive).

$$\begin{gathered} \begin{array}{c}\forall Omega:\mathrm{Type},mu:\mathrm{Measure}(Omega),k:\mathrm{Nat},\\ alpha:\mathrm{Real},E:\mathrm{Fin}(k)\to \mathrm{Set}(Omega),\\ \mathrm{IsProbabilityMeasure}(mu)\wedge \forall i:\mathrm{Fin}(k),\mathrm{Measurable}(\mathrm{event}(E,i))\wedge \mathrm{Pr}(mu,\mathrm{event}(E,i))=alpha\wedge 0\le alpha\wedge alpha\le 1\Rightarrow \\ \mathrm{iIndepSet}(E,mu)\Rightarrow \mathrm{Pr}(mu,\mathrm{iInterCompl}(E))={1-alpha}^k\wedge \\ \mathrm{Pr}(mu,\mathrm{iUnion}(E))=1-{1-alpha}^k\wedge \\ \forall m,n:\mathrm{Nat},m\le n\Rightarrow 1-{1-alpha}^m\le 1-{1-alpha}^n\wedge \\ (2\le k\wedge 0<alpha\wedge alpha<1\Rightarrow alpha<\mathrm{Pr}(mu,\mathrm{iUnion}(E)))\wedge \\ \mathrm{Pr}(mu,\mathrm{iUnion}(E))\le k\times alpha.\end{array} \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Experiment/MultipleTestingFalsePositive.at_least_one_false_positive (✓ std3). ∎

Source. Repository-derived.

Commentary.

The outcome space, probability measure, finite family of measurable false-positive events, common single-test rate alpha, and number of tests k are public source primitives.

Under mutual independence, the no-error intersection has probability (1-alpha)^k and its complementary union has probability 1-(1-alpha)^k. The displayed family of search-wide rates is nondecreasing in k.

For k at least two and 0 < alpha < 1, the search-wide probability is strictly larger than alpha. This is the formal obstruction to reporting only the most successful test while retaining the single-test threshold as the whole-search error rate.

The final public conjunct does not assume independence: Mathlib’s finite union bound gives probability at most k times alpha for every measurable family with the stated marginal rates.

Pinned Mathlib exact hits compute independent intersections, probability complements, finite union bounds, constant products, and power monotonicity. No repository theorem packages all five source clauses.

References

• Truth anchor: D5/S3/ConceptDynamics/Experiment/MultipleTestingFalsePositive.at_least_one_false_positive