Partial identification

Every theorem in this tutorial so far has been an identification result wearing an estimator’s clothes. Horvitz–Thompson is unbiased because the design tells you, exactly, how often each potential outcome is revealed; Neyman’s variance formula is a statement about the same enumeration. The design is doing all the work, and the design is an assumption — an unusually credible one, because the experimenter made it true on purpose, but an assumption.

Manski’s question is what happens when you take it away, or when it only half-survives contact with the field. The answer is not “nothing”. It is that the estimand stops being a single number determined by the data and becomes a set of numbers: every average treatment effect that some population consistent with what you saw could have had. Assumptions are then priced in the only currency that matters — how much they shrink that set.

This chapter formalizes the deterministic core of that program, and its autoformalization lesson is the sharpest one in the book. “These are bounds” and “this is the identified set” are different claims. The first is an inclusion and is easy. The second is an equality of sets, and its second half — sharpness — is the part a plausible-looking formalization almost always drops.

The identified set is a `Set ℝ`

Two ingredients. First, what it means for a population to be compatible with what you observed:

Consistency with the dataNew tabOpens with 1,098 lines of library preamble — the code above is at the bottom of the editor.

/-- The population `P` is **consistent with** the data `(z, y)`: running `P` under the
assignment `z` produces exactly the observed outcome vector `y`.

This is an equality of *functions* `Fin n → ℝ`, so proving one takes `funext` and using one
gives you a fact about every unit (`congrFun`). -/
def ConsistentWith (z : Assignment n) (y : Fin n → ℝ) (P : Population n) : Prop :=
  Yobs P z = y

Yobs P z = y is an equality of functions Fin n → ℝ. There is no probability here and no estimator: z is the assignment that was run, y is the vector that came back, and ConsistentWith z y P says that P, run under z, would have produced y exactly. Chapter 6 made the point that many populations satisfy this; the arithmetic is that consistency constrains $n$ of a population’s $2 n$ numbers and leaves the other $n$ entirely free.

Free, but not unconstrained, if you are willing to say something about the outcome’s range:

Bounded potential outcomesNew tabOpens with 1,121 lines of library preamble — the code above is at the bottom of the editor.

/-- Every potential outcome of `P` — observed or not — lies in the interval `[a, b]`.

This is the substantive assumption of the whole file.  It is an assumption about the
*counterfactual* outcomes, which is exactly why it cannot be tested: the data only ever show
one of the two. -/
def Bounded (a b : ℝ) (P : Population n) : Prop :=
  ∀ i, a ≤ P.y1 i ∧ P.y1 i ≤ b ∧ a ≤ P.y0 i ∧ P.y0 i ≤ b

Read Bounded slowly, because the quantifier is over P.y1 i and P.y0 i — both potential outcomes, for every unit, including the one that was never observed. That is what makes it an assumption rather than a description of the sample. A bounded outcome is common enough (a proportion, a score on a fixed scale, a duration censored at the end of follow-up), and it is exactly the kind of claim a subject-matter expert can make without knowing anything about the experiment.

Put the two together and you get the object of interest:

The identified setNew tabOpens with 1,151 lines of library preamble — the code above is at the bottom of the editor.

/-- The **identified set** of the data `(z, y)` under the bound `[a, b]`: every average
treatment effect that some consistent, bounded population could have.

Read the braces as a set-builder: `t` belongs when *there exists* a population `P` that
reproduces the data, respects the bound, and has `P.tau = t`.  Point identification is the
special case in which this set is a singleton; the theorems below say it never is, unless
`a = b`. -/
def identifiedSet (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) : Set ℝ :=
  { t | ∃ P : Population n, ConsistentWith z y P ∧ Bounded a b P ∧ P.tau = t }

identifiedSet z y a b : Set ℝ. Not an estimator, not an interval, not a number: a set of reals, defined by an existential. Point identification is the special case in which the set happens to be a singleton, and the theorem below says that with at least one unit and Bounded alone it never is, unless $a = b$ .

One hypothesis will appear throughout, and it is about the data rather than the population: InRange a b y, i.e. ∀ i, a ≤ y i ∧ y i ≤ b. It is not an extra assumption smuggled in — it is a consequence of the others, and proving that is the first exercise:

ExerciseIn-range data (warm-up)

by_cases hi : i ∈ z splits on whether unit i was treated. In the treated branch, hcon.y1_eq hi : P.y1 i = y i lets you rewrite the goal a ≤ y i ∧ y i ≤ b into a statement about P.y1 i, which is the first half of hb i; the control branch is the same with y0. Note the direction of the rewrite: you want rw [← hcon.y1_eq hi], replacing y i by P.y1 i.

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

/-- Exercise (warm-up).  If some bounded population explains the data, the data themselves
are in range.

This is the sanity check that keeps the main theorem from being vacuous: `InRange` is exactly
the hypothesis under which the identified set is non-empty.  Split on `i ∈ z` with `by_cases`,
then rewrite the observed outcome into the corresponding potential outcome using
`ConsistentWith.y1_eq` / `ConsistentWith.y0_eq` and read the bound off `hb i`. -/
theorem InRange.of_consistentWith {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ}
    {P : Population n} (hcon : ConsistentWith z y P) (hb : Bounded a b P) :
    InRange a b y := by
  sorry

Show solution

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

/-- Exercise (warm-up).  If some bounded population explains the data, the data themselves
are in range.

This is the sanity check that keeps the main theorem from being vacuous: `InRange` is exactly
the hypothesis under which the identified set is non-empty.  Split on `i ∈ z` with `by_cases`,
then rewrite the observed outcome into the corresponding potential outcome using
`ConsistentWith.y1_eq` / `ConsistentWith.y0_eq` and read the bound off `hb i`. -/
theorem InRange.of_consistentWith {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ}
    {P : Population n} (hcon : ConsistentWith z y P) (hb : Bounded a b P) :
    InRange a b y := by
  intro i
  obtain ⟨h1, h2, h3, h4⟩ := hb i
  by_cases hi : i ∈ z
  · rw [← hcon.y1_eq hi]
    exact ⟨h1, h2⟩
  · rw [← hcon.y0_eq hi]
    exact ⟨h3, h4⟩

The reason to care: if the data are not in range, no consistent bounded population exists and identifiedSet z y a b = ∅. The main theorem below would then be equating the empty set with a non-empty interval, so InRange is load-bearing rather than decorative. Keep that in mind when the theorem statement arrives — it is the first thing to check.

Manski’s worst-case bounds

Informally. Fix the data. For a treated unit you saw $y_{1 i}$ and know only that $y_{0 i} \in [a, b]$ , so its effect lies in $[y_{i} - b, y_{i} - a]$ . For a control unit you saw $y_{0 i}$ and the effect lies in $[a - y_{i}, b - y_{i}]$ . Average the pointwise minima to get the smallest ATE anyone could argue for, and the pointwise maxima to get the largest:

τ_{L} = \frac{1}{n} \sum_{i} [Z_{i} (y_{i} - b) + (1 - Z_{i}) (a - y_{i})], τ_{U} = \frac{1}{n} \sum_{i} [Z_{i} (y_{i} - a) + (1 - Z_{i}) (b - y_{i})] .

Formally.

manskiLower and manskiUpperNew tabOpens with 1,174 lines of library preamble — the code above is at the bottom of the editor.

/-- The **Manski worst-case lower bound**: impute the missing potential outcome of every unit
at whichever endpoint of `[a, b]` makes its effect as small as possible.  A treated unit gets
`y0 i = b`; a control unit gets `y1 i = a`. -/
noncomputable def manskiLower (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) : ℝ :=
  mean fun i => Z z i * (y i - b) + (1 - Z z i) * (a - y i)

