Structures and definitions

This chapter combines terms, tactics, real numbers, and finite sums into the definitions used later in the book. It introduces Population, mean, tau, Assignment, Z, Yobs, Design, and expect, then proves a basic linearity result. These definitions match the corresponding library definitions, with fewer supporting lemmas.

Why bundle anything

A finite population is two functions, $y_{1}$ and $y_{0}$ , both from units to reals. You could carry them around as two separate arguments forever:

theorem tau_eq (n : ℕ) (y1 y0 : Fin n → ℝ) : … := …
theorem tau_add (n : ℕ) (y1 y0 y1' y0' : Fin n → ℝ) : … := …

Two arguments become four when you compare two populations, and every lemma statement has to re-establish that they share the same $n$ . A structure gives the pair a name, so that “a population” is one thing with one type, Population n, and the shared $n$ is part of that type.

That is the whole motivation. Structures are not an abstraction mechanism here; they are a naming mechanism.

Declaring a structure

A structure, three ways to build one, and its projectionsNew tab

structure SummaryStats where
  size : ℕ
  xbar : ℚ

def treatedGroup : SummaryStats := { size := 4, xbar := 7 / 2 }
def controlGroup : SummaryStats := ⟨6, 5 / 2⟩
def wholeSample : SummaryStats := SummaryStats.mk 10 3

#eval treatedGroup.size
#eval SummaryStats.xbar controlGroup
#eval wholeSample.xbar

Declaring structure SummaryStats with fields size and xbar creates several things at once:

the type SummaryStats;
a constructor SummaryStats.mk : ℕ → ℚ → SummaryStats;
one projection per field, SummaryStats.size : SummaryStats → ℕ and SummaryStats.xbar : SummaryStats → ℚ;
the anonymous-constructor notation ⟨6, 5/2⟩, which means “build the structure the goal is asking for, from these fields in order”.

The three definitions in the block above build the same kind of value in the three available styles. Named fields ({ size := 4, xbar := 7 / 2 }) are the readable one and the one to prefer; ⟨_, _⟩ is convenient when the type is already known from context; SummaryStats.mk is what the other two elaborate into.

#eval treatedGroup.size prints 4. The dot is doing something specific, which is worth being precise about before it multiplies.

Dot notation is namespace resolution

`P.totalEffect` is `Population.totalEffect P`New tab

def Population.totalEffect (P : Population n) : ℝ := ∑ i, P.effect i

#check fun (P : Population 3) => P.totalEffect

theorem totalEffect_eq (P : Population n) :
    P.totalEffect = ∑ i, (P.y1 i - P.y0 i) := rfl

When Lean sees P.foo and P : Population n, it looks for a constant named Population.foo and applies it to P in the first argument position whose type is a Population. That is the entire rule. It works for projections because a projection is a function named Population.y1, and it works for anything else you define in the same namespace.

So namespace Population … end Population is not decoration: putting effect and tau inside it is what makes P.effect i and P.tau legal. The library does the same for designs — everything about a Design lives in namespace Design, which is why chapter 7 can write D.expect f and D.expect_add.

The population

Informally. A population of $n$ units is a pair of outcome vectors $y_{1}, y_{0} : {1, \dots, n} \to R$ , both fixed. Unit $i$ ‘s treatment effect is $y_{1} (i) - y_{0} (i)$ , and the average treatment effect is

τ = \frac{1}{n} \sum_{i = 1}^{n} (y_{1} (i) - y_{0} (i)) .

Formally.

Population, mean, effect, tauNew tab

structure Population (n : ℕ) where
  y1 : Fin n → ℝ
  y0 : Fin n → ℝ

noncomputable def mean (v : Fin n → ℝ) : ℝ := (∑ i, v i) / n

namespace Population

def effect (P : Population n) (i : Fin n) : ℝ := P.y1 i - P.y0 i

noncomputable def tau (P : Population n) : ℝ := mean P.effect

end Population

Four things in that block are decisions rather than transcription.

The type enforces SUTVA. y1 : Fin n → ℝ takes a unit and returns a number. It cannot consult any other unit’s treatment status, because it is not given one. No-interference is not an assumption written down somewhere and possibly forgotten; it is the arity of a function. This is the single best argument for formalizing design-based inference: the assumption that is easiest to violate on paper is impossible to violate here without changing a type.

mean divides by (n : ℝ), and $n$ may be zero. Lean defines x / 0 = 0, so mean on an empty population is 0 rather than undefined. Chapter 3 covered the convention; the consequence for a definition is that mean is total — it needs no hypothesis, so neither do the definitions built on it, and positivity hypotheses can appear exactly where the mathematics needs them instead of being threaded through every signature. This is a deliberate choice, not an accident of the definition.

tau is defined from effect, not spelled out. Population.tau P = mean P.effect is a composition of two definitions, each of which has its own lemmas. The alternative — writing (∑ i, (P.y1 i - P.y0 i)) / n directly — would be equal by rfl but would give you nothing to rewrite with.

