Bridge to Mathlib's probability

The preceding chapters define expectations as finite sums over assignments. This is sufficient for the finite-population results developed there. Mathlib’s general probability library instead uses measurable spaces, measures, and Bochner integrals. An unfamiliar statement may therefore express unbiasedness as

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

where μ[·] denotes an integral. This chapter provides the translation between the finite design and Mathlib’s measure-theoretic language. It constructs a pmf and measure from a design, relates finite expectations to integrals, and transfers the earlier unbiasedness and variance results across that bridge.

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 826 lines of library preamble — the code above is at the bottom of the editor.

instance instMeasurableSpaceAssignment : MeasurableSpace (Assignment n) := ⊤

theorem measurableSet_assignment (s : Set (Assignment n)) : MeasurableSet s := trivial

instance instMeasurableSingletonClassAssignment :
    MeasurableSingletonClass (Assignment n) :=
  ⟨fun z => measurableSet_assignment {z}⟩

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. Three 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.
instMeasurableSingletonClassAssignment records the consequence Mathlib asks for by name: singletons are measurable. Its single field is measurableSet_assignment {z}, i.e. the first fact at a one-element set. Trivial as a proof, load-bearing as an instance — PMF.integral_eq_sum below will not fire without it.

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,028 lines of library preamble — the code above is at the bottom of the editor.

example (x : ℝ) (hx : 0 ≤ x) : (ENNReal.ofReal x).toReal = x :=
  ENNReal.toReal_ofReal hx

example : ENNReal.ofReal (-2 : ℝ) = 0 := by simp

example : (⊤ : ℝ≥0∞).toReal = 0 := ENNReal.toReal_top

example : (1 : ℝ≥0∞) - 2 = 0 := tsub_eq_zero_of_le (by norm_num)

example (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) :
    ENNReal.ofReal (x + y) = ENNReal.ofReal x + ENNReal.ofReal y :=
  ENNReal.ofReal_add hx hy

```
ENNReal.toReal_ofReal hx
```
Round-tripping a nonnegative real is the identity. The hypothesis 0 ≤ x is the whole content: without it ofReal has clamped and nothing comes back.
```
by simp
```
ENNReal.ofReal (-2) = 0. The clamping, witnessed. simp knows ENNReal.ofReal_eq_zero, which says ofReal x = 0 ↔ x ≤ 0, and closes the numeric side condition itself.
```
ENNReal.toReal_top
```
(⊤ : ℝ≥0∞).toReal = 0. Not a rounding convention but a definition, and the trap of the chapter: a real-valued conclusion obtained through toReal is satisfied by infinity as readily as by zero.
```
tsub_eq_zero_of_le (by norm_num)
```
(1 : ℝ≥0∞) - 2 = 0. Subtraction in ℝ≥0∞ is truncated: tsub_eq_zero_of_le says a - b = 0 whenever a ≤ b, and by norm_num supplies 1 ≤ 2. This is why every algebraic manipulation in this chapter happens after a toReal.
```
ENNReal.ofReal_add hx hy
```
Addition, on the other hand, does commute with ofReal — provided both summands are nonnegative, which is what hx and hy say. This is the lemma the pmf construction below leans on.

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:

Proposition. Every design determines a probability mass function on the assignments, whose mass at $z$ is $\underset{D}{Pr} (z)$ .

Proof.

The design’s masses are nonnegative reals, so they sit inside $[0, \infty]$ without loss. There are finitely many assignments, so the unconditional sum of the masses is the ordinary finite sum of them; that sum is $1$ by the design’s own axiom, and $1$ in the reals is $1$ in $[0, \infty]$ .∎

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

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 Lean makes the same three moves, in the same order.

```
fun z => ENNReal.ofReal (D.prob z)
```
A PMF is a subtype: a function into ℝ≥0∞ together with a proof that it sums to one, and the definition supplies both in an anonymous constructor. This is the first component — the design’s masses pushed through ofReal — and it is where nonnegativity is silently spent, since ofReal clamps rather than complaining. The second component is the by block, whose goal is the HasSum above.
Goal
```
D : Design n
⊢ HasSum (fun z => ENNReal.ofReal (D.prob z)) 1
```

have h : HasSum (fun z : Assignment n => ENNReal.ofReal (D.prob z))
    (∑ z, ENNReal.ofReal (D.prob z)) := hasSum_fintype _