/-- The **Manski worst-case upper bound**: the mirror image.  A treated unit gets `y0 i = a`;
a control unit gets `y1 i = b`. -/
noncomputable def manskiUpper (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) : ℝ :=
  mean fun i => Z z i * (y i - a) + (1 - Z z i) * (b - y i)

The definitions are written with the real indicator Z z i rather than an if i ∈ z then … else …, for the reason given in chapter 6: indicator algebra is ordinary field algebra, so ring closes almost every step below. The case-split form is available as manskiLower_eq_mean_ite when you want to read it as a statistician would.

Notice what the endpoints depend on: z, y, a, b. No design, no population, no estimator. They are computable from the data by anybody who accepts the range.

The easy half

The bounds are boundsNew tabOpens with 1,259 lines of library preamble — the code above is at the bottom of the editor.

/-- **Every consistent, bounded population has its ATE above `manskiLower`.**

No design, no expectation: this is a deterministic statement about one population and one
assignment.  The proof is `mean_le_mean` applied unit by unit; on a treated unit the observed
outcome pins `P.y1 i` and the bound `P.y0 i ≤ b` does the rest. -/
theorem manskiLower_le_tau {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ} {P : Population n}
    (hcon : ConsistentWith z y P) (hb : Bounded a b P) : manskiLower z y a b ≤ P.tau := by
  rw [manskiLower, Population.tau]
  refine mean_le_mean fun i => ?_
  obtain ⟨h1, _, _, h4⟩ := hb i
  simp only [Population.effect]
  by_cases hi : i ∈ z
  · rw [Z_of_mem hi, hcon.y1_eq hi]
    linarith
  · rw [Z_of_not_mem hi, hcon.y0_eq hi]
    linarith

/-- **Every consistent, bounded population has its ATE below `manskiUpper`.** -/
theorem tau_le_manskiUpper {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ} {P : Population n}
    (hcon : ConsistentWith z y P) (hb : Bounded a b P) : P.tau ≤ manskiUpper z y a b := by
  rw [manskiUpper, Population.tau]
  refine mean_le_mean fun i => ?_
  obtain ⟨_, h2, h3, _⟩ := hb i
  simp only [Population.effect]
  by_cases hi : i ∈ z
  · rw [Z_of_mem hi, hcon.y1_eq hi]
    linarith
  · rw [Z_of_not_mem hi, hcon.y0_eq hi]
    linarith

Both proofs are mean_le_mean — the mean is monotone — applied unit by unit, followed by linarith in each of two branches. Take manskiLower_le_tau in the treated branch. rw [Z_of_mem hi] collapses the indicator, and rw [hcon.y1_eq hi] replaces P.y1 i on the right by the observed y i; the goal is then 1 * (y i - b) + (1 - 1) * (a - y i) ≤ y i - P.y0 i, which linarith gets from P.y0 i ≤ b. That is the entire mathematical content: one inequality per unit, and the only thing the bound uses is the half of Bounded that constrains the unobserved outcome.

mean_le_mean is worth a look, because at n = 0 it is doing something quietly sensible:

ExerciseMeans are monotone (core)

Two lemmas and no case analysis. Finset.sum_le_sum needs ∀ i ∈ Finset.univ, u i ≤ v i, which is fun i _ => h i; then div_le_div_of_nonneg_right divides both sides by (n : ℝ), whose non-negativity is Nat.cast_nonneg n. Deliberately not 0 < n: at n = 0 both means are 0 / 0 = 0 and the inequality is 0 ≤ 0.

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

/-- Exercise (core).  **The mean is monotone**: entrywise `≤` gives `≤` on means.

Every bound in this file is an instance of this lemma, so it is worth doing by hand.  Two
steps: `Finset.sum_le_sum` compares the numerators, and `div_le_div_of_nonneg_right` divides
both sides by the same non-negative number.  That number is `(n : ℝ)`, whose non-negativity is
`Nat.cast_nonneg n` — note that `0 < n` is *not* needed, because at `n = 0` both means are
`0 / 0 = 0`. -/
theorem mean_le_mean {u v : Fin n → ℝ} (h : ∀ i, u i ≤ v i) : mean u ≤ mean v := by
  sorry

Show solution

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

/-- Exercise (core).  **The mean is monotone**: entrywise `≤` gives `≤` on means.

Every bound in this file is an instance of this lemma, so it is worth doing by hand.  Two
steps: `Finset.sum_le_sum` compares the numerators, and `div_le_div_of_nonneg_right` divides
both sides by the same non-negative number.  That number is `(n : ℝ)`, whose non-negativity is
`Nat.cast_nonneg n` — note that `0 < n` is *not* needed, because at `n = 0` both means are
`0 / 0 = 0`. -/
theorem mean_le_mean {u v : Fin n → ℝ} (h : ∀ i, u i ≤ v i) : mean u ≤ mean v := by
  exact div_le_div_of_nonneg_right (Finset.sum_le_sum fun i _ => h i) (Nat.cast_nonneg n)

From the pointwise bracket, one inclusion of the main theorem is three lines:

ExerciseThe bounds contain the identified set (core)

rintro t ⟨P, hcon, hb, rfl⟩ does three things at once: it introduces t, destructs the existential in identifiedSet, and — this is the rfl pattern — uses P.tau = t to substitute P.tau for t everywhere. Membership in Set.Icc unfolds definitionally to a conjunction of two inequalities, so the anonymous constructor ⟨_, _⟩ closes the goal with the two bracket lemmas.

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

/-- Exercise (core).  The identified set is contained in the Manski interval.

This is the half of the main theorem that a formalisation almost never gets wrong.
`rintro t ⟨P, hcon, hb, rfl⟩` destructs the existential *and* substitutes `P.tau` for `t` in
one move; membership in `Set.Icc` is a pair of inequalities, which is what
`manskiLower_le_tau` and `tau_le_manskiUpper` supply. -/
theorem identifiedSet_subset_Icc (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) :
    identifiedSet z y a b ⊆ Set.Icc (manskiLower z y a b) (manskiUpper z y a b) := by
  sorry

Show solution

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

/-- Exercise (core).  The identified set is contained in the Manski interval.

This is the half of the main theorem that a formalisation almost never gets wrong.
`rintro t ⟨P, hcon, hb, rfl⟩` destructs the existential *and* substitutes `P.tau` for `t` in
one move; membership in `Set.Icc` is a pair of inequalities, which is what
`manskiLower_le_tau` and `tau_le_manskiUpper` supply. -/
theorem identifiedSet_subset_Icc (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) :
    identifiedSet z y a b ⊆ Set.Icc (manskiLower z y a b) (manskiUpper z y a b) := by
  rintro t ⟨P, hcon, hb, rfl⟩
  exact ⟨manskiLower_le_tau hcon hb, tau_le_manskiUpper hcon hb⟩

The hard half: sharpness

Here is the claim that makes the bounds worth stating. Not merely ” $τ$ is in this interval”, but “every point of this interval is the ATE of some population that fits the data and respects the range” — so no cleverness can narrow the interval without a new assumption.

The construction is a single family. Impute the missing halves and see what you get:

Filling in the counterfactualsNew tabOpens with 1,312 lines of library preamble — the code above is at the bottom of the editor.

/-- The population obtained from the data `(z, y)` by **imputing** the missing half: control
units are given `u i` as their treated outcome, treated units are given `v i` as their control
outcome, and everybody keeps their observed value.

Every population consistent with the data is of this form, so this single definition covers the
whole identified set; the theorems below only have to choose `u` and `v`. -/
noncomputable def imputePop (z : Assignment n) (y u v : Fin n → ℝ) : Population n where
  y1 := fun i => Z z i * y i + (1 - Z z i) * u i
  y0 := fun i => Z z i * v i + (1 - Z z i) * y i

u i is the treated outcome handed to a control unit, v i the control outcome handed to a treated unit. Every population consistent with the data is of this form, which is why one definition suffices for the whole theorem.

