Reals and finite sums

Design-based inference has one enormous technical advantage over the model-based kind: there is no limit, no integral and no measure. A population is $n$ units with fixed potential outcomes. An assignment is a subset of them. A design is a probability mass function on the $2^n$ assignments. An expectation is

a finite sum, and every theorem in Part II — unbiasedness, Neyman’s variance, the blocked estimator, the validity of a randomization test — is an identity or an inequality between finite sums of real numbers.

So this chapter is the real prerequisite. Chapter 1 taught you to read a statement and chapter 2 taught you to move a goal, but neither will get you through a single line of chapter 8 unless you know what ∑ i, f i means, which lemma splits it, and where the coercions come from. Nothing here is deep. All of it is load-bearing.

Everything is quoted from lean/MrCLean/Fundamentals/Ch03Sums.lean. Its preamble — the part that travels invisibly with every snippet you send to the playground — defines the one object the chapter needs, and is worth reading once:

import Mathlib

namespace MrCLean.Fundamentals.Ch03

open Finset

variable {n : ℕ}

/-- The finite-population mean of an outcome vector `v : Fin n → ℝ`.

`noncomputable` is required of every `ℝ`-valued definition — real division has no
algorithm — and costs nothing: proofs never run. -/
noncomputable def mean (v : Fin n → ℝ) : ℝ := (∑ i, v i) / n

variable {n : ℕ} declares a population size that every declaration in the file may use implicitly, so mean really has type {n : ℕ} → (Fin n → ℝ) → ℝ and you never write the n.

Units are a type

/- `Fin n` is the type of units: it has exactly `n` elements, `0, 1, …, n-1`, and
a value of type `Fin n` carries a proof that it is in range.  An outcome vector
is a function `Fin n → ℝ`; a study of `n` units needs no list, no length
hypothesis and no index-out-of-bounds case. -/
#check (2 : Fin 5)                 -- 2 : Fin 5
#eval (2 : Fin 5) + (4 : Fin 5)    -- 1  — arithmetic in `Fin 5` wraps around!
#eval (Fintype.card (Fin 7))       -- 7

/-- The number of units is what you think it is.  This lemma is the bridge
between "the index type" and "the sample size `n`". -/
theorem card_units : Fintype.card (Fin 7) = 7 := Fintype.card_fin 7

Fin n has $n$ elements, and a term of it carries a proof that it is in range. An outcome vector is a function Fin n → ℝ; there is no length hypothesis to carry around, no out-of-bounds branch, and Fintype.card (Fin n) = n is the bridge from “the index type” to “the sample size”.

One warning, immediately, because it costs people hours:

#eval (2 : Fin 5) + (4 : Fin 5)    -- 1

Arithmetic on Fin n is modular. Fin 5 is the integers mod 5 with a different name, and 2 + 4 = 1 there. This is the right definition for a type that is always inhabited and always in range, and it is a trap whenever an index expression appears in a statement. Units are labels; do not do arithmetic on them unless you mean it.

All the units

/- Two ways to describe "all the units".

* `Finset.univ : Finset (Fin n)` is the finite set of *all* elements of `Fin n`.
  This is what `∑ i, f i` sums over, and the one to use for a population.
* `Finset.range n : Finset ℕ` is `{0, 1, …, n-1}` as a set of naturals.  Handy
  for sequences, awkward for units, because the elements are unconstrained `ℕ`s. -/
#eval (Finset.univ : Finset (Fin 4)).card    -- 4
#eval (Finset.range 4).card                  -- 4

/-- `Finset.card_univ` and `Fintype.card_fin` together turn `#(univ : Finset (Fin n))`
into `n`.  You will use this in every calculation involving a sample size. -/
theorem card_univ_fin (m : ℕ) : (Finset.univ : Finset (Fin m)).card = m := by
  rw [Finset.card_univ, Fintype.card_fin]

A Finset α is a finite set of elements of α with a decidable membership test — a list without duplicates and without an order that anyone is allowed to observe. It is the workhorse type of this subject: the treated set is a Finset (Fin n), a block is a Finset (Fin n), and the set of all assignments is a Finset (Finset (Fin n)).

Two ways to say “all the units”. Finset.univ : Finset (Fin n) is the finite set of everything in Fin n, and it is what ∑ i, f i sums over. Finset.range n : Finset ℕ is $\{0,\dots ,n-1\}$ as a set of naturals; it is convenient for sequences and wrong for units, because its elements are unconstrained ℕs that carry no proof of being in range.