hasSum_fintype says that on a Fintype the unconditional sum converges to the ordinary Finset.sum. It is stated as a HasSum, so this have produces a hypothesis of exactly the goal’s shape with the wrong value; the next three rewrites turn that value into 1.

Goal

h : HasSum (fun z => ENNReal.ofReal (D.prob z)) (∑ z, ENNReal.ofReal (D.prob z))
⊢ HasSum (fun z => ENNReal.ofReal (D.prob z)) 1

```
rw [← ENNReal.ofReal_sum_of_nonneg fun z _ => D.nonneg z] at h
```
ENNReal.ofReal_sum_of_nonneg states that ofReal commutes with a finite sum of nonnegative reals. Used right-to-left, inside h, it pulls the ofReal outside the sum, so what is being summed is now the design’s own real-valued masses.
Goal
```
h : HasSum (fun z => ENNReal.ofReal (D.prob z)) (ENNReal.ofReal (∑ i, D.prob i))
⊢ HasSum (fun z => ENNReal.ofReal (D.prob z)) 1
```

rw [D.sum_one] at h

The design’s axiom: those masses sum to 1.

Goal

h : HasSum (fun z => ENNReal.ofReal (D.prob z)) (ENNReal.ofReal 1)
⊢ HasSum (fun z => ENNReal.ofReal (D.prob z)) 1

```
rwa [ENNReal.ofReal_one] at h
```
ENNReal.ofReal_one is ofReal 1 = 1. After it h is the goal, and the a in rwa is assumption — rewrite the hypothesis until it matches, then use it. (The three rewrites are one rwa in the source; they are split here.)

The reverse direction reads the probabilities off with toReal:

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

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 proof is not the mirror image of the one above, and the asymmetry is worth a minute. ofReal is total, so going into ℝ≥0∞ needs no side condition; coming back out needs to know that nothing was infinite.

```
prob z := (p z).toReal
```
The first field. nonneg is the next line and is free: ENNReal.toReal_nonneg holds for every element of ℝ≥0∞, including ⊤, whose toReal is 0. What is left is the sum_one field, now a statement about real numbers.
Goal
```
p : PMF (Assignment n)
⊢ ∑ z, (p z).toReal = 1
```
```
have h : ∑ z, p z = (1 : ℝ≥0∞) := by rw [← p.tsum_coe, tsum_fintype]
```
A detour through the pmf’s own axiom, which is stated with a tsum. PMF.tsum_coe is ∑' a, p a = 1; rewriting the goal’s 1 with it right-to-left leaves a finite sum against an unconditional one, and tsum_fintype — the same fact used in the other direction above — identifies them. So h is the pmf’s axiom in Finset form.
Goal
```
p : PMF (Assignment n)
⊢ ∑ z, p z = ∑' (a : Assignment n), p a
```
```
rw [← ENNReal.toReal_sum fun z _ => p.apply_ne_top z]
```
The step with real content. ENNReal.toReal_sum says toReal commutes with a finite sum provided no summand is ⊤, and used right-to-left it pulls the toReal outside. Its hypothesis is discharged by PMF.apply_ne_top: a pmf’s values are at most 1, hence finite. Without that hypothesis the lemma is false — one infinite mass makes the left-hand side collapse to 0, since toReal ∞ = 0, while the right-hand side still counts the finite masses.
Goal
```
h : ∑ z, p z = 1
⊢ (∑ a, p a).toReal = 1
```
```
rw [← ENNReal.toReal_sum fun z _ => p.apply_ne_top z, h, ENNReal.toReal_one]
```
The remaining two rewrites of the same rw. h replaces the inner sum by 1, and ENNReal.toReal_one evaluates (1 : ℝ≥0∞).toReal to 1, closing the goal by reflexivity.

Proposition (the correspondence). The two translations are mutually inverse: a design read as a pmf and back is the same design, and a pmf read as a design and back is the same pmf. Designs and probability mass functions on a finite set are therefore the same objects in two notations.

Proof.

Both statements are pointwise, because a design is determined by its masses and a pmf by its values. In one direction the composite sends $Pr (z)$ to $toReal (ofReal (Pr (z)))$ , which is $Pr (z)$ because $Pr (z) \geq 0$ . In the other it sends the value $u$ to $ofReal (toReal (u))$ , which is $u$ because $u \neq \infty$ .∎