noncomputable. Every $R$ -valued definition needs the keyword, because real division has no algorithm. It is a compilation concern and never a proof concern; Fin n → ℝ functions are perfectly good mathematical objects that Lean simply declines to run. effect escapes the keyword only because addition, subtraction and multiplication of reals are computable on Lean’s Cauchy-sequence representation while inversion is not — if that distinction ever bites you, add noncomputable and move on.

Three ways to name a thing

`abbrev`, `def`, `theorem`New tabOpens with 52 lines of library preamble — the code above is at the bottom of the editor.

example : Assignment 3 = Finset (Fin 3) := rfl

example (z : Assignment 3) (i : Fin 3) : Z z i = if i ∈ z then 1 else 0 := rfl

#check @Assignment

abbrev is a def marked reducible. Lean will unfold it silently, during unification, without being asked. Assignment n and Finset (Fin n) are therefore interchangeable everywhere: a lemma about Finset (Fin n) applies to an Assignment n with no coaxing. Use abbrev when you want a synonym and nothing more.
def unfolds when you ask — with unfold, with simp only [name], or automatically during rfl-checking. Use it for a real definition whose unfolding you want to control.
theorem produces a proof. Proofs are opaque: by proof irrelevance any two proofs of the same proposition are equal, and nothing ever inspects the term. This is why a theorem can be replaced by a different proof without breaking anything downstream, and why def should be used for data even when theorem would typecheck.

The practical difference between abbrev and def shows up in error messages. If Assignment were a def, Finset.card_powersetCard would fail to apply to an assignment until you unfolded it by hand, and the error would say two types are not equal that visibly are.

Assignments, and the indicator

Informally. An assignment is the set of treated units. The indicator $Z_{i}$ is $1$ for treated units and $0$ otherwise, and the observed outcome is $Y_{i} = Z_{i} y_{1} (i) + (1 - Z_{i}) y_{0} (i)$ .

Formally.

Assignment, Z, YobsNew tabOpens with 45 lines of library preamble — the code above is at the bottom of the editor.

abbrev Assignment (n : ℕ) := Finset (Fin n)

def Z (z : Assignment n) (i : Fin n) : ℝ := if i ∈ z then 1 else 0

def Yobs (P : Population n) (z : Assignment n) (i : Fin n) : ℝ :=
  Z z i * P.y1 i + (1 - Z z i) * P.y0 i

Two modeling choices require explanation.

An assignment is a treated set, not a vector of bits. The obvious alternative is Fin n → Bool. Finset (Fin n) wins because it makes the combinatorics somebody else’s problem: “exactly $n_{1}$ units treated” is literally Finset.powersetCard n₁ univ, a Mathlib object whose cardinality Mathlib already knows; the control group is zᶜ for free; and Finset (Fin n) is a Fintype, so summing over all assignments works without extra instances. With Fin n → Bool every one of those counting facts would have to be redeveloped.

The indicator is real-valued, not Bool or Prop. Design-based inference is algebra with indicators: $Z_{i}^{2} = Z_{i}$ , $E [Z_{i}] = π_{i}$ , $Y_{i} = Z_{i} y_{1} (i) + (1 - Z_{i}) y_{0} (i)$ . Keeping Z in $R$ makes those ordinary equations in a field, so ring, field_simp and linarith apply to them. A Bool-valued indicator would need a coercion at every step, and a Prop-valued one could not be added at all.

Nothing downstream ever pattern-matches on the Finset; the algebra is written in terms of Z, and the set is what the counting lemmas see.

Opening up a definition

Having made a definition, you need to be able to take it apart. There are four tactics for this and they differ in how much they do without asking.

`unfold` and `simp only [defn]`New tabOpens with 58 lines of library preamble — the code above is at the bottom of the editor.

theorem Z_mul_self (z : Assignment n) (i : Fin n) : Z z i * Z z i = Z z i := by
  unfold Z
  split <;> norm_num

theorem Z_sq (z : Assignment n) (i : Fin n) : Z z i ^ 2 = Z z i := by
  simp only [Z, sq]
  split <;> norm_num

unfold Z replaces every occurrence of Z in the goal by its body. It is blunt: it does not simplify afterwards, and it unfolds everywhere.

simp only [Z] uses the equation lemma Lean generated for Z as a rewrite rule, and then keeps simplifying with the other rules you listed — here sq, which relates x ^ 2 to x * x. simp only is a simplifier restricted to exactly the facts you name, which is why the library prefers it to a bare simp: the list of facts used is written down in the proof, so a reader can see the argument and a Mathlib bump that breaks it breaks it loudly.

split is the tactic for an if in the goal: it produces one goal per branch, each with the corresponding hypothesis about the condition available. Here both branches are numeric identities, so norm_num finishes them, and <;> applies norm_num to every goal split produced.

