Potential outcomes

This chapter defines the deterministic part of the design-based model: a finite population of fixed potential outcomes and an assignment that determines which outcome is observed for each unit. Probability enters in Chapter 7. The present definitions are already sufficient to state and prove that the average treatment effect is not identified from a single assignment and outcome vector.

The population is two vectors

There are $n$ units. Unit $i$ carries two numbers: $y_{1} (i)$ , the outcome it would show under treatment, and $y_{0} (i)$ , the outcome it would show under control. Both numbers exist for every unit. At most one of them is ever seen.

DefinitionFinite population

A finite population consists of $n$ units together with, for each unit $i$ , a pair of fixed real numbers $y_{1} (i)$ and $y_{0} (i)$ — its outcomes under treatment and under control. These $2 n$ numbers are the population; nothing about them is random, and no distribution is attached to them.

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

structure … where declares a record; y1 and y0 are its fields. Each is a function Fin n → ℝ, and Fin n is the type with exactly n elements, so a Population 500 is literally a pair of length-500 real vectors. To build one you supply both fields; to take one apart you write P.y1 and P.y0.

Read what is not there. There is no distribution, no error term, no superpopulation the units were drawn from, and no random variable of any kind. P.y1 i is a real number in the same sense that $π$ is: fixed, and mostly unknown to you.¹

The average treatment effect is the mean of the individual effects:

Individual effect and the ATEOpens with 60 lines of library preamble — the code above is at the bottom of the editor.

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

noncomputable def tau : ℝ := mean P.effect

with mean the obvious thing:

The finite-population meanOpens with 43 lines of library preamble — the code above is at the bottom of the editor.

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

tau is a noncomputable def because real division has no algorithm. effect is not, because subtraction does. Neither fact affects a single proof; Lean just insists you say so.

The identity every applied paper opens with is that the average effect is the difference of the two average outcomes.

Proposition. For every population, $τ = {\bar{y}}_{1} - {\bar{y}}_{0}$ , where ${\bar{y}}_{1} = \frac{1}{n} \sum_{i = 1}^{n} y_{1} (i)$ and ${\bar{y}}_{0} = \frac{1}{n} \sum_{i = 1}^{n} y_{0} (i)$ .

Proof.

By definition $τ = \frac{1}{n} \sum_{i = 1}^{n} (y_{1} (i) - y_{0} (i))$ . A finite sum of differences is the difference of the sums, and division distributes over a difference, so

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

No hypothesis on $n$ is needed. At $n = 0$ all three quantities are the empty sum divided by zero, which the division convention makes $0$ , and $0 = 0 - 0$ .∎

τ = mean y1 − mean y0New tabOpens with 64 lines of library preamble — the code above is at the bottom of the editor.

theorem tau_eq_mean_sub_mean : P.tau = mean P.y1 - mean P.y0 :=
  mean_sub P.y1 P.y0

```
mean_sub P.y1 P.y0
```
There is no by: this is a term-mode proof, and the term is the general lemma applied to the two outcome vectors. mean_sub u v : mean (fun i => u i - v i) = mean u - mean v is the whole informal argument in one equation, and it is proved in Basic.lean by the one-line simp only you are asked to reproduce for the additive version in the exercises below: Finset.sum_sub_distrib splits the sum of differences, sub_div splits the division. Instantiated at u := P.y1 and v := P.y0 it reads mean (fun i => P.y1 i - P.y0 i) = mean P.y1 - mean P.y0, and the goal’s left-hand side P.tau unfolds — through tau, then effect — to precisely that mean. Lean checks a term against the goal up to unfolding definitions, so there is nothing left to do.

Interrogating a definition

Three commands do almost all the work of reading someone else’s Lean. #check e prints the type of e. #check @f prints it with the implicit arguments made visible — @ switches off Lean’s habit of filling them in, and it is usually what you want when you are auditing a statement. #print f prints the body of f, which is where the content of a definition lives. And example states a proposition with no name, to be checked and thrown away.

Poking at the definitionsNew tabOpens with 770 lines of library preamble — the code above is at the bottom of the editor.

#check @Population
#check @Population.y1
#check @Population.tau
#check @Z
#check @Yobs

#print Yobs
#print Population.effect

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

example (P : Population 3) (z : Assignment 3) (i : Fin 3) :
    Yobs P z i = Z z i * P.y1 i + (1 - Z z i) * P.y0 i := rfl

rfl proves an equation that holds by unfolding definitions alone. Both examples above are proved by rfl, and that is a meaningful check: the first says Assignment 3 is the same type as Finset (Fin 3) rather than a copy of it, the second says Yobs is by definition the algebraic expression and not merely equal to it by some argument.

Nothing here is abstract. A three-unit population can be written down and its $τ$ computed by hand. Take $y_{1} = (3, 5, 4)$ and $y_{0} = (1, 2, 3)$ ; the individual effects are $(2, 3, 1)$ , so

τ = \frac{(3 - 1) + (5 - 2) + (4 - 3)}{3} = \frac{2 + 3 + 1}{3} = 2,

and treating the first and third units — which Lean, indexing from zero, calls {0, 2} — reveals $y_{1}$ for those two and $y_{0}$ for the middle one, giving the observed vector $(3, 2, 4)$ .

Three units, in fullNew tabOpens with 785 lines of library preamble — the code above is at the bottom of the editor.

def toy : Population 3 where
  y1 := ![3, 5, 4]
  y0 := ![1, 2, 3]

example : toy.tau = 2 := by
  norm_num [Population.tau, mean, Population.effect, toy, Fin.sum_univ_three,
    Matrix.cons_val_two, Matrix.tail_cons, Matrix.head_cons]

