Bridge to Mathlib's probability

Everything so far has been a finite sum. A design is a list of $2^{n}$ numbers that add to one, an expectation is $\sum_{z} Pr (z) f (z)$ , and linearity of expectation is a simp only with three lemmas in it. That was a deliberate choice, and for design-based inference it costs nothing: there is no superpopulation, no limit, no continuum, so there is nothing for measure theory to do.

Mathlib does not know that. Mathlib states probability the way probabilists state it — measurable spaces, measures, Bochner integrals — and so does almost every autoformalized statistics statement you will ever be handed, because the model has read the same library. If someone shows you

theorem tau_hat_unbiased : μ[fun ω => tauHat ω] = tau

you need to know that μ[·] is an integral, that the integral is unbiasedness and not something else, and which of the four decorations around it are load bearing.

This chapter is the dictionary. Nothing in it is new mathematics: every theorem below is one of the theorems you already have, composed with a translation lemma. That is the point. The translation is the content.

It is also the last chapter of Part II. The previous one took the elementary machinery in the opposite direction — partial identification, where the ATE is not a number but an interval, and the theorems are order-theoretic facts about a fixed population. This one keeps the theorems fixed and changes the language. Between them they mark the two edges of what the finite-population setup can be made to say: how little you can assume and still conclude something, and how the little you assumed looks once it is written the way the rest of the world writes it.

The σ-algebra you never think about

A measure space needs a σ-algebra, and Assignment n = Finset (Fin n) is a finite type with $2^{2^{n}}$ subsets. There is exactly one sensible choice: take all of them.

Every subset is an event, every function is measurableNew tabOpens with 1,067 lines of library preamble — the code above is at the bottom of the editor.

/-- The σ-algebra on assignments: **all** subsets are events.

A finite probability space carries no interesting measurability structure, so we take the
largest σ-algebra, `⊤`.  Every subset of `Assignment n` is then measurable and every function
out of `Assignment n` is measurable, which is why no measurability hypothesis appears
anywhere below. -/
instance instMeasurableSpaceAssignment : MeasurableSpace (Assignment n) := ⊤

/-- Every set of assignments is an event. -/
theorem measurableSet_assignment (s : Set (Assignment n)) : MeasurableSet s := trivial

/-- Singletons are events, which is what lets us read probabilities off the pmf. -/
instance instMeasurableSingletonClassAssignment :
    MeasurableSingletonClass (Assignment n) :=
  ⟨fun z => measurableSet_assignment {z}⟩

/-- Every real-valued statistic of the assignment is measurable. -/
theorem measurable_of_assignment (f : Assignment n → ℝ) : Measurable f :=
  measurable_from_top

MeasurableSpace α is a typeclass — a structure Lean carries around implicitly and finds by instance search — so declaring instMeasurableSpaceAssignment once means every later statement about assignments silently uses ⊤, the largest σ-algebra. Two consequences, and they are the reason this chapter is short:

measurableSet_assignment proves MeasurableSet s for any s, by trivial: in the ⊤ σ-algebra the predicate MeasurableSet is True.
measurable_of_assignment proves Measurable f for any f, by measurable_from_top.

So every measurability side condition in every Mathlib probability lemma discharges automatically here. When you read a statement about a finite randomization distribution and it is festooned with Measurable, AEStronglyMeasurable and MeasurableSet hypotheses, none of them are doing mathematical work — but you still have to check they are satisfiable, which they are only if the σ-algebra is the one you think it is. More on that at the end.

`ℝ≥0∞`, and why probabilities live in it

Mathlib measures take values in ℝ≥0∞ (ENNReal), the interval $[0, \infty]$ with a point at infinity attached. The reason is that a measure must be able to say “this set is infinite” as a value rather than as an error, and must be countably additive without side conditions. The cost is that ℝ≥0∞ is not a field: subtraction is truncated, $\infty - \infty = 0$ , and division is a convention.

Five facts about ℝ≥0∞ that will bite youNew tabOpens with 1,373 lines of library preamble — the code above is at the bottom of the editor.

/- `ℝ≥0∞` is `[0, ∞]`.  Everything below is total — no side conditions, no
partiality — which is exactly why measure theory is stated in it, and exactly
why arithmetic done in it does not behave like arithmetic in `ℝ`. -/

/-- `ofReal` and `toReal` are inverse on `[0, ∞)`, which is where probabilities live. -/
example (x : ℝ) (hx : 0 ≤ x) : (ENNReal.ofReal x).toReal = x :=
  ENNReal.toReal_ofReal hx

/-- `ofReal` clamps: a negative real becomes `0` rather than an error. -/
example : ENNReal.ofReal (-2 : ℝ) = 0 := by simp

/-- **`toReal` of `∞` is `0`.**  The trap: `μ s = ∞` and `μ s = 0` are different
statements about the measure but give the *same* real number. -/
example : (⊤ : ℝ≥0∞).toReal = 0 := ENNReal.toReal_top

/-- Subtraction is truncated, so `a - b + b = a` is false in general. -/
example : (1 : ℝ≥0∞) - 2 = 0 := tsub_eq_zero_of_le (by norm_num)

/-- Addition, at least, matches `ℝ` on nonnegative arguments. -/
example (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) :
    ENNReal.ofReal (x + y) = ENNReal.ofReal x + ENNReal.ofReal y :=
  ENNReal.ofReal_add hx hy

The two conversions are ENNReal.ofReal : ℝ → ℝ≥0∞, which clamps negatives to 0, and ENNReal.toReal : ℝ≥0∞ → ℝ, which sends ∞ to 0. They are mutually inverse exactly on $[0, \infty)$ , which is where probabilities live, so for us they are harmless — but toReal ∞ = 0 is a trap worth memorizing now, because it means a real-valued conclusion can be silently true for the wrong reason.

Measure.real μ s, written μ.real s, is just (μ s).toReal. It is the thing a statistician means by “the probability of $s$ ”, and it is the form in which I state everything real-valued below.

A design is a probability mass function