```
unfold Z
```
Z z i is replaced by its body, an if, in all three places it occurs. The goal is now about a conditional and no longer mentions the definition at all — which is the point: nothing downstream can be proved about Z until Z has been opened up once.
Goal
```
n : ℕ
z : Assignment n
i : Fin n
⊢ ((if i ∈ z then 1 else 0) * if i ∈ z then 1 else 0) = if i ∈ z then 1 else 0
```
```
split
```
Two goals, one per branch of the if, each carrying the hypothesis that makes that branch the live one, and each with the conditional already collapsed to the branch’s value. Lean names the cases isTrue and isFalse, and since the script never refers to the hypothesis it is left inaccessible — that is what the dagger on h✝ means.
Goal
```
case isTrue
n : ℕ
z : Assignment n
i : Fin n
h✝ : i ∈ z
⊢ 1 * 1 = 1

case isFalse
n : ℕ
z : Assignment n
i : Fin n
h✝ : i ∉ z
⊢ 0 * 0 = 0
```
```
<;> norm_num
```
t <;> s runs s on every goal t produced, so one norm_num disposes of both 1 * 1 = 1 and 0 * 0 = 0. Writing it this way, rather than as two bullets, is a claim that the branches are not worth distinguishing.

Z_sq is the same proof with the unfolding done differently: simp only [Z, sq] uses the equation lemma for Z and sq : a ^ 2 = a * a, so after one line the goal is the same conditional product as above and the same split <;> norm_num closes it. Two tactics, one goal state, and the reason to know both is that unfold takes only definitions while simp only takes definitions and lemmas together.

`show` and `change`New tabOpens with 66 lines of library preamble — the code above is at the bottom of the editor.

theorem Yobs_apply (P : Population n) (z : Assignment n) (i : Fin n) :
    Yobs P z i = Z z i * P.y1 i + (1 - Z z i) * P.y0 i := by
  show Z z i * P.y1 i + (1 - Z z i) * P.y0 i = Z z i * P.y1 i + (1 - Z z i) * P.y0 i
  rfl

theorem tau_unfold (P : Population n) : P.tau = (∑ i, (P.y1 i - P.y0 i)) / n := by
  change (∑ i, P.effect i) / (n : ℝ) = (∑ i, (P.y1 i - P.y0 i)) / n
  rfl

show restates the goal as something definitionally equal to it — Lean checks the two are interchangeable by unfolding, and refuses if they are not. Nothing changes about what must be proved; what changes is what the proof says. In Yobs_apply the show line is redundant in the sense that rfl alone would close the goal, and useful in the sense that it documents what the goal had become. In a twenty-line proof this is worth a great deal.

change is the same operation under a different keyword, usable mid-proof. tau_unfold uses it to replace P.tau by the sum-over-effect form, which is what tau reduces to, before finishing with rfl.

```
show Z z i * P.y1 i + (1 - Z z i) * P.y0 i = …
```
In Yobs_apply the left-hand side Yobs P z i is replaced by what it unfolds to, which makes the two sides of the goal visibly identical. Lean checks the restatement is definitionally equal to the previous goal and would refuse it otherwise.
```
rfl
```
Both sides are now the same term, so reflexivity closes it. Note that rfl alone, with no show at all, would also have closed the original goal: the line above buys nothing from the compiler and tells the reader what Yobs unfolded to.
```
change (∑ i, P.effect i) / (n : ℝ) = …
```
tau_unfold does the same for tau, and here the restatement is a genuine step of reading: P.tau is mean P.effect, and mean divides a sum by ↑n, so the goal one level down is a sum over effect divided by the sample size. change and show are the same operation; the two keywords exist so that show can read as the statement of a goal and change as an edit to one.
```
rfl
```
P.effect i is P.y1 i - P.y0 i by definition, so the two sides are again the same term. Both theorems are rfl theorems, with all the content in the restatement — exactly the pattern the callout above warns about, used here for its legitimate purpose of pinning down what a definition unfolds to.

When are two of these things equal?

funext, ext, and structure equalityNew tabOpens with 75 lines of library preamble — the code above is at the bottom of the editor.

theorem outcomes_eq (u v : Fin n → ℝ) (h : ∀ i, u i = v i) : u = v := by
  funext i
  exact h i

theorem assignments_eq (z w : Assignment n) (h : ∀ i, i ∈ z ↔ i ∈ w) : z = w := by
  ext i
  exact h i

theorem population_eq {P Q : Population n}
    (h1 : ∀ i, P.y1 i = Q.y1 i) (h0 : ∀ i, P.y0 i = Q.y0 i) : P = Q := by
  obtain ⟨a1, a0⟩ := P
  obtain ⟨b1, b0⟩ := Q
  rw [Population.mk.injEq]
  exact ⟨funext h1, funext h0⟩

Functions. Two outcome vectors are equal exactly when they agree at every unit. That principle — function extensionality — is not a definitional fact in Lean’s type theory: core derives it from the quotient axiom Quot.sound, and the tactic that applies it is funext. funext i turns a goal u = v between functions into u i = v i with i fresh.