example : Yobs toy {0, 2} = ![3, 2, 4] := by
  funext i
  fin_cases i <;> simp [Yobs_eq_ite, toy]

![3, 5, 4] is Mathlib’s notation for a vector, i.e. for a function Fin 3 → ℝ; it is nested, ![a, b, c] being Matrix.vecCons a ![b, c], and that nesting is why the first proof needs the lemma list it does.

```
norm_num [Population.tau, mean, Population.effect, toy, Fin.sum_univ_three,
  Matrix.cons_val_two, Matrix.tail_cons, Matrix.head_cons]
```
One tactic. norm_num [l₁, l₂, …] is simp with the named lemmas added, plus a decision procedure for numeric goals; naming a definition in the list unfolds it. The eight entries do three jobs — unfold the definitions, write the three-term sum out, and read entries out of the vector literals — and are taken in that order below.
```
Population.tau, mean, Population.effect
```
The three definitions. Unfolding them turns toy.tau = 2 into an explicit quotient: the sum over Fin 3 of toy.y1 i - toy.y0 i, divided by 3.
```
Fin.sum_univ_three
```
∑ i, f i = f 0 + f 1 + f 2 for f : Fin 3 → M. There are exactly three units, so the sum is written out. This is the lemma that makes a small design computable at all; the general n case has no such expansion.
```
toy
```
Unfolding toy replaces toy.y1 and toy.y0 by the two vector literals, and what is left is arithmetic on entries of literals.
Goal
```
⊢ (![3, 5, 4] 0 - ![1, 2, 3] 0 + (![3, 5, 4] 1 - ![1, 2, 3] 1) + (![3, 5, 4] 2 - ![1, 2, 3] 2)) / ↑3 = 2
```
```
Matrix.cons_val_two, Matrix.tail_cons, Matrix.head_cons
```
Reading an entry out of ![3, 5, 4] means unwrapping the nesting. Matrix.cons_val_two : (vecCons x u) 2 = vecHead (vecTail u) takes the third entry to the head of the tail, and tail_cons/head_cons then peel one layer each. Entries 0 and 1 need no help — Matrix.cons_val_zero and Matrix.cons_val_one are already simp lemmas — which is exactly why only the index-2 lemmas appear in the list. Drop them and norm_num stops half-way, leaving (8 + ![3, 5, 4] 2 - (3 + ![1, 2, 3] 2)) / 3 = 2.
```
norm_num
```
With every entry a numeral, the arithmetic half of the tactic finishes: $(2 + 3 + 1) / 3 = 2$ in $R$ .

The second example is the whole chapter in miniature. Treating units 0 and 2 reveals y1 0, y0 1, y1 2 — and the three numbers y0 0, y1 1, y0 2, which $τ$ depends on just as much, are not in the observed vector anywhere. Its proof is the standard way to prove two concrete vectors equal.

```
funext i
```
Yobs toy {0, 2} and ![3, 2, 4] are functions Fin 3 → ℝ. Two functions are equal when they agree at every argument, and funext is how you say so: the goal becomes the equation at an arbitrary unit i.
Goal
```
i : Fin 3
⊢ Yobs toy {0, 2} i = ![3, 2, 4] i
```
```
fin_cases i
```
i : Fin 3 has exactly three inhabitants, so fin_cases replaces the variable by each of them in turn, leaving three goals — the equation at unit 0, at unit 1 and at unit 2. (Each index arrives wrapped in the redex (fun i => i) ⟨0, _⟩ that fin_cases leaves behind; simp beta-reduces it without being asked.)
```
<;> simp [Yobs_eq_ite, toy]
```
<;> runs what follows on every goal the previous tactic produced, so one simp call discharges all three branches. In each, Yobs_eq_ite turns the observed outcome into if i ∈ {0, 2} then toy.y1 i else toy.y0 i; membership in a literal set of Fin 3 is decidable, so simp resolves the if by itself — 0 and 2 take the treated branch, 1 the control branch — and toy plus the matrix-literal simp lemmas evaluate both sides to the same numeral.

An assignment is the treated set

An assignment says who got treated. The obvious encoding is a vector of zeros and ones, Fin n → Bool. The library uses the set of treated units instead.

DefinitionAssignment

An assignment is a subset $z \subseteq {1, \dots, n}$ : the units that receive treatment.

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

This is a design decision worth a paragraph, because it is the one that decides how hard the rest of the library is to prove.

“Exactly $n_{1}$ units are treated” becomes Finset.powersetCard n₁ univ, an object Mathlib already knows how to count. Complete randomization in chapter 7 is then a Mathlib lemma away rather than a bespoke combinatorial argument.
Bernoulli assignment sums become Finset.prod_add, again already in Mathlib.
The control group is free: it is zᶜ, and every lemma proved about the treated side transfers to the control side by complementation.
Finset (Fin n) is a Fintype, so ∑ z, … over all $2^{n}$ assignments is a finite sum that needs no extra bookkeeping. That sum is what an expectation over a design will be.

abbrev rather than def matters: an abbrev is reducible, so Lean will unfold Assignment n to Finset (Fin n) on its own, and every Finset lemma and instance applies to an assignment without a word from you.

Nothing downstream pattern-matches on the set. The algebra is written in terms of the indicator, which is real-valued:

The treatment indicatorNew tabOpens with 76 lines of library preamble — the code above is at the bottom of the editor.

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

@[simp] theorem Z_of_mem {z : Assignment n} {i : Fin n} (h : i ∈ z) : Z z i = 1 := ite_eq_left h

@[simp] theorem Z_of_not_mem {z : Assignment n} {i : Fin n} (h : i ∉ z) : Z z i = 0 := ite_eq_right h