Whatever you impute, the data come backNew tabOpens with 1,328 lines of library preamble — the code above is at the bottom of the editor.

/-- **The imputed population reproduces the data, whatever was imputed.**

The algebra is entirely `Z z i * Z z i = Z z i`: the indicator selects the observed half twice
and the imputed half never.  `linear_combination c * h` proves a goal `L = R` by checking that
`L - R` equals `c` times `h`'s own `lhs - rhs`; here `h` is `Z_mul_self` and the coefficient is
`2 * y i - u i - v i`. -/
theorem imputePop_consistentWith (z : Assignment n) (y u v : Fin n → ℝ) :
    ConsistentWith z y (imputePop z y u v) := by
  funext i
  simp only [Yobs, imputePop_y1, imputePop_y0]
  linear_combination (2 * y i - u i - v i) * Z_mul_self z i

The proof deserves a sentence, because it shows what Z is for. Expanding Yobs (imputePop z y u v) z i gives a quadratic in Z z i, and the difference between it and y i factors as $(Z^{2} - Z) (2 y_{i} - u_{i} - v_{i})$ . Since Z_mul_self : Z z i * Z z i = Z z i, that factor is zero. linear_combination is the tactic for exactly this shape: linear_combination c * h closes a goal L = R by checking, with ring, that L - R equals c times h’s own lhs - rhs. It is ring with a certificate, and it is much more robust than hunting for the right rewrite.

Two choices of (u, v) give the endpoints: (a, b) gives manskiLower, (b, a) gives manskiUpper. Everything in between comes from mixing them.

Convex combinations of the two extremesNew tabOpens with 1,377 lines of library preamble — the code above is at the bottom of the editor.

/-- **Convex combinations of the two extreme populations are again consistent and bounded**, and
their ATE is the corresponding convex combination of the endpoints.

This is the engine of sharpness.  `tau` is an *affine* function of the potential outcomes, so
mixing the imputed values mixes the ATEs; and `[a, b]` is convex, so a mixture of two admissible
imputations is admissible.  Together they say the identified set contains the whole segment
between its endpoints. -/
theorem mix_mem_identifiedSet {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ}
    (hy : InRange a b y) {lam : ℝ} (h0 : 0 ≤ lam) (h1 : lam ≤ 1) :
    (1 - lam) * manskiLower z y a b + lam * manskiUpper z y a b ∈ identifiedSet z y a b := by
  refine ⟨imputePop z y (fun _ => (1 - lam) * a + lam * b) (fun _ => (1 - lam) * b + lam * a),
    imputePop_consistentWith z y _ _, ?_, ?_⟩
  · refine imputePop_bounded hy (fun i => ?_) (fun i => ?_) <;>
      · have hab : a ≤ b := le_trans (hy i).1 (hy i).2
        constructor <;>
          linarith [mul_nonneg h0 (sub_nonneg.mpr hab),
            mul_nonneg (sub_nonneg.mpr h1) (sub_nonneg.mpr hab)]
  · rw [tau_imputePop, manskiLower, manskiUpper, ← mean_const_mul, ← mean_const_mul, ← mean_add]
    exact mean_congr fun i => by ring

Two facts are at work, and both are worth naming because they are the reason identified sets in this subject are so often intervals.

tau is affine in the potential outcomes. Mixing the imputations mixes the ATEs, exactly: the last step of the proof is rw [tau_imputePop, manskiLower, manskiUpper, ← mean_const_mul, ← mean_const_mul, ← mean_add] followed by mean_congr fun i => by ring. Every rewrite is pushing the convex combination inside the mean, where it becomes a pointwise identity that ring verifies.
[a, b] is convex. A mixture of two admissible imputations is admissible, which is what imputePop_bounded needs; the four goals are discharged by linarith from the two products $λ (b - a) \geq 0$ and $(1 - λ) (b - a) \geq 0$ .

With the segment in hand, sharpness is a matter of picking $λ$ :

ExerciseSharpness (stretch)

The only real content is choosing the mixing weight. If L = U the interval is a point and mix_mem_identifiedSet at lam = 0 already gives it. Otherwise L < U, and the weight that lands on t is lam = (t - L) / (U - L): div_nonneg and div_le_one give 0 ≤ lam ≤ 1, and div_mul_cancel₀ _ hne : (t - L) / (U - L) * (U - L) = t - L is the one fact linarith needs to see that (1 - lam) * L + lam * U = t. set L := … before you start, or the goals become unreadable.

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

/-- Exercise (stretch).  **Sharpness**: every point of the Manski interval is attained.

This is the inclusion that makes the bounds worth stating, and the one an autoformalisation
tends to leave out.  Two cases.  If the interval is a single point, `mix_mem_identifiedSet` at
`lam = 0` already gives it (`simpa` cleans up `(1 - 0) * L + 0 * U`).  Otherwise
`L < U` and the required mixing weight is `lam = (t - L) / (U - L)`: check `0 ≤ lam ≤ 1` with
`div_nonneg` and `div_le_one`, then `field_simp` verifies `(1 - lam) * L + lam * U = t`. -/
theorem mem_identifiedSet_of_mem_Icc {z : Assignment n} {y : Fin n → ℝ} {a b t : ℝ}
    (hy : InRange a b y) (ht : t ∈ Set.Icc (manskiLower z y a b) (manskiUpper z y a b)) :
    t ∈ identifiedSet z y a b := by
  sorry

Show solution

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

/-- Exercise (stretch).  **Sharpness**: every point of the Manski interval is attained.

This is the inclusion that makes the bounds worth stating, and the one an autoformalisation
tends to leave out.  Two cases.  If the interval is a single point, `mix_mem_identifiedSet` at
`lam = 0` already gives it (`simpa` cleans up `(1 - 0) * L + 0 * U`).  Otherwise
`L < U` and the required mixing weight is `lam = (t - L) / (U - L)`: check `0 ≤ lam ≤ 1` with
`div_nonneg` and `div_le_one`, then `field_simp` verifies `(1 - lam) * L + lam * U = t`. -/
theorem mem_identifiedSet_of_mem_Icc {z : Assignment n} {y : Fin n → ℝ} {a b t : ℝ}
    (hy : InRange a b y) (ht : t ∈ Set.Icc (manskiLower z y a b) (manskiUpper z y a b)) :
    t ∈ identifiedSet z y a b := by
  obtain ⟨htl, htu⟩ := ht
  set L := manskiLower z y a b
  set U := manskiUpper z y a b
  rcases eq_or_lt_of_le (htl.trans htu) with hEq | hLt
  · have hte : t = L := le_antisymm (hEq ▸ htu) htl
    have hmix := mix_mem_identifiedSet (z := z) (y := y) (a := a) (b := b) hy
      (lam := 0) le_rfl zero_le_one
    simpa [hte] using hmix
  · have hd : (0 : ℝ) < U - L := sub_pos.mpr hLt
    have hne : U - L ≠ 0 := ne_of_gt hd
    have h0 : 0 ≤ (t - L) / (U - L) := div_nonneg (by linarith) hd.le
    have h1 : (t - L) / (U - L) ≤ 1 := (div_le_one hd).mpr (by linarith)
    have hmix := mix_mem_identifiedSet (z := z) (y := y) (a := a) (b := b) hy h0 h1
    have hcancel : (t - L) / (U - L) * (U - L) = t - L := div_mul_cancel₀ _ hne
    have heq : (1 - (t - L) / (U - L)) * L + (t - L) / (U - L) * U = t := by linarith
    rwa [heq] at hmix

The theorem.

Under a bounded outcome, the set of average treatment effects consistent with the observed data is exactly the closed interval whose endpoints impute every missing potential outcome at the worse, respectively better, end of the range.

identifiedSet_eq_IccNew tabOpens with 1,424 lines of library preamble — the code above is at the bottom of the editor.