Finsets. ext i is the general version: it looks up whichever extensionality lemma is registered for the goal’s type and applies it. For Finset that lemma is membership, so ext i turns z = w into i ∈ z ↔ i ∈ w. You will use ext far more often than funext, because it also handles functions. In both of those proofs the second line is exact h i: the hypothesis is exactly the family of facts that the extensionality step asked for, one per unit, so applying it at the fresh i closes the goal. Chapter 2 walked both scripts.

Structures. Two populations are equal when both fields are. Lean generates Population.mk.injEq alongside the structure — an equation saying that Population.mk a₁ a₀ = Population.mk b₁ b₀ is equivalent to a₁ = b₁ ∧ a₀ = b₀ — and the proof combines it with funext on each field.

```
obtain ⟨a1, a0⟩ := P
```
Destructuring: the opaque P is replaced everywhere by an explicit { y1 := a1, y0 := a0 }, so the goal and both hypotheses are now stated in terms of the two functions rather than the bundle.

obtain ⟨b1, b0⟩ := Q

The same for Q. Both sides of the goal are now literal applications of the constructor, which is the shape the next lemma needs.

Goal

n : ℕ
a1 a0 b1 b0 : Fin n → ℝ
h1 : ∀ (i : Fin n), { y1 := a1, y0 := a0 }.y1 i = { y1 := b1, y0 := b0 }.y1 i
h0 : ∀ (i : Fin n), { y1 := a1, y0 := a0 }.y0 i = { y1 := b1, y0 := b0 }.y0 i
⊢ { y1 := a1, y0 := a0 } = { y1 := b1, y0 := b0 }

```
rw [Population.mk.injEq]
```
mk.injEq says that two structures built by the constructor are equal exactly when their fields are, and it is an = between propositions, so rw can replace the goal by the conjunction. This is the step that would have failed before destructuring: mk.injEq matches only constructor applications.
Goal
```
n : ℕ
a1 a0 b1 b0 : Fin n → ℝ
h1 : ∀ (i : Fin n), { y1 := a1, y0 := a0 }.y1 i = { y1 := b1, y0 := b0 }.y1 i
h0 : ∀ (i : Fin n), { y1 := a1, y0 := a0 }.y0 i = { y1 := b1, y0 := b0 }.y0 i
⊢ a1 = b1 ∧ a0 = b0
```
```
exact ⟨funext h1, funext h0⟩
```
Two goals in a pair. h1 gives the treated outcomes agreeing unit by unit, and funext h1 upgrades that to equality of the two functions; h0 does the same for the control outcomes. Reading the four lines as one sentence: take the two populations apart, use that a structure is determined by its fields, and settle each field by extensionality.

One thing ext will not do is Population: nobody tagged the structure with @[ext], which is why the proof above goes through mk.injEq by hand. Extensionality for a user-defined structure is available but not automatic.

Summing over every assignment

This is the step that makes the whole approach possible. There are $2^{n}$ assignments; expectation over the design will be a sum over all of them; and Lean needs to be told that this is a finite, enumerable collection before it will accept the notation.

Assignment n is a FintypeNew tabOpens with 90 lines of library preamble — the code above is at the bottom of the editor.

#eval Fintype.card (Assignment 3)
#eval (Finset.univ : Finset (Assignment 3)).card

theorem card_assignments (m : ℕ) : Fintype.card (Assignment m) = 2 ^ m := by
  rw [Fintype.card_finset, Fintype.card_fin]

Fintype α is a typeclass carrying a Finset α containing every element of α, together with a proof that it does. Mathlib provides the instance for Finset (Fin n), so Fintype.card (Assignment 3) evaluates to 8, and — the part that matters — the notation ∑ z, f z with z : Assignment n means “sum over Finset.univ : Finset (Assignment n)”, which is the sum over all $2^{n}$ subsets.

```
rw [Fintype.card_finset]
```
Fintype.card_finset : Fintype.card (Finset α) = 2 ^ Fintype.card α is the lemma $| P (α) | = 2^{| α |}$ . It applies to Assignment m without any unfolding because Assignment is an abbrev, so Lean sees Finset (Fin m).
Goal
```
⊢ 2 ^ Fintype.card (Fin m) = 2 ^ m
```
```
Fintype.card_fin
```
Fintype.card_fin : Fintype.card (Fin m) = m turns the exponent into the sample size, both sides read 2 ^ m, and the goal closes. Counting the assignments of an $m$ -unit study is two rewrites, and neither of them is about experiments.

There is no measure theory anywhere in this tutorial, and this instance is why. An expectation is a finite sum against a list of probabilities. That is not a simplification of the general definition — for a finite sample space it is the general definition — but it does mean every probabilistic lemma reduces to Finset manipulation, which is chapter 3’s material.

Assignments of a fixed size

