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 lean/MrCLean/, 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 this library’s compiled theorems.
axiom	A trusted, unproven assumption	Every Lean development rests on a short axiom list — propext, Classical.choice, Quot.sound here, see how this site is verified. #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”	Unused anywhere in this library: every Design is a finite discrete probability space, so a probability-zero set is literally empty, and every statement holds everywhere, not merely a.e.

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	Complete randomization at the cluster level, pushed down to unit-level assignments.
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 this file).
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.