Structures and definitions

The previous three chapters were about the ingredients: terms, types, tactics, real numbers, finite sums. This chapter is about assembling them into vocabulary — the handful of named objects that the rest of the tutorial talks about — and about the tactics you need in order to work with a definition once you have made one.

By the end of it you will have rebuilt, in miniature, the library that Part II uses: Population, mean, tau, Assignment, Z, Yobs, Design, expect, and linearity of expectation. Not an analogue of it, and not a simplification of it — the same names, with the same definitions, differing only in how many lemmas hang off them. Everything you prove here is proved again in lean/MrCLean/, at scale.

Every code block on this page is quoted from lean/MrCLean/Fundamentals/Ch04Structures.lean, which CI compiles.

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:

-- workable, and unpleasant
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` is a labelled tuple.  Declaring one gives you, for free: a
constructor `SummaryStats.mk`, one projection per field, and the anonymous
constructor notation `⟨_, _, _⟩`. -/
structure SummaryStats where
  /-- Number of observations. -/
  size : ℕ
  /-- Sample mean. -/
  xbar : ℚ

/-- Three ways to write the same value: named fields, the anonymous constructor,
and the explicit constructor. -/
def treatedGroup : SummaryStats := { size := 4, xbar := 7 / 2 }
def controlGroup : SummaryStats := ⟨6, 5 / 2⟩
def wholeSample : SummaryStats := SummaryStats.mk 10 3

/- Projections are applied like any function, and `s.field` is sugar for
`SummaryStats.field s`. -/
#eval treatedGroup.size          -- 4
#eval SummaryStats.xbar controlGroup  -- 5/2
#eval wholeSample.xbar           -- 3

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

/-- Anything defined in `namespace Population` whose first explicit argument is a
`Population` can be written with a dot: `P.totalEffect` *is*
`Population.totalEffect P`.  That is all dot notation is, and it is why the
library puts facts about designs in `namespace Design`. -/
def Population.totalEffect (P : Population n) : ℝ := ∑ i, P.effect i

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

/-- Dot notation chains: `P.effect i` inside, `P.totalEffect` outside. -/
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 \mathbb{R}$, both fixed. Unit $i$‘s treatment effect is $y_1(i)-y_0(i)$, and the average treatment effect is

Formally.

/-- A **finite population** of `n` units, described by its potential outcomes.
`y1 i` is what unit `i` would show if treated, `y0 i` what it would show under
control.  Both are fixed real numbers: nothing here is random.

Because `y1` and `y0` are functions of a single unit, no unit's outcome can
depend on anybody else's assignment — SUTVA is enforced by the type. -/
structure Population (n : ℕ) where
  /-- Outcome under treatment. -/
  y1 : Fin n → ℝ
  /-- Outcome under control. -/
  y0 : Fin n → ℝ

/-- The finite-population mean, `(∑ i, v i) / n`. -/
noncomputable def mean (v : Fin n → ℝ) : ℝ := (∑ i, v i) / n

namespace Population

/-- The individual treatment effect of unit `i`. -/
def effect (P : Population n) (i : Fin n) : ℝ := P.y1 i - P.y0 i

/-- The average treatment effect, `τ = (1/n) ∑ i, (y1 i - 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. lean/SPEC.md §3.5 records this as a deliberate choice.

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 $\mathbb{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

/-- Three ways to name something, differing only in how eagerly Lean unfolds it.

* `abbrev` is a definition marked *reducible*: `Assignment n` and
  `Finset (Fin n)` are interchangeable without asking.
* `def` unfolds when you ask (`unfold`, `simp only [name]`, or `rfl`).
* `theorem` produces a proof, and proofs are opaque: two proofs of the same
  proposition are equal and their content is never inspected. -/
example : Assignment 3 = Finset (Fin 3) := rfl

/-- A `def` still unfolds definitionally, so `rfl` sees through it. -/
example (z : Assignment 3) (i : Fin 3) : Z z i = if i ∈ z then 1 else 0 := rfl

/- Use `abbrev` for a synonym you want Lean to see through everywhere, and `def`
for a real definition you want to control with `simp only [defn]`. -/
#check @Assignment      -- ℕ → Type

• 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.

/-- An **assignment** is the set of treated units. -/
abbrev Assignment (n : ℕ) := Finset (Fin n)

/-- The **treatment indicator**, as a real number so that ordinary algebra
applies to it. -/
def Z (z : Assignment n) (i : Fin n) : ℝ := if i ∈ z then 1 else 0

/-- The **observed outcome**: the potential outcome the assignment reveals. -/
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 choices here are load-bearing enough that lean/SPEC.md argues for them at length.

An assignment is a treated set, not a vector of bits (§3.1). 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 (§3.2). Design-based inference is algebra with indicators: $Z_i^2=Z_i$, $\mathbb{E}[Z_i]={\pi }_i$, $Y_i=Z_i{y}_1(i)+(1-Z_i)y_0(i)$. Keeping Z in $\mathbb{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.

/-- Three ways to open up a definition, from bluntest to most controlled.
`unfold Z` replaces `Z` by its body everywhere; `simp only [Z]` does the same via
the equation lemma and keeps simplifying; `show` restates the goal in a form you
choose.  The `split` tactic then handles the `if`. -/
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

/-- Same lemma, `simp only` style — the style the library prefers, because the
list of facts used is written down. -/
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 (1 * 1 = 1 and 0 * 0 = 0), so norm_num finishes them, and <;> applies norm_num to every goal split produced.

/-- `show` and `change` both restate the goal as something *definitionally* equal.
`show` is the readable one: it documents, in the proof, what you believe the goal
now is.  If you are wrong, Lean says so immediately. -/
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

/-- `change` is the same move with a different keyword, and is happy in the
middle of a proof. -/
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.

When are two of these things equal?

/-- Outcome vectors are functions, so they are equal exactly when they agree unit
by unit.  That is `funext`. -/
theorem outcomes_eq (u v : Fin n → ℝ) (h : ∀ i, u i = v i) : u = v := by
  funext i
  exact h i

/-- `ext` is the general form: it looks up whichever extensionality lemma fits the
goal.  Assignments are `Finset`s, and for those extensionality is membership. -/
theorem assignments_eq (z w : Assignment n) (h : ∀ i, i ∈ z ↔ i ∈ w) : z = w := by
  ext i
  exact h i

/-- Structures are equal when their fields are.  Lean generates the injectivity
lemma `Population.mk.injEq` alongside the structure; with `funext` it gives
extensionality for populations.  (`ext` itself does not fire here: nobody tagged
`Population` with the `@[ext]` attribute.) -/
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.

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. The obtain ⟨a1, a0⟩ := P lines are destructuring: they replace the opaque P by its two fields, which is what lets mk.injEq fire.

Note the parenthetical in the docstring: ext does not work on Population, because nobody tagged the structure with @[ext]. 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 = Finset (Fin n)` is a `Fintype`: Lean knows how to enumerate
all `2 ^ n` assignments, which is exactly what makes `∑ z, …` — an expectation
over the design — a legal finite sum with no measure theory in sight. -/
#eval Fintype.card (Assignment 3)                       -- 8
#eval (Finset.univ : Finset (Assignment 3)).card        -- 8

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.

Fintype.card_finset is the lemma $|\mathcal{P}(\alpha )|=2^{|\alpha |}$, and Fintype.card_fin says $|\mathrm{Fin}n|=n$; chaining the two rewrites gives $2^n$.

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.

/- Complete randomisation treats exactly `n₁` units, so its support is the set of
assignments of size `n₁`.  That set is a Mathlib object: `Finset.powersetCard`,
whose cardinality is the binomial coefficient. -/
#eval ((Finset.univ : Finset (Fin 4)).powersetCard 2).card    -- 6 = C(4,2)

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 $(\genfrac{}{}{0ex}{}{|s|}{k})$ of them. This is the payoff from §3.1’s 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 ${\pi }_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.

/-- A **design** is a probability mass function on assignments — the only random
object in design-based inference. -/
structure Design (n : ℕ) where
  /-- Probability of drawing the assignment `z`. -/
  prob : Assignment n → ℝ
  /-- Probabilities are nonnegative. -/
  nonneg : ∀ z, 0 ≤ prob z
  /-- Probabilities sum to one over all `2 ^ n` assignments. -/
  sum_one : ∑ z, prob z = 1

/-- Expectation over the randomisation: a finite sum, no measure theory. -/
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.

lean/SPEC.md §3.3 argues for the explicit pmf over a Mathlib PMF or a measure. The argument 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.

/-- Building a `Design` means supplying the pmf *and* proving the two axioms —
the structure will not let you forget.  Here is the simplest design: every one of
the `2 ^ n` assignments equally likely, which is the Bernoulli design at
`p = 1/2`. -/
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

/-- Its probabilities are what you expect. -/
theorem uniformDesign_prob (m : ℕ) (z : Assignment m) :
    (uniformDesign m).prob z = 1 / 2 ^ m := rfl

Building uniformDesign means proving the two axioms, and the sum_one proof is a worked example of summing over assignments: Finset.sum_const (a sum of a constant is the cardinality smul the constant), Finset.card_univ and Fintype.card_finset supply $2^n$ terms, nsmul_eq_mul converts the scalar action into multiplication, push_cast moves the coercion ℕ → ℝ inward past the 2 ^ m, and field_simp clears the denominator. positivity proves the nonneg field: it is a tactic that proves goals of the form 0 ≤ e or 0 < e by structural recursion on e.

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.

/-- Exercise (warm-up).  A treated unit has indicator `1`.  Open the definition
(`unfold Z`) and dispatch the `if` — `ite_eq_left h` is the term that says
"the condition holds, so take the left branch". -/
theorem ex_Z_of_mem {z : Assignment n} {i : Fin n} (h : i ∈ z) : Z z i = 1 := by
  sorry

/-- Exercise (warm-up).  A treated unit has indicator `1`.  Open the definition
(`unfold Z`) and dispatch the `if` — `ite_eq_left h` is the term that says
"the condition holds, so take the left branch". -/
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

/-- Exercise (warm-up).  A control unit has indicator `0`.  Same shape as the
previous exercise, with `ite_eq_right`. -/
theorem ex_Z_of_not_mem {z : Assignment n} {i : Fin n} (h : i ∉ z) : Z z i = 0 := by
  sorry

/-- Exercise (warm-up).  A control unit has indicator `0`.  Same shape as the
previous exercise, with `ite_eq_right`. -/
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

/-- Exercise (core).  **The control indicator is the indicator of the complement**:
`1 - Z z i = Z zᶜ i`.  This is what makes every treated-side lemma reusable on
the control side.

Unfold `Z` and split on `i ∈ z`; `simp [h]` finishes each branch (it needs
`Finset.mem_compl` to see through the complement). -/
theorem ex_one_sub_Z (z : Assignment n) (i : Fin n) : 1 - Z z i = Z zᶜ i := by
  sorry

/-- Exercise (core).  **The control indicator is the indicator of the complement**:
`1 - Z z i = Z zᶜ i`.  This is what makes every treated-side lemma reusable on
the control side.

Unfold `Z` and split on `i ∈ z`; `simp [h]` finishes each branch (it needs
`Finset.mem_compl` to see through the complement). -/
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]

/-- Exercise (core).  **The observed outcome is the revealed potential outcome.**
The algebraic definition `Z·y1 + (1-Z)·y0` agrees with the case split a
statistician would write.  The algebraic form is the one that plays well with
linearity of expectation; this lemma says you lose nothing by using it. -/
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

/-- Exercise (core).  **The observed outcome is the revealed potential outcome.**
The algebraic definition `Z·y1 + (1-Z)·y0` agrees with the case split a
statistician would write.  The algebraic form is the one that plays well with
linearity of expectation; this lemma says you lose nothing by using it. -/
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]

/-- Exercise (core).  **The ATE is the difference of the two potential-outcome
means.**  Unfold `tau`, `effect` and `mean`, then split the sum
(`Finset.sum_sub_distrib`) and the division (`sub_div`). -/
theorem ex_tau_eq_mean_sub_mean (P : Population n) :
    P.tau = mean P.y1 - mean P.y0 := by
  sorry

/-- Exercise (core).  **The ATE is the difference of the two potential-outcome
means.**  Unfold `tau`, `effect` and `mean`, then split the sum
(`Finset.sum_sub_distrib`) and the division (`sub_div`). -/
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]

/-- Exercise (core).  **The expectation of a constant is that constant.**  This is
the one place where the axiom `sum_one` is used, and it is the reason a `Design`
has to carry it.  Pull the constant out with `← Finset.sum_mul`, then rewrite
with `D.sum_one`. -/
theorem ex_expect_const (D : Design n) (c : ℝ) : D.expect (fun _ => c) = c := by
  sorry

/-- Exercise (core).  **The expectation of a constant is that constant.**  This is
the one place where the axiom `sum_one` is used, and it is the reason a `Design`
has to carry it.  Pull the constant out with `← Finset.sum_mul`, then rewrite
with `D.sum_one`. -/
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]

/-- Exercise (core).  **Linearity of expectation**, additive half.  Note what is
*not* needed: no independence, no distributional assumption.  It is
`Finset.sum_add_distrib` wearing a hat. -/
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

/-- Exercise (core).  **Linearity of expectation**, additive half.  Note what is
*not* needed: no independence, no distributional assumption.  It is
`Finset.sum_add_distrib` wearing a hat. -/
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]

/-- Exercise (core).  **Linearity of expectation**, scalar half.  `Finset.mul_sum`
moves the constant inside the sum; `ring` fixes up the order of the factors
termwise via `Finset.sum_congr`. -/
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

/-- Exercise (core).  **Linearity of expectation**, scalar half.  `Finset.mul_sum`
moves the constant inside the sum; `ring` fixes up the order of the factors
termwise via `Finset.sum_congr`. -/
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

/-- Exercise (stretch).  **The expected observed outcome of one unit.**  Writing
`π i` for the propensity `E[Z i]`, the observed outcome of unit `i` averages to
`π i · y1 i + (1 - π i) · y0 i`: the design mixes the two potential outcomes in
the proportion in which it reveals them.

This is the first genuinely statistical theorem in the tutorial, and it needs
only the pieces you have already proved: linearity, and `sum_one`.

Shape of the proof: unfold `expect` and `Yobs`, distribute
(`mul_add`, `Finset.sum_add_distrib`), pull the constants `y1 i`, `y0 i` out with
`← Finset.sum_mul` after re-associating, and use `sum_one` for the `1`. -/
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

/-- Exercise (stretch).  **The expected observed outcome of one unit.**  Writing
`π i` for the propensity `E[Z i]`, the observed outcome of unit `i` averages to
`π i · y1 i + (1 - π i) · y0 i`: the design mixes the two potential outcomes in
the proportion in which it reveals them.

This is the first genuinely statistical theorem in the tutorial, and it needs
only the pieces you have already proved: linearity, and `sum_one`.

Shape of the proof: unfold `expect` and `Yobs`, distribute
(`mul_add`, `Finset.sum_add_distrib`), pull the constants `y1 i`, `y0 i` out with
`← Finset.sum_mul` after re-associating, and use `sum_one` for the `1`. -/
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]

What you have just built

/-- **This is Part II's library, in miniature.**

`lean/MrCLean/Basic.lean` and `lean/MrCLean/Design.lean` contain exactly the
definitions above — same names, same conventions — plus the lemmas the headline
theorems need:

* `Basic.lean`: `Population`, `mean`, `Population.effect`, `Population.tau`,
  `Assignment`, `Z`, `Yobs`, and the rewriting lemmas `Z_of_mem`, `one_sub_Z`,
  `sum_Z`, `prod_Z`, `Yobs_eq_ite`.
* `Design.lean`: `Design`, `Design.expect` and its linearity lemmas,
  `Design.propensity`, `Design.var`, `Design.cov`.

Everything you prove below is proved there too.  The only difference is scale:
the real files add the counting lemmas for concrete designs and then
`HT_unbiased` and `DiM_unbiased_completeRandomization`. -/
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. lean/MrCLean/Basic.lean declares the same Population, the same mean, the same Assignment, the same Z and the same Yobs; lean/MrCLean/Design.lean declares the same Design and the same Design.expect. Part II adds lemmas, not concepts:

The design decisions behind those definitions are recorded in lean/SPEC.md §3, and they are worth reading once before Part II: assignments as treated sets rather than indicator vectors (§3.1), the real-valued indicator (§3.2), the explicit pmf rather than a measure (§3.3), one inclusion-probability lemma per design (§3.4), the division-by-zero convention (§3.5), and noncomputable (§3.6). 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.

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.