Reals and finite sums

The formalization uses finite populations and finite assignment spaces. A population contains $n$ fixed potential-outcome pairs, an assignment is a set of treated units, and a design is a probability mass function on the $2^n$ assignments. Expectations therefore have the form

a finite sum. Later results about unbiasedness, variance, blocking, and randomization tests reduce to identities or inequalities between such sums.

This chapter introduces ℝ, Fin n, Finset, coercions, and the lemmas used to manipulate finite sums. The following preamble is included automatically with each playground example:

import Mathlib

namespace MrCLean.Fundamentals.Ch03

open Finset

variable {n : ℕ}

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

#check (2 : Fin 5)
#eval (2 : Fin 5) + (4 : Fin 5)
#eval (Fintype.card (Fin 7))

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”. That lemma is Fintype.card_fin, and card_units is nothing but it applied at 7, handed over as a term with no by in sight.

Arithmetic on Fin n is modular. For example, the following command evaluates to 1:

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

Here 2 + 4 = 1 because the result is reduced modulo 5. This behavior keeps values in range, but it is usually inappropriate for unit labels. Arithmetic on an index should be used only when modular indexing is intended.

All the units

#eval (Finset.univ : Finset (Fin 4)).card
#eval (Finset.range 4).card

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, and you will do it in almost every calculation that mentions a sample size.

1. rw [Finset.card_univ]

   Finset.card_univ : #(univ : Finset α) = Fintype.card α trades the Finset notion of size for the Fintype one. Both are “how many elements”, but they belong to different parts of the library, and this is the lemma that crosses between them.

   Goal

   m : ℕ
   ⊢ Fintype.card (Fin m) = m

2. rw [Fintype.card_fin]

   Fintype.card_fin : Fintype.card (Fin m) = m is the fact that the index type of an $m$-unit study has $m$ elements. After it both sides read m and the goal closes by reflexivity. Remember the pair; the next section’s mean calculations all end with it.

Sums

#eval ∑ i : Fin 4, (i.val + 1)
#eval ∑ i ∈ ({0, 2} : Finset (Fin 4)), (i.val + 1)

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.

#check fun (m : ℕ) => (m : ℝ)

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.

cast_sum is the case that comes up constantly: a sum of counts, cast once at the end, against the sum of the counts cast one at a time.

1. push_cast

   The cast starts outside the sum. push_cast drives it inward — the lemma it uses here is Nat.cast_sum, which is tagged for exactly this — so the left side becomes a sum of casts, and the two sides now differ only in the name of the bound variable.

   Goal

   n : ℕ
   c : Fin n → ℕ
   ⊢ ∑ x, ↑(c x) = ∑ i, ↑(c i)

2. ring

   Closes the goal. There is nothing algebraic left to do; ring is standing in for “and now the two sides are the same”, which is the usual way a push_cast line ends.

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

theorem cast_sub_of_le (m k : ℕ) (h : k ≤ m) : ((m - k : ℕ) : ℝ) = (m : ℝ) - k :=
  Nat.cast_sub h

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

theorem div_by_zero (x : ℝ) : x / 0 = 0 := div_zero x

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]

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

mean_of_empty is where the 0 comes from. simp only applies its list wherever anything matches, until nothing does; run one lemma at a time, in the order they appear, and each contributes exactly one step.

1. mean

   Naming a definition in a simp only list unfolds it: mean v becomes (∑ i, v i) / ↑n, and here n is 0 because v : Fin 0 → ℝ.

   Goal

   v : Fin 0 → ℝ
   ⊢ (∑ i, v i) / ↑0 = 0

2. Finset.univ_eq_empty

   Finset.univ_eq_empty : (univ : Finset α) = ∅ holds when α is empty, and Fin 0 is. So the index set of the sum is the empty finset.

   Goal

   v : Fin 0 → ℝ
   ⊢ (∑ x ∈ ∅, v x) / ↑0 = 0

3. Finset.sum_empty

   Finset.sum_empty : ∑ i ∈ ∅, f i = 0. An empty sum is zero — no units, no outcomes to add — so the numerator is 0.

   Goal

   v : Fin 0 → ℝ
   ⊢ 0 / ↑0 = 0

4. Nat.cast_zero

   Nat.cast_zero : ((0 : ℕ) : ℝ) = 0 removes the coercion around the sample size. Only now is the denominator a real 0 rather than the cast of a natural 0, which is why this lemma has to be in the list at all.

   Goal

   v : Fin 0 → ℝ
   ⊢ 0 / 0 = 0

5. div_zero

   div_zero : x / 0 = 0 is the convention itself, and it closes the goal. Reading the five lemmas back: the index set is empty, so the sum is zero, so the mean is zero over zero, which the convention makes zero. Only the last step is a convention; the first four are ordinary mathematics.

vacuous_at_zero then needs nothing but that lemma twice — rw [mean_of_empty, mean_of_empty] rewrites the left-hand mean to 0 and then the right-hand one, after which the goal is 0 = 0 and rw closes it. Two rewrites, and a theorem that looks like a statement about rescaling is revealed as a statement about the empty population.

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.

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

Both theorems there are the Mathlib lemma itself, handed over as a term with no tactic block at all: Finset.sum_add_distrib splits $\sum _i(u_i+v_i)$ and Finset.sum_sub_distrib u v splits $\sum _i(u_i-v_i)$, the second taking its two functions explicitly because the lemma’s binders happen to be stated that way. When a theorem is a library lemma, that is how to write it, and #check @Finset.sum_sub_distrib is how to find out which arguments it wants.

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

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.

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. This four-rewrite dance is how the letter $n$ gets into a mean calculation, and it appears in every proof below; learn it once here and it will be recognizable everywhere.