#s is notation for s.card, the number of elements. Turning #(univ : Finset (Fin n)) into n takes two rewrites, Finset.card_univ and Fintype.card_fin, and you will do it in almost every calculation that mentions a sample size.

Sums

/- `∑ i, f i` means `∑ i ∈ Finset.univ, f i`: sum over every unit.  `∑ i ∈ s, f i`
sums over a subgroup `s` — the treated units, say.  These are ordinary finite
sums, defined by folding, with no convergence conditions anywhere. -/
#eval ∑ i : Fin 4, (i.val + 1)                        -- 1+2+3+4 = 10
#eval ∑ i ∈ ({0, 2} : Finset (Fin 4)), (i.val + 1)    -- 1+3 = 4

/-- Sum over all units and sum over `univ` are the same thing by definition. -/
theorem sum_univ (v : Fin n → ℝ) : ∑ i, v i = ∑ i ∈ Finset.univ, v i := rfl

∑ i, f i is ∑ i ∈ Finset.univ, f i — sum over every unit — and the two are the same term, which is why sum_univ is proved by rfl. ∑ i ∈ s, f i sums over a subgroup: the treated units, a block, a cluster.

These are Finset.sum, defined by folding + over the underlying multiset. There is no convergence condition, no summability hypothesis, no ordering subtlety. Commutativity and associativity of + make the fold well defined, and that is the entire theory.

Coercions, and the ↑ you keep seeing

Sample sizes are natural numbers. Means are real. Lean does not silently mix them.

/- Sample sizes are natural numbers, means are real.  `(n : ℝ)` inserts the
*coercion* `Nat.cast`, printed `↑n`.  Lean will not silently mix the two: an `↑`
in a goal is a signal that `push_cast` / `norm_cast` may be needed. -/
#check fun (m : ℕ) => (m : ℝ)      -- fun m => ↑m : ℕ → ℝ

/-- `push_cast` drives coercions inwards, towards the leaves.  Here it turns the
cast of a `ℕ`-sum into a real sum of casts (`Nat.cast_sum`). -/
theorem cast_sum (c : Fin n → ℕ) : ((∑ i, c i : ℕ) : ℝ) = ∑ i, (c i : ℝ) := by
  push_cast
  ring

Writing (n : ℝ) where n : ℕ inserts the coercion Nat.cast, which the pretty-printer shows as ↑n. An ↑ in a goal is a signal, not a problem: it means there is a type boundary in the expression, and that two tactics exist to push it around. push_cast drives coercions towards the leaves — ↑(a + b) becomes ↑a + ↑b — which is usually what you want before ring. norm_cast tries to remove them altogether, and is what closes a goal that is “the same statement” on both sides of the boundary.

They are not interchangeable with the surrounding algebra, and the reason is subtraction.

/-- The one coercion that bites.  `ℕ`-subtraction *truncates*: `3 - 5 = 0` in `ℕ`.
So `((n - k : ℕ) : ℝ) = (n : ℝ) - k` is **false** in general, and `Nat.cast_sub`
demands the hypothesis `k ≤ n`.

Whenever an autoformalized statement writes the number of controls as `n - n₁`,
check which subtraction it means: over `ℕ` a "theorem" about `n₁ > n` can be
vacuously true. -/
theorem cast_sub_of_le (m k : ℕ) (h : k ≤ m) : ((m - k : ℕ) : ℝ) = (m : ℝ) - k :=
  Nat.cast_sub h

/-- The failure, made concrete: over `ℕ`, three minus five is zero. -/
theorem nat_sub_truncates : (3 : ℕ) - 5 = 0 := by decide

ℕ-subtraction truncates: 3 - 5 = 0, not -2. So ((n - k : ℕ) : ℝ) = (n : ℝ) - k is false in general, Nat.cast_sub demands k ≤ n, and push_cast will refuse to move a cast through a ℕ-subtraction without it — which is the tactic telling you the mathematics is wrong, not that you picked the wrong tactic.

This matters here more than in most subjects, because $n_0=n-n_1$ is written down in every second line of design-based statistics. In ℝ it is subtraction; in ℕ it is truncated subtraction, and a formalization that keeps it in ℕ will be silently true when . Chapter 8’s DiM_eq_HT_of_card threads a hypothesis n₁ ≤ n through twenty lines for exactly this reason.