Mathlib’s PMF α is a function α → ℝ≥0∞ whose unconditional sum (tsum, written ∑') is 1. Our Design n carries the same data over ℝ, with nonnegativity as a separate field. The translation in one direction is ENNReal.ofReal:

Design → PMFNew tabOpens with 1,089 lines of library preamble — the code above is at the bottom of the editor.

/-- **A `Design` is a `PMF`.**

Mathlib's `PMF α` is a function `α → ℝ≥0∞` whose *unconditional* sum (`tsum`, `∑'`) is `1`.
Our `Design` carries the same data over `ℝ`, with nonnegativity as a separate field.  The
translation is `ENNReal.ofReal`, and the sum condition transfers because the index type is
finite: an unconditional sum over a `Fintype` is just a `Finset.sum` (`hasSum_fintype`), and
`ENNReal.ofReal` turns a sum of nonnegative reals into a sum in `ℝ≥0∞`. -/
noncomputable def Design.toPMF (D : Design n) : PMF (Assignment n) :=
  ⟨fun z => ENNReal.ofReal (D.prob z), by
    have h : HasSum (fun z : Assignment n => ENNReal.ofReal (D.prob z))
        (∑ z, ENNReal.ofReal (D.prob z)) := hasSum_fintype _
    rwa [← ENNReal.ofReal_sum_of_nonneg fun z _ => D.nonneg z, D.sum_one,
      ENNReal.ofReal_one] at h⟩

The proof obligation is the sum condition, and the whole of it is bookkeeping: hasSum_fintype says an unconditional sum over a Fintype is the corresponding Finset.sum, ENNReal.ofReal_sum_of_nonneg moves ofReal across a sum of nonnegative reals, and then D.sum_one finishes. rwa is rw followed by assumption — rewrite the hypothesis h until it is the goal.

The reverse direction reads the probabilities off with toReal:

PMF → DesignNew tabOpens with 1,112 lines of library preamble — the code above is at the bottom of the editor.

/-- **A `PMF` on assignments is a `Design`.**

The reverse translation: read off the probabilities with `ENNReal.toReal`.  The sum condition
comes from `PMF.tsum_coe` (the `tsum` is `1`), `tsum_fintype` (a `tsum` over a finite type is
a `Finset.sum`), and `ENNReal.toReal_sum`, whose hypothesis "no summand is `∞`" is supplied
by `PMF.apply_ne_top`.

A Lean nicety: this declaration is `MrCLean.PMF.toDesign`, not `PMF.toDesign`, so the dot
notation `p.toDesign` does **not** work — write `PMF.toDesign p`.  (Dot notation resolves the
head symbol of the type, `PMF`, in the root namespace only.) -/
noncomputable def PMF.toDesign (p : PMF (Assignment n)) : Design n where
  prob z := (p z).toReal
  nonneg _ := ENNReal.toReal_nonneg
  sum_one := by
    have h : ∑ z, p z = (1 : ℝ≥0∞) := by rw [← p.tsum_coe, tsum_fintype]
    rw [← ENNReal.toReal_sum fun z _ => p.apply_ne_top z, h, ENNReal.toReal_one]

The two translations are inverse, which is what licenses calling them “the same object in two notations”. Both round trips are one-liners once you have extensionality for designs.

ExerciseWarm-up: the round trip on a single probability

Design.toPMF_apply unfolds the pmf to ENNReal.ofReal (D.prob z), and ENNReal.toReal_ofReal needs exactly the nonnegativity that a Design carries in its nonneg field. One rw with two lemmas in it.

New tabOpens with 1,106 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (warm-up).  Going into `ℝ≥0∞` and back is the identity, because probabilities
are nonnegative and finite.  `ENNReal.toReal_ofReal` is the lemma you want. -/
@[simp] theorem Design.toPMF_apply_toReal (D : Design n) (z : Assignment n) :
    (D.toPMF z).toReal = D.prob z := by
  sorry

Show solution

New tabOpens with 1,106 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (warm-up).  Going into `ℝ≥0∞` and back is the identity, because probabilities
are nonnegative and finite.  `ENNReal.toReal_ofReal` is the lemma you want. -/
@[simp] theorem Design.toPMF_apply_toReal (D : Design n) (z : Assignment n) :
    (D.toPMF z).toReal = D.prob z := by
  rw [Design.toPMF_apply, ENNReal.toReal_ofReal (D.nonneg z)]

ExerciseCore: both round trips

Two proofs. For Design.toPMF_toDesign, ext z reduces equality of designs to equality of probabilities (that is what the @[ext] attribute on Design.ext buys), and the previous exercise is then exactly the goal. For PMF.toDesign_toPMF, PMF.ext plays the same role, and the round trip runs the other way: ENNReal.ofReal_toReal needs p z ≠ ∞, which is PMF.apply_ne_top.

New tabOpens with 1,134 lines of library preamble — the code above is at the bottom of the editor.

/-- **Extensionality for designs**: two designs with the same probabilities are equal.

The `nonneg` and `sum_one` fields are propositions, so proof irrelevance makes them
automatically equal once the `prob` fields agree. -/
@[ext] theorem Design.ext {D D' : Design n} (h : ∀ z, D.prob z = D'.prob z) : D = D' := by
  cases D; cases D'
  congr 1
  funext z
  exact h z

/-- Exercise (core).  Design → PMF → Design is the identity. -/
@[simp] theorem Design.toPMF_toDesign (D : Design n) : PMF.toDesign D.toPMF = D := by
  sorry

/-- Exercise (core).  PMF → Design → PMF is the identity.  Here the round trip is
`ENNReal.ofReal ((p z).toReal) = p z`, which needs `p z ≠ ∞` (`PMF.apply_ne_top`). -/
@[simp] theorem PMF.toDesign_toPMF (p : PMF (Assignment n)) : (PMF.toDesign p).toPMF = p := by
  sorry

Show solution

New tabOpens with 1,134 lines of library preamble — the code above is at the bottom of the editor.

/-- **Extensionality for designs**: two designs with the same probabilities are equal.

The `nonneg` and `sum_one` fields are propositions, so proof irrelevance makes them
automatically equal once the `prob` fields agree. -/
@[ext] theorem Design.ext {D D' : Design n} (h : ∀ z, D.prob z = D'.prob z) : D = D' := by
  cases D; cases D'
  congr 1
  funext z
  exact h z

/-- Exercise (core).  Design → PMF → Design is the identity. -/
@[simp] theorem Design.toPMF_toDesign (D : Design n) : PMF.toDesign D.toPMF = D := by
  ext z
  exact D.toPMF_apply_toReal z

/-- Exercise (core).  PMF → Design → PMF is the identity.  Here the round trip is
`ENNReal.ofReal ((p z).toReal) = p z`, which needs `p z ≠ ∞` (`PMF.apply_ne_top`). -/
@[simp] theorem PMF.toDesign_toPMF (p : PMF (Assignment n)) : (PMF.toDesign p).toPMF = p := by
  refine PMF.ext fun z => ?_
  rw [Design.toPMF_apply, PMF.toDesign_prob, ENNReal.ofReal_toReal (p.apply_ne_top z)]

From pmf to measure

PMF.toMeasure turns a pmf into a genuine Measure by summing the mass over a set: p.toMeasure s = ∑' z, s.indicator p z, promoted from an outer measure. With the ⊤ σ-algebra every set is measurable, so the outer measure and the measure agree everywhere and no subtleties survive. I write $μ$ for D.toPMF.toMeasure throughout.

That $μ$ is a probability measure is registered as an instance, so IsProbabilityMeasure μ — the typeclass that most Mathlib probability lemmas require — is available without being asked for.

ExerciseWarm-up: total mass one, as a real number

Design.toMeasure_univ is μ Set.univ = 1 in ℝ≥0∞. To get the real-valued version, unfold μ.real with measureReal_def and push toReal through with ENNReal.toReal_one. Three rewrites, in that order.

New tabOpens with 1,398 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (warm-up).  The total mass is `1`, as a *real* number.

`Design.toMeasure_univ` gives `μ Set.univ = 1` in `ℝ≥0∞`; `measureReal_def`
unfolds `μ.real s` to `(μ s).toReal`, and `ENNReal.toReal_one` finishes. -/
theorem measureReal_univ (D : Design n) :
    (D.toPMF.toMeasure).real (Set.univ : Set (Assignment n)) = 1 := by
  sorry

Show solution

New tabOpens with 1,398 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (warm-up).  The total mass is `1`, as a *real* number.

`Design.toMeasure_univ` gives `μ Set.univ = 1` in `ℝ≥0∞`; `measureReal_def`
unfolds `μ.real s` to `(μ s).toReal`, and `ENNReal.toReal_one` finishes. -/
theorem measureReal_univ (D : Design n) :
    (D.toPMF.toMeasure).real (Set.univ : Set (Assignment n)) = 1 := by
  rw [measureReal_def, D.toMeasure_univ, ENNReal.toReal_one]

ExerciseWarm-up: the probability of a single assignment

Same shape as the previous exercise, but the value is D.prob z rather than 1, so the last step is ENNReal.toReal_ofReal with D.nonneg z.

New tabOpens with 1,172 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (warm-up).  The measure of a single assignment, as a real number, is exactly
`D.prob z`.  `Measure.real μ s` is notation for `(μ s).toReal`; unfold it with
`measureReal_def`. -/
theorem Design.measureReal_singleton (D : Design n) (z : Assignment n) :
    (D.toPMF.toMeasure).real {z} = D.prob z := by
  sorry

Show solution

New tabOpens with 1,172 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (warm-up).  The measure of a single assignment, as a real number, is exactly
`D.prob z`.  `Measure.real μ s` is notation for `(μ s).toReal`; unfold it with
`measureReal_def`. -/
theorem Design.measureReal_singleton (D : Design n) (z : Assignment n) :
    (D.toPMF.toMeasure).real {z} = D.prob z := by
  rw [measureReal_def, D.toMeasure_singleton, ENNReal.toReal_ofReal (D.nonneg z)]

An event was a decidable predicate on assignments, and its probability was a sum over a Finset.filter. In Mathlib an event is a set and its probability is the measure of that set. Design.toMeasure_setOf is the bridge, and the propensity score comes out as the special case you would guess:

Events are sets; the propensity is the measure of oneNew tabOpens with 1,185 lines of library preamble — the code above is at the bottom of the editor.

/-- **`Design.probOf` is the measure of the corresponding set.**

An "event" in the tutorial is a decidable predicate on assignments and its probability is a
sum over a `Finset.filter`; an event in Mathlib is a set and its probability is the measure of
that set.  `PMF.toMeasure_apply_finset` is what connects the two. -/
theorem Design.toMeasure_setOf (D : Design n) (p : Assignment n → Prop) [DecidablePred p] :
    D.toPMF.toMeasure {z | p z} = ENNReal.ofReal (D.probOf p) := by
  have hset : ({z | p z} : Set (Assignment n)) = ↑((univ : Finset (Assignment n)).filter p) := by
    ext z
    simp only [Set.mem_ofPred_eq, Finset.coe_filter, Finset.mem_univ, true_and]
  rw [hset, PMF.toMeasure_apply_finset, Design.probOf,
    ENNReal.ofReal_sum_of_nonneg fun z _ => D.nonneg z]
  exact Finset.sum_congr rfl fun z _ => D.toPMF_apply z

/-- The real-valued version: `μ.real {z | p z} = D.probOf p`. -/
theorem Design.measureReal_setOf (D : Design n) (p : Assignment n → Prop) [DecidablePred p] :
    (D.toPMF.toMeasure).real {z | p z} = D.probOf p := by
  rw [measureReal_def, D.toMeasure_setOf, ENNReal.toReal_ofReal (D.probOf_nonneg p)]

/-- **The propensity score is the measure of the event "unit `i` is treated"**, which is how
an autoformalized statement would write it. -/
theorem Design.measureReal_treated (D : Design n) (i : Fin n) :
    (D.toPMF.toMeasure).real {z : Assignment n | i ∈ z} = D.propensity i := by
  rw [D.measureReal_setOf, D.propensity_eq_probOf]

Read Design.measureReal_treated slowly, because it is the single most useful line in the file for reading other people’s Lean:

μ ({z ∣ i \in z}) = π_{i} .

The left-hand side is how an autoformalization will write “the probability that unit $i$ is treated”; the right-hand side is what a design-based statistician calls the propensity score. They are the same number, and the proof is two rewrites. (In Lean it is μ.real, not μ, because the right-hand side is a real number and the left-hand side would otherwise be an ℝ≥0∞.)

The second-order version is worth doing yourself, because joint propensities are where designs actually differ from one another.

ExerciseCore: the joint propensity is the measure of an intersection

The displayed lemma does the elementary work: Z z i * Z z j is the indicator of “both treated”, so Design.expect_indicator converts it into a probOf. The by_cases hi : i ∈ z <;> by_cases hj : j ∈ z splits into the four membership cases and simp [Z, hi, hj] closes each by computing the indicator. The exercise is then one rewrite with Design.measureReal_setOf and one with the lemma above.

New tabOpens with 1,418 lines of library preamble — the code above is at the bottom of the editor.

/-- The joint propensity is the probability of the event "`i` and `j` are both
treated".  The proof is the same two steps as `Design.propensity_eq_probOf`:
`Z z i * Z z j` is the indicator of that event, and the expectation of an
indicator is a probability. -/
theorem jointPropensity_eq_probOf (D : Design n) (i j : Fin n) :
    D.jointPropensity i j = D.probOf (fun z => i ∈ z ∧ j ∈ z) := by
  rw [Design.jointPropensity, ← D.expect_indicator (fun z => i ∈ z ∧ j ∈ z)]
  refine D.expect_congr fun z => ?_
  by_cases hi : i ∈ z <;> by_cases hj : j ∈ z <;> simp [Z, hi, hj]

/-- Exercise (core).  **The joint propensity is the measure of the event.**

One rewrite with `Design.measureReal_setOf` (which turns `μ.real {z | p z}` into
`D.probOf p`) and one with the lemma just above. -/
theorem measureReal_both_treated (D : Design n) (i j : Fin n) :
    (D.toPMF.toMeasure).real {z : Assignment n | i ∈ z ∧ j ∈ z}
      = D.jointPropensity i j := by
  sorry

Show solution

New tabOpens with 1,418 lines of library preamble — the code above is at the bottom of the editor.

/-- The joint propensity is the probability of the event "`i` and `j` are both
treated".  The proof is the same two steps as `Design.propensity_eq_probOf`:
`Z z i * Z z j` is the indicator of that event, and the expectation of an
indicator is a probability. -/
theorem jointPropensity_eq_probOf (D : Design n) (i j : Fin n) :
    D.jointPropensity i j = D.probOf (fun z => i ∈ z ∧ j ∈ z) := by
  rw [Design.jointPropensity, ← D.expect_indicator (fun z => i ∈ z ∧ j ∈ z)]
  refine D.expect_congr fun z => ?_
  by_cases hi : i ∈ z <;> by_cases hj : j ∈ z <;> simp [Z, hi, hj]

/-- Exercise (core).  **The joint propensity is the measure of the event.**

One rewrite with `Design.measureReal_setOf` (which turns `μ.real {z | p z}` into
`D.probOf p`) and one with the lemma just above. -/
theorem measureReal_both_treated (D : Design n) (i j : Fin n) :
    (D.toPMF.toMeasure).real {z : Assignment n | i ∈ z ∧ j ∈ z}
      = D.jointPropensity i j := by
  rw [D.measureReal_setOf, jointPropensity_eq_probOf]

Expectation is integration

Here is the lemma the rest of the chapter is a corollary of.

The finite sum is the Bochner integralNew tabOpens with 1,212 lines of library preamble — the code above is at the bottom of the editor.

/-- **The finite weighted sum `D.expect f` is the Bochner integral against `μ`.**

This is the single lemma that makes the rest of the file one-liners.  `PMF.integral_eq_sum`
does the work: on a finite space the integral against a pmf's measure is
`∑ z, (p z).toReal • f z`, and `(D.toPMF z).toReal` is `D.prob z`.

Read it in either direction: left to right it lets you compute a Mathlib integral by an
elementary sum; right to left it lets you state an elementary theorem in Mathlib's language. -/
@[simp] theorem Design.integral_toMeasure (D : Design n) (f : Assignment n → ℝ) :
    ∫ z, f z ∂(D.toPMF.toMeasure) = D.expect f := by
  rw [PMF.integral_eq_sum]
  refine Finset.sum_congr rfl fun z _ => ?_
  rw [smul_eq_mul, D.toPMF_apply_toReal]

∫ z, f z ∂μ is Mathlib’s Bochner integral: it is defined by approximation with simple functions, it is 0 by convention when f is not integrable, and on a finite space it collapses to a finite weighted sum. PMF.integral_eq_sum does that collapse for us — it needs Fintype and MeasurableSingletonClass, both of which the σ-algebra section supplied — and the remaining step is (D.toPMF z).toReal = D.prob z, the warm-up exercise from earlier.

The theorem is tagged @[simp], so from here on simp turns any integral against a design’s measure into an elementary expectation. Design.expect_eq_integral is the same fact in the other direction and in the notation Mathlib prefers: μ[f], which is defined as ∫ z, f z ∂μ. When you see μ[f] in an autoformalized statement, read it as $E_{μ} [f]$ and remember that it is a Bochner integral with all the conventions that implies.

ExerciseCore: E[Z_i] = π_i, in Mathlib's vocabulary

Design.integral_toMeasure turns the goal into a statement about D.expect (fun z => Z z i), and Design.expect_Z says that is the propensity — by rfl, since that is how propensity was defined. Two lines.

New tabOpens with 1,408 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (core).  **The propensity score is the integral of the treatment
indicator.**  This is `E[Z_i] = π_i` in Mathlib's vocabulary.

Rewrite with `Design.integral_toMeasure` to turn the integral into
`D.expect (fun z => Z z i)`, and then `Design.expect_Z` is the definition. -/
theorem integral_Z (D : Design n) (i : Fin n) :
    ∫ z, Z z i ∂(D.toPMF.toMeasure) = D.propensity i := by
  sorry

Show solution

New tabOpens with 1,408 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (core).  **The propensity score is the integral of the treatment
indicator.**  This is `E[Z_i] = π_i` in Mathlib's vocabulary.

Rewrite with `Design.integral_toMeasure` to turn the integral into
`D.expect (fun z => Z z i)`, and then `Design.expect_Z` is the definition. -/
theorem integral_Z (D : Design n) (i : Fin n) :
    ∫ z, Z z i ∂(D.toPMF.toMeasure) = D.propensity i := by
  rw [D.integral_toMeasure]
  exact D.expect_Z i

Variance transfers just as cleanly, though the definition on the Mathlib side takes a detour. ProbabilityTheory.variance f μ, written Var[f; μ], is defined as (evariance f μ).toReal, where evariance is an ℝ≥0∞-valued Lebesgue integral — so that it exists for any function whatsoever, integrable or not. variance_eq_integral recovers the familiar $\int (f - μ [f])^{2}$ as soon as f is a.e.-measurable, which here is free. Keep the detour in mind: it is the subject of one of the pitfalls at the end of the chapter.

ExerciseStretch: Var[f; μ] is Design.var

Rewrite with variance_eq_integral, whose hypothesis is discharged by (measurable_of_assignment f).aemeasurable. Then note that after that rewrite there are two integrals against μ: the outer one and the mean μ[f] sitting inside it. That is why the next step is simp only [Design.integral_toMeasure] rather than a single rw, which would only fire on the first occurrence. What remains is Design.var unfolded, so rfl closes it.

New tabOpens with 1,237 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (stretch).  **`Design.var` is Mathlib's `ProbabilityTheory.variance`.**

`variance f μ` is defined through an `ℝ≥0∞`-valued `evariance`, but
`ProbabilityTheory.variance_eq_integral` gives the familiar `∫ (f - μ[f])²` as soon as `f` is
a.e.-measurable — which here is free.  After that, rewriting with `Design.integral_toMeasure`
twice (once for the outer integral, once for the mean inside it) lands on `Design.var`. -/
theorem Design.variance_toMeasure (D : Design n) (f : Assignment n → ℝ) :
    variance f (D.toPMF.toMeasure) = D.var f := by
  sorry

Show solution

New tabOpens with 1,237 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (stretch).  **`Design.var` is Mathlib's `ProbabilityTheory.variance`.**

`variance f μ` is defined through an `ℝ≥0∞`-valued `evariance`, but
`ProbabilityTheory.variance_eq_integral` gives the familiar `∫ (f - μ[f])²` as soon as `f` is
a.e.-measurable — which here is free.  After that, rewriting with `Design.integral_toMeasure`
twice (once for the outer integral, once for the mean inside it) lands on `Design.var`. -/
theorem Design.variance_toMeasure (D : Design n) (f : Assignment n → ℝ) :
    variance f (D.toPMF.toMeasure) = D.var f := by
  rw [variance_eq_integral (measurable_of_assignment f).aemeasurable]
  simp only [Design.integral_toMeasure]
  rfl

The headline theorems, restated

With Design.integral_toMeasure in hand, the payoff theorems of Part II restate themselves. Horvitz–Thompson first:

HT unbiasedness, in measure-theoretic clothingNew tabOpens with 1,251 lines of library preamble — the code above is at the bottom of the editor.

/-- **Horvitz–Thompson is unbiased, stated with an integral.**

`∫ z, HT D P z ∂μ = τ`, where `μ` is the measure of the design.  This is the form you would
find in an autoformalized paper; it is `HT_unbiased` composed with
`Design.integral_toMeasure`, and nothing else. -/
theorem HT_unbiased_integral (D : Design n) (P : Population n)
    (hlo : ∀ i, 0 < D.propensity i) (hhi : ∀ i, D.propensity i < 1) :
    ∫ z, HT D P z ∂(D.toPMF.toMeasure) = P.tau := by
  rw [D.integral_toMeasure]
  exact HT_unbiased D P hlo hhi

Two lines: rewrite the integral into an expectation, quote HT_unbiased. The mathematical content was done in the unbiasedness chapter and none of it is repeated here — which is exactly the claim this chapter is making. A measure-theoretic statement about a finite design is a notational variant of a finite sum identity, and if it were anything more, the proof could not be two lines.

ExerciseCore: difference in means, with an integral

Identical in shape to HT_unbiased_integral: one rw [Design.integral_toMeasure] and then exact the core theorem DiM_unbiased_completeRandomization applied to its three hypotheses. Note the hypotheses are unchanged by the translation — the measure-theoretic version needs $0 < n_{1} < n$ for exactly the same reason the elementary one does, namely that DiM divides by $n_{1}$ and $n_{0}$ .

New tabOpens with 1,262 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (core).  **Difference-in-means is unbiased under complete randomisation**, with
an integral.  Rewrite with `Design.integral_toMeasure` and quote the core theorem. -/
theorem DiM_unbiased_completeRandomization_integral {n₁ : ℕ} (hle : n₁ ≤ n) (P : Population n)
    (hpos : 0 < n₁) (hlt : n₁ < n) :
    ∫ z, DiM P z ∂((completeRandomization n n₁ hle).toPMF.toMeasure) = P.tau := by
  sorry

Show solution

New tabOpens with 1,262 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (core).  **Difference-in-means is unbiased under complete randomisation**, with
an integral.  Rewrite with `Design.integral_toMeasure` and quote the core theorem. -/
theorem DiM_unbiased_completeRandomization_integral {n₁ : ℕ} (hle : n₁ ≤ n) (P : Population n)
    (hpos : 0 < n₁) (hlt : n₁ < n) :
    ∫ z, DiM P z ∂((completeRandomization n n₁ hle).toPMF.toMeasure) = P.tau := by
  rw [Design.integral_toMeasure]
  exact DiM_unbiased_completeRandomization hle P hpos hlt

Independence, at last

Design-based inference does not need independence anywhere — that is one of its selling points — but Mathlib’s probability library is largely about independence, and the Bernoulli design is the one place in this tutorial where it genuinely holds. It is worth seeing the vocabulary on an example you can already compute.

The treatment events are mutually independentNew tabOpens with 1,289 lines of library preamble — the code above is at the bottom of the editor.

/-- **Under the Bernoulli design the events "unit `i` is treated" are mutually independent.**

`ProbabilityTheory.iIndepSet` is Mathlib's *mutual* (not merely pairwise) independence for a
family of events, and `iIndepSet_iff_meas_biInter` reduces it to exactly one identity: for
every finite set `S` of units,

`μ (⋂ i ∈ S, {z | i ∈ z}) = ∏ i ∈ S, μ {z | i ∈ z}`.

The left-hand side is the event "all of `S` is treated", whose probability is the inclusion
probability `p ^ #S` (`bernoulli_inclusion`); the right-hand side is `p` multiplied by itself
`#S` times.  So the whole of mutual independence is the one counting lemma the Bernoulli
chapter already proved. -/
theorem bernoulli_iIndepSet_treated {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    iIndepSet (fun i : Fin n => {z : Assignment n | i ∈ z})
      ((bernoulliDesign n p hp0 hp1).toPMF.toMeasure) := by
  classical
  set D := bernoulliDesign n p hp0 hp1 with hD
  rw [iIndepSet_iff_meas_biInter fun i => measurableSet_assignment _]
  intro S
  -- "every unit of `S` is treated" is the event `S ⊆ z`
  have hInter : (⋂ i ∈ S, {z : Assignment n | i ∈ z}) = {z : Assignment n | S ⊆ z} := by
    ext z
    simp [Finset.subset_iff]
  have hleft : D.toPMF.toMeasure (⋂ i ∈ S, {z : Assignment n | i ∈ z})
      = ENNReal.ofReal (p ^ #S) := by
    rw [hInter, D.toMeasure_setOf, ← D.inclusion_eq_probOf, hD, bernoulli_inclusion]
  have hright : ∀ i : Fin n,
      D.toPMF.toMeasure {z : Assignment n | i ∈ z} = ENNReal.ofReal p := by
    intro i
    rw [D.toMeasure_setOf, ← D.propensity_eq_probOf, hD, bernoulli_propensity]
  rw [hleft, Finset.prod_congr rfl fun i _ => hright i, Finset.prod_const,
    ENNReal.ofReal_pow hp0]

ProbabilityTheory.iIndepSet is mutual independence of a family of events, not pairwise independence. The characterization iIndepSet_iff_meas_biInter says precisely this: for every finite set $S$ of indices,

μ (⋂_{i \in S} A_{i}) = \prod_{i \in S} μ (A_{i}) .

Quantified over all finite $S$ , that is strictly stronger than the $| S | = 2$ case (the standard counterexample: three pairwise independent coin events that are not mutually independent). It is also, for us, exactly the inclusion probability: the left-hand side is the probability that everyone in $S$ is treated, which bernoulli_inclusion computed as $p^{# S}$ , and the right-hand side is $p$ multiplied by itself $# S$ times. Mutual independence came for free from the one counting lemma the designs chapter already proved.

Independence of events upgrades to independence of random variables with one lemma, because our Z is literally an indicator:

The indicators are mutually independent random variablesNew tabOpens with 1,322 lines of library preamble — the code above is at the bottom of the editor.

/-- **Under the Bernoulli design the treatment indicators are mutually independent random
variables.**

`ProbabilityTheory.iIndepFun` is independence of a family of random variables; for indicator
variables it follows from independence of the underlying events
(`iIndepSet.iIndepFun_indicator`).  The only thing to check is that our `Z` really *is* the
indicator of the event "`i` is treated", which is true by definition of both. -/
theorem bernoulli_iIndepFun_Z {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    iIndepFun (fun (i : Fin n) (z : Assignment n) => Z z i)
      ((bernoulliDesign n p hp0 hp1).toPMF.toMeasure) := by
  have hZ : (fun (i : Fin n) (z : Assignment n) => Z z i)
      = fun i : Fin n => ({z : Assignment n | i ∈ z}).indicator fun _ => (1 : ℝ) := by
    funext i z
    by_cases h : i ∈ z <;> simp [Z, h]
  rw [hZ]
  exact (bernoulli_iIndepSet_treated hp0 hp1).iIndepFun_indicator

The funext i z; by_cases h : i ∈ z <;> simp [Z, h] step is the whole proof: it checks that Z z i and Set.indicator {z | i ∈ z} (fun _ => 1) z agree at every point, by computing both branches of the if. Then iIndepSet.iIndepFun_indicator does the rest.

ExerciseCore: independence written out as a product of probabilities

iIndepSet is an abstract predicate; this is the same statement for two units, written the way you would check it by hand. Rewrite the three probabilities into propensities using the exercise from earlier plus Design.measureReal_treated, then quote bernoulli_jointPropensity (which needs $i \neq j$ ) and bernoulli_propensity. Finish by turning $p^{2}$ into $p \cdot p$ with sq.

New tabOpens with 1,437 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (core).  **Independence, spelled out as a product of probabilities.**

`bernoulli_iIndepSet_treated` states mutual independence abstractly; this is the
two-unit case written the way a statistician would check it, with no
`iIndepSet` in sight.  Rewrite the three probabilities into propensities
(`measureReal_both_treated`, `Design.measureReal_treated`) and then quote
`bernoulli_jointPropensity` and `bernoulli_propensity`. -/
theorem bernoulli_measureReal_both {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {i j : Fin n}
    (hij : i ≠ j) :
    ((bernoulliDesign n p hp0 hp1).toPMF.toMeasure).real
        {z : Assignment n | i ∈ z ∧ j ∈ z}
      = ((bernoulliDesign n p hp0 hp1).toPMF.toMeasure).real {z : Assignment n | i ∈ z}
        * ((bernoulliDesign n p hp0 hp1).toPMF.toMeasure).real
            {z : Assignment n | j ∈ z} := by
  sorry

Show solution

New tabOpens with 1,437 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (core).  **Independence, spelled out as a product of probabilities.**

`bernoulli_iIndepSet_treated` states mutual independence abstractly; this is the
two-unit case written the way a statistician would check it, with no
`iIndepSet` in sight.  Rewrite the three probabilities into propensities
(`measureReal_both_treated`, `Design.measureReal_treated`) and then quote
`bernoulli_jointPropensity` and `bernoulli_propensity`. -/
theorem bernoulli_measureReal_both {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {i j : Fin n}
    (hij : i ≠ j) :
    ((bernoulliDesign n p hp0 hp1).toPMF.toMeasure).real
        {z : Assignment n | i ∈ z ∧ j ∈ z}
      = ((bernoulliDesign n p hp0 hp1).toPMF.toMeasure).real {z : Assignment n | i ∈ z}
        * ((bernoulliDesign n p hp0 hp1).toPMF.toMeasure).real
            {z : Assignment n | j ∈ z} := by
  rw [measureReal_both_treated, Design.measureReal_treated, Design.measureReal_treated,
    bernoulli_jointPropensity hij, bernoulli_propensity, bernoulli_propensity, sq]

Side conditions, and what `∀ᵐ` really says

Mathlib’s probability statements carry four decorations that a statistician does not write down. On a finite space three of them are free; knowing why they are free is what lets you check whether a statement you are handed is about the space you think it is.

The four decorationsNew tabOpens with 1,484 lines of library preamble — the code above is at the bottom of the editor.

/-- Every function out of `Assignment n` is strongly measurable, because the
σ-algebra is `⊤`.  This is the hypothesis `AEStronglyMeasurable f μ` that
decorates every Bochner-integral lemma. -/
example (D : Design n) (f : Assignment n → ℝ) :
    AEStronglyMeasurable f (D.toPMF.toMeasure) :=
  (measurable_of_assignment f).aestronglyMeasurable

/-- Every statistic is integrable, because the space is finite. -/
example (D : Design n) (f : Assignment n → ℝ) : Integrable f (D.toPMF.toMeasure) :=
  D.integrable f

/-- The pushforward of a probability measure is a probability measure: this is
the "distribution of the statistic `T`", and Mathlib finds it by instance search. -/
example (D : Design n) (T : Assignment n → ℝ) :
    IsProbabilityMeasure ((D.toPMF.toMeasure).map T) :=
  inferInstance

/-- **Change of variables**, and the one place a measurability hypothesis is
*not* free: `g` maps `ℝ → ℝ`, and the σ-algebra on `ℝ` is the Borel one, not
`⊤`, so `Measurable g` is a real assumption rather than a formality. -/
theorem integral_map_eq (D : Design n) (T : Assignment n → ℝ) {g : ℝ → ℝ}
    (hg : Measurable g) :
    ∫ x, g x ∂((D.toPMF.toMeasure).map T) = D.expect (fun z => g (T z)) := by
  rw [integral_map (measurable_of_assignment T).aemeasurable hg.aestronglyMeasurable,
    Design.integral_toMeasure]

AEStronglyMeasurable f μ is the regularity hypothesis on every Bochner integral: f agrees $μ$ -almost everywhere with a measurable function with separable range. Free here, because every function out of Assignment n is measurable.
Integrable f μ is $\int | f | d μ < \infty$ . Free here, by Integrable.of_finite. It is not free in general, and it matters: the Bochner integral of a non-integrable function is defined to be 0, exactly the way x / 0 = 0. A statement ∫ … = 0 can therefore be true because the integral does not exist.
IsProbabilityMeasure μ is μ Set.univ = 1. Free here, from sum_one.
Measure.map T μ is the pushforward: the distribution of the statistic T, i.e. the randomization distribution. The change-of-variables lemma integral_map is the one place a measurability hypothesis is genuinely needed — g : ℝ → ℝ lives on the Borel σ-algebra, not on ⊤, so Measurable g is a real assumption. Notice the asymmetry: measurability is free going out of our space, never into an arbitrary one.

∀ᵐ z ∂μ, p z means ” $p$ holds almost everywhere”: the set where it fails has measure zero. Mathlib states hypotheses this way because it must work in general. On our space it is nearly the same as ∀ z, p z — but only nearly, and the gap is where mistranslations hide.

ExerciseCore: an a.e. statement says nothing off the support

The easy direction is Filter.Eventually.of_forall. For the converse, start with by_contra hp, then rw [ae_iff] at h turns the hypothesis into μ {w | ¬ p w} = 0. The singleton {z} is a subset of that null set, so measure_mono bounds μ {z} by 0; nonpos_iff_eq_zero turns the bound into an equation, and Design.toMeasure_singleton plus ENNReal.ofReal_pos contradict 0 < D.prob z.

New tabOpens with 1,456 lines of library preamble — the code above is at the bottom of the editor.

/-- A statement true at every assignment is true almost everywhere.  This
direction is free and holds for any measure. -/
theorem ae_of_forall (D : Design n) (p : Assignment n → Prop) (h : ∀ z, p z) :
    ∀ᵐ z ∂(D.toPMF.toMeasure), p z :=
  Filter.Eventually.of_forall h

/-- Exercise (core).  **The converse holds only on the support.**

An `∀ᵐ` hypothesis says nothing at all about assignments the design never
produces; at an assignment with positive probability it does say what you want.
Start with `by_contra`, turn the hypothesis into a statement about a null set
with `ae_iff`, and squeeze `μ {z}` between `0` and that null set with
`measure_mono`.  `Design.toMeasure_singleton` and `ENNReal.ofReal_pos` supply the
contradiction. -/
theorem of_ae_of_prob_pos (D : Design n) (p : Assignment n → Prop)
    (h : ∀ᵐ z ∂(D.toPMF.toMeasure), p z) {z : Assignment n} (hz : 0 < D.prob z) : p z := by
  sorry

Show solution

New tabOpens with 1,456 lines of library preamble — the code above is at the bottom of the editor.

/-- A statement true at every assignment is true almost everywhere.  This
direction is free and holds for any measure. -/
theorem ae_of_forall (D : Design n) (p : Assignment n → Prop) (h : ∀ z, p z) :
    ∀ᵐ z ∂(D.toPMF.toMeasure), p z :=
  Filter.Eventually.of_forall h

/-- Exercise (core).  **The converse holds only on the support.**

An `∀ᵐ` hypothesis says nothing at all about assignments the design never
produces; at an assignment with positive probability it does say what you want.
Start with `by_contra`, turn the hypothesis into a statement about a null set
with `ae_iff`, and squeeze `μ {z}` between `0` and that null set with
`measure_mono`.  `Design.toMeasure_singleton` and `ENNReal.ofReal_pos` supply the
contradiction. -/
theorem of_ae_of_prob_pos (D : Design n) (p : Assignment n → Prop)
    (h : ∀ᵐ z ∂(D.toPMF.toMeasure), p z) {z : Assignment n} (hz : 0 < D.prob z) : p z := by
  by_contra hp
  rw [ae_iff] at h
  have hsub : ({z} : Set (Assignment n)) ⊆ {w | ¬ p w} := by
    intro w hw
    rw [Set.mem_singleton_iff] at hw
    exact hw ▸ hp
  have hle : D.toPMF.toMeasure {z} ≤ 0 := h ▸ measure_mono hsub
  rw [D.toMeasure_singleton, nonpos_iff_eq_zero] at hle
  exact (ENNReal.ofReal_pos.mpr hz).ne' hle

The last piece of vocabulary is ProbabilityTheory.IdentDistrib f g μ ν: “identically distributed”, which unfolds to three things — f is a.e.-measurable, g is a.e.-measurable, and the pushforwards agree, μ.map f = ν.map g. Note what it does not say: nothing about $f$ and $g$ being independent, or defined on the same space.

ExerciseStretch: equal propensities means identically distributed indicators

The two measurability fields are (measurable_of_assignment _).aemeasurable. For map_eq, Measure.ext reduces to μ (f ⁻¹' s) = μ (g ⁻¹' s) for every measurable s ⊆ ℝ, and Measure.map_apply performs the reduction. An indicator takes only two values, so by_cases h1 : (1 : ℝ) ∈ s <;> by_cases h0 : (0 : ℝ) ∈ s gives four cases in which the preimage is Set.univ, {z | k ∈ z}, its complement, or ∅. Each identification is ext z; by_cases hk : k ∈ z <;> simp [Z, hk, h1, h0], and the complement case additionally needs measure_compl.

New tabOpens with 1,512 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (stretch).  **Two units with the same propensity have identically
distributed treatment indicators.**

`IdentDistrib f g μ ν` is three things: `f` is a.e.-measurable, `g` is
a.e.-measurable, and the pushforwards agree, `μ.map f = ν.map g`.  The first two
are free here.  For the third, `Measure.ext` reduces to `μ (f ⁻¹' s) = μ (g ⁻¹' s)`
for every measurable `s ⊆ ℝ`, and `Measure.map_apply` performs that reduction.
An indicator takes only the values `0` and `1`, so there are four cases
according to which of them lie in `s`: the preimage is `univ`, the treated set,
its complement, or `∅`. -/
theorem identDistrib_Z_of_propensity_eq (D : Design n) {i j : Fin n}
    (h : D.propensity i = D.propensity j) :
    IdentDistrib (fun z : Assignment n => Z z i) (fun z : Assignment n => Z z j)
      (D.toPMF.toMeasure) (D.toPMF.toMeasure) := by
  sorry

Show solution

New tabOpens with 1,512 lines of library preamble — the code above is at the bottom of the editor.

/-- Exercise (stretch).  **Two units with the same propensity have identically
distributed treatment indicators.**

`IdentDistrib f g μ ν` is three things: `f` is a.e.-measurable, `g` is
a.e.-measurable, and the pushforwards agree, `μ.map f = ν.map g`.  The first two
are free here.  For the third, `Measure.ext` reduces to `μ (f ⁻¹' s) = μ (g ⁻¹' s)`
for every measurable `s ⊆ ℝ`, and `Measure.map_apply` performs that reduction.
An indicator takes only the values `0` and `1`, so there are four cases
according to which of them lie in `s`: the preimage is `univ`, the treated set,
its complement, or `∅`. -/
theorem identDistrib_Z_of_propensity_eq (D : Design n) {i j : Fin n}
    (h : D.propensity i = D.propensity j) :
    IdentDistrib (fun z : Assignment n => Z z i) (fun z : Assignment n => Z z j)
      (D.toPMF.toMeasure) (D.toPMF.toMeasure) := by
  have hA : ∀ k : Fin n, D.toPMF.toMeasure {z : Assignment n | k ∈ z}
      = ENNReal.ofReal (D.propensity k) := by
    intro k
    rw [D.toMeasure_setOf, D.propensity_eq_probOf]
  refine ⟨(measurable_of_assignment _).aemeasurable,
    (measurable_of_assignment _).aemeasurable, Measure.ext fun s hs => ?_⟩
  rw [Measure.map_apply (measurable_of_assignment _) hs,
    Measure.map_apply (measurable_of_assignment _) hs]
  by_cases h1 : (1 : ℝ) ∈ s <;> by_cases h0 : (0 : ℝ) ∈ s
  · have e : ∀ k : Fin n, ((fun z : Assignment n => Z z k) ⁻¹' s) = Set.univ := by
      intro k; ext z; by_cases hk : k ∈ z <;> simp [Z, hk, h1, h0]
    rw [e i, e j]
  · have e : ∀ k : Fin n,
        ((fun z : Assignment n => Z z k) ⁻¹' s) = {z : Assignment n | k ∈ z} := by
      intro k; ext z; by_cases hk : k ∈ z <;> simp [Z, hk, h1, h0]
    rw [e i, e j, hA i, hA j, h]
  · have e : ∀ k : Fin n,
        ((fun z : Assignment n => Z z k) ⁻¹' s) = {z : Assignment n | k ∈ z}ᶜ := by
      intro k; ext z; by_cases hk : k ∈ z <;> simp [Z, hk, h1, h0]
    rw [e i, e j,
      measure_compl (measurableSet_assignment _) (measure_ne_top _ _),
      measure_compl (measurableSet_assignment _) (measure_ne_top _ _), hA i, hA j, h]
  · have e : ∀ k : Fin n, ((fun z : Assignment n => Z z k) ⁻¹' s) = (∅ : Set (Assignment n)) := by
      intro k; ext z; by_cases hk : k ∈ z <;> simp [Z, hk, h1, h0]
    rw [e i, e j]

Reading autoformalized Lean

You now have the whole vocabulary. Here is how to use it on something you did not write.

Strip an autoformalized unbiasedness claim of its decoration and this is what is left:

DefinitionWhat unbiasedness looks like in the abstract

$E_{μ} [T] = θ$ , and nothing else. Every autoformalized unbiasedness claim is this proposition with $Ω$ , $μ$ , $T$ and $θ$ filled in; the whole question is whether the four of them are what you meant.

New tab

open MeasureTheory in
/-- `T` is unbiased for `θ` under `μ`. -/
def Unbiased {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (T : Ω → ℝ) (θ : ℝ) : Prop :=
∫ ω, T ω ∂μ = θ

Ask a model to formalize “the difference-in-means estimator is unbiased under complete randomization” and you get that proposition dressed in a measure, a typeclass and a hypothesis. A plausible output:

-- plausible, and in fact fine
theorem dim_unbiased {n n₁ : ℕ} (P : Population n) (hpos : 0 < n₁) (hlt : n₁ < n)
    (μ : Measure (Assignment n)) [IsProbabilityMeasure μ]
    (hμ : ∀ z : Assignment n, μ.real {z} = if #z = n₁ then ((n.choose n₁ : ℝ))⁻¹ else 0) :
    μ[fun z => DiM P z] = P.tau := by
  sorry

It is not obviously wrong. Reading it is a matter of checking four things, in this order.

Is the measure a probability measure? [IsProbabilityMeasure μ] says so. Without it nothing rules out μ = 0, against which every integral is 0 and the conclusion reads $0 = τ$ . The typeclass is what makes μ[·] an expectation rather than an arbitrary linear functional.
Is it the right probability measure? This is the check people skip. [IsProbabilityMeasure μ] alone would make the statement a claim about every distribution over assignments, which is plainly false — put all the mass on one assignment and the difference in means is whatever that assignment gives. Here hμ pins $μ$ down to complete randomization, so the statement is the one intended. Whenever the measure is universally quantified, look for the hypothesis that ties it to the design; if there isn’t one, the statement is wrong.
Is the integrand integrable? Here, yes, automatically. In general, a missing Integrable hypothesis can make an integral identity true by the convention $\int = 0$ .
Is the σ-algebra the intended one? The statement above uses whatever MeasurableSpace (Assignment n) instance is in scope. Ours is ⊤. If the file instead opens with variable [MeasurableSpace (Assignment n)], the σ-algebra is an unconstrained parameter, {z} need not be measurable, and hμ may be unsatisfiable — in which case the theorem is vacuous.

And #print axioms dim_unbiased at the end, always, to catch the sorry.

Universally quantified measure, no link to the design

theorem dim_unbiased' {n n₁ : ℕ} (P : Population n) (hpos : 0 < n₁) (hlt : n₁ < n)
    (μ : Measure (Assignment n)) [IsProbabilityMeasure μ] :
    μ[fun z => DiM P z] = P.tau

This is the previous statement with hμ deleted, and it is false: take $μ$ to be a point mass at a single assignment $z$ , and the left side is $\hat{τ} (z)$ , which is not $τ$ in general. The tell is a bound measure variable that appears in the conclusion but in no hypothesis. Design-based unbiasedness is a statement about one specific distribution; a formalization that quantifies over measures without constraining them has thrown away the design, which is the only random object in the problem.

`∀ᵐ` where an integral was meant

theorem dim_unbiased'' {n n₁ : ℕ} (hle : n₁ ≤ n) (P : Population n) :
    ∀ᵐ z ∂((completeRandomization n n₁ hle).toPMF.toMeasure), DiM P z = P.tau

This says the estimator equals $τ$ almost surely, which is not unbiasedness — it is a strictly stronger claim, and it fails the moment the estimator varies over the support of the design, which for four units and two treated it does under all but the most degenerate populations. (It is not always false: give every unit the same pair of potential outcomes and DiM is constant. That is exactly the sort of edge case that makes a wrong statement survive a couple of sanity checks.) The ∀ᵐ is doing the damage: it looks like a harmless regularity flourish and is in fact a different theorem.

Two habits protect you. First, when you see ∀ᵐ, ask what it says off the support: nothing at all, which is the content of of_ae_of_prob_pos above. Second, when the measure is a parameter rather than a fixed design, mentally instantiate it at 0 and at a Dirac mass. Against the zero measure every property holds almost everywhere, so a statement of this shape with an unconstrained measure and no IsProbabilityMeasure has instances that say nothing whatsoever.

`toReal` hiding an infinity

-- "the estimator has zero variance"
theorem no_variance (μ : Measure (Assignment n)) (P : Population n) :
    variance (DiM P) μ = 0

ProbabilityTheory.variance X μ is defined as (evariance X μ).toReal, and toReal ∞ = 0. So this conclusion is satisfied both by a degenerate estimator and by one whose variance is infinite, and nothing in the statement rules the second out. The same trap in a different costume: μ.real s = 0 does not say that s is null — it says μ s = 0 or μ s = ∞. On a probability measure the ambiguity disappears (measure_ne_top), which is precisely why IsProbabilityMeasure is load bearing even when the conclusion is real-valued and looks innocent. Whenever a real number in a statement was obtained by .toReal, ask what the statement would say if the underlying ℝ≥0∞ were ∞.

Independence smuggled in

theorem var_dim (hindep : iIndepFun (fun i z => Z z i) μ) : ...

An independence hypothesis on treatment indicators is a Bernoulli assumption in disguise (bernoulli_iIndepFun_Z is the only design in this library that satisfies it). Under complete randomization it is false, and a variance formula derived from it will be missing the finite-population correction. Independence hypotheses are cheap to state and expensive to satisfy; check which design, if any, actually has the property.

The pattern behind all four: in measure-theoretic notation the object — which measure, on which σ-algebra, with which finiteness — is carried by typeclasses and bound variables rather than by the prose around the formula. The formula almost always looks right. Read the binders first, the conclusion second.

End of Part II

That is the design-based half of the tutorial finished. What you have is a library of some thirty theorems — potential outcomes, designs and propensities, unbiasedness of Horvitz–Thompson and of difference in means, Neyman’s variance and its conservative estimator, blocking and clustering, regression as algebra, exact randomization tests, and the partial-identification bounds of the previous chapter — every one of them a finite statement about a fixed population, and every one of them machine-checked. None of it needed measure theory, and this chapter is the evidence: the measure-theoretic restatements are two-line corollaries, so the measure theory was never carrying any of the weight.

What the measure-theoretic vocabulary is good for is reading. You will be handed statements written in the Mathlib dialect — by a colleague, by a paper’s artefact, by a model — and the dictionary above is what lets you check whether such a statement says the thing you would have wanted to prove. Four questions, in order: is the measure a probability measure, is it the measure of the design, is the integrand integrable, and is the σ-algebra the intended one. Then #print axioms.

What remains is reference: a tactic cheatsheet, a Lean-to-statistics glossary, and an account of exactly how the claims on this site are verified.

The σ-algebra you never think about

ℝ≥0∞, and why probabilities live in it

A design is a probability mass function

From pmf to measure

Expectation is integration

The headline theorems, restated

Independence, at last

Side conditions, and what ∀ᵐ really says

Reading autoformalized Lean

End of Part II

`ℝ≥0∞`, and why probabilities live in it

Side conditions, and what `∀ᵐ` really says