Both round trips are one line each once you have extensionality for designs, and they are the next two exercises.

ExerciseWarm-up: the round trip on a single probability

Going into ℝ≥0∞ and back is the identity on a single probability: (D.toPMF z).toReal = D.prob z.

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

@[simp] theorem Design.toPMF_apply_toReal (D : Design n) (z : Assignment n) :
    (D.toPMF z).toReal = D.prob z := by
  sorry

Hint

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.

Show solution

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

@[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: Design → PMF → Design and PMF → Design → PMF are both the identity.

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

@[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

@[simp] theorem Design.toPMF_toDesign (D : Design n) : PMF.toDesign D.toPMF = D := by
  sorry

@[simp] theorem PMF.toDesign_toPMF (p : PMF (Assignment n)) : (PMF.toDesign p).toPMF = p := by
  sorry

Hint

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.

Show solution

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

@[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

@[simp] theorem Design.toPMF_toDesign (D : Design n) : PMF.toDesign D.toPMF = D := by
  ext z
  exact D.toPMF_apply_toReal z

@[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

The total mass of $μ$ is 1, stated as a real number: μ.real Set.univ = 1.

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

theorem measureReal_univ (D : Design n) :
    (D.toPMF.toMeasure).real (Set.univ : Set (Assignment n)) = 1 := by
  sorry

Hint

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

Show solution

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

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

The measure of a single assignment, as a real number, is exactly D.prob z.

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

theorem Design.measureReal_singleton (D : Design n) (z : Assignment n) :
    (D.toPMF.toMeasure).real {z} = D.prob z := by
  sorry

Hint

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

Show solution

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

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 906 lines of library preamble — the code above is at the bottom of the editor.

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

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)]

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]

Three theorems, and only the first does any work: it identifies a set defined by a predicate with the coercion of the Finset that probOf sums over.

```
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]
```
The set identity, proved by extensionality at an arbitrary z. The two simp lemmas are the two coercions involved: Set.mem_ofPred_eq says membership in {z | p z} is p z, and Finset.coe_filter says the underlying set of univ.filter p is {z ∈ univ | p z}; Finset.mem_univ and true_and drop the vacuous membership in univ. Both sides are then p z.
Goal
```
z : Assignment n
⊢ z ∈ {z | p z} ↔ z ∈ ↑(filter p univ)
```
```
rw [hset]
```
Rewriting with it turns the measure of a set into the measure of a Finset, which is the form Mathlib has a formula for.
Goal
```
hset : {z | p z} = ↑(filter p univ)
⊢ D.toPMF.toMeasure ↑(filter p univ) = ENNReal.ofReal (D.probOf p)
```
```
rw [PMF.toMeasure_apply_finset]
```
And that formula: the measure a pmf assigns to a finite set is the sum of the pmf over it. The goal is now ∑ x with p x, D.toPMF x = ENNReal.ofReal (D.probOf p) — an identity between two finite sums, one in ℝ≥0∞ and one in ℝ.
```
rw [hset, PMF.toMeasure_apply_finset, Design.probOf,
  ENNReal.ofReal_sum_of_nonneg fun z _ => D.nonneg z]
```
The remaining two rewrites of the same rw. Design.probOf unfolds the right-hand side into its own filtered sum, and ENNReal.ofReal_sum_of_nonneg — the lemma from the pmf construction, needing nonnegativity again — pushes ofReal inside it. Both sides are now sums over the same Finset.
Goal
```
⊢ ∑ x with p x, D.toPMF x = ∑ i with p i, ENNReal.ofReal (D.prob i)
```
```
exact Finset.sum_congr rfl fun z _ => D.toPMF_apply z
```
Finset.sum_congr compares two sums termwise over the same index set, and at each term the equation is D.toPMF z = ENNReal.ofReal (D.prob z), which is the definition of toPMF.
```
rw [measureReal_def, D.toMeasure_setOf, ENNReal.toReal_ofReal (D.probOf_nonneg p)]
```
measureReal_setOf is the real-valued version, and three rewrites long. measureReal_def unfolds μ.real s to (μ s).toReal; the theorem just proved replaces μ s by ofReal (D.probOf p); and ENNReal.toReal_ofReal cancels the round trip, its nonnegativity hypothesis supplied by D.probOf_nonneg.
```
rw [D.measureReal_setOf, D.propensity_eq_probOf]
```
And measureReal_treated is two rewrites: the event “unit i is treated” is a set of the form {z | p z}, so the previous theorem turns its measure into a probOf, and propensity_eq_probOf says that particular probOf is the propensity score. This is the line quoted below.

Read Design.measureReal_treated slowly, because it is the single most useful line in this chapter 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 joint propensity $π_{i j}$ is the measure of the event that both i and j are treated. The displayed lemma jointPropensity_eq_probOf does the elementary work: Z z i * Z z j is the indicator of “both treated”, so Design.expect_indicator converts its expectation into a probOf, and by_cases hi : i ∈ z <;> by_cases hj : j ∈ z with simp [Z, hi, hj] settles the four membership cases.

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

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]

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