Division by zero

/-- Lean defines `x / 0 = 0`.  This is a *convention*, not a theorem about
mathematics, and the library leans on it: the mean of an empty population is `0`
rather than undefined, so every lemma below can be an unconditional equation with
`0 < n` appearing only where it is genuinely needed. -/
theorem div_by_zero (x : ℝ) : x / 0 = 0 := div_zero x

/-- Consequence: the mean of a population with no units is `0`. -/
theorem mean_of_empty (v : Fin 0 → ℝ) : mean v = 0 := by
  simp only [mean, Finset.univ_eq_empty, Finset.sum_empty, Nat.cast_zero, div_zero]

/-- The flip side, and the first thing to check in an autoformalized statement:
an equation about a ratio is *trivially true* when the denominator is zero, so a
"theorem" that quantifies over all `n` may be saying nothing at `n = 0`. -/
theorem vacuous_at_zero (v : Fin 0 → ℝ) : mean v = mean (fun i => 2 * v i) := by
  rw [mean_of_empty, mean_of_empty]

In Lean, x / 0 = 0. This is a convention that makes division a total function; it is not a claim that dividing by nothing is meaningful. Every proof assistant does something like this, because the alternative — division as a partial function, with a proof of non-vanishing at every use site — makes ordinary algebra unbearable.

Two consequences you must internalize before reading anyone’s formalization.

The good one: definitions can be total. mean v is defined for Fin 0 → ℝ and equals 0; DiM is defined on the assignment where nobody is treated. So positivity hypotheses appear exactly where the mathematics needs them, rather than being sprinkled defensively over every definition, and when you see 0 < n in a statement you know it is doing work.

The bad one: an equation between two ratios is trivially true when both denominators vanish. vacuous_at_zero in the snippet above is a real theorem saying that the mean of v equals the mean of 2 • v — for a population of zero units, where both are 0. A statement quantified over all n may therefore be saying nothing at all at n = 0, and if the interesting content was supposed to come with 0 < n, its absence is invisible.

The sum lemmas

There are about ten. Between them they close every algebraic step in Part II, and they are worth knowing by name, because simp will not always find the one you want and exact? is slow.

/-- Sums split over `+` and `-`.  These two lemmas plus `Finset.mul_sum` are
essentially all of "linearity" that any of the estimator proofs needs. -/
theorem sum_add (u v : Fin n → ℝ) :
    ∑ i, (u i + v i) = (∑ i, u i) + ∑ i, v i := Finset.sum_add_distrib

theorem sum_sub (u v : Fin n → ℝ) :
    ∑ i, (u i - v i) = (∑ i, u i) - ∑ i, v i := Finset.sum_sub_distrib u v

/-- A constant comes out of a sum.  `Finset.mul_sum` and `Finset.sum_mul` are the
same fact with the constant on either side; the direction you need is usually
`←`, pulling the constant *out*. -/
theorem const_mul_sum (c : ℝ) (v : Fin n → ℝ) :
    c * ∑ i, v i = ∑ i, c * v i := Finset.mul_sum Finset.univ v c

theorem sum_mul_const (c : ℝ) (v : Fin n → ℝ) :
    (∑ i, v i) * c = ∑ i, v i * c := Finset.sum_mul Finset.univ v c

/-- Division is multiplication by an inverse, so it distributes too. -/
theorem sum_div_const (c : ℝ) (v : Fin n → ℝ) :
    (∑ i, v i) / c = ∑ i, v i / c := Finset.sum_div Finset.univ v c

Finset.mul_sum and Finset.sum_mul are the same fact with the constant on either side, and Finset.sum_div is the version for division, which works because dividing is multiplying by an inverse. The direction you usually want is backwards — rw [← Finset.mul_sum] to pull a constant out of a sum — and forgetting the ← is the most common way to watch a rewrite fail.

/-- Summing a constant counts the index set: `∑ i ∈ s, c = #s • c`.  Turning the
scalar action `•` into ordinary multiplication is `nsmul_eq_mul`, and this three-
step dance (`sum_const`, `card_univ`/`card_fin`, `nsmul_eq_mul`) is how `n`
appears in every mean calculation. -/
theorem sum_const_eq (c : ℝ) : ∑ _i : Fin n, c = (n : ℝ) * c := by
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]