Complete randomization treats exactly $n_{1}$ units, so its support is the set of assignments of size $n_{1}$ . Mathlib has that set already.

Finset.powersetCardNew tabOpens with 96 lines of library preamble — the code above is at the bottom of the editor.

#eval ((Finset.univ : Finset (Fin 4)).powersetCard 2).card

theorem card_balanced_assignments (m k : ℕ) :
    ((Finset.univ : Finset (Fin m)).powersetCard k).card = m.choose k := by
  rw [Finset.card_powersetCard, Finset.card_univ, Fintype.card_fin]

s.powersetCard k is the finset of subsets of s with exactly k elements, and Finset.card_powersetCard says there are $(\binom{| s |}{k})$ of them.

```
rw [Finset.card_powersetCard]
```
Finset.card_powersetCard : #(s.powersetCard k) = (#s).choose k. The number of size- $k$ subsets of a set of size $| s |$ is the binomial coefficient — the one counting fact complete randomization needs, and Mathlib has it.
Goal
```
⊢ (#univ).choose k = m.choose k
```
```
Finset.card_univ
```
The same card_univ as in chapter 3, applied inside the binomial coefficient.
Goal
```
⊢ (Fintype.card (Fin m)).choose k = m.choose k
```
```
Fintype.card_fin
```
And the same card_fin, after which both sides are $(\binom{m}{k})$ . The whole proof is the two-rewrite dance for #univ wrapped around one Mathlib counting lemma.

This is the payoff from the treated-set decision: because an assignment is a Finset, complete randomization’s support is a Mathlib object with Mathlib’s counting lemmas attached, including the one nobody wants to prove by hand — Finset.card_filter_powersetCard_subset, which counts the size- $k$ subsets containing a fixed set, and which is what turns into $π_{i} = n_{1} / n$ in chapter 7.

The design

Informally. A design is a probability distribution over assignments. Since there are finitely many assignments, it is a list of $2^{n}$ non-negative numbers summing to one, and the expectation of a statistic is the weighted sum.

Formally.

Design and expectNew tabOpens with 102 lines of library preamble — the code above is at the bottom of the editor.

structure Design (n : ℕ) where
  prob : Assignment n → ℝ
  nonneg : ∀ z, 0 ≤ prob z
  sum_one : ∑ z, prob z = 1

noncomputable def Design.expect (D : Design n) (f : Assignment n → ℝ) : ℝ :=
  ∑ z, D.prob z * f z

A structure may carry proofs as fields, and this one carries two: nonneg and sum_one are propositions, so a value of type Design n is a pmf together with the evidence that it is one. You cannot construct a Design without discharging both. This is the second real use of structures: bundling data with its invariants, so that every downstream lemma gets the invariants for free.

The explicit pmf is a deliberate choice over a Mathlib PMF or a measure, and the argument for it is pedagogical as much as technical: Design.expect D f = ∑ z, D.prob z * f z is the definition of expectation a statistician already knows, and linearity of expectation is then a two-line simp only rather than a citation. Chapter 14 does the translation into PMF and MeasureTheory.integral for readers who need to recognize it.

Note what Design does not bundle: no $n_{1}$ , no propensity scores, no variance. Those are definitions on top of it, so that defining a new design means supplying a pmf and nothing else.

A design you can buildNew tabOpens with 110 lines of library preamble — the code above is at the bottom of the editor.

noncomputable def uniformDesign (m : ℕ) : Design m where
  prob := fun _ => 1 / 2 ^ m
  nonneg := fun _ => by positivity
  sum_one := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_finset, Fintype.card_fin,
      nsmul_eq_mul]
    push_cast
    field_simp

theorem uniformDesign_prob (m : ℕ) (z : Assignment m) :
    (uniformDesign m).prob z = 1 / 2 ^ m := rfl

Building uniformDesign means proving the two axioms. Informally there is nothing to prove: every one of the $2^{m}$ assignments gets probability $2^{- m}$ , these are positive, and there are $2^{m}$ of them, so they sum to one. Formally that sentence is seven lines, and every one of them is bookkeeping about where the $2^{m}$ lives.

```
nonneg := fun _ => by positivity
```
The first field. For each assignment the claim is 0 ≤ 1 / 2 ^ m, and positivity proves goals of the form 0 ≤ e, 0 < e or e ≠ 0 by walking the syntax of e: a quotient of a positive numeral by a power of a positive numeral is positive.
```
rw [Finset.sum_const]
```
The second field starts from ∑ z, 1 / 2 ^ m = 1, a constant summed over every assignment, so Finset.sum_const replaces it by the number of assignments scaled by the constant.
Goal
```
⊢ #univ • (1 / 2 ^ m) = 1
```
```
Finset.card_univ
```
#univ becomes Fintype.card (Assignment m) — the same first half of the dance as always, except that here the index type is the assignment space rather than the units.
Goal
```
⊢ Fintype.card (Assignment m) • (1 / 2 ^ m) = 1
```
```
Fintype.card_finset
```
Which is where the previous section’s counting lemma pays off: the number of assignments is 2 ^ Fintype.card (Fin m).
Goal
```
⊢ 2 ^ Fintype.card (Fin m) • (1 / 2 ^ m) = 1
```

