Glossary

Two tables. The first translates Lean/type-theory vocabulary into terms a statistician already has. The second is the library’s own vocabulary — every headline name in the library, with the chapter that introduces it.

Lean ↔ statistics

Lean	Statistics analogue	Note
Term	A value, of some type	Anything with a type is a term — 3, fun x => x + 1, and a completed proof are all terms.
Type	The set/space a value lives in	x : T reads ”$x$ is an element of $T$”; ℝ, Fin n → ℝ, Design n are all types.
Proposition (Prop)	A statement that could be true or false	A p : Prop names a claim; a term hp : p is a specific proof that it holds — under Curry–Howard, propositions are types and proofs are their elements.
Proof	A construction the type-checker verifies	Proving p means building a term of type p; there is no separate “proof checker” step, elaboration is the check.
Prop vs Bool	A claim vs. a computed answer	Prop has no runtime representation — you cannot ask “is it true?” by running code. Bool is true/false, computable and pattern-matchable. decide bridges a decidable Prop to the Bool check.
Fin n	Unit labels $1,\dots ,n$	A natural number below n, bundled with a proof that it is. Fin n → ℝ is exactly an outcome vector over n units.
Finset α	A finite subset, with membership you can test	Assignment n := Finset (Fin n) is the treated set; ∑ i ∈ s, f i sums over one.
Fintype α	”$\alpha$ is finite, and Lean can enumerate it”	Lets you write ∑ i, f i / ∏ i, f i over all of α (Finset.univ) without naming a subset.
∑ (Finset.sum)	$\sum$	∑ i ∈ s, f i is Finset.sum s f; ∑ i, f i sums over univ when the index type is a Fintype.
Coercion ↑	An implicit cast, made explicit	(n : ℝ) / ↑n turns a ℕ into the real number it denotes. Missing or misapplied coercions are the single most common “wrong type” bug in this library.
noncomputable	“Exists, but Lean won’t execute it”	Marks a definition Lean cannot run — real division and Classical.choice aren’t computable. It changes nothing about what is proved; #eval just won’t work on it.
structure fields	The assumptions of a model	A structure’s fields are exactly what you’d list before a theorem on paper: Design’s three fields are a pmf, its nonnegativity, and that it sums to one.
Design.prob / Design.expect vs. pmf / expectation	The same objects, spelled as code	D.prob z is $Pr(Z=z)$ for one specific assignment; D.expect f is $\mathbb{E}[f]=\sum _{z}D.\mathrm{prob}(z)\cdot f(z)$ — a finite sum, because there are only $2^n$ assignments and no measure theory is needed.
propensity	${\pi }_i=Pr(\text{unit }i\text{ treated})$	D.propensity i = D.expect (fun z => Z z i), the marginal probability unit i lands in the treated set.
Assignment n	The treated set, not an indicator vector	abbrev Assignment n := Finset (Fin n). z : Assignment n is the set of treated units; Z z i recovers the familiar 0/1 indicator from it.
sorry	An admitted gap, flagged	Closes any goal, emits a warning, and is recorded as the axiom sorryAx forever after — visible to #print axioms. Never appears in any theorem of this library.
axiom	A trusted, unproven assumption	Every Lean development rests on a short axiom list — propext, Classical.choice, Quot.sound here, see the appendix on verification. #print axioms shows exactly which ones a given proof used.
instance	Typeclass evidence, found automatically	Declares e.g. “here is how Fin n is a Fintype”; Lean’s elaborator searches for these silently, which is why ∑ i, f i just works once the instance exists.
namespace	A dot-notation prefix, not a module	namespace Design … end lets Design.expect_add be written D.expect_add for D : Design n. Purely notational.
open	Bring names into scope	open Finset BigOperators lets you write sum for Finset.sum and use ∑ notation. Can also shadow names — Mathlib’s bernoulli : ℕ → ℚ is why this library uses bernoulliDesign.
simp lemma	A rewrite rule in the default simplification set	Any @[simp]-tagged equation simp fires automatically; generally one with an unambiguous left-to-right normal form.
@[simp]	Registers a lemma with simp’s database	Tags a theorem for automatic use. This library prefers simp only [named, lemmas] in proofs meant to be read, and reserves plain simp for genuinely routine steps.
Decidable	A proposition with an algorithm that settles it	DecidableEq, DecidablePred are what let if i ∈ z then … else … and decide work. Every proposition about a Finset/Fin n here is decidable.
Classical	Non-constructive reasoning, on tap	Classical.choice and Classical.em (excluded middle) cover propositions with no algorithm. by_cases, and every fact about ℝ, uses it — ℝ itself is built with Classical.choice.
ENNReal (ℝ≥0∞)	Nonnegative extended reals, with a genuine $\mathrm{\infty }$	The value type of a PMF. Needs open ENNReal (or open scoped ENNReal) for the ≥/∞ notation to parse; ordinary probability arithmetic mostly wants the .toReal cast back to ℝ.
PMF α	A measure-theoretic probability mass function on α	Mathlib’s object, not this library’s Design. Design.toPMF / PMF.toDesign round-trip between the two — see the bridge chapter.
MeasureTheory.integral (∫)	$\mathbb{E}[f]$, in measure-theoretic language	∫ z, f z ∂μ is Mathlib’s expectation. Design.integral_toMeasure proves it equals D.expect f for a design’s induced measure: two vocabularies, one number.
∀ᵐ (a.e., “almost everywhere”)	“except possibly on a probability-zero set”	Appears only in the bridge chapter. ae_of_forall: a statement true at every assignment is true a.e., for free. of_ae_of_prob_pos: the converse holds only at assignments the design gives positive probability — a design’s null sets are the assignments it never produces, and an a.e. statement says nothing about them.