/-- **The Manski worst-case bounds are sharp.**

The identified set is *exactly* the closed interval `[manskiLower, manskiUpper]`, an equality of
sets proved by `Set.ext` from the two inclusions.  The only hypothesis is that the observed
outcomes lie in `[a, b]` — which, by `InRange.of_consistentWith`, is precisely the condition
under which any consistent bounded population exists at all. -/
theorem identifiedSet_eq_Icc {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ} (hy : InRange a b y) :
    identifiedSet z y a b = Set.Icc (manskiLower z y a b) (manskiUpper z y a b) :=
  Set.ext fun _ =>
    ⟨fun ht => identifiedSet_subset_Icc z y a b ht, fun ht => mem_identifiedSet_of_mem_Icc hy ht⟩

Set.ext is the extensionality principle for sets: two sets are equal when they have the same members, so the proof is a ↔ at each t, supplied here by the two inclusions. This is the shape to look for when someone hands you a formalized identification result. An equality of sets proved by Set.ext from two inclusions is a sharpness claim. A lone ⊆ is a bound, and a bound is worth much less: identifiedSet z y a b ⊆ Set.Icc (a - b) (b - a) is also true and says essentially nothing.

Having the equality, the order-theoretic vocabulary comes for free:

IsLeast, IsGreatest, sInf, sSupNew tabOpens with 1,435 lines of library preamble — the code above is at the bottom of the editor.

/-- The lower bound is the *least* element of the identified set: it is in the set, and it is a
lower bound for it.  `IsLeast` bundles exactly those two facts, and it is the honest formal
statement of "this is the sharp lower bound". -/
theorem isLeast_identifiedSet {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ} (hy : InRange a b y) :
    IsLeast (identifiedSet z y a b) (manskiLower z y a b) := by
  rw [identifiedSet_eq_Icc hy]
  exact isLeast_Icc (manskiLower_le_manskiUpper hy)

/-- The upper bound is the greatest element of the identified set. -/
theorem isGreatest_identifiedSet {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ}
    (hy : InRange a b y) :
    IsGreatest (identifiedSet z y a b) (manskiUpper z y a b) := by
  rw [identifiedSet_eq_Icc hy]
  exact isGreatest_Icc (manskiLower_le_manskiUpper hy)

/-- Consequently the infimum of the identified set is the lower bound, and it is attained. -/
theorem csInf_identifiedSet {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ} (hy : InRange a b y) :
    sInf (identifiedSet z y a b) = manskiLower z y a b :=
  (isLeast_identifiedSet hy).csInf_eq

/-- And the supremum is the upper bound. -/
theorem csSup_identifiedSet {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ} (hy : InRange a b y) :
    sSup (identifiedSet z y a b) = manskiUpper z y a b :=
  (isGreatest_identifiedSet hy).csSup_eq

IsLeast S x is x ∈ S ∧ ∀ y ∈ S, x ≤ y — membership and minimality. That conjunction is the honest formal rendering of “this is the sharp lower bound”, and it is strictly stronger than ∀ y ∈ S, x ≤ y alone. IsLeast.csInf_eq then hands you sInf (identifiedSet …) = manskiLower …, which is the statement an econometrics paper would write. Note that going through IsLeast is not laziness: sInf on ℝ is a conditional infimum and returns 0 for an unbounded or empty set, so sInf S = L on its own does not imply that L is attained, or even that S is non-empty.

The width of the interval is the range of the outcome

ExerciseThe width fact (core)

← mean_sub turns the difference of two means into the mean of the pointwise difference; mean_congr fun i => by ring then observes that that difference is the constant b - a — the indicator cancels identically, which is the whole point — and mean_const hn evaluates the mean of a constant. 0 < n is the only hypothesis, and it enters solely through mean_const; in particular the identity holds whether or not the data are in range.

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

/-- Exercise (core).  **The width of the worst-case bounds is the range of the outcome**, full
stop: it does not depend on the data, on the assignment, or on `n`.

Each unit contributes exactly `(b - a)/n` of missing information and none of it is ever
recovered, so the total is `b - a`.  This is the fact that makes worst-case bounds
uncomfortable in practice and is worth checking against your intuition about sample size.

Proof shape: turn the difference of means into the mean of the difference with `← mean_sub`,
observe with `mean_congr … (by ring)` that the difference is the constant `b - a`, then
`mean_const hn`. -/
theorem manskiUpper_sub_manskiLower (hn : 0 < n) (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) :
    manskiUpper z y a b - manskiLower z y a b = b - a := by
  sorry

Show solution

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

/-- Exercise (core).  **The width of the worst-case bounds is the range of the outcome**, full
stop: it does not depend on the data, on the assignment, or on `n`.

Each unit contributes exactly `(b - a)/n` of missing information and none of it is ever
recovered, so the total is `b - a`.  This is the fact that makes worst-case bounds
uncomfortable in practice and is worth checking against your intuition about sample size.

Proof shape: turn the difference of means into the mean of the difference with `← mean_sub`,
observe with `mean_congr … (by ring)` that the difference is the constant `b - a`, then
`mean_const hn`. -/
theorem manskiUpper_sub_manskiLower (hn : 0 < n) (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) :
    manskiUpper z y a b - manskiLower z y a b = b - a := by
  have h : manskiUpper z y a b - manskiLower z y a b = mean (fun _ : Fin n => b - a) := by
    rw [manskiUpper, manskiLower, ← mean_sub]
    exact mean_congr fun i => by ring
  rw [h, mean_const hn]

Every unit contributes exactly $(b - a) / n$ of missing information: whichever arm it landed in, one of its two potential outcomes is unknown to within the full range. Summing and dividing by $n$ , the $n$ ‘s cancel. So:

the worst-case interval has width $b - a$ for every data set;
it does not shrink as $n$ grows;
it is not a confidence interval, and reporting it as one is a category error. Sampling error goes to zero; identification failure does not.

A companion fact makes the same point in a way that stings more:

Zero is always in the identified setNew tabOpens with 1,460 lines of library preamble — the code above is at the bottom of the editor.

/-- **Worst-case bounds never exclude "no effect".**

`0` is always in the identified set, because a population in which every unit's missing
potential outcome equals its observed one is consistent with the data, respects the bound, and
has `τ = 0`.  So no amount of data, and no design, can rule out the sharp null by bounds alone:
that is what the assumption-free position costs.  Compare chapter 12, where the sharp null
*can* be rejected — at the price of assuming it in order to impute. -/
theorem zero_mem_identifiedSet {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ}
    (hy : InRange a b y) : (0 : ℝ) ∈ identifiedSet z y a b := by
  rw [identifiedSet_eq_Icc hy]
  exact ⟨manskiLower_nonpos hy, manskiUpper_nonneg hy⟩

Worst-case bounds can never sign an effect. The witness is the population that imputes each unit’s missing outcome to equal its observed one: it is consistent with any data whatsoever, respects the range, and has $τ = 0$ . (The Lean proof takes the shorter route through identifiedSet_eq_Icc and the two one-sided facts manskiLower_nonpos and manskiUpper_nonneg, which is the same argument with the construction already done.) Compare chapter 12, where the sharp null can be rejected — at the price of assuming it, in order to impute the missing outcomes, before computing the null distribution. Fisher’s test and Manski’s bounds are the same imputation problem answered with opposite temperaments.

Four units, and nothing learned

The general statements are easier to believe against numbers. Four units, two treated, a binary outcome, and the cleanest possible result: both treated units responded, neither control unit did.

The dataNew tabOpens with 1,765 lines of library preamble — the code above is at the bottom of the editor.

/-- The observed outcomes: both treated units responded, neither control unit did. -/
def yEx : Fin 4 → ℝ := ![1, 1, 0, 0]

/-- The assignment that was run: units `0` and `1` were treated. -/
def zEx : Assignment 4 := {0, 1}