1. rw [Finset.sum_const]

   Finset.sum_const : ∑ _i ∈ s, c = #s • c. Adding the same number once per element is that number scaled by the number of elements, and Mathlib says “scaled” with • rather than * because it wants one lemma covering every type where repeated addition makes sense.

   Goal

   n : ℕ
   c : ℝ
   ⊢ #univ • c = ↑n * c

2. Finset.card_univ

   Now the size of the index set has to become the letter $n$, which is the pair from the section above: Finset.card_univ turns #univ into Fintype.card (Fin n).

   Goal

   n : ℕ
   c : ℝ
   ⊢ Fintype.card (Fin n) • c = ↑n * c

3. Fintype.card_fin

   And Fintype.card_fin turns that into n. The scalar is now the sample size itself.

   Goal

   n : ℕ
   c : ℝ
   ⊢ n • c = ↑n * c

4. nsmul_eq_mul

   nsmul_eq_mul : n • x = ↑n * x replaces the scalar action by multiplication in ℝ, inserting the coercion ↑n — which is where the ↑ in every mean calculation comes from. Both sides are now ↑n * c and the goal closes.

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.

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]

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.

1. rw [Finset.sum_ite_mem]

   Finset.sum_ite_mem : (∑ i ∈ s, if i ∈ t then f i else 0) = ∑ i ∈ s ∩ t, f i. Dropping the terms where the indicator is zero is the same as intersecting the index set with the treated set — here s is univ, so the result is univ ∩ z.

   Goal

   n : ℕ
   z : Finset (Fin n)
   v : Fin n → ℝ
   ⊢ ∑ i ∈ univ ∩ z, v i = ∑ i ∈ z, v i

2. Finset.univ_inter

   Finset.univ_inter : univ ∩ t = t. Intersecting with everybody changes nothing, so the index set is just the treated set and the goal closes. The statistical reading of the pair: “sum over all units, counting only the treated” and “sum over the treated” are the same number, and this is the rewrite that says so.

sum_over_treated goes the other way with a single lemma application: Finset.sum_filter states that summing over {i ∈ univ | i ∈ z} equals summing an if over all of univ, which is sum_ite_mem read backwards through the filter notation.

theorem sum_sq_nonneg (v : Fin n → ℝ) : 0 ≤ ∑ i, (v i) ^ 2 :=
  Finset.sum_nonneg fun i _ => sq_nonneg (v 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.

One more lemma belongs on the list even though no snippet above uses it, because the exercises do. Finset.sum_congr compares two sums termwise:

Finset.sum_congr : s₁ = s₂ → (∀ i ∈ s₂, f i = g i) → ∑ i ∈ s₁, f i = ∑ i ∈ s₂, g i

Two sums are equal if they run over the same index set and their summands agree at every index. It takes those two facts as its two arguments, which in practice means Finset.sum_congr rfl h: rfl proves that the index set is unchanged, and h is a function taking an index (and a proof, usually ignored, that the index is in the set) to the equality of the two summands at it. When the summands differ by algebra, that function is fun i _ => by ring, and the whole rewriting of a sum is one line. It is the formal version of “it is enough to check the identity for a single unit”.

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.

theorem ex_mean_const (hn : 0 < n) (c : ℝ) : mean (fun _ : Fin n => c) = c := by
  sorry

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.

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

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]

theorem ex_mean_const_mul (c : ℝ) (v : Fin n → ℝ) :
    mean (fun i => c * v i) = c * mean v := by
  sorry

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.

theorem ex_sum_sub_mean (hn : 0 < n) (v : Fin n → ℝ) :
    ∑ i, (v i - mean v) = 0 := by
  sorry

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.

The Lean proof is that argument in three calc steps, and the hypothesis is spent in exactly one place: turning $\overline{v}$ back into $\sum _i{v}_i/n$ requires the division to cancel, which needs $n\ne 0$ in $\mathbb{R}$.

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

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.

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

Proposition. Let $S$ be a set of $m$ units and let $p\in \mathbb{R}$. Then $\sum _{z\subseteq S}{p}^{|z|}(1-p{)}^{m-|z|}=1$.

s.powerset is the Finset of all subsets of s, so this is a sum over $2^m$ terms, one per assignment the Bernoulli design can produce.

1. rw [Finset.sum_pow_mul_eq_add_pow]

   Finset.sum_pow_mul_eq_add_pow states ∑ t ∈ s.powerset, a ^ #t * b ^ (#s - #t) = (a + b) ^ #s: the binomial theorem written as a sum over subsets rather than over an index $k$, which is exactly the shape a Bernoulli pmf comes in. At a := p, b := 1 - p the whole sum collapses to the power shown below. (The exponent #s - #t is ℕ subtraction, which is safe here because t ranges over subsets of s.)

   Goal

   n : ℕ
   s : Finset (Fin n)
   p : ℝ
   ⊢ (p + (1 - p)) ^ #s = 1

2. norm_num

   p + (1 - p) is 1 and 1 ^ #s is 1, both of which norm_num knows.

When chapter 7 defines bernoulliDesign, its sum_one field is this identity with $S$ the whole population, reached there as the empty-set case of a more general lemma rather than by this rewrite.

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

theorem ex_mean_indicator (z : Finset (Fin n)) :
    mean (fun i => if i ∈ z then (1 : ℝ) else 0) = (#z : ℝ) / n := by
  sorry

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]

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

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

theorem ex_cauchy_schwarz (x y : Fin n → ℝ) :
    (∑ i, x i * y i) ^ 2 ≤ (∑ i, (x i) ^ 2) * ∑ i, (y i) ^ 2 := by
  sorry

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.