The two lemmas beside the definition are the only ways anyone ever gets rid of the if, and both are one-term proofs.

```
ite_eq_left h
```
ite_eq_left : c → (if c then t else e) = t says that an if whose condition holds is its then branch. Applied to h : i ∈ z it proves (if i ∈ z then 1 else 0) = 1, and that is Z z i = 1 once Z is unfolded — which Lean does on its own, since a term is checked against the goal up to unfolding definitions.
```
ite_eq_right h
```
The mirror image: ite_eq_right : ¬c → (if c then t else e) = e picks the else branch, so h : i ∉ z gives Z z i = 0. Both lemmas are tagged @[simp], which is what lets a later simp [hi] clear every indicator out of a goal the moment i’s membership is known.

Z z i is 1 or 0 — the number, not the Boolean and not the proposition. Design-based inference is algebra with indicators. In Bool you would be writing a coercion at every occurrence of Z; in Prop you would be reasoning about propositions rather than computing with them. In ℝ the usual identities are ordinary equations in a field, which is what lets every later chapter hand them to ring, field_simp and linarith. The two that everything is built from have to be proved by hand first, from the case split.

Lemma. For every assignment $z$ and every unit $i$ : (i) $Z_{i}^{2} = Z_{i}$ , and (ii) $1 - Z_{i}$ is the indicator of the control group, $1 - Z_{i} = 1 {i \notin z}$ .

Proof.

$Z_{i}$ takes only the values $0$ and $1$ . For (i), $0^{2} = 0$ and $1^{2} = 1$ , so in both cases $Z_{i}^{2} = Z_{i}$ . For (ii), if $i$ is treated the left side is $1 - 1 = 0$ and $i$ does not lie in the complement of $z$ , so the right side is $0$ too; if $i$ is not treated the left side is $1 - 0 = 1$ and $i$ does lie in the complement, so the right side is $1$ .∎

Z is idempotentOpens with 90 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
  rw [sq, Z_mul_self]

The two theorems in that block are the same fact stated with a product and with a square, and they are proved differently on purpose: the first does the case split, the second reduces to the first.

```
unfold Z
```
unfold Z replaces every Z z i in the goal by its body. Nothing is proved by this; it exposes the if, which is the only thing in the goal a tactic can act on.
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
```
split finds an if in the goal and splits on its condition, producing one goal per branch with the branch already substituted — so both remaining goals are numeric. The hypothesis it introduces is named h✝, with the dagger marking it inaccessible: neither branch needs to mention it, because the condition has already done its work.
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
```
<;> applies what follows to both goals split produced. norm_num evaluates 1 * 1 = 1 and 0 * 0 = 0 in $R$ and closes each.
```
rw [sq, Z_mul_self]
```
The squared form, Z_sq, is now two rewrites. sq : a ^ 2 = a * a (a lemma, despite the name) turns the power into a product, leaving Z z i * Z z i = Z z i; that is exactly Z_mul_self, whose left-hand side rewrites to Z z i, and rw closes a goal that has become rfl.

The control indicatorOpens with 96 lines of library preamble — the code above is at the bottom of the editor.

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

```
unfold Z
```
Both sides carry an indicator, and they are indicators of different sets, so unfolding leaves two ifs with different conditions: i ∈ z on the left, i ∈ zᶜ on the right.
Goal
```
n : ℕ
z : Assignment n
i : Fin n
⊢ (1 - if i ∈ z then 1 else 0) = if i ∈ zᶜ then 1 else 0
```
```
by_cases h : i ∈ z
```
Two goals, one with h : i ∈ z and one with h : i ∉ z. Where Z_mul_self could use split, here it cannot: the two ifs have different conditions, and what is needed is a named hypothesis about i ∈ z that can be used to resolve both of them. by_cases is the tactic that supplies one.
```
<;> simp [h]
```
In the treated branch h sends the left if to 1, and Finset.mem_compl : a ∈ sᶜ ↔ a ∉ s — a simp lemma — turns the right condition into i ∉ z, which h contradicts, so the right if goes to 0; simp then checks 1 - 1 = 0. In the control branch the same two facts point the other way and the goal is 1 - 0 = 1.

The second lemma is the complementation trick made precise: 1 - Z z i is not merely like an indicator, it is the indicator of zᶜ. Every control-side lemma in the rest of the book is a treated-side lemma with zᶜ written for z.

Counting the two groups

Write $n_{1}$ for the number of treated units, $| z |$ , and $n_{0} = n - n_{1}$ for the number of controls. In Lean the treated count arrives as a sum of indicators.

ExerciseThe treated count

Warm-up. The number of treated units is the sum of the indicators: $\sum_{i = 1}^{n} Z_{i} = n_{1}$ .

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