@[simp] theorem yEx_zero : yEx 0 = 1 := rfl
@[simp] theorem yEx_one : yEx 1 = 1 := rfl
@[simp] theorem yEx_two : yEx 2 = 0 := rfl
@[simp] theorem yEx_three : yEx 3 = 0 := rfl

/-- Membership in a `Finset (Fin 4)` given by a literal is decidable, so each of these four
indicators is settled by evaluation. -/
@[simp] theorem Z_zEx_zero : Z zEx 0 = 1 := Z_of_mem (by decide)
@[simp] theorem Z_zEx_one : Z zEx 1 = 1 := Z_of_mem (by decide)
@[simp] theorem Z_zEx_two : Z zEx 2 = 0 := Z_of_not_mem (by decide)
@[simp] theorem Z_zEx_three : Z zEx 3 = 0 := Z_of_not_mem (by decide)

/-- The outcomes are in `[0, 1]`, which is the hypothesis every sharpness result needs. -/
theorem inRange_yEx : InRange 0 1 yEx := by
  intro i
  fin_cases i <;> simp

Z_of_mem/Z_of_not_mem turn each indicator into 1 or 0 once membership is settled, and membership in a Finset (Fin 4) written as a literal is decidable, so by decide settles it by evaluation. fin_cases i splits the range check into its four instances.

Difference in means is $1$ — and it is $1$ for every population consistent with the data, since the estimator only ever touches the outcomes the assignment revealed:

The estimateNew tabOpens with 1,790 lines of library preamble — the code above is at the bottom of the editor.

/-- **Difference in means is `1`, for every population consistent with the data.**

`DiM_eq_observed` says the estimator only ever touches the revealed outcomes, and
`ConsistentWith.apply` says those are `yEx`; after that the sum over `{0, 1}` and the sum over
its complement `{2, 3}` are four numbers.  The `decide` computes the complement. -/
theorem DiM_data {P : Population 4} (hP : ConsistentWith zEx yEx P) : DiM P zEx = 1 := by
  rw [DiM_eq_observed, Finset.sum_congr rfl fun i _ => hP.apply i,
    Finset.sum_congr rfl fun i _ => hP.apply i,
    show zExᶜ = ({2, 3} : Finset (Fin 4)) from by decide,
    show zEx = ({0, 1} : Finset (Fin 4)) from rfl,
    Finset.sum_insert (by decide), Finset.sum_singleton,
    Finset.sum_insert (by decide), Finset.sum_singleton,
    Finset.card_insert_of_notMem (by decide), Finset.card_singleton,
    Finset.card_insert_of_notMem (by decide), Finset.card_singleton]
  norm_num

And the bounds:

The identified setNew tabOpens with 1,806 lines of library preamble — the code above is at the bottom of the editor.

/-- **The worst-case lower bound is `0`.**  A treated unit's missing control outcome is imputed
at `b = 1`, so each of units `0` and `1` contributes `y i - 1 = 0`; a control unit's missing
treated outcome is imputed at `a = 0`, so units `2` and `3` contribute `0 - y i = 0`. -/
theorem manskiLower_data : manskiLower zEx yEx 0 1 = 0 := by
  simp only [manskiLower, mean, Fin.sum_univ_four, Z_zEx_zero, Z_zEx_one, Z_zEx_two,
    Z_zEx_three, yEx_zero, yEx_one, yEx_two, yEx_three]
  norm_num

/-- **The worst-case upper bound is `1`.**  The mirror image: every unit contributes `1`. -/
theorem manskiUpper_data : manskiUpper zEx yEx 0 1 = 1 := by
  simp only [manskiUpper, mean, Fin.sum_univ_four, Z_zEx_zero, Z_zEx_one, Z_zEx_two,
    Z_zEx_three, yEx_zero, yEx_one, yEx_two, yEx_three]
  norm_num

/-- **The identified set is the whole of `[0, 1]`.**

`identifiedSet_eq_Icc` is sharpness: the interval is not a bound someone was too lazy to
improve, it is exactly the set of average treatment effects a consistent bounded population can
have.  Here it is the same interval `[a, b] = [0, 1]` that the boundedness assumption gave us
before the experiment ran, so the data have ruled out nothing at all — including `τ = 0`. -/
theorem identifiedSet_data : identifiedSet zEx yEx 0 1 = Set.Icc 0 1 := by
  rw [identifiedSet_eq_Icc inRange_yEx, manskiLower_data, manskiUpper_data]

/-- The estimate is not in doubt and the estimand is entirely undetermined: `DiM = 1`, while the
identified set still contains `0`. -/
theorem zero_mem_identifiedSet_data : (0 : ℝ) ∈ identifiedSet zEx yEx 0 1 := by
  rw [identifiedSet_data]
  exact Set.mem_Icc.mpr ⟨le_refl 0, by norm_num⟩

The identified set is $[0, 1]$ : the entire range the boundedness assumption allowed before anybody ran anything. Every value the outcome scale admits is still available, including $τ = 0$ . The estimate is the largest it could possibly have been, the estimand is completely undetermined, and both statements are checked by the same compiler. The data look decisive and the bounds say nothing.

That is not a pathology of the example, and no cleverer data set escapes it. manskiUpper_sub_manskiLower fixes the width at $b - a = 1$ for every binary data set, and manskiLower_nonpos together with manskiUpper_nonneg puts $0$ inside it for every binary data set. So the identified set is always $[ℓ, ℓ + 1]$ with $- 1 \leq ℓ \leq 0$ : a unit interval that always contains zero. What the data choose is where in $[- 1, 0]$ the left endpoint sits — never how wide the interval is, and never whether it signs the effect.

Monotone treatment response

MTRNew tabOpens with 1,487 lines of library preamble — the code above is at the bottom of the editor.

/-- **Monotone treatment response**: treatment never lowers any unit's outcome.

Note what this is *not*: it is not `0 ≤ P.tau`, which is a statement about the average.  MTR is
a hypothesis about every unit separately, and it is strictly stronger. -/
def MTR (P : Population n) : Prop := ∀ i, P.y0 i ≤ P.y1 i

MTR says nobody is hurt by treatment. It is a statement about every unit separately and is strictly stronger than $τ \geq 0$ ; the implication one way is the warm-up:

ExerciseMTR implies a non-negative ATE (warm-up)

An average of non-negative numbers is non-negative. Say it through mean_le_mean against the zero vector rather than by hand, so that the n = 0 case takes care of itself, and finish with simpa [mean] to evaluate mean (fun _ => 0). sub_nonneg.mpr (h i) turns P.y0 i ≤ P.y1 i into 0 ≤ P.y1 i - P.y0 i, which is 0 ≤ P.effect i after unfolding.

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

/-- Exercise (warm-up).  Under MTR the ATE is non-negative.

An average of non-negative numbers is non-negative — but say it through `mean_le_mean` against
the zero vector rather than by hand, so that the `n = 0` case (where both sides are `0`) takes
care of itself.  `simpa [mean]` disposes of `mean (fun _ => 0)`. -/
theorem tau_nonneg_of_MTR {P : Population n} (h : MTR P) : 0 ≤ P.tau := by
  sorry

Show solution

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

/-- Exercise (warm-up).  Under MTR the ATE is non-negative.

An average of non-negative numbers is non-negative — but say it through `mean_le_mean` against
the zero vector rather than by hand, so that the `n = 0` case (where both sides are `0`) takes
care of itself.  `simpa [mean]` disposes of `mean (fun _ => 0)`. -/
theorem tau_nonneg_of_MTR {P : Population n} (h : MTR P) : 0 ≤ P.tau := by
  have hz : mean (fun _ : Fin n => (0 : ℝ)) ≤ P.tau :=
    mean_le_mean fun i => by simpa [Population.effect] using sub_nonneg.mpr (h i)
  simpa [mean] using hz