Hint

One rewrite with Design.measureReal_setOf (which turns μ.real {z | p z} into D.probOf p) and one with jointPropensity_eq_probOf.

Show solution

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

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]

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.

Proposition. For every statistic $f$ on the assignments,

\int f d μ = E_{D} [f] = \sum_{z} \underset{D}{Pr} (z) f (z) .

Proof.

The space is finite and every subset is measurable, so $f$ is itself a simple function: it takes finitely many values, each on a measurable set. The Bochner integral of a simple function is the sum of its values weighted by the measures of the sets where they are taken, which here is the sum over assignments of $μ ({z}) f (z)$ . And $μ ({z})$ is $\underset{D}{Pr} (z)$ .∎

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

@[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]

```
rw [PMF.integral_eq_sum]
```
The collapse, done once and for all by Mathlib: against a pmf’s measure on a Fintype whose singletons are measurable, the Bochner integral is the finite sum of (p z).toReal • f z. Both typeclass hypotheses were installed by the σ-algebra section — this is what that section was for.
Goal
```
⊢ ∑ a, (D.toPMF a).toReal • f a = D.expect f
```

refine Finset.sum_congr rfl fun z _ => ?_

Two sums over the same index set, so compare them termwise. What is left is one assignment’s worth of the identity.

Goal

z : Assignment n
x✝ : z ∈ univ
⊢ (D.toPMF z).toReal • f z = D.prob z * f z

```
rw [smul_eq_mul, D.toPMF_apply_toReal]
```
smul_eq_mul says that scalar multiplication of reals by reals is multiplication, and Design.toPMF_apply_toReal — the warm-up exercise above — says (D.toPMF z).toReal = D.prob z. The two sides are then identical.

∫ 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

The propensity score is the integral of the treatment indicator — $E [Z_{i}] = π_{i}$ in Mathlib’s vocabulary.

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

theorem integral_Z (D : Design n) (i : Fin n) :
    ∫ z, Z z i ∂(D.toPMF.toMeasure) = D.propensity i := by
  sorry

Hint

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.

Show solution

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

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

Mathlib’s ProbabilityTheory.variance f μ is Design.var f.

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

theorem Design.variance_toMeasure (D : Design n) (f : Assignment n → ℝ) :
    variance f (D.toPMF.toMeasure) = D.var f := by
  sorry

Hint

Rewrite with variance_eq_integral, whose hypothesis is discharged by (measurable_of_assignment f).aemeasurable. After that rewrite there are two integrals against μ — the outer one and the mean μ[f] sitting inside it — which 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.

Show solution

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

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 950 lines of library preamble — the code above is at the bottom of the editor.

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

```
rw [D.integral_toMeasure]
```
The theorem above, applied to the integrand HT D P. Every trace of measure theory leaves the goal at this line.
Goal
```
⊢ D.expect (HT D P) = P.tau
```
```
exact HT_unbiased D P hlo hhi
```
And what remains is the theorem of chapter 8, with its two hypotheses — every propensity strictly between 0 and 1 — passed through unchanged. The translation adds no hypotheses and removes none.

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

Difference in means is unbiased under complete randomization, stated with an integral. 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 956 lines of library preamble — the code above is at the bottom of the editor.

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

Hint

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.

Show solution

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

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.

Theorem. Under Bernoulli assignment with common treatment probability $p$ , the events $A_{i} = {i is treated}$ , for $i = 1, \dots, n$ , are mutually independent.

Proof.

Mutual independence of a family of events means that for every finite set $S$ of indices, $Pr (⋂_{i \in S} A_{i}) = \prod_{i \in S} Pr (A_{i})$ .