Fintype.card_fin

And the exponent is the sample size.

Goal

⊢ 2 ^ m • (1 / 2 ^ m) = 1

```
nsmul_eq_mul
```
The scalar action of the natural number 2 ^ m becomes multiplication in ℝ, which introduces the coercion ↑(2 ^ m).
Goal
```
⊢ ↑(2 ^ m) * (1 / 2 ^ m) = 1
```
```
push_cast
```
The cast is around a power of a numeral, and push_cast drives it inward until it disappears: ↑(2 ^ m) becomes (2 : ℝ) ^ m. Now both occurrences of $2^{m}$ are the same real number, which they were not a line ago.
Goal
```
⊢ 2 ^ m * (1 / 2 ^ m) = 1
```
```
field_simp
```
Clear the denominator and close the goal. field_simp needs (2 : ℝ) ^ m ≠ 0 to do that, and unlike the ↑n ≠ 0 of a sample size it can establish this one for itself: the base is a numeral.

The moral of the seven lines is worth stating: the mathematics is one sentence, and the formal work is entirely in moving a number across the boundary between counting (ℕ, •) and arithmetic (ℝ, *, /). That ratio is typical, and it is why chapter 3 spent its length on those lemmas.

uniformDesign_prob is then a one-word rfl: the prob field of a structure built with where is the function supplied for it, so (uniformDesign m).prob z reduces to 1 / 2 ^ m and there is nothing to prove. It is worth stating anyway, because later proofs rewrite with it rather than unfolding the design.

This design is the Bernoulli design at $p = 1 / 2$ , which chapter 7 defines properly.

Linearity, and the rest of the exercises

Everything from here is an exercise, because everything from here is short. The core sequence — expect_const, expect_add, expect_const_mul — is linearity of expectation, and it is worth doing all three, because their proofs are the template for every expectation computation in Part II.

Read the proofs for what is not in them: no independence, no distributional assumption, no exchangeability. Linearity of expectation is a rearrangement of a finite sum, and in this setting the Lean makes that unusually obvious.

ExerciseA treated unit has indicator 1 (warm-up)

A treated unit has indicator 1.

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

theorem ex_Z_of_mem {z : Assignment n} {i : Fin n} (h : i ∈ z) : Z z i = 1 := by
  sorry

Hint

unfold Z turns the goal into (if i ∈ z then 1 else 0) = 1, and ite_eq_left h is the term saying “the condition holds, so the if is its left branch”; in Lean v4.34 this is the replacement for the older if_pos.

Show solution

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

theorem ex_Z_of_mem {z : Assignment n} {i : Fin n} (h : i ∈ z) : Z z i = 1 := by
  unfold Z
  exact ite_eq_left h

ExerciseA control unit has indicator 0 (warm-up)

A control unit has indicator 0. Together with the previous exercise these are the library’s Z_of_mem and Z_of_not_mem, both tagged @[simp] there so that simp disposes of indicators automatically.

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

theorem ex_Z_of_not_mem {z : Assignment n} {i : Fin n} (h : i ∉ z) : Z z i = 0 := by
  sorry

Hint

The mirror image of the previous exercise: unfold Z, then ite_eq_right h.

Show solution

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

theorem ex_Z_of_not_mem {z : Assignment n} {i : Fin n} (h : i ∉ z) : Z z i = 0 := by
  unfold Z
  exact ite_eq_right h

ExerciseThe control indicator is the complement's indicator (core)

1 - Z z i = Z zᶜ i. This is the lemma that halves the work in every later proof: anything true of the treated side is true of the control side with z replaced by zᶜ.

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

theorem ex_one_sub_Z (z : Assignment n) (i : Fin n) : 1 - Z z i = Z zᶜ i := by
  sorry

Hint

After unfold Z, by_cases h : i ∈ z splits into the two cases with h : i ∈ z and h : i ∉ z respectively, and simp [h] closes each — it needs Finset.mem_compl to see that i ∈ zᶜ is i ∉ z, which is why simp rather than simp only is appropriate here.

Show solution

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

theorem ex_one_sub_Z (z : Assignment n) (i : Fin n) : 1 - Z z i = Z zᶜ i := by
  unfold Z
  by_cases h : i ∈ z <;> simp [h]

ExerciseThe observed outcome is the revealed potential outcome (core)

The algebraic definition and the case-split definition agree. This matters because the two forms are good at different things: Z·y1 + (1-Z)·y0 is what linearity of expectation can act on, and if i ∈ z then y1 i else y0 i is what a reader recognizes.

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

theorem ex_Yobs_eq_ite (P : Population n) (z : Assignment n) (i : Fin n) :
    Yobs P z i = if i ∈ z then P.y1 i else P.y0 i := by
  sorry