What does MTR buy? For a treated unit, y0 i ≤ y1 i = y i, so its missing outcome is confined to $[a, y_{i}]$ and its effect to $[0, y_{i} - a]$ ; the upper end is unchanged and the lower end moves up to zero. For a control unit, y1 i ≥ y0 i = y i and the same happens. Pointwise, the lower bound becomes zero at every unit, so the new interval is $[0, τ_{U}]$ : MTR buys the entire lower half and nothing else.

The MTR identified set, and its sharpnessNew tabOpens with 1,513 lines of library preamble — the code above is at the bottom of the editor.

/-- **The MTR bounds, and their sharpness.**

Under monotone treatment response the identified set is exactly `[0, manskiUpper]`: the upper
endpoint is unchanged, and the lower endpoint moves from `manskiLower` (which is `≤ 0` by
`manskiLower_nonpos`) all the way up to `0`.

The two inclusions again.  `⊆` is `tau_nonneg_of_MTR` together with `tau_le_manskiUpper`.  For
`⊇`, the family that sweeps the interval imputes `(1 - lam) * y i + lam * b` for a control
unit's treated outcome and `(1 - lam) * y i + lam * a` for a treated unit's control outcome: at
`lam = 0` every unit is given a zero effect, at `lam = 1` the worst-case upper bound is
recovered, and the ATE along the way is exactly `lam * manskiUpper`. -/
theorem mtrIdentifiedSet_eq_Icc {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ}
    (hy : InRange a b y) :
    mtrIdentifiedSet z y a b = Set.Icc 0 (manskiUpper z y a b) := by
  refine Set.ext fun t => ⟨?_, ?_⟩
  · rintro ⟨P, hcon, hb, hmtr, rfl⟩
    exact ⟨tau_nonneg_of_MTR hmtr, tau_le_manskiUpper hcon hb⟩
  · rintro ⟨ht0, htU⟩
    -- Choose the mixing weight, taking care of the degenerate interval `manskiUpper = 0`.
    obtain ⟨lam, h0, h1, hlam⟩ :
        ∃ lam : ℝ, 0 ≤ lam ∧ lam ≤ 1 ∧ lam * manskiUpper z y a b = t := by
      rcases eq_or_lt_of_le (manskiUpper_nonneg hy) with hU | hU
      · exact ⟨0, le_rfl, zero_le_one, by
          have : t = 0 := le_antisymm (hU ▸ htU) ht0
          simp [this]⟩
      · exact ⟨t / manskiUpper z y a b, div_nonneg ht0 hU.le, (div_le_one hU).mpr htU,
          by field_simp⟩
    refine ⟨imputePop z y (fun i => (1 - lam) * y i + lam * b)
      (fun i => (1 - lam) * y i + lam * a), imputePop_consistentWith z y _ _, ?_, ?_, ?_⟩
    · refine imputePop_bounded hy (fun i => ?_) (fun i => ?_) <;>
        · obtain ⟨hy1, hy2⟩ := hy i
          have hb1 : (0 : ℝ) ≤ lam * (b - a) := mul_nonneg h0 (by linarith)
          have hb2 : (0 : ℝ) ≤ (1 - lam) * (y i - a) := mul_nonneg (by linarith) (by linarith)
          have hb3 : (0 : ℝ) ≤ (1 - lam) * (b - y i) := mul_nonneg (by linarith) (by linarith)
          constructor <;> linarith
    · intro i
      obtain ⟨hy1, hy2⟩ := hy i
      by_cases hi : i ∈ z
      · simp only [imputePop_y1, imputePop_y0, Z_of_mem hi]
        linarith [mul_nonneg h0 (sub_nonneg.mpr hy1)]
      · simp only [imputePop_y1, imputePop_y0, Z_of_not_mem hi]
        linarith [mul_nonneg h0 (sub_nonneg.mpr hy2)]
    · rw [tau_imputePop, ← hlam, manskiUpper, ← mean_const_mul]
      exact mean_congr fun i => by ring

The proof repeats the pattern, which is the point of showing it twice. ⊆ is two lemmas. For ⊇, the sweeping family imputes $(1 - λ) y_{i} + λ b$ for a control unit’s treated outcome and $(1 - λ) y_{i} + λ a$ for a treated unit’s control outcome: at $λ = 0$ every unit is given a zero effect, at $λ = 1$ the worst-case upper bound is recovered, and the ATE along the way is exactly $λ \cdot τ_{U}$ . The degenerate case $τ_{U} = 0$ has to be split off, because the weight is $t / τ_{U}$ .

This is what a partial-identification result looks like in general: an assumption, a shorter interval, and a proof that the shorter interval is still exactly attained. If the third part is missing you have a bound, not an identified set, and you cannot tell whether the assumption was worth making.

Bounds under a design

Everything above is deterministic. Reintroduce the design and the endpoints become statistics — functions of the assignment, computed from the data that assignment produced:

The estimated boundsNew tabOpens with 1,578 lines of library preamble — the code above is at the bottom of the editor.

/-- The **estimated** Manski lower bound: the lower endpoint computed from the data that the
assignment `z` actually produced.  Unlike `manskiLower`, this is a statistic — a function of
the assignment — so a design can take its expectation. -/
noncomputable def manskiLowerHat (P : Population n) (a b : ℝ) (z : Assignment n) : ℝ :=
  manskiLower z (Yobs P z) a b

/-- The estimated Manski upper bound. -/
noncomputable def manskiUpperHat (P : Population n) (a b : ℝ) (z : Assignment n) : ℝ :=
  manskiUpper z (Yobs P z) a b

They bracket τ for every assignmentNew tabOpens with 1,588 lines of library preamble — the code above is at the bottom of the editor.

/-- **The estimated bounds bracket the true ATE for every assignment.**

Not "with high probability", not "in expectation": for every single `z`.  The proof is
`manskiLower_le_tau` with `y := Yobs P z`, whose consistency hypothesis is `rfl` — the
population is trivially consistent with the data it generated. -/
theorem manskiHat_brackets {a b : ℝ} {P : Population n} (hb : Bounded a b P)
    (z : Assignment n) :
    manskiLowerHat P a b z ≤ P.tau ∧ P.tau ≤ manskiUpperHat P a b z :=
  ⟨manskiLower_le_tau rfl hb, tau_le_manskiUpper rfl hb⟩

Not “with probability $1 - α$ ” and not “in expectation”: for every single z. The consistency hypothesis of manskiLower_le_tau is discharged by rfl, because a population is trivially consistent with the data it generated. Taking expectations is then monotonicity and nothing else:

ExerciseBounds in expectation (core)

Two steps, no computation. Design.expect_mono (from chapter 7) turns the pointwise inequality of manskiHat_brackets into an inequality of expectations against the constant statistic fun _ => P.tau, and Design.expect_const evaluates that expectation. A calc block reads best; note that expect_mono takes its two statistics explicitly, so the call is D.expect_mono _ _ h.

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

/-- Exercise (core).  **In expectation under any design, the lower bound is still a lower
bound.**

Two steps and no computation: `Design.expect_mono` turns the pointwise inequality of
`manskiHat_brackets` into an inequality of expectations, and `Design.expect_const` evaluates
the expectation of the constant statistic `fun _ => P.tau`.  A `calc` block reads best. -/
theorem expect_manskiLowerHat_le (D : Design n) {a b : ℝ} {P : Population n}
    (hb : Bounded a b P) : D.expect (manskiLowerHat P a b) ≤ P.tau := by
  sorry

Show solution

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

/-- Exercise (core).  **In expectation under any design, the lower bound is still a lower
bound.**