Fix such an $S$ . The intersection $⋂_{i \in S} A_{i}$ is the event that every unit of $S$ is treated, i.e. that $S$ is a subset of the treated set; its probability is the inclusion probability of $S$ , which under Bernoulli assignment is $p^{| S |}$ . Each factor on the right is $Pr (A_{i}) = π_{i} = p$ , and there are $| S |$ of them. The two sides agree.∎

Quantified over all finite $S$ , that is strictly stronger than the $| S | = 2$ case: the standard counterexample is three pairwise independent coin events that are not mutually independent. So mutual independence here follows from the one counting lemma the designs chapter already proved, and from nothing else.

ProbabilityTheory.iIndepSet is that predicate, and iIndepSet_iff_meas_biInter is the characterization the proof just used.

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

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
  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]

```
classical
```
Defensive bookkeeping. Design.probOf sums over a Finset.filter, which needs its predicate to be decidable, and classical makes every proposition decidable so that no instance search can fail. As it happens the predicates below — i ∈ z and S ⊆ z — are decidable anyway and the proof goes through without this line; it changes no mathematics either way, and recognizing that is part of reading someone else’s Lean.

set D := bernoulliDesign n p hp0 hp1 with hD

An abbreviation, and hD remembers what it abbreviates so that it can be unfolded again when a Bernoulli-specific lemma is needed. Without it every goal below spells bernoulliDesign n p hp0 hp1 out in full.

Goal

D : Design n := bernoulliDesign n p hp0 hp1
hD : D = bernoulliDesign n p hp0 hp1
⊢ ∀ (s : Finset (Fin n)), D.toPMF.toMeasure (⋂ i ∈ s, {z | i ∈ z}) = ∏ i ∈ s, D.toPMF.toMeasure {z | i ∈ z}