Hint

Same shape of proof as the previous exercise: unfold Yobs Z, then by_cases h : i ∈ z and simp [h] in each branch.

Show solution

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

theorem ex_Yobs_eq_ite (P : Population n) (z : Assignment n) (i : Fin n) :
    Yobs P z i = if i ∈ z then P.y1 i else P.y0 i := by
  unfold Yobs Z
  by_cases h : i ∈ z <;> simp [h]

ExerciseThe ATE is the difference of the two means (core)

The average treatment effect is the mean treated outcome minus the mean control outcome. Nothing here needs $n > 0$ : both sides are $0 / 0 = 0$ when $n = 0$ .

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

theorem ex_tau_eq_mean_sub_mean (P : Population n) :
    P.tau = mean P.y1 - mean P.y0 := by
  sorry

Hint

One simp only with the right list: unfold tau, effect and mean, split the sum with Finset.sum_sub_distrib (chapter 3) and the division with sub_div.

Show solution

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

theorem ex_tau_eq_mean_sub_mean (P : Population n) :
    P.tau = mean P.y1 - mean P.y0 := by
  simp only [Population.tau, Population.effect, mean, Finset.sum_sub_distrib, sub_div]

ExerciseE[c] = c (core)

The expectation of a constant is that constant. This is the first place the sum_one field is used, and the reason Design has to carry it (the stretch exercise below spends it once more).

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

theorem ex_expect_const (D : Design n) (c : ℝ) : D.expect (fun _ => c) = c := by
  sorry

Hint

Unfold Design.expect; rewriting with ← Finset.sum_mul pulls c out of ∑ z, D.prob z * c to give (∑ z, D.prob z) * c, D.sum_one turns the parenthesis into 1, and one_mul finishes. Note the dot: D.sum_one is the proof stored in the structure.

Show solution

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

theorem ex_expect_const (D : Design n) (c : ℝ) : D.expect (fun _ => c) = c := by
  simp only [Design.expect, ← Finset.sum_mul, D.sum_one, one_mul]

ExerciseE[f + g] = E[f] + E[g] (core)

Linearity of expectation, additive half. The proof is the entire content of linearity of expectation in a finite sample space, and it is why no independence assumption appears anywhere in Part II’s unbiasedness proofs.

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

theorem ex_expect_add (D : Design n) (f g : Assignment n → ℝ) :
    D.expect (fun z => f z + g z) = D.expect f + D.expect g := by
  sorry

Hint

Unfold Design.expect, distribute D.prob z over the sum with mul_add, then split the finite sum with Finset.sum_add_distrib — one simp only.

Show solution

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

theorem ex_expect_add (D : Design n) (f g : Assignment n → ℝ) :
    D.expect (fun z => f z + g z) = D.expect f + D.expect g := by
  simp only [Design.expect, mul_add, Finset.sum_add_distrib]

ExerciseE[c·f] = c·E[f] (core)

Linearity of expectation, scalar half.

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

theorem ex_expect_const_mul (D : Design n) (f : Assignment n → ℝ) (c : ℝ) :
    D.expect (fun z => c * f z) = c * D.expect f := by
  sorry

Hint

Finset.mul_sum moves c inside the sum, leaving a goal whose two sides differ only in the order of three factors. Finset.sum_congr rfl fun z _ => by ring proves it termwise: rfl says the index set is unchanged, and the function supplies, for each z, a proof that the summands agree.

Show solution

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

theorem ex_expect_const_mul (D : Design n) (f : Assignment n → ℝ) (c : ℝ) :
    D.expect (fun z => c * f z) = c * D.expect f := by
  simp only [Design.expect, Finset.mul_sum]
  exact Finset.sum_congr rfl fun z _ => by ring

ExerciseThe expected observed outcome of one unit (stretch)

The first statistical theorem in the tutorial: unit $i$ ‘s observed outcome averages to $π_{i} y_{1} (i) + (1 - π_{i}) y_{0} (i)$ , where $π_{i} = E [Z_{i}]$ is the propensity. It follows from linearity and sum_one alone, with no assumption about the design.

Notice that this is not an identification result. It says the observed outcome is a $π_{i}$ -weighted mixture of the two potential outcomes, which is a statement about $E [Y_{i}]$ , not about $τ$ . Turning it into a statement about $τ$ is chapter 8’s job and needs the inverse-probability weights.

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

noncomputable def propensity (D : Design n) (i : Fin n) : ℝ :=
  D.expect (fun z => Z z i)

theorem ex_expect_Yobs (D : Design n) (P : Population n) (i : Fin n) :
    D.expect (fun z => Yobs P z i)
      = propensity D i * P.y1 i + (1 - propensity D i) * P.y0 i := by
  sorry

Hint