Two steps and no computation: `Design.expect_mono` turns the pointwise inequality of
`manskiHat_brackets` into an inequality of expectations, and `Design.expect_const` evaluates
the expectation of the constant statistic `fun _ => P.tau`.  A `calc` block reads best. -/
theorem expect_manskiLowerHat_le (D : Design n) {a b : ℝ} {P : Population n}
    (hb : Bounded a b P) : D.expect (manskiLowerHat P a b) ≤ P.tau := by
  calc D.expect (manskiLowerHat P a b)
      ≤ D.expect (fun _ => P.tau) := D.expect_mono _ _ fun z => (manskiHat_brackets hb z).1
    _ = P.tau := D.expect_const _

And now the sentence this chapter exists for:

The expected width is b − a, under every designNew tabOpens with 1,617 lines of library preamble — the code above is at the bottom of the editor.

/-- **The expected width of the estimated bounds is `b - a`, under every design.**

This is the sentence the chapter is for.  Randomisation is what makes the *point* estimator
unbiased (`HT_unbiased`, `DiM_unbiased_completeRandomization`); it does nothing whatsoever to
the worst-case bounds, whose expected width is the outcome range no matter which design you
run, how large `n` is, or how the units happen to be split.  Design buys identification, not
information about the counterfactual. -/
theorem expect_manskiHat_width (hn : 0 < n) (D : Design n) (P : Population n) (a b : ℝ) :
    D.expect (manskiUpperHat P a b) - D.expect (manskiLowerHat P a b) = b - a := by
  rw [← D.expect_sub,
    D.expect_congr (f := fun z => manskiUpperHat P a b z - manskiLowerHat P a b z)
      (g := fun _ => b - a) fun z => manskiUpper_sub_manskiLower hn z (Yobs P z) a b]
  exact D.expect_const _

D : Design n is universally quantified. Bernoulli, complete randomization, stratified, clustered, a pmf you invented this morning: the expected distance between the estimated bounds is the range of the outcome, always. Set that beside chapter 8:

The point estimate lives inside the boundsNew tabOpens with 1,631 lines of library preamble — the code above is at the bottom of the editor.

/-- Under complete randomisation the difference in means is unbiased for `τ`, and `τ` sits
between the expected bounds.  Two different kinds of guarantee about the same experiment: the
first is an equality that depends entirely on the design, the second an interval that does not
depend on the design at all. -/
theorem dim_expect_mem_bounds {n₁ : ℕ} (hle : n₁ ≤ n) (P : Population n) (hpos : 0 < n₁)
    (hlt : n₁ < n) {a b : ℝ} (hb : Bounded a b P) :
    (completeRandomization n n₁ hle).expect (DiM P) ∈
      Set.Icc ((completeRandomization n n₁ hle).expect (manskiLowerHat P a b))
        ((completeRandomization n n₁ hle).expect (manskiUpperHat P a b)) := by
  rw [DiM_unbiased_completeRandomization hle P hpos hlt]
  exact ⟨expect_manskiLowerHat_le _ hb, le_expect_manskiUpperHat _ hb⟩

Randomization buys point identification — an estimator whose expectation is $τ$ on the nose — and it buys nothing at all against the counterfactual you did not observe. Those are different goods, and the design only purchases the first. That is not a criticism of randomized experiments; it is a description of what they are for, and the two Lean statements make the division of labour exact rather than rhetorical.

Attrition

The one place where the distinction bites in a real experiment. Randomization fixes selection into treatment; it does nothing about selection into being measured. If a unit does not respond, neither of its potential outcomes is observed, and all you know about its effect is that it lies in $[a - b, b - a]$ .

Bounds from responders onlyNew tabOpens with 1,653 lines of library preamble — the code above is at the bottom of the editor.

/-- The worst-case lower bound computed from **responders only**: a responder contributes its
Manski term, a non-responder contributes `a - b`, the smallest its effect could possibly be. -/
noncomputable def attritionLower (z : Assignment n) (R : Finset (Fin n)) (y : Fin n → ℝ)
    (a b : ℝ) : ℝ :=
  mean fun i => Z R i * (Z z i * (y i - b) + (1 - Z z i) * (a - y i)) + (1 - Z R i) * (a - b)

/-- The matching upper bound: a non-responder contributes `b - a`. -/
noncomputable def attritionUpper (z : Assignment n) (R : Finset (Fin n)) (y : Fin n → ℝ)
    (a b : ℝ) : ℝ :=
  mean fun i => Z R i * (Z z i * (y i - a) + (1 - Z z i) * (b - y i)) + (1 - Z R i) * (b - a)

R : Finset (Fin n) is the set of responders. Because Assignment n is Finset (Fin n), the indicator Z R i of the response set is the same function Z used for treatment — no new machinery, which is a small dividend of the representation choice made in chapter 6.

The responder-only bounds still bracket τNew tabOpens with 1,664 lines of library preamble — the code above is at the bottom of the editor.

/-- **The responder-only bounds still bracket the true ATE.**

The hypothesis is deliberately weak: `y` has to match the population's observed outcome only on
`R`.  Off `R` the vector `y` may be anything at all — it is not used.  Four cases (respond or
not, treated or not) and `linarith` in each. -/
theorem attrition_brackets {z : Assignment n} {R : Finset (Fin n)} {y : Fin n → ℝ} {a b : ℝ}
    {P : Population n} (hb : Bounded a b P) (hr : ∀ i ∈ R, Yobs P z i = y i) :
    attritionLower z R y a b ≤ P.tau ∧ P.tau ≤ attritionUpper z R y a b := by
  constructor
  · rw [attritionLower, Population.tau]
    refine mean_le_mean fun i => ?_
    obtain ⟨h1, _, _, h4⟩ := hb i
    simp only [Population.effect]
    by_cases hiR : i ∈ R
    · rw [Z_of_mem hiR]
      by_cases hi : i ∈ z
      · rw [Z_of_mem hi, ← hr i hiR, Yobs_of_mem hi]
        linarith
      · rw [Z_of_not_mem hi, ← hr i hiR, Yobs_of_not_mem hi]
        linarith
    · rw [Z_of_not_mem hiR]
      linarith
  · rw [attritionUpper, Population.tau]
    refine mean_le_mean fun i => ?_
    obtain ⟨_, h2, h3, _⟩ := hb i
    simp only [Population.effect]
    by_cases hiR : i ∈ R
    · rw [Z_of_mem hiR]
      by_cases hi : i ∈ z
      · rw [Z_of_mem hi, ← hr i hiR, Yobs_of_mem hi]
        linarith
      · rw [Z_of_not_mem hi, ← hr i hiR, Yobs_of_not_mem hi]
        linarith
    · rw [Z_of_not_mem hiR]
      linarith

The hypothesis is deliberately weak: y has to agree with the population’s observed outcome only on R. Off R the vector y may be anything at all, because it is never used. That is the formal content of “we do not know what the non-respondents would have shown”. Four cases — respond or not, treated or not — and linarith in each.