theorem sum_Z (z : Assignment n) : ∑ i, Z z i = (#z : ℝ) := by
  sorry

Hint

A single simp only. Unfold Z; Finset.sum_ite_mem turns the sum of if i ∈ z into a sum over univ ∩ z; Finset.univ_inter simplifies that to z; then Finset.sum_const, nsmul_eq_mul and mul_one turn ∑ i ∈ z, (1 : ℝ) into #z.

Show solution

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

theorem sum_Z (z : Assignment n) : ∑ i, Z z i = (#z : ℝ) := by
  simp only [Z, Finset.sum_ite_mem, Finset.univ_inter, Finset.sum_const, nsmul_eq_mul, mul_one]

and the control count follows by complementation, with no new work:

ExerciseThe control count

Warm-up. The control indicators sum to the number of control units: $\sum_{i = 1}^{n} (1 - Z_{i}) = n_{0}$ .

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

theorem sum_one_sub_Z (z : Assignment n) : ∑ i, (1 - Z z i) = (#zᶜ : ℝ) := by
  sorry

Hint

Two lines. simp only [one_sub_Z] turns every 1 - Z z i into Z zᶜ i, and the goal is then exactly sum_Z zᶜ.

Show solution

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

theorem sum_one_sub_Z (z : Assignment n) : ∑ i, (1 - Z z i) = (#zᶜ : ℝ) := by
  simp only [one_sub_Z]
  exact sum_Z zᶜ

The cast is where it gets annoying. card_compl says #zᶜ = n - #z in ℕ, where subtraction is truncated, and getting that into ℝ requires knowing that the subtraction does not truncate:

ExerciseThe control count, over ℝ

Core. The control count as a real number, $n_{0} = n - n_{1}$ , with the subtraction taken in $R$ . This obstacle recurs in every later chapter that mentions $n_{0}$ .

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

theorem card_compl_cast (z : Assignment n) : ((#zᶜ : ℕ) : ℝ) = (n : ℝ) - #z := by
  sorry

Hint

card_compl gives #zᶜ = n - #z in ℕ, and Nat.cast_sub moves the cast across the subtraction once you hand it a proof of #z ≤ n. Finset.card_le_univ z gives #z ≤ Fintype.card (Fin n), and simpa reduces the right-hand side to n.

Show solution

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

theorem card_compl_cast (z : Assignment n) : ((#zᶜ : ℕ) : ℝ) = (n : ℝ) - #z := by
  have h : #z ≤ n := by simpa using Finset.card_le_univ z
  rw [MrCLean.card_compl, Nat.cast_sub h]

The observed outcome

You see $y_{1} (i)$ for treated units and $y_{0} (i)$ for control units, and that is all you see.

DefinitionObserved outcome

The observed outcome of unit $i$ under an assignment $z$ is the one potential outcome that $z$ reveals: $y_{1} (i)$ if $i$ is treated and $y_{0} (i)$ if it is not. In terms of the treatment indicator,

Y_{i}^{obs} = Z_{i} y_{1} (i) + (1 - Z_{i}) y_{0} (i) .

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

The library takes the algebraic form as the definition and proves the if form as a lemma, rather than the other way round. That ordering is deliberate: the algebraic form is linear in Z, which is what makes every expectation computation in chapters 8 and 9 a rewrite rather than a case split.

ExerciseThe two forms agree

Warm-up. The algebraic form of Yobs agrees with the case split: the observed outcome is y1 i for a treated unit and y0 i for a control unit.

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

theorem 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

unfold Yobs Z replaces both names by their bodies; then by_cases h : i ∈ z splits on membership and simp [h] closes each branch. Note the <;>: it runs the tactic on both goals the by_cases produced.

Show solution

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

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

Once you have that, the two branches follow, and they are the lemmas you will actually reach for.

Lemma. If unit $i$ is treated then $Y_{i}^{obs} = y_{1} (i)$ ; if it is not, $Y_{i}^{obs} = y_{0} (i)$ .

Proof.

Substitute $Z_{i} = 1$ into $Z_{i} y_{1} (i) + (1 - Z_{i}) y_{0} (i)$ for the first, and $Z_{i} = 0$ for the second.∎

What a treated unit and a control unit revealOpens with 146 lines of library preamble — the code above is at the bottom of the editor.

theorem Yobs_of_mem {P : Population n} {z : Assignment n} {i : Fin n} (h : i ∈ z) :
    Yobs P z i = P.y1 i := by rw [Yobs_eq_ite, ite_eq_left h]

theorem Yobs_of_not_mem {P : Population n} {z : Assignment n} {i : Fin n} (h : i ∉ z) :
    Yobs P z i = P.y0 i := by rw [Yobs_eq_ite, ite_eq_right h]

```
rw [Yobs_eq_ite, ite_eq_left h]
```
Two rewrites, and the goal shown is the state between them. Yobs_eq_ite is the exercise above, used left to right: it replaces the algebraic form by the case split. ite_eq_left h then collapses that if using h : i ∈ z, leaving P.y1 i = P.y1 i, which rw closes automatically. Notice that the argument is the informal proof run backwards — rather than substituting $Z_{i} = 1$ into the algebra, it moves to the if form first, where the hypothesis applies directly.
Goal
```
P : Population n
z : Assignment n
i : Fin n
h : i ∈ z
⊢ (if i ∈ z then P.y1 i else P.y0 i) = P.y1 i
```
```
rw [Yobs_eq_ite, ite_eq_right h]
```
The control case, with ite_eq_right for the else branch and h : i ∉ z. Both lemmas take their membership hypothesis implicitly, which is why the statements can be quantified over {i : Fin n} in braces and read like ordinary mathematics at the point of use: Yobs_of_mem hi is “unit i is treated, so it shows y1”.

An exercise in reading Yobs as a regression writes it:

ExerciseThe regression form

Core. The observed outcome written the way a regression writes it: the control outcome plus the individual effect, switched on by the indicator.

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

theorem Yobs_eq_y0_add_Z_mul_effect (P : Population n) (z : Assignment n) (i : Fin n) :
    Yobs P z i = P.y0 i + Z z i * P.effect i := by
  sorry

Hint

simp only [Yobs, Population.effect] unfolds both definitions and then ring proves the resulting polynomial identity in Z z i, P.y1 i, P.y0 i. There is no case split: this is an identity, not a fact about indicators.

Show solution

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

theorem Yobs_eq_y0_add_Z_mul_effect (P : Population n) (z : Assignment n) (i : Fin n) :
    Yobs P z i = P.y0 i + Z z i * P.effect i := by
  simp only [Yobs, Population.effect]
  ring

No interference is a type, not an assumption

In a paper, SUTVA is a numbered assumption you state and then hope nobody checks. Here there is nothing to state. y1 : Fin n → ℝ takes a unit and returns a number; it has no argument in which anybody else’s treatment could appear. A model with interference would need

structure InterferingPopulation (n : ℕ) where
  y : Assignment n → Fin n → ℝ

which is a different structure, so the assumption is not something you can forget: you would have to rewrite the model to violate it.

The consequence is provable rather than assumed.

Proposition (no interference). Let $z$ and $z^{'}$ be assignments that agree about unit $i$ , meaning that $i \in z$ if and only if $i \in z^{'}$ . Then $Y_{i}^{obs} (z) = Y_{i}^{obs} (z^{'})$ , however differently the other $n - 1$ units are treated.

Proof.

By hypothesis, either $i$ is treated under both assignments or under neither. In the first case the previous lemma gives $Y_{i}^{obs} (z) = y_{1} (i) = Y_{i}^{obs} (z^{'})$ ; in the second it gives $Y_{i}^{obs} (z) = y_{0} (i) = Y_{i}^{obs} (z^{'})$ . The rest of $z$ never enters, because $y_{1} (i)$ and $y_{0} (i)$ do not take it as an argument.∎

No interferenceNew tabOpens with 798 lines of library preamble — the code above is at the bottom of the editor.

theorem Yobs_congr (P : Population n) (z z' : Assignment n) (i : Fin n)
    (h : i ∈ z ↔ i ∈ z') : Yobs P z i = Yobs P z' i := by
  rw [Yobs_eq_ite, Yobs_eq_ite]
  by_cases hi : i ∈ z
  · rw [ite_eq_left hi, ite_eq_left (h.mp hi)]
  · rw [ite_eq_right hi, ite_eq_right fun hc => hi (h.mpr hc)]

Read the statement: if two assignments agree about unit i then unit i shows the same observed outcome under both, no matter how differently the other $n - 1$ units are treated. The proof is the informal case split, with ite_eq_left / ite_eq_right — the lemmas that collapse an if once you know which branch you are in — doing the substitution in each case.²

```
rw [Yobs_eq_ite, Yobs_eq_ite]
```
The lemma name appears twice because rw chooses its instantiation from the first match it finds. The first pass matches Yobs P z i, fixing the assignment to z, and rewrites every occurrence of that instance; the second pass then picks up Yobs P z' i. After both, each side of the goal is an if, and the two conditions are the two memberships the hypothesis relates.
Goal
```
P : Population n
z z' : Assignment n
i : Fin n
h : i ∈ z ↔ i ∈ z'
⊢ (if i ∈ z then P.y1 i else P.y0 i) = if i ∈ z' then P.y1 i else P.y0 i
```
```
by_cases hi : i ∈ z
```
The case split of the informal proof, on the left assignment. Two goals, one with hi : i ∈ z and one with hi : i ∉ z, and in each the hypothesis h will transport that membership to z'.
```
· rw [ite_eq_left hi, ite_eq_left (h.mp hi)]
```
The treated branch — the · is a bullet, which focuses the first remaining goal. ite_eq_left hi collapses the left if to P.y1 i. For the right if the condition is i ∈ z', and h.mp hi supplies a proof of it: h is an Iff, so h.mp is its forward direction, and applying it to hi gives i ∈ z'. The goal becomes P.y1 i = P.y1 i and rw closes it.
```
· rw [ite_eq_right hi, ite_eq_right fun hc => hi (h.mpr hc)]
```
The control branch, and the one place in this chapter where a proof term is built inline. ite_eq_right needs i ∉ z', which is by definition i ∈ z' → False, so a function is what has to be supplied: given hc : i ∈ z', the backward direction h.mpr hc turns it into i ∈ z, and feeding that to hi : i ∉ z yields False. Both sides become P.y0 i.

The fundamental problem of causal inference

Informally: you observe one potential outcome per unit, never both, so $τ$ is not a function of the data. Stated that baldly it is not yet a theorem — “function of the data” needs saying in a way Lean can check. The sharp version is that the observed vector constrains $τ$ not at all.

Theoremτ is not identified

Suppose $n \geq 1$ . Fix an assignment $z$ , a population $P$ and any real number $t$ . Then there is a population $P^{'}$ with exactly the same observed outcome vector under $z$ and with $τ (P^{'}) = t$ .

An analyst who sees $Y^{obs}$ and knows $z$ — which is everything a single experiment yields — can therefore rule out no value of $τ$ whatsoever.

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

theorem exists_population_tau_eq (hn : 0 < n) (P : Population n) (z : Assignment n) (t : ℝ) :
    ∃ P' : Population n, Yobs P' z = Yobs P z ∧ P'.tau = t := by
  refine ⟨shift P z (t - P.tau), Yobs_shift P z _, ?_⟩
  rw [tau_shift hn]
  ring

Proof.

Put $c = t - τ (P)$ and define $P^{'}$ by leaving every observed potential outcome where it is and moving each unobserved one just far enough to raise that unit’s effect by $c$ : a treated unit’s $y_{0}$ down by $c$ , a control unit’s $y_{1}$ up by $c$ .

y_{1}^{'} (i) = {\begin{cases} y_{1} (i) & i \in z \\ y_{1} (i) + c & i \notin z, \end{cases} y_{0}^{'} (i) = {\begin{cases} y_{0} (i) - c & i \in z \\ y_{0} (i) & i \notin z . \end{cases}

Under $z$ every unit reveals the outcome that was left alone — a treated unit its $y_{1}$ , a control unit its $y_{0}$ — so $Y^{obs} (P^{'}, z) = Y^{obs} (P, z)$ . And in both cases the individual effect rises by exactly $c$ : for a treated unit $y_{1}^{'} (i) - y_{0}^{'} (i) = y_{1} (i) - (y_{0} (i) - c)$ , and for a control unit $y_{1}^{'} (i) - y_{0}^{'} (i) = y_{1} (i) + c - y_{0} (i)$ , which is the same number. Averaging over the $n$ units, $τ (P^{'}) = τ (P) + c = t$ , which is where $n \geq 1$ is used: the average of the constant $c$ is $c$ only when there is at least one unit to average over.∎

The construction is one definition, and it is the display above transcribed:

Perturbing what you cannot seeOpens with 815 lines of library preamble — the code above is at the bottom of the editor.

def shift (P : Population n) (z : Assignment n) (c : ℝ) : Population n where
  y1 := fun i => if i ∈ z then P.y1 i else P.y1 i + c
  y0 := fun i => if i ∈ z then P.y0 i - c else P.y0 i

The two ifs lean opposite ways for the reason the informal proof gives — the entry a treated unit hides is its y0, the entry a control unit hides is its y1 — and that is exactly why nothing observable moves:

Same observed dataNew tabOpens with 820 lines of library preamble — the code above is at the bottom of the editor.

theorem Yobs_shift (P : Population n) (z : Assignment n) (c : ℝ) :
    Yobs (shift P z c) z = Yobs P z := by
  funext i
  by_cases h : i ∈ z <;> simp [Yobs_eq_ite, shift, h]

```
funext i
```
The statement is an equation between two vectors, Yobs (shift P z c) z and Yobs P z. Two functions are equal when they agree everywhere, and funext is how you say so in Lean: the goal becomes the equation at an arbitrary unit i.
Goal
```
P : Population n
z : Assignment n
c : ℝ
i : Fin n
⊢ Yobs (shift P z c) z i = Yobs P z i
```
```
by_cases h : i ∈ z
```
The case split of the informal proof, on whether i was treated. Both branches are needed because shift is defined by an if on exactly this condition.
```
<;> simp [Yobs_eq_ite, shift, h]
```
One simp call closes both goals. Yobs_eq_ite turns each side into an if; shift unfolds the perturbed population’s two fields; h then resolves every if in sight — the two Yobs_eq_ite produced, one per side, and the one inside whichever shift field the first of them selected — and both sides reduce to P.y1 i in the treated branch and to P.y0 i in the control branch. That the unshifted outcome survives is the whole content: the entry shift moved is the entry this assignment does not reveal.

The effect moves uniformly, so the average moves with it:

τ moves by exactly cNew tabOpens with 825 lines of library preamble — the code above is at the bottom of the editor.

theorem tau_shift (hn : 0 < n) (P : Population n) (z : Assignment n) (c : ℝ) :
    (shift P z c).tau = P.tau + c := by
  have heff : (shift P z c).effect = fun i => P.effect i + c := by
    funext i
    by_cases h : i ∈ z <;> simp [Population.effect, shift, h] <;> ring
  calc (shift P z c).tau
      = mean (fun i => P.effect i + c) := by simp only [Population.tau, heff]
    _ = mean P.effect + mean (fun _ : Fin n => c) := mean_add P.effect fun _ => c
    _ = P.tau + c := by simp only [mean_const hn, Population.tau]

```
have heff : (shift P z c).effect = fun i => P.effect i + c := by
```
The pointwise half of the informal proof, isolated as a named fact because the calc chain below needs it as a rewrite. It says the shifted effect vector is the original plus the constant c — an equation between functions, so its own proof starts with funext.
```
funext i
```
Inside the have: reduce the vector equation to the equation at one unit.
Goal
```
⊢ (shift P z c).effect i = P.effect i + c
```
```
by_cases h : i ∈ z <;> simp [Population.effect, shift, h] <;> ring
```
Split on membership, then simp unfolds effect and shift and resolves the ifs, and the two goals shown are what it leaves. Both are true by ordinary algebra but neither is syntactically the goal — the treated branch has to move a minus sign across a bracket, the control branch has to reassociate — so a second <;> hands each to ring, which proves any identity that holds in a commutative ring. Note that this is the step where the two opposite ifs in shift pay off: a treated unit gains c by having y0 lowered, a control unit by having y1 raised, and the two branches end up at the same expression.
Goal
```
case pos
h : i ∈ z
⊢ P.y1 i - (P.y0 i - c) = P.y1 i - P.y0 i + c

case neg
h : i ∉ z
⊢ P.y1 i + c - P.y0 i = P.y1 i - P.y0 i + c
```
```
calc (shift P z c).tau = mean (fun i => P.effect i + c) := by simp only [Population.tau, heff]
```
The averaging half, as a calc chain: three steps, each stating an equation whose right-hand side is the next step’s left-hand side. Here Population.tau unfolds $τ$ to the mean of the effect vector, and heff rewrites that vector to fun i => P.effect i + c.
```
_ = mean P.effect + mean (fun _ : Fin n => c) := mean_add P.effect fun _ => c
```
The _ stands for the previous right-hand side. This step is the exercise at the end of the chapter, applied in term mode: the mean of a pointwise sum is the sum of the means. Its two arguments are the two summands, P.effect and the constant function fun _ => c.
```
_ = P.tau + c := by simp only [mean_const hn, Population.tau]
```
mean_const hn : mean (fun _ : Fin n => c) = c — and this is the one place hn : 0 < n is used, because with no units the mean of a constant is $0 / 0 = 0$ , not $c$ . Folding mean P.effect back into P.tau finishes the chain. With no units at all every population has $τ = 0 / 0 = 0$ and nothing can be shifted, which is why the hypothesis is not decoration.

That is everything the theorem needs. Its own proof — the three lines beside the statement at the head of this section — spends the two lemmas just proved and does no mathematics of its own.

```
refine ⟨shift P z (t - P.tau), Yobs_shift P z _, ?_⟩
```
The goal is an existential with a conjunction inside it, so one anonymous constructor ⟨…⟩ supplies all three pieces at once: the witness $P^{'}$ , which is P shifted by c = t - P.tau; the proof that the observed vectors agree, which is Yobs_shift with _ for the shift amount Lean can read off the goal; and ?_, which postpones the last component as a new goal. refine is exact with holes.
```
rw [tau_shift hn]
```
The remaining goal is (shift P z (t - P.tau)).tau = t. Rewriting with tau_shift hn replaces the left-hand side by P.tau + (t - P.tau).
```
ring
```
P.tau + (t - P.tau) = t is an identity in a commutative ring, and ring proves it. The cancellation is the reason the witness was t - P.tau rather than anything more clever: choosing the shift is choosing the answer.

The form one usually says out loud follows immediately.

Corollary (the fundamental problem). Suppose $n \geq 1$ and fix an assignment $z$ . Then there are two populations with the same observed outcome vector under $z$ and different average treatment effects.

Proof.

Let $P$ be the population with $y_{1} \equiv y_{0} \equiv 0$ , so that $τ (P) = 0$ . Apply the theorem to $P$ , $z$ and $t = 1$ : it produces a population $P^{'}$ with $Y^{obs} (P^{'}, z) = Y^{obs} (P, z)$ and $τ (P^{'}) = 1 \neq 0 = τ (P)$ . The pair $(P, P^{'})$ is the one required.∎

Two populations, one data setNew tabOpens with 841 lines of library preamble — the code above is at the bottom of the editor.

theorem fundamental_problem (hn : 0 < n) (z : Assignment n) :
    ∃ P P' : Population n, Yobs P z = Yobs P' z ∧ P.tau ≠ P'.tau := by
  obtain ⟨P', hY, ht⟩ :=
    exists_population_tau_eq hn (⟨fun _ => 0, fun _ => 0⟩ : Population n) z 1
  refine ⟨⟨fun _ => 0, fun _ => 0⟩, P', hY.symm, ?_⟩
  have h0 : (⟨fun _ => 0, fun _ => 0⟩ : Population n).tau = 0 := by
    simp [Population.tau, Population.effect, mean]
  rw [h0, ht]
  norm_num

```
obtain ⟨P', hY, ht⟩ := exists_population_tau_eq hn (⟨fun _ => 0, fun _ => 0⟩ : Population n) z 1
```
Instantiate the theorem at the all-zero population — ⟨fun _ => 0, fun _ => 0⟩ is the anonymous constructor again, building a Population n out of its two fields — and at $t = 1$ . What comes back is an existential, and obtain destructures it in one move: P' is the witness, hY the agreement of the observed vectors, ht the fact that P'.tau = 1.
Goal
```
n : ℕ
hn : 0 < n
z : Assignment n
P' : Population n
hY : Yobs P' z = Yobs { y1 := fun x => 0, y0 := fun x => 0 } z
ht : P'.tau = 1
⊢ ∃ P P', Yobs P z = Yobs P' z ∧ P.tau ≠ P'.tau
```
```
refine ⟨⟨fun _ => 0, fun _ => 0⟩, P', hY.symm, ?_⟩
```
Supply the two populations of the corollary, in the order the statement wants them: the all-zero one first, P' second. hY.symm rather than hY because the theorem produced Yobs P' z = Yobs P z and the goal asks for the reverse — .symm on an equation flips it. The inequality is left as ?_.
Goal
```
hY : Yobs P' z = Yobs { y1 := fun x => 0, y0 := fun x => 0 } z
ht : P'.tau = 1
⊢ { y1 := fun x => 0, y0 := fun x => 0 }.tau ≠ P'.tau
```
```
have h0 : (⟨fun _ => 0, fun _ => 0⟩ : Population n).tau = 0 := by simp [Population.tau, Population.effect, mean]
```
The one arithmetic fact the corollary needs: the all-zero population has $τ = 0$ . Unfolding the three definitions makes the goal (∑ i, (0 - 0)) / n = 0, and simp finishes it — the sum of zeros is zero, and 0 / n is 0 whatever n is, so hn is not needed here.
```
rw [h0, ht]
```
Rewrite both sides of the inequality with the values just computed: h0 replaces the left-hand $τ$ by 0, ht the right-hand one by 1. The goal is now (0 : ℝ) ≠ 1.
```
norm_num
```
A numeric fact about $R$ , which is what norm_num is for. Note how little of the work is here: the mathematics was the shift construction, and this last theorem only picks a convenient $P$ and a convenient $t$ .

What the data does pin down is exactly the treated units’ y1 and the control units’ y0:

ExerciseEverything an experiment tells you

Core. Two populations have the same observed vector under $z$ exactly when they agree on y1 over the treated units and on y0 over the control units. Read the right-hand side as the exact inventory of what a single experiment can ever tell you.

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

theorem Yobs_eq_iff (P P' : Population n) (z : Assignment n) :
    Yobs P z = Yobs P' z ↔ (∀ i ∈ z, P.y1 i = P'.y1 i) ∧ (∀ i ∉ z, P.y0 i = P'.y0 i) := by
  sorry

Hint

constructor splits the ↔. Forward: congrFun h i gives the equation at unit i, and rewriting both sides with Yobs_of_mem hi (or Yobs_of_not_mem hi, depending on the branch) reads off the answer — rwa is rw followed by assumption. Backward: funext i, by_cases hi : i ∈ z, and the same two lemmas together with h1 i hi or h0 i hi.

Show solution

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

theorem Yobs_eq_iff (P P' : Population n) (z : Assignment n) :
    Yobs P z = Yobs P' z ↔ (∀ i ∈ z, P.y1 i = P'.y1 i) ∧ (∀ i ∉ z, P.y0 i = P'.y0 i) := by
  constructor
  · intro h
    refine ⟨fun i hi => ?_, fun i hi => ?_⟩
    · have hc := congrFun h i
      rwa [Yobs_of_mem hi, Yobs_of_mem hi] at hc
    · have hc := congrFun h i
      rwa [Yobs_of_not_mem hi, Yobs_of_not_mem hi] at hc
  · rintro ⟨h1, h0⟩
    funext i
    by_cases hi : i ∈ z
    · rw [Yobs_of_mem hi, Yobs_of_mem hi, h1 i hi]
    · rw [Yobs_of_not_mem hi, Yobs_of_not_mem hi, h0 i hi]

None of this is fixed by collecting more units, and none of it is fixed by measuring more carefully. It is fixed — in the weaker sense of “made estimable on average” — by making $z$ random, which is the subject of the next chapter. The estimators of chapter 8 are not functions that recover $τ$ from the data; they are functions whose average over the design equals $τ$ . Chapter 9 then asks how far from $τ$ any single realization is likely to be.

Exercises

The exercises above are the load-bearing ones. Three more, in increasing order of effort.

ExerciseWarm-up: the mean is additive

The mean of a pointwise sum is the sum of the means.

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

theorem mean_add (u v : Fin n → ℝ) : mean (fun i => u i + v i) = mean u + mean v := by
  sorry

Hint

One simp only with three lemmas: mean to unfold the definition, Finset.sum_add_distrib to split the sum, add_div to split the division.

Show solution

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

theorem mean_add (u v : Fin n → ℝ) : mean (fun i => u i + v i) = mean u + mean v := by
  simp only [mean, Finset.sum_add_distrib, add_div]

ExerciseWarm-up: everybody treated

If everybody is treated, the observed vector is y1. Note the corollary: even in this extreme case y0 is entirely unobserved, so exists_population_tau_eq still applies.

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

theorem Yobs_univ (P : Population n) : Yobs P Finset.univ = P.y1 := by
  sorry

Hint

funext i reduces to a single unit, and Yobs_of_mem (Finset.mem_univ i) is the whole proof — Finset.mem_univ i is the proof that every unit belongs to univ.

Show solution

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

theorem Yobs_univ (P : Population n) : Yobs P Finset.univ = P.y1 := by
  funext i
  exact Yobs_of_mem (Finset.mem_univ i)

ExerciseStretch: the mean of the observed vector

The mean of the observed vector is the treated units’ y1 and the control units’ y0, averaged over the whole population. Having proved it, notice that z appears in the statement and $τ$ does not: this quantity estimates nothing.

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

theorem mean_Yobs (P : Population n) (z : Assignment n) :
    mean (Yobs P z) = ((∑ i ∈ z, P.y1 i) + ∑ i ∈ zᶜ, P.y0 i) / n := by
  sorry

Hint

Work on the right-hand side: sum_mem_eq_sum_Z_mul and sum_compl_eq_sum_one_sub_Z_mul, used left to right, turn the two group sums into indicator-weighted sums over everybody, and ← Finset.sum_add_distrib merges them into one sum. Both sides are then the same expression up to unfolding mean and Yobs, so rfl finishes. Resist simp here: mean and the two sum lemmas loop against each other, which is what the “possibly looping simp theorem” warning is telling you.

Show solution

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

theorem mean_Yobs (P : Population n) (z : Assignment n) :
    mean (Yobs P z) = ((∑ i ∈ z, P.y1 i) + ∑ i ∈ zᶜ, P.y0 i) / n := by
  rw [sum_mem_eq_sum_Z_mul, sum_compl_eq_sum_one_sub_Z_mul, ← Finset.sum_add_distrib]
  rfl

Reading autoformalized Lean

Suppose you asked a model to formalize “the fundamental problem of causal inference” and got one of the following. Each type-checks. None of them says it.

The quantifiers swapped

theorem fundamental_problem (hn : 0 < n) (z : Assignment n) (P P' : Population n) :
    Yobs P z = Yobs P' z → P.tau ≠ P'.tau

The hypothesis nobody can satisfy

theorem fundamental_problem' (hn : 0 < n) (z : Assignment n) (y : Fin n → ℝ)
    (h : ∀ P : Population n, Yobs P z = y) :
    ∃ P P' : Population n, Yobs P z = Yobs P' z ∧ P.tau ≠ P'.tau

The definition doing the theorem’s work

def Yobs (P : Population n) (z : Assignment n) (i : Fin n) : ℝ := P.y1 i

This is Neyman’s 1923 model, and the reason the tutorial is arranged around it is that its randomness has exactly one source. A Lean development of the superpopulation version would need measure theory on page one; this one needs finite sums. ↩
If you have read older Lean 4 code you will know these as if_pos and if_neg. They are deprecated as of v4.34, and Mathlib is mid-migration on several such names. ↩

The population is two vectors

Interrogating a definition

An assignment is the treated set

Counting the two groups

The observed outcome

No interference is a type, not an assumption

The fundamental problem of causal inference

Exercises

Reading autoformalized Lean

The quantifiers swapped

The hypothesis nobody can satisfy

The definition doing the theorem’s work

Footnotes