```
rw [iIndepSet_iff_meas_biInter fun i => measurableSet_assignment _]
```
The characterization quoted above, and the definition the informal proof used. Its hypothesis is that each event is measurable, which on the ⊤ σ-algebra is measurableSet_assignment, i.e. trivial. The goal becomes the displayed product formula, universally quantified over finite index sets.
```
intro S
```
Fix such an S. Everything below is about this one finite set of units.
```
have hInter : (⋂ i ∈ S, {z : Assignment n | i ∈ z}) = {z : Assignment n | S ⊆ z} := by
  ext z
  simp [Finset.subset_iff]
```
The step that makes the rest possible, and the one a reader is most likely to skip. ⋂ i ∈ S, {z | i ∈ z} is an intersection of events; {z | S ⊆ z} is a single event. They are equal, and Finset.subset_iff is why: S ⊆ z unfolds to ∀ a ∈ S, a ∈ z, which is precisely the membership condition for the intersection. This is the sentence “the intersection is the event that every unit of S is treated”, and it is what lets the inclusion probability be used at all.
Goal
```
S : Finset (Fin n)
z : Assignment n
⊢ z ∈ ⋂ i ∈ S, {z | i ∈ z} ↔ z ∈ {z | S ⊆ z}
```
```
rw [hInter, D.toMeasure_setOf, ← D.inclusion_eq_probOf, hD, bernoulli_inclusion]
```
The left-hand side. hInter replaces the intersection by the single event; Design.toMeasure_setOf turns its measure into ofReal of a probOf; Design.inclusion_eq_probOf, used right-to-left, recognizes that probOf as the inclusion probability of S — the probability that every unit of S is treated; and hD then unfolds D so that bernoulli_inclusion — the counting lemma from the designs chapter — can evaluate it as p ^ #S.
Goal
```
⊢ ENNReal.ofReal (D.inclusion S) = ENNReal.ofReal (p ^ #S)
```
```
rw [D.toMeasure_setOf, ← D.propensity_eq_probOf, hD, bernoulli_propensity]
```
The right-hand factors, by the same route one unit at a time: the event that i is treated has measure ofReal (D.propensity i), and bernoulli_propensity says that propensity is p.
```
rw [hleft, Finset.prod_congr rfl fun i _ => hright i, Finset.prod_const,
  ENNReal.ofReal_pow hp0]
```
Assembling. hleft replaces the left-hand side by ofReal (p ^ #S); Finset.prod_congr rfl fun i _ => hright i replaces every factor of the product by ofReal p; Finset.prod_const turns that product of a constant into ofReal p ^ #S; and ENNReal.ofReal_pow, whose hypothesis is 0 ≤ p, moves the power inside the conversion, closing the goal. The intermediate goal after the first two rewrites is ENNReal.ofReal (p ^ #S) = ∏ i ∈ S, ENNReal.ofReal p.
Goal
```
⊢ ENNReal.ofReal (p ^ #S) = ENNReal.ofReal p ^ #S
```

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,001 lines of library preamble — the code above is at the bottom of the editor.

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

```
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]
```
The only content: our Z and Mathlib’s Set.indicator are the same function. funext i z reduces the equality of two families of functions to agreement at one unit and one assignment, and by_cases h : i ∈ z <;> simp [Z, h] computes both branches — 1 on the treated side, 0 on the other — for each of the two definitions.
Goal
```
i : Fin n
z : Assignment n
⊢ Z z i = {z | i ∈ z}.indicator (fun x => 1) z
```

rw [hZ]

Rewriting the goal with that identity restates it about indicators, which is the vocabulary the next lemma speaks.

Goal

hZ : (fun i z => Z z i) = fun i => {z | i ∈ z}.indicator fun x => 1
⊢ iIndepFun (fun i => {z | i ∈ z}.indicator fun x => 1) (bernoulliDesign n p hp0 hp1).toPMF.toMeasure

```
exact (bernoulli_iIndepSet_treated hp0 hp1).iIndepFun_indicator
```
iIndepSet.iIndepFun_indicator upgrades independence of a family of events to independence of their indicator random variables. Nothing probabilistic happens here; the theorem above did that work.

ExerciseCore: independence written out as a product of probabilities

iIndepSet is an abstract predicate; this is the same statement for two units of a Bernoulli design, written the way you would check it by hand: the probability that both are treated is the product of the two marginal probabilities.

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

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

Hint

Rewrite the three probabilities into propensities using measureReal_both_treated from earlier plus Design.measureReal_treated (twice), then quote bernoulli_jointPropensity (which needs $i \neq j$ ) and bernoulli_propensity. Finish by turning $p^{2}$ into $p \cdot p$ with sq; all of it fits in one rw.

Show solution

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

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,092 lines of library preamble — the code above is at the bottom of the editor.

example (D : Design n) (f : Assignment n → ℝ) :
    AEStronglyMeasurable f (D.toPMF.toMeasure) :=
  (measurable_of_assignment f).aestronglyMeasurable

example (D : Design n) (f : Assignment n → ℝ) : Integrable f (D.toPMF.toMeasure) :=
  D.integrable f

example (D : Design n) (T : Assignment n → ℝ) :
    IsProbabilityMeasure ((D.toPMF.toMeasure).map T) :=
  inferInstance

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, and inherited by the pushforward μ.map T — which is why the third line is inferInstance and not a proof.
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.

Only the fourth is a tactic proof rather than a one-term citation, and it is two rewrites.

```
rw [integral_map (measurable_of_assignment T).aemeasurable hg.aestronglyMeasurable,
  Design.integral_toMeasure]
```
integral_map is the change-of-variables formula: integrating g against the pushforward of μ along T is integrating g ∘ T against μ. It takes two side conditions — T a.e.-measurable, which is free here, and g a.e.-strongly-measurable, which is not free and comes from the explicit hypothesis hg : Measurable g. That asymmetry is the bullet above, in Lean. The second rewrite, Design.integral_toMeasure, then turns the remaining integral over Assignment n into an expectation, which closes the goal by reflexivity.
Goal
```
⊢ ∫ (x : Assignment n), g (T x) ∂D.toPMF.toMeasure = D.expect fun z => g (T z)
```

∀ᵐ 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

An ∀ᵐ hypothesis says nothing about assignments the design never produces; at an assignment with positive probability it does say what you want. The easy direction, ae_of_forall, is displayed with its proof; the exercise is the converse.

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

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

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

Hint

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.

Show solution

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

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

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

Two units with the same propensity have identically distributed treatment indicators. IdentDistrib f g μ ν unfolds to three things — f is a.e.-measurable, g is a.e.-measurable, and μ.map f = ν.map g.

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

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

Hint

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]; the middle two cases rewrite the treated set’s measure with D.toMeasure_setOf and D.propensity_eq_probOf and then use h, and the complement case additionally needs measure_compl.

Show solution

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

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
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:

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

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 appendix on verification.

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