A have key step is where sum_one enters: ∑ z, D.prob z * (1 - Z z i) becomes 1 - ∑ z, D.prob z * Z z i by mul_sub, mul_one, Finset.sum_sub_distrib and D.sum_one. After that the goal is bookkeeping in one simp only — mul_add, Finset.sum_add_distrib, ← mul_assoc and ← Finset.sum_mul to pull the constants P.y1 i and P.y0 i out of their sums, then key.

Show solution

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

noncomputable def propensity (D : Design n) (i : Fin n) : ℝ :=
  D.expect (fun z => Z z i)

theorem ex_expect_Yobs (D : Design n) (P : Population n) (i : Fin n) :
    D.expect (fun z => Yobs P z i)
      = propensity D i * P.y1 i + (1 - propensity D i) * P.y0 i := by
  have key : ∑ z, D.prob z * (1 - Z z i) = 1 - ∑ z, D.prob z * Z z i := by
    simp only [mul_sub, mul_one, Finset.sum_sub_distrib, D.sum_one]
  simp only [propensity, Design.expect, Yobs, mul_add, Finset.sum_add_distrib,
    ← mul_assoc, ← Finset.sum_mul, key]

Summary of the definitions

The miniature library, and where the real one isNew tabOpens with 122 lines of library preamble — the code above is at the bottom of the editor.

theorem miniature_matches_library (P : Population n) :
    P.tau = mean (fun i => P.y1 i - P.y0 i) := rfl

The claim in that docstring is meant literally. The library’s MrCLean.Basic declares the same Population, the same mean, the same Assignment, the same Z and the same Yobs; its MrCLean.Design declares the same Design and the same Design.expect. Part II adds lemmas, not concepts:

You proved here	Part II calls it
`ex_Z_of_mem`, `ex_Z_of_not_mem`	`Z_of_mem`, `Z_of_not_mem`
`ex_one_sub_Z`	`one_sub_Z`
`ex_Yobs_eq_ite`	`Yobs_eq_ite`
`ex_tau_eq_mean_sub_mean`	`Population.tau_eq_mean_sub_mean`
`ex_expect_const`	`Design.expect_const`
`ex_expect_add`	`Design.expect_add`
`ex_expect_const_mul`	`Design.expect_const_mul`
`propensity`	`Design.propensity`

Six design decisions sit behind those definitions, and they are worth having in mind before Part II: assignments as treated sets rather than indicator vectors, the real-valued indicator, the explicit pmf rather than a measure, one inclusion-probability lemma per design, the division-by-zero convention, and noncomputable. Each is a choice that could have gone the other way, and each has consequences that show up in the shape of every subsequent proof.

Reading autoformalized Lean

Definitions are where autoformalization goes wrong most quietly, because a wrong definition produces a theorem that is true — just not about your problem. Both of the declarations below type-check; neither says what its names suggest.

A population whose outcomes depend on the assignment

structure Population (n : ℕ) where
  y1 : Assignment n → Fin n → ℝ
  y0 : Assignment n → Fin n → ℝ

Asked for “potential outcomes for a population of $n$ units”, a model may produce this, on the reasonable-sounding grounds that outcomes are observed under an assignment. It is a strictly more general object — and it is exactly the object the no-interference assumption exists to rule out, since y1 z i may depend on the treatment status of every unit. Any “unbiasedness” theorem proved about it is a theorem about a different model, and τ is not even well defined: mean (fun i => y1 z i - y0 z i) depends on z.

The tell is an argument that should not be there. Read the type of every field, not the field names: y1 : Fin n → ℝ takes a unit; y1 : Assignment n → Fin n → ℝ takes an experiment. Interference models are a real subject and a type like the second one is how you would formalize one — but then the estimand and every theorem must change too, and a formalization that changes the type without changing anything else has quietly switched problems.

A design that forgot an axiom

structure Design (n : ℕ) where
  prob : Assignment n → ℝ
  nonneg : ∀ z, 0 ≤ prob z

noncomputable def Design.expect (D : Design n) (f : Assignment n → ℝ) : ℝ :=
  ∑ z, D.prob z * f z

example (D : Design n) (c : ℝ) : D.expect (fun _ => c) = c := by
  sorry

Dropping sum_one still gives you something you can define expect on, and expect still satisfies additivity and homogeneity — the two linearity lemmas in this chapter never use sum_one. What fails is E[c] = c, and with it every result that normalizes: unbiasedness, the variance decomposition, the law of total expectation.

The failure is silent in a specific way. Nothing about the definition of expect complains; the missing axiom shows up only when a downstream proof needs it, and if the downstream statements were autoformalized too, they may have been weakened until they no longer do. So audit structures on their own terms: for each field, ask what it is preventing, and construct a value of the type to see what is allowed through. Here ⟨fun _ => 0, fun _ => le_refl 0⟩ type-checks, and it is the zero measure.

The general form of both traps: the theorem is not wrong, the vocabulary is. In the next chapter this becomes a checklist you can run on any statement, including the ones where the vocabulary is Mathlib’s rather than your own.