∑ i ∈ s, c = #s • c, with • the scalar action of ℕ on ℝ, which nsmul_eq_mul turns into ordinary multiplication. The three-step dance sum_const, card_univ/card_fin, nsmul_eq_mul is how the letter $n$ gets into a mean calculation, and it appears in every proof below.

/-- Two finite sums can always be exchanged — no Fubini, no integrability side
conditions.  This is the step that turns "average over assignments of a sum over
units" into "sum over units of an average over assignments". -/
theorem exchange (f : Fin n → Fin n → ℝ) :
    ∑ i, ∑ j, f i j = ∑ j, ∑ i, f i j := Finset.sum_comm

This is the one to appreciate. Exchanging $\mathbb{E}$ and $\sum _i$ — the step that turns “the expectation of a sum over units” into “the sum over units of an expectation” — is Finset.sum_comm, with no integrability side condition, because both sums are finite. Fubini’s theorem, in this subject, is a rewrite.

/-- Indicators.  `∑ i, (if i ∈ z then f i else 0)` is a sum over the treated units
`z`, and `Finset.sum_ite_mem` says so.  With `Finset.univ_inter` the intersection
with `univ` disappears. -/
theorem sum_indicator_mul (z : Finset (Fin n)) (v : Fin n → ℝ) :
    ∑ i, (if i ∈ z then v i else 0) = ∑ i ∈ z, v i := by
  rw [Finset.sum_ite_mem, Finset.univ_inter]

/-- `Finset.sum_filter` is the same statement read the other way: a sum over a
filtered set is a sum of an `if`.  `Finset.sum_ite` splits a two-branch `if` into
the two filtered pieces — the treated group and the control group. -/
theorem sum_over_treated (z : Finset (Fin n)) (v : Fin n → ℝ) :
    ∑ i ∈ Finset.univ with i ∈ z, v i = ∑ i, (if i ∈ z then v i else 0) :=
  Finset.sum_filter _ v

Indicators are if … then … else 0, and the two directions you need are: Finset.sum_ite_mem turns a sum over everybody weighted by an indicator into a sum over the treated set, and Finset.sum_filter turns a sum over a filtered set back into a sum of an if. Being able to move between the two spellings is what makes the treated and control halves of an estimator symmetric.

/-- A sum of nonnegative terms is nonnegative: the reason a sum of squares — any
sample variance — is never negative. -/
theorem sum_sq_nonneg (v : Fin n → ℝ) : 0 ≤ ∑ i, (v i) ^ 2 :=
  Finset.sum_nonneg fun i _ => sq_nonneg (v i)

/-- Sums are monotone termwise.  Note the shape of the hypothesis: `∀ i ∈ s, …`,
not `∀ i, …`. -/
theorem sum_le (u v : Fin n → ℝ) (h : ∀ i, u i ≤ v i) : ∑ i, u i ≤ ∑ i, v i :=
  Finset.sum_le_sum fun i _ => h i

Note the shape of the hypothesis in Finset.sum_le_sum: it is ∀ i ∈ s, …, not ∀ i, …, so you supply fun i _ => … with the membership proof ignored. This is the standard shape for a sum lemma and it catches everyone once.

Here is the whole toolkit, in the form of the statistical move each lemma performs:

Identities about the mean

Everything above is machinery. Here is what it buys, stated informally first and then handed to you as exercises, because these are proofs you should have done once with your own hands before you read chapter 8.

The mean of a constant is that constant, provided there is a unit. If $v_i=c$ for every $i$ then $\overline{v}=nc/n=c$ — and the proviso is not pedantry, it is the x / 0 = 0 convention: at $n=0$ the mean is $0$, so the statement is false for every $c\ne 0$ without 0 < n.

/-- Exercise (warm-up).  The mean of a constant outcome vector is that constant —
provided there is at least one unit, since at `n = 0` the mean is `0 / 0 = 0`.
`Finset.sum_const`, `Finset.card_univ`, `Fintype.card_fin`, `nsmul_eq_mul` reduce
the sum to `n * c`; then `field_simp` needs to know `(n : ℝ) ≠ 0`. -/
theorem ex_mean_const (hn : 0 < n) (c : ℝ) : mean (fun _ : Fin n => c) = c := by
  sorry