attritionUpper_sub_attritionLower prices the damage: the width is $(b - a) (2 - # R / n)$ , so each non-respondent costs a second full copy of the outcome range. Full response recovers the Manski width:

ExerciseFull response (warm-up)

A sanity check on the definition. Finset.univ is the response set in which everybody answers, and Z_of_mem (Finset.mem_univ i) rewrites Z univ i to 1; ring then finishes each summand. Do it with mean_congr fun i => ?_ so you are working one unit at a time.

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

/-- Exercise (warm-up).  With full response the attrition bounds are the Manski bounds.

A sanity check on the definition, and a reminder that `Finset.univ` is the response set in
which everybody answers.  `Z_of_mem (Finset.mem_univ i)` rewrites `Z univ i` to `1`; then
`ring` finishes each summand. -/
theorem attritionLower_univ (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) :
    attritionLower z Finset.univ y a b = manskiLower z y a b := by
  sorry

Show solution

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

/-- Exercise (warm-up).  With full response the attrition bounds are the Manski bounds.

A sanity check on the definition, and a reminder that `Finset.univ` is the response set in
which everybody answers.  `Z_of_mem (Finset.mem_univ i)` rewrites `Z univ i` to `1`; then
`ring` finishes each summand. -/
theorem attritionLower_univ (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) :
    attritionLower z Finset.univ y a b = manskiLower z y a b := by
  refine mean_congr fun i => ?_
  rw [Z_of_mem (Finset.mem_univ i)]
  ring

Exercises

The exercises above run through the chapter; three more that are worth doing in order.

ExerciseConstants pull out of a mean (warm-up)

Needed twice in mix_mem_identifiedSet, in the ← direction, to push a convex combination inside a mean. Finset.mul_sum moves the constant into the sum and mul_div_assoc moves the division out; one simp only with both, plus mean, does it.

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

/-- Exercise (warm-up).  The mean is homogeneous: a constant pulls out.

`Finset.mul_sum : b * ∑ i ∈ s, f i = ∑ i ∈ s, b * f i` and `mul_div_assoc` are the two lemmas
involved; the goal after unfolding `mean` is `(∑ i, c * v i) / n = c * ((∑ i, v i) / n)`. -/
theorem mean_const_mul (c : ℝ) (v : Fin n → ℝ) :
    mean (fun i => c * v i) = c * mean v := by
  sorry

Show solution

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

/-- Exercise (warm-up).  The mean is homogeneous: a constant pulls out.

`Finset.mul_sum : b * ∑ i ∈ s, f i = ∑ i ∈ s, b * f i` and `mul_div_assoc` are the two lemmas
involved; the goal after unfolding `mean` is `(∑ i, c * v i) / n = c * ((∑ i, v i) / n)`. -/
theorem 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]

ExerciseThe interval is non-empty (core)

mean_le_mean, then a single have key : … = b - a := by ring computing the pointwise difference of the two integrands, then linarith. You will need a ≤ b, which is le_trans (hy i).1 (hy i).2 — available only inside the fun i => …, since with no units there is nothing to derive it from. That is why the theorem needs InRange rather than a bare a ≤ b.

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

/-- Exercise (core).  The lower bound really is below the upper bound.

The pointwise difference of the two integrands is `b - a` *identically* — the indicator
cancels, which is the whole content of the width theorem below.  So the proof is
`mean_le_mean`, then a `have … := by ring` computing that difference, then `linarith` with
`a ≤ b` (which you can extract from `hy i`, since `a ≤ y i ≤ b`). -/
theorem manskiLower_le_manskiUpper {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ}
    (hy : InRange a b y) : manskiLower z y a b ≤ manskiUpper z y a b := by
  sorry

Show solution

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

/-- Exercise (core).  The lower bound really is below the upper bound.

The pointwise difference of the two integrands is `b - a` *identically* — the indicator
cancels, which is the whole content of the width theorem below.  So the proof is
`mean_le_mean`, then a `have … := by ring` computing that difference, then `linarith` with
`a ≤ b` (which you can extract from `hy i`, since `a ≤ y i ≤ b`). -/
theorem manskiLower_le_manskiUpper {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ}
    (hy : InRange a b y) : manskiLower z y a b ≤ manskiUpper z y a b := by
  refine mean_le_mean fun i => ?_
  have hab : a ≤ b := le_trans (hy i).1 (hy i).2
  have key : Z z i * (y i - a) + (1 - Z z i) * (b - y i)
      - (Z z i * (y i - b) + (1 - Z z i) * (a - y i)) = b - a := by ring
  linarith

Exercise (stretch, on paper). Suppose the design treats 90% of the units. The treated units’ missing outcomes are then 90% of the missing information — so why does the width of the worst-case interval not depend on that fraction?

Reading autoformalized Lean

Three failures, in decreasing order of how often you will meet them.

A bound advertised as an identified set

-- WRONG: true, but it is not the theorem it is named after
theorem manski_identified_set (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) :
    identifiedSet z y a b ⊆ Set.Icc (manskiLower z y a b) (manskiUpper z y a b) := by
  rintro t ⟨P, hcon, hb, rfl⟩
  exact ⟨manskiLower_le_tau hcon hb, tau_le_manskiUpper hcon hb⟩

This compiles, it is true, and it is half the theorem. Nothing in it rules out a smaller interval — and there is no shortage of true inclusions: identifiedSet z y a b ⊆ Set.Icc (a - b) (b - a) is one, and it is useless. The word “sharp” in the informal statement corresponds precisely to the missing inclusion, and it is the harder one because it requires constructing populations rather than reasoning about an arbitrary one.

The check is mechanical: does the conclusion contain = or ⊆? If ⊆, does a companion result supply the other direction, or an IsLeast/IsGreatest? If the answer is a lone ⊆ and the prose says “identified set”, the formalization does not say what the prose says.

An assumption about the data pretending to be an assumption about the counterfactuals

-- WRONG: this hypothesis has no content at all
def BoundedObserved (a b : ℝ) (z : Assignment n) (P : Population n) : Prop :=
  ∀ i, a ≤ Yobs P z i ∧ Yobs P z i ≤ b

theorem manski_bad (z : Assignment n) (y : Fin n → ℝ) (a b : ℝ) (P : Population n)
    (hcon : ConsistentWith z y P) (hb : BoundedObserved a b z P) :
    manskiLower z y a b ≤ P.tau := by
  sorry

Bounded quantifies over P.y1 i and P.y0 i; BoundedObserved quantifies over Yobs P z i, which is whichever of the two the assignment revealed. The second is a statement you can verify from the sample — and precisely for that reason it constrains nothing about the missing half, so the claim is false and the sorry cannot be filled. This substitution is easy to make and hard to see, because both definitions read as “the outcome is between a and b”.

The habit that catches it: for every assumption in a partial-identification statement, ask whether it is refutable by data. If it is, it is not doing identification work. Genuine identifying assumptions — Bounded, MTR, the sharp null, unconfoundedness — are all statements about quantities that are never jointly observed.

A hypothesis nothing satisfies

-- WRONG: vacuous whenever 0 < n and a < b
theorem manski_vacuous {z : Assignment n} {y : Fin n → ℝ} {a b : ℝ}
    (hy : ∀ i, b ≤ y i ∧ y i ≤ a) :
    identifiedSet z y a b = Set.Icc (manskiLower z y a b) (manskiUpper z y a b) := by
  sorry

The two inequalities in InRange have been swapped, so hy forces b ≤ a. With a < b and at least one unit, no y satisfies it and the theorem is vacuously true — which does not stop it from looking exactly like identifiedSet_eq_Icc. The check from chapter 8 applies unchanged: exhibit one object satisfying the hypotheses. If you cannot, the theorem is worthless however impressive its statement.

Note the sting in the tail: manski_vacuous becomes non-vacuous at n = 0, where hy is an empty conjunction. So “the hypotheses are satisfiable” is not quite the right question either; the right one is “are they satisfiable in the cases I care about”.

Two smaller checks, both specific to this chapter. First, Set.Icc is the closed interval; Set.Ico and Set.Ioo are one and two endpoints short, and a partial-identification theorem stated with Set.Ioo is asserting that the extreme populations do not fit the data — the opposite of sharpness. Second, manskiUpper_sub_manskiLower needs 0 < n and nothing else: it is an algebraic identity that holds even when the data are out of range and the identified set is empty. A formalization that attaches InRange to the width theorem is not wrong, but it is a hint that the author did not know which hypothesis was doing what — and hypotheses that are not doing anything are where vacuity hides.

The identified set is a Set ℝ

Manski’s worst-case bounds

The easy half

The hard half: sharpness

The width of the interval is the range of the outcome

Four units, and nothing learned

Monotone treatment response

Bounds under a design

Attrition

Exercises

Reading autoformalized Lean

The identified set is a `Set ℝ`