The library’s vocabulary

Every headline definition and theorem, grouped by the file (and chapter) that owns it. D is a Design n, P a Population n, z an Assignment n, π the propensity.

MrCLean/Basic.lean — potential outcomes

Name	What it is
Population	A structure: y1, y0 — the two potential outcomes per unit. SUTVA is enforced by the type, not assumed.
mean	(∑ i, v i) / n, the average of a vector over all units.
Population.tau	The population ATE, mean P.effect.
Assignment n	Finset (Fin n) — the treated set.
Z	The indicator, if i ∈ z then 1 else 0, valued in ℝ so ordinary algebra applies.
Yobs	The observed outcome, Z z i * P.y1 i + (1 - Z z i) * P.y0 i.

MrCLean/Design.lean, Bernoulli.lean, CompleteRandomization.lean — designs

Name	What it is
Design	A structure: an explicit pmf over assignments, its nonnegativity, and that it sums to one.
Design.expect	∑ z, D.prob z * f z — expectation as a finite sum.
Design.propensity, Design.jointPropensity	First- and second-order inclusion probabilities, ${\pi }_i$ and ${\pi }_{ij}$.
Design.var, Design.cov	Design-based variance and covariance of a statistic.
Design.probOf	The probability of an event on assignments.
bernoulliDesign	Each unit independently treated with probability p.
completeRandomization	Uniform over assignments of exactly n₁ treated units.
completeRandomization_propensity	${\pi }_i=n_1/n$, for every unit, with no lower bound on n₁.
completeRandomization_jointPropensity	${\pi }_{ij}=n_1(n_1-1)/(n(n-1))$ for $i\ne j$.

MrCLean/Estimators.lean — unbiasedness

Name	What it is
HT	The Horvitz–Thompson estimator: inverse-propensity-weighted outcomes.
DiM	The difference-in-means estimator.
HT_unbiased	$\mathbb{E}[\mathrm{HT}]=\tau$ under any design with for every unit.
DiM_unbiased_completeRandomization	$\mathbb{E}[\mathrm{DiM}]=\tau$ under complete randomization with .

MrCLean/Variance.lean — variance

Name	What it is
fpVar, fpCov	Finite-population variance and covariance, ∑(v - mean v)² / (n - 1) and its two-argument analogue.
Population.S1sq, S0sq, Stausq	fpVar of y1, y0, and the treatment effect — the $S_1^2,S_0^2,S_{\tau }^2$ of Neyman’s formula.
neyman_variance	$\mathrm{Var}(\mathrm{DiM})=S_1^2/n_1+S_0^2/n_0-S_{\tau }^2/n$ under complete randomization.
neymanVarEst	The usual variance estimator, s1²/n1 + s0²/n0.
neymanVarEst_bias	$\mathbb{E}[\hat{v}]=\mathrm{Var}(\mathrm{DiM})+S_{\tau }^2/n$ — the estimator is conservative, and the bias is identified exactly.

MrCLean/Blocking.lean — blocking and clustering

Name	What it is
Design.map	Pushforward of a design along a map of assignments — the tool both designs below are built from.
stratifiedDesign	Complete randomization done independently within each block, as a uniform design over the jointly-balanced support.
blockedDiM	The blockwise difference-in-means, reweighted by block size — plain DiM is biased once blocks differ in treated fraction.
blockedDiM_unbiased	$\mathbb{E}[\mathrm{blockedDiM}]=\tau$ under the stratified design.
clusterDesign	Any design on the clusters, pushed down to unit-level assignments by treating every member of a treated cluster. clusterHT_unbiased specialises it to complete randomization of the clusters.
clusterHT_unbiased	$\mathbb{E}[\mathrm{HT}]=\tau$ under cluster-randomized assignment.

MrCLean/Regression.lean — regression as linear algebra

Name	What it is
IsOLS	The normal equations, (Xᵀ * X) *ᵥ β = Xᵀ *ᵥ y, stated for any candidate β — no rank condition.
ols	(Xᵀ * X)⁻¹ *ᵥ (Xᵀ *ᵥ y), the closed-form solution (defined even when singular; meaningful only when Xᵀ X is invertible).
simpleMatrix_ols_coeff	The slope on a single treatment dummy, regressed with an intercept, equals DiM — a finite algebraic identity, no asymptotics.
ols_simpleMatrix_unbiased_completeRandomization	That regression coefficient is unbiased under complete randomization — inherited from DiM_unbiased_completeRandomization.
groupMatrix_ols_coeff	Regression on group dummies alone recovers each group’s mean.
isOLS_interactedMatrix_iff	The decoupling lemma: fully-interacted (Lin) regression is equivalent to two separate simple regressions, one per treatment arm.
lin_coeff	The treatment coefficient in Lin’s fully-interacted regression, as an exact finite-sample identity.

MrCLean/Fisher.lean — Fisher randomization tests

Name	What it is
SharpNull	∀ i, P.y1 i = P.y0 i — every unit’s effect is exactly zero.
Design.probEvent	The design’s probability of an event on assignments (a renamed probOf, used throughout the Fisher chapter).
pValue	D.probEvent (fun z => T z₀ ≤ T z) — the fraction of the randomization distribution at least as extreme as what was observed.
pValue_valid	$Pr(p\text{-value}\le \alpha )\le \alpha$, for any test statistic, as a finite counting fact.
randomization_test_valid	The same, with the statistic built from the observed data under the sharp null — the form you actually run.

MrCLean/Bridge.lean — bridge to Mathlib probability

Name	What it is
Design.toPMF, PMF.toDesign	The round-trip between this library’s Design and Mathlib’s PMF.
Design.integral_toMeasure	∫ z, f z ∂μ = D.expect f — the two notions of expectation agree.
Design.variance_toMeasure	ProbabilityTheory.variance f μ = D.var f.
HT_unbiased_integral, DiM_unbiased_completeRandomization_integral	This chapter’s two theorems, restated in measure-theoretic language — same proofs, translated statements.
bernoulli_iIndepSet_treated, bernoulli_iIndepFun_Z	Independence of treatment across units under the Bernoulli design, in Mathlib’s iIndepSet/iIndepFun vocabulary.