/-- Exercise (warm-up).  The mean of a constant outcome vector is that constant —
provided there is at least one unit, since at `n = 0` the mean is `0 / 0 = 0`.
`Finset.sum_const`, `Finset.card_univ`, `Fintype.card_fin`, `nsmul_eq_mul` reduce
the sum to `n * c`; then `field_simp` needs to know `(n : ℝ) ≠ 0`. -/
theorem ex_mean_const (hn : 0 < n) (c : ℝ) : mean (fun _ : Fin n => c) = c := by
  have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
  simp only [mean, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  field_simp

The mean is linear: $\overline{u+v}=\overline{u}+\overline{v}$ and $\overline{cv}=c\overline{v}$. No hypotheses at all — not even , because both sides divide by the same $n$ and $0/0=0/0$. This is the fact that makes linearity of expectation trivial in Part II: an expectation under a design is a weighted sum of the same shape, and these are the lemmas that split it.

/-- Exercise (core).  **The mean is linear**, additive half.  Split the sum, then
split the division.  Two lemma names in a single `simp only` will do it. -/
theorem ex_mean_add (u v : Fin n → ℝ) :
    mean (fun i => u i + v i) = mean u + mean v := by
  sorry

/-- Exercise (core).  **The mean is linear**, additive half.  Split the sum, then
split the division.  Two lemma names in a single `simp only` will do it. -/
theorem ex_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]

/-- Exercise (core).  **The mean is linear**, scalar half: rescaling every outcome
rescales the mean.  Pull the constant out of the sum (`Finset.mul_sum`, used
backwards) and out of the division (`mul_div_assoc`). -/
theorem ex_mean_const_mul (c : ℝ) (v : Fin n → ℝ) :
    mean (fun i => c * v i) = c * mean v := by
  sorry

/-- Exercise (core).  **The mean is linear**, scalar half: rescaling every outcome
rescales the mean.  Pull the constant out of the sum (`Finset.mul_sum`, used
backwards) and out of the division (`mul_div_assoc`). -/
theorem ex_mean_const_mul (c : ℝ) (v : Fin n → ℝ) :
    mean (fun i => c * v i) = c * mean v := by
  simp only [mean, ← Finset.mul_sum, mul_div_assoc]

Deviations from the mean sum to zero: $\sum _i(v_i-\overline{v})=0$. This is why the mean is the least-squares center, it is the first step of every variance calculation, and in Part II it is what makes the sum of the estimated individual effects behave.

/-- Exercise (core).  **Deviations from the mean sum to zero.**  The identity that
makes the mean the least-squares centre, and the first step of every variance
calculation.

Split the sum with `Finset.sum_sub_distrib`, evaluate `∑ i, mean v` with
`Finset.sum_const`, then unfold `mean` and cancel: the goal becomes
`∑ v - n * (∑ v / n) = 0`, which is `mul_div_cancel₀` followed by `sub_self`. -/
theorem ex_sum_sub_mean (hn : 0 < n) (v : Fin n → ℝ) :
    ∑ i, (v i - mean v) = 0 := by
  sorry

/-- Exercise (core).  **Deviations from the mean sum to zero.**  The identity that
makes the mean the least-squares centre, and the first step of every variance
calculation.

Split the sum with `Finset.sum_sub_distrib`, evaluate `∑ i, mean v` with
`Finset.sum_const`, then unfold `mean` and cancel: the goal becomes
`∑ v - n * (∑ v / n) = 0`, which is `mul_div_cancel₀` followed by `sub_self`. -/
theorem ex_sum_sub_mean (hn : 0 < n) (v : Fin n → ℝ) :
    ∑ i, (v i - mean v) = 0 := by
  have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
  rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
    nsmul_eq_mul, mean, mul_div_cancel₀ _ hn', sub_self]

The computational formula for the variance: $\sum _i(v_i-\overline{v}{)}^2=\sum _i{v}_i^2-n{\overline{v}}^2$. Every variance calculation in chapter 9 passes through this identity or its covariance sibling.

/-- Exercise (core).  **The computational formula for the variance**:
`∑ (xᵢ - x̄)² = ∑ xᵢ² - n x̄²`.

The shape of the proof: expand the square termwise (`Finset.sum_congr` with
`ring`), split the sum, pull constants out, and use `∑ xᵢ = n x̄` — which is just
`mean` with the division cleared. -/
theorem ex_variance_identity (hn : 0 < n) (v : Fin n → ℝ) :
    ∑ i, (v i - mean v) ^ 2 = (∑ i, (v i) ^ 2) - (n : ℝ) * (mean v) ^ 2 := by
  sorry

/-- Exercise (core).  **The computational formula for the variance**:
`∑ (xᵢ - x̄)² = ∑ xᵢ² - n x̄²`.

The shape of the proof: expand the square termwise (`Finset.sum_congr` with
`ring`), split the sum, pull constants out, and use `∑ xᵢ = n x̄` — which is just
`mean` with the division cleared. -/
theorem ex_variance_identity (hn : 0 < n) (v : Fin n → ℝ) :
    ∑ i, (v i - mean v) ^ 2 = (∑ i, (v i) ^ 2) - (n : ℝ) * (mean v) ^ 2 := by
  have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
  have hsum : ∑ i, v i = (n : ℝ) * mean v := by
    rw [mean]
    exact (mul_div_cancel₀ _ hn').symm
  calc ∑ i, (v i - mean v) ^ 2
      = ∑ i, ((v i) ^ 2 - 2 * mean v * v i + (mean v) ^ 2) :=
        Finset.sum_congr rfl fun i _ => by ring
    _ = (∑ i, (v i) ^ 2) - 2 * mean v * (∑ i, v i) + (n : ℝ) * (mean v) ^ 2 := by
        rw [Finset.sum_add_distrib, Finset.sum_sub_distrib, ← Finset.mul_sum,
          Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    _ = (∑ i, (v i) ^ 2) - (n : ℝ) * (mean v) ^ 2 := by
        rw [hsum]
        ring

Everything in Part II is a finite sum

To make the claim in the first paragraph concrete: an expectation under a Bernoulli design is a sum over all subsets of the population, each weighted by $p^{|z|}(1-p{)}^{n-|z|}$. That those weights sum to one — the fact that makes a Design a probability distribution at all — is the binomial theorem, and in Mathlib it is one rewrite.

/-- A sum over *all subsets* of a set, which is what an expectation under a
Bernoulli design is: each unit is treated independently with probability `p`, so
the assignment `z ⊆ s` has probability `p ^ #z * (1 - p) ^ (#s - #z)`, and those
probabilities sum to one.  In Mathlib this is one rewrite: the binomial theorem
in the form `Finset.sum_pow_mul_eq_add_pow`. -/
theorem bernoulli_weights_sum_one (s : Finset (Fin n)) (p : ℝ) :
    ∑ z ∈ s.powerset, p ^ #z * (1 - p) ^ (#s - #z) = 1 := by
  rw [Finset.sum_pow_mul_eq_add_pow]
  norm_num

s.powerset is the Finset of all subsets of s, so this is a sum over $2^{\mathrm{\#}s}$ terms. Finset.sum_pow_mul_eq_add_pow is the binomial theorem in exactly the shape a Bernoulli pmf needs, and norm_num finishes by evaluating $(p+(1-p){)}^{\mathrm{\#}s}=1$. When chapter 7 defines bernoulliDesign, this is the proof of its second field.

That is the pattern for the rest of the tutorial. A probabilistic statement becomes a statement about a finite sum; a finite sum is manipulated with the dozen lemmas above; and the only genuinely probabilistic content — that the indicator has expectation ${\pi }_i$ — is true by definition.

Exercises

/-- Exercise (core).  **The mean of an indicator is a proportion.**  If `z` is the
set of treated units, the average of the treatment indicator over the population
is the treated fraction `#z / n`.

`Finset.sum_ite_mem` turns the sum into a sum over `univ ∩ z`; `Finset.univ_inter`
drops the `univ`; `Finset.sum_const` with `nsmul_eq_mul` and `mul_one` counts. -/
theorem ex_mean_indicator (z : Finset (Fin n)) :
    mean (fun i => if i ∈ z then (1 : ℝ) else 0) = (#z : ℝ) / n := by
  sorry

/-- Exercise (core).  **The mean of an indicator is a proportion.**  If `z` is the
set of treated units, the average of the treatment indicator over the population
is the treated fraction `#z / n`.

`Finset.sum_ite_mem` turns the sum into a sum over `univ ∩ z`; `Finset.univ_inter`
drops the `univ`; `Finset.sum_const` with `nsmul_eq_mul` and `mul_one` counts. -/
theorem ex_mean_indicator (z : Finset (Fin n)) :
    mean (fun i => if i ∈ z then (1 : ℝ) else 0) = (#z : ℝ) / n := by
  simp only [mean, Finset.sum_ite_mem, Finset.univ_inter, Finset.sum_const, nsmul_eq_mul,
    mul_one]

/-- Exercise (stretch).  **The computational formula for a covariance**:
`∑ (xᵢ - x̄)(yᵢ - ȳ) = ∑ xᵢyᵢ - n x̄ȳ`.  Same proof as the variance identity, with
one more `∑ = n · mean` fact to feed in. -/
theorem ex_covariance_identity (hn : 0 < n) (x y : Fin n → ℝ) :
    ∑ i, (x i - mean x) * (y i - mean y)
      = (∑ i, x i * y i) - (n : ℝ) * mean x * mean y := by
  sorry

/-- Exercise (stretch).  **The computational formula for a covariance**:
`∑ (xᵢ - x̄)(yᵢ - ȳ) = ∑ xᵢyᵢ - n x̄ȳ`.  Same proof as the variance identity, with
one more `∑ = n · mean` fact to feed in. -/
theorem ex_covariance_identity (hn : 0 < n) (x y : Fin n → ℝ) :
    ∑ i, (x i - mean x) * (y i - mean y)
      = (∑ i, x i * y i) - (n : ℝ) * mean x * mean y := by
  have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne'
  have hx : ∑ i, x i = (n : ℝ) * mean x := by rw [mean]; exact (mul_div_cancel₀ _ hn').symm
  have hy : ∑ i, y i = (n : ℝ) * mean y := by rw [mean]; exact (mul_div_cancel₀ _ hn').symm
  calc ∑ i, (x i - mean x) * (y i - mean y)
      = ∑ i, (x i * y i - mean y * x i - mean x * y i + mean x * mean y) :=
        Finset.sum_congr rfl fun i _ => by ring
    _ = (∑ i, x i * y i) - mean y * (∑ i, x i) - mean x * (∑ i, y i)
          + (n : ℝ) * (mean x * mean y) := by
        rw [Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.sum_sub_distrib,
          ← Finset.mul_sum, ← Finset.mul_sum, Finset.sum_const, Finset.card_univ,
          Fintype.card_fin, nsmul_eq_mul]
    _ = (∑ i, x i * y i) - (n : ℝ) * mean x * mean y := by
        rw [hx, hy]
        ring

/-- Exercise (stretch).  **Cauchy–Schwarz** for a finite population:
`(∑ xᵢyᵢ)² ≤ (∑ xᵢ²)(∑ yᵢ²)`.  Do not prove it by hand — find it.  `exact?` on
this goal reports the Mathlib lemma, whose name follows the conventions of
chapter 05: a sum of products, squared, bounded by a product of sums of squares. -/
theorem ex_cauchy_schwarz (x y : Fin n → ℝ) :
    (∑ i, x i * y i) ^ 2 ≤ (∑ i, (x i) ^ 2) * ∑ i, (y i) ^ 2 := by
  sorry

/-- Exercise (stretch).  **Cauchy–Schwarz** for a finite population:
`(∑ xᵢyᵢ)² ≤ (∑ xᵢ²)(∑ yᵢ²)`.  Do not prove it by hand — find it.  `exact?` on
this goal reports the Mathlib lemma, whose name follows the conventions of
chapter 05: a sum of products, squared, bounded by a product of sums of squares. -/
theorem ex_cauchy_schwarz (x y : Fin n → ℝ) :
    (∑ i, x i * y i) ^ 2 ≤ (∑ i, (x i) ^ 2) * ∑ i, (y i) ^ 2 := by
  exact Finset.sum_mul_sq_le_sq_mul_sq Finset.univ x y

Reading autoformalized Lean

Both of the following compile. Both are about finite populations. Neither says what it looks like it says, and in both cases the culprit is a type.

The general lesson of this chapter is that the finite-population setting hands you three number types — ℕ for counts, Fin n for labels, ℝ for outcomes — and each has an operation that misbehaves when you treat it as one of the others: truncated subtraction and integer division in ℕ, modular arithmetic in Fin n, and x / 0 = 0 in ℝ. All three are deliberate, all three are documented, and all three will silently absorb a mistake. Reading a statement means reading its types.

Next: structures, so that “a population” and “a design” become single objects rather than piles of loose functions.