Partial identification

When the observed data and assumptions do not determine a unique average treatment effect, the estimand is partially identified. Its identified set contains the effects of all populations consistent with the observations and the maintained assumptions.

This chapter derives Manski’s bounds for bounded outcomes. It distinguishes a valid outer bound from a sharp characterization of the identified set. A proof of sharpness must show that every value in the proposed interval is attained by some compatible population; proving only containment is insufficient.

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 846 lines of library preamble — the code above is at the bottom of the editor.

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 864 lines of library preamble — the code above is at the bottom of the editor.

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 882 lines of library preamble — the code above is at the bottom of the editor.

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)

If some bounded population is consistent with the data, the data themselves are in range: InRange a b y.

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

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

Hint

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.

Show solution

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

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 necessary rather than decorative. This distinction matters 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 898 lines of library preamble — the code above is at the bottom of the editor.

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)

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

Proposition (the bounds are bounds). Let $P$ be a population consistent with the data $(z, y)$ and with every potential outcome in $[a, b]$ . Then

τ_{L} \leq τ (P) \leq τ_{U} .

Proof.

The mean is monotone, so it suffices to bound each unit’s effect below by the corresponding summand of $τ_{L}$ .

Let $i$ be a treated unit. Consistency gives $y_{1 i} = y_{i}$ , and boundedness gives $y_{0 i} \leq b$ , so $y_{1 i} - y_{0 i} \geq y_{i} - b$ , which is the $i$ -th summand of $τ_{L}$ . Let $i$ be a control unit. Then $y_{0 i} = y_{i}$ and $a \leq y_{1 i}$ , so $y_{1 i} - y_{0 i} \geq a - y_{i}$ , again the $i$ -th summand. Averaging over $i = 1, \dots, n$ gives $τ_{L} \leq τ (P)$ .

The upper bound is the mirror image, using the other two halves of the boundedness assumption: $a \leq y_{0 i}$ for a treated unit and $y_{1 i} \leq b$ for a control unit.

Notice which half of boundedness each inequality consumed: only the constraint on the outcome that was not observed. The observed one needs no assumption at all, because consistency has already pinned it down.∎

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

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

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 theorems have the same nine-line shape; here is the lower one.

```
rw [manskiLower, Population.tau]
```
Unfold both sides to the means they are. Population.tau is mean P.effect and manskiLower is the mean of the pointwise lower bound, so the goal is now an inequality between two means — the shape the monotonicity lemma wants.
Goal
```
⊢ (mean fun i => Z z i * (y i - b) + (1 - Z z i) * (a - y i)) ≤ mean P.effect
```
```
refine mean_le_mean fun i => ?_
```
mean_le_mean is the monotonicity of the mean proved above: from ∀ i, u i ≤ v i it concludes mean u ≤ mean v. Supplying its argument as fun i => ?_ reduces the whole inequality to one arbitrary unit — the “unit by unit” of the informal proof.
Goal
```
i : Fin n
⊢ Z z i * (y i - b) + (1 - Z z i) * (a - y i) ≤ P.effect i
```
```
obtain ⟨h1, _, _, h4⟩ := hb i
```
Bounded a b P is a four-fold conjunction at each unit. Destructuring it here names only the two components this branch needs — h1 : a ≤ P.y1 i and h4 : P.y0 i ≤ b — and discards the other two with underscores, which is the formal record of “only the unobserved half is used”. The following simp only [Population.effect] replaces P.effect i by P.y1 i - P.y0 i.
Goal
```
h1 : a ≤ P.y1 i
left✝¹ : P.y1 i ≤ b
left✝ : a ≤ P.y0 i
h4 : P.y0 i ≤ b
⊢ Z z i * (y i - b) + (1 - Z z i) * (a - y i) ≤ P.y1 i - P.y0 i
```
```
by_cases hi : i ∈ z
```
Split on whether unit i was treated. This is the case distinction the informal proof makes, and it is the only case distinction in the file: Z z i is 1 in one branch and 0 in the other.
```
rw [Z_of_mem hi, hcon.y1_eq hi]
```
The treated branch. Z_of_mem rewrites the indicator Z z i to 1, and hcon.y1_eq hi : P.y1 i = y i — consistency at a treated unit — replaces the population’s treated outcome on the right by the observed number. Both sides now speak of y i and the single unknown P.y0 i.
Goal
```
hi : i ∈ z
⊢ 1 * (y i - b) + (1 - 1) * (a - y i) ≤ y i - P.y0 i
```
```
linarith
```
The goal is linear in y i, a, b and P.y0 i: after cancelling the (1 - 1) term it reads y i - b ≤ y i - P.y0 i, which follows from h4 : P.y0 i ≤ b. linarith finds that combination.
```
rw [Z_of_not_mem hi, hcon.y0_eq hi]
```
The control branch. Z_of_not_mem rewrites the indicator to 0, and hcon.y0_eq hi : P.y0 i = y i replaces the control outcome by the observed number. The goal reduces to a - y i ≤ P.y1 i - y i, and the closing linarith gets it from h1 : a ≤ P.y1 i.
Goal
```
hi : i ∉ z
⊢ 0 * (y i - b) + (1 - 0) * (a - y i) ≤ P.y1 i - y i
```

tau_le_manskiUpper is the same proof with the other two components of hb named (obtain ⟨_, h2, h3, _⟩) and manskiUpper in place of manskiLower; the two linarith calls then use P.y1 i ≤ b and a ≤ P.y0 i.

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

ExerciseMeans are monotone (core)

If u i ≤ v i for every unit then mean u ≤ mean v. Deliberately not assuming 0 < n: at n = 0 both means are 0 / 0 = 0 and the inequality is 0 ≤ 0.

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

theorem mean_le_mean {u v : Fin n → ℝ} (h : ∀ i, u i ≤ v i) : mean u ≤ mean v := by
  sorry

Hint

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. One exact.

Show solution

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

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 two lines:

ExerciseThe bounds contain the identified set (core)

Every ATE in the identified set lies in the Manski interval — the easy inclusion of the main theorem.

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

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

Hint

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 manskiLower_le_tau and tau_le_manskiUpper.

Show solution

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

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

The sharpness result states more than ” $τ$ is in this interval.” It states that every point of the interval is the ATE of a population that fits the data and respects the range. The interval therefore cannot be narrowed without an additional assumption.

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

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

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.

Lemma. For any imputed vectors $u$ and $v$ , the population above is consistent with the data: running it under $z$ returns $y$ exactly.

Proof.

Take a unit $i$ . If $i$ is treated, its observed outcome under $z$ is its treated potential outcome, which the construction set to $y_{i}$ . If $i$ is a control, its observed outcome is its control potential outcome, which the construction also set to $y_{i}$ . Either way $Y_{i}^{o b s} = y_{i}$ , and the two vectors agree at every unit.∎

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

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 Lean proof does not case-split, and that is worth watching, because it shows what the real indicator Z is for.

```
funext i
```
ConsistentWith z y P is the equality of functions Yobs P z = y, so the proof opens by reducing it to agreement at an arbitrary unit i.
Goal
```
⊢ Yobs (imputePop z y u v) z i = y i
```
```
simp only [Yobs, imputePop_y1, imputePop_y0]
```
Unfold everything. Yobs is itself written with the indicator — Z z i * y1 i + (1 - Z z i) * y0 i — and the two imputePop_* lemmas replace those potential outcomes by their definitions, which are again indicator combinations. The result is a quadratic in Z z i.
Goal
```
⊢ Z z i * (Z z i * y i + (1 - Z z i) * u i) + (1 - Z z i) * (Z z i * v i + (1 - Z z i) * y i) = y i
```
```
linear_combination (2 * y i - u i - v i) * Z_mul_self z i
```
Expand the quadratic and subtract y i: everything cancels except $(Z^{2} - Z) (2 y_{i} - u_{i} - v_{i})$ , and $Z^{2} = Z$ because an indicator is idempotent. Z_mul_self is that idempotence, and linear_combination c * h closes a goal L = R by checking with ring that L - R is exactly c times h’s own lhs - rhs. It is ring with a certificate, and much more robust than hunting for the right rewrite.

That is the dividend of writing the indicator as a real number rather than as an if: a fact that would need two branches becomes one polynomial identity.

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

Proposition. Suppose the data are in range. For every $λ \in [0, 1]$ ,

(1 - λ) τ_{L} + λ τ_{U} \in the identified set .

Proof.

Impute every missing treated outcome at $(1 - λ) a + λ b$ and every missing control outcome at $(1 - λ) b + λ a$ , and keep the observed values where they are observed. Call the resulting population $P_{λ}$ ; it is consistent with the data by the previous lemma.

It is also bounded. Both imputed values are convex combinations of $a$ and $b$ , and $[a, b]$ is convex, so they lie in $[a, b]$ ; the observed values do too, since the data are in range.

Finally, the average treatment effect is affine in the imputed outcomes. A treated unit of $P_{λ}$ contributes $y_{i} - ((1 - λ) b + λ a)$ , which is $(1 - λ) (y_{i} - b) + λ (y_{i} - a)$ : the same convex combination of the two extreme contributions. A control unit contributes $(1 - λ) (a - y_{i}) + λ (b - y_{i})$ for the same reason. Averaging, $τ (P_{λ}) = (1 - λ) τ_{L} + λ τ_{U}$ .∎

Those two facts — that $[a, b]$ is convex and that $τ$ is affine in the potential outcomes — are the reason identified sets in this subject are so often intervals rather than exotic sets.

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

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

refine ⟨imputePop z y (fun _ => (1 - lam) * a + lam * b) (fun _ => (1 - lam) * b + lam * a), imputePop_consistentWith z y _ _, ?_, ?_⟩

Membership in identifiedSet is an existential over populations with three components, so the proof supplies the witness $P_{λ}$ and the first component in one anonymous constructor: consistency is imputePop_consistentWith, already proved for every u and v. Two goals remain, exactly the last two paragraphs of the informal proof.

Goal

case refine_1
⊢ Bounded a b (imputePop z y (fun x => (1 - lam) * a + lam * b) fun x => (1 - lam) * b + lam * a)

case refine_2
⊢ (imputePop z y (fun x => (1 - lam) * a + lam * b) fun x => (1 - lam) * b + lam * a).tau =
    (1 - lam) * manskiLower z y a b + lam * manskiUpper z y a b

```
refine imputePop_bounded hy (fun i => ?_) (fun i => ?_)
```
imputePop_bounded reduces boundedness of the imputed population to three conditions: the data are in range (that is hy), and each of the two imputed vectors is in range. Both imputed vectors are constant, so the two remaining goals say the same thing at every unit — but a unit is still bound, which the next line needs. In the source a <;> · runs one shared script against both goals rather than repeating it.
Goal
```
⊢ a ≤ (1 - lam) * a + lam * b ∧ (1 - lam) * a + lam * b ≤ b
```
```
have hab : a ≤ b := le_trans (hy i).1 (hy i).2
```
Convexity needs a ≤ b, which the statement never assumed — and cannot, since at n = 0 there is nothing to derive it from. With a unit i in hand it comes from the data: a ≤ y i ≤ b.
```
constructor <;> linarith [mul_nonneg h0 (sub_nonneg.mpr hab), mul_nonneg (sub_nonneg.mpr h1) (sub_nonneg.mpr hab)]
```
constructor splits the conjunction into the two inequalities, and <;> applies the same closing tactic to both. The two hints handed to linarith are $λ (b - a) \geq 0$ and $(1 - λ) (b - a) \geq 0$ ; adding the first to a gives the lower bound and subtracting the second from b gives the upper one. That is convexity of $[a, b]$ , written as two linear facts.

rw [tau_imputePop]

The second goal. tau_imputePop computes the ATE of an imputed population unit by unit: a treated unit contributes y i - v i and a control unit u i - y i. The left-hand side is now a mean.

Goal

⊢ (mean fun i => Z z i * (y i - ((1 - lam) * b + lam * a)) + (1 - Z z i) * ((1 - lam) * a + lam * b - y i)) =
    (1 - lam) * manskiLower z y a b + lam * manskiUpper z y a b

```
rw [manskiLower, manskiUpper, ← mean_const_mul, ← mean_const_mul, ← mean_add]
```
Four rewrites that push the convex combination inside the mean on the right, so that both sides are means of explicit functions. manskiLower and manskiUpper unfold the two endpoints; mean_const_mul, used right-to-left twice, turns c * mean v into mean (fun i => c * v i); mean_add, also right-to-left, turns the sum of two means into the mean of the sum. Nothing has been proved yet — the goal is still an equation — but it is now an equation between two means.
Goal
```
⊢ (mean fun i => Z z i * (y i - ((1 - lam) * b + lam * a)) + (1 - Z z i) * ((1 - lam) * a + lam * b - y i)) =
    mean fun i =>
      (1 - lam) * (Z z i * (y i - b) + (1 - Z z i) * (a - y i)) + lam * (Z z i * (y i - a) + (1 - Z z i) * (b - y i))
```
```
exact mean_congr fun i => by ring
```
mean_congr says two vectors that agree entrywise have the same mean, which is how one rewrites underneath a fun i => … binder. At each unit the two summands differ by rearrangement only, so ring verifies them: this is the “averaging” step of the informal proof.

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

ExerciseSharpness (stretch)

Every point of the Manski interval is the ATE of some population that fits the data and respects the range — the inclusion an autoformalization tends to leave out.

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

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

Hint

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 (simpa cleans up). 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.

Show solution

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

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

Theorem (Manski). Suppose the observed outcomes lie in $[a, b]$ . Then the identified set of the average treatment effect is exactly the closed interval

[τ_{L}, τ_{U}] .

In words: under a bounded outcome and nothing else, the set of average treatment effects consistent with the observed data is precisely the interval whose endpoints impute every missing potential outcome at the worse, respectively better, end of the range.

Proof.

Two inclusions. Any consistent bounded population has its ATE in the interval, by the bracketing proposition. Conversely, any point $t$ of the interval is $(1 - λ) τ_{L} + λ τ_{U}$ for $λ = (t - τ_{L}) / (τ_{U} - τ_{L})$ when the interval is non-degenerate, and for $λ = 0$ when it is a single point; that $λ$ lies in $[0, 1]$ , so the mixing proposition exhibits a consistent bounded population with $τ = t$ .∎

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

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 fun _ => ⟨_, _⟩
```
No tactic block: the whole proof is a term. Set.ext is the extensionality principle for sets — two sets are equal when they have the same members — so it wants, for each real number t, an Iff between the two membership statements. The anonymous constructor ⟨_, _⟩ supplies that Iff as its two implications, which are the two inclusions of the informal proof.
```
fun ht => identifiedSet_subset_Icc z y a b ht
```
The forward implication, from the exercise above: any ATE in the identified set is bracketed. Note it needs no hypothesis on the data.
```
fun ht => mem_identifiedSet_of_mem_Icc hy ht
```
The reverse implication, from the sharpness exercise, and the only place hy is used: without in-range data the identified set can be empty while the interval is not.

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,094 lines of library preamble — the code above is at the bottom of the editor.

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)

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)

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

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

```
rw [identifiedSet_eq_Icc hy]
```
Both order-theoretic statements begin the same way: replace the identified set by the interval it equals. After this rewrite nothing about populations survives, and the goal is a fact about Set.Icc.
```
exact isLeast_Icc (manskiLower_le_manskiUpper hy)
```
isLeast_Icc is Mathlib’s statement that the left endpoint of a non-empty closed interval is its least element. Its one hypothesis is non-emptiness, manskiLower ≤ manskiUpper, which is the exercise at the end of the chapter. isGreatest_identifiedSet is the same two lines with isGreatest_Icc.
```
(isLeast_identifiedSet hy).csInf_eq
```
IsLeast.csInf_eq converts “least element” into “conditional infimum”: if x is the least element of S then sInf S = x. csSup_identifiedSet is the mirror image through IsGreatest.csSup_eq. Both are one term, because the work was done by the theorem above.

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

Proposition. For every assignment, every data vector and every $n \geq 1$ ,

τ_{U} - τ_{L} = b - a .

Proof.

Compare the two endpoints unit by unit. A treated unit contributes $(y_{i} - a) - (y_{i} - b) = b - a$ ; a control unit contributes $(b - y_{i}) - (a - y_{i}) = b - a$ . The contribution is the same in both arms, so the difference of the two averages is the average of the constant $b - a$ , which is $b - a$ .∎

The proof used neither the data nor the assignment, and that is the content of the result: every unit is missing exactly one number, and the arm it landed in changes which endpoint imputes which, not how much is unknown. A textbook would not state the hypothesis $n \geq 1$ at all — with no units there is no average to speak of. Lean has to, because it defines $0 / 0 = 0$ : at $n = 0$ both endpoints are $0$ and their difference is $0$ , not $b - a$ .

ExerciseThe width fact (core)

The width of the worst-case interval is exactly b - a: it does not depend on the data, on the assignment, or on n. 0 < n is the only hypothesis; in particular the identity holds whether or not the data are in range.

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

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

Hint

Unfold manskiUpper and manskiLower, then ← mean_sub turns the difference of two means into the mean of the pointwise difference; mean_congr fun i => by ring 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, which is the only place 0 < n enters.

Show solution

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

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]

Three consequences:

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.

Proposition. If the observed outcomes lie in $[a, b]$ then $0$ belongs to the identified set. Worst-case bounds can never sign an effect.

Proof.

Impute each unit’s missing outcome to equal its observed one. The resulting population is consistent with the data, its outcomes all lie in $[a, b]$ because the data do, and every unit has zero effect, so $τ = 0$ .

Equivalently, and this is the route the formal proof takes: each summand of $τ_{L}$ is $- Z_{i} (b - y_{i}) - (1 - Z_{i}) (y_{i} - a)$ , and both of those products are non-negative when the data are in range, so $τ_{L} \leq 0$ . Symmetrically $τ_{U} \geq 0$ . So $0$ lies in $[τ_{L}, τ_{U}]$ , which by the theorem is the identified set.∎

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

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⟩

```
rw [identifiedSet_eq_Icc hy]
```
Trade the identified set for the interval. This is what makes the short route available: with the sharpness theorem in hand, exhibiting a population is no longer necessary — membership in the interval suffices.
Goal
```
⊢ 0 ∈ Set.Icc (manskiLower z y a b) (manskiUpper z y a b)
```
```
exact ⟨manskiLower_nonpos hy, manskiUpper_nonneg hy⟩
```
Membership in Set.Icc unfolds definitionally to a pair of inequalities, so the anonymous constructor takes the two one-sided facts directly. manskiLower_nonpos and manskiUpper_nonneg are each proved by comparing the endpoint with the mean of the zero vector, one mean_le_mean and two mul_nonnegs apiece.

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,322 lines of library preamble — the code above is at the bottom of the editor.

def yEx : Fin 4 → ℝ := ![1, 1, 0, 0]

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

@[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)

theorem inRange_yEx : InRange 0 1 yEx := by
  intro i
  fin_cases i <;> simp

```
@[simp] theorem yEx_zero : yEx 0 = 1 := rfl
```
Four of these. yEx is a Matrix.of-style literal ![1, 1, 0, 0], and evaluating it at a numeral is definitional, so each entry is rfl. Marking them @[simp] puts the data into the simp set, which is what makes the arithmetic below one word.
```
@[simp] theorem Z_zEx_zero : Z zEx 0 = 1 := Z_of_mem (by decide)
```
Four more, and these are not rfl: Z is defined by a case split on membership, so each value needs a membership proof. Z_of_mem turns i ∈ z into Z z i = 1 and Z_of_not_mem turns i ∉ z into Z z i = 0; membership in a literal Finset (Fin 4) is decidable, so by decide supplies the proof by evaluation.
```
intro i
```
InRange 0 1 yEx is a ∀ i, so the proof of inRange_yEx opens by taking an arbitrary unit.
Goal
```
i : Fin 4
⊢ 0 ≤ yEx i ∧ yEx i ≤ 1
```

fin_cases i <;> simp

fin_cases replaces the arbitrary i : Fin 4 by its four possible values, leaving four concrete goals; <;> simp then discharges each with the eight @[simp] facts above. The range check is arithmetic on numerals, which is why nothing cleverer is needed.

Goal

case «0»
⊢ 0 ≤ yEx ((fun i => i) ⟨0, ⋯⟩) ∧ yEx ((fun i => i) ⟨0, ⋯⟩) ≤ 1

case «1»
⊢ 0 ≤ yEx ((fun i => i) ⟨1, ⋯⟩) ∧ yEx ((fun i => i) ⟨1, ⋯⟩) ≤ 1

case «2»
⊢ 0 ≤ yEx ((fun i => i) ⟨2, ⋯⟩) ∧ yEx ((fun i => i) ⟨2, ⋯⟩) ≤ 1

case «3»
⊢ 0 ≤ yEx ((fun i => i) ⟨3, ⋯⟩) ∧ yEx ((fun i => i) ⟨3, ⋯⟩) ≤ 1

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,341 lines of library preamble — the code above is at the bottom of the editor.

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

The proof is a single rw chain, and the chain is the hand computation: $(1 + 1) / 2 - (0 + 0) / 2 = 1$ .

```
rw [DiM_eq_observed]
```
DiM is defined on a population; DiM_eq_observed rewrites it as the difference of two averages of the observed vector, which is the form in which consistency can be used. This is the step that makes the estimate depend on the data alone.
Goal
```
⊢ (∑ i ∈ zEx, Yobs P zEx i) / ↑(#zEx) - (∑ i ∈ zExᶜ, Yobs P zEx i) / ↑(#zExᶜ) = 1
```
```
rw [Finset.sum_congr rfl fun i _ => hP.apply i, Finset.sum_congr rfl fun i _ => hP.apply i]
```
Finset.sum_congr rewrites a sum termwise: with the same index set (rfl) and hP.apply i : Yobs P zEx i = yEx i at each term, both sums become sums of the data. It appears twice because there are two sums, the treated and the control. This is where “the estimator only touches what the assignment revealed” becomes a formal step.
Goal
```
⊢ Finset.sum zEx yEx / ↑(#zEx) - zExᶜ.sum yEx / ↑(#zExᶜ) = 1
```
```
rw [show zExᶜ = ({2, 3} : Finset (Fin 4)) from by decide, show zEx = ({0, 1} : Finset (Fin 4)) from rfl]
```
Two show … from … terms supply small facts inline: the complement of the treated set is {2, 3} (a computation, hence decide), and zEx is {0, 1} (a definition, hence rfl). Both index sets are now literals.
Goal
```
⊢ {0, 1}.sum yEx / ↑(#{0, 1}) - {2, 3}.sum yEx / ↑(#{2, 3}) = 1
```
```
rw [Finset.sum_insert (by decide), Finset.sum_singleton, Finset.sum_insert (by decide), Finset.sum_singleton]
```
Expand the sums. Finset.sum_insert peels the first element off {0, 1} — its side condition, that 0 ∉ {1}, is by decide — and Finset.sum_singleton finishes the remaining one-element sum. Twice, once per group.
Goal
```
⊢ (yEx 0 + yEx 1) / ↑(#{0, 1}) - (yEx 2 + yEx 3) / ↑(#{2, 3}) = 1
```

rw [Finset.card_insert_of_notMem (by decide), Finset.card_singleton, Finset.card_insert_of_notMem (by decide), Finset.card_singleton]

The same peeling for the two denominators: card_insert_of_notMem gives #{0, 1} = #{1} + 1 and card_singleton gives #{1} = 1.

Goal

⊢ (yEx 0 + yEx 1) / ↑(1 + 1) - (yEx 2 + yEx 3) / ↑(1 + 1) = 1

```
norm_num
```
What is left is $(1 + 1) / 2 - (0 + 0) / 2 = 1$ over the reals, with the four data values supplied by the @[simp] lemmas of the previous snippet. norm_num evaluates it.

And the bounds:

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

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

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

theorem identifiedSet_data : identifiedSet zEx yEx 0 1 = Set.Icc 0 1 := by
  rw [identifiedSet_eq_Icc inRange_yEx, manskiLower_data, manskiUpper_data]

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⟩

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]

One pass that leaves nothing symbolic. manskiLower and mean unfold the definition to a sum over Fin 4 divided by 4; Fin.sum_univ_four writes that sum out as four explicit terms; and the eight data lemmas replace every indicator and every outcome by a numeral. What remains is arithmetic.

Goal

⊢ (1 * (1 - 1) + (1 - 1) * (0 - 1) + (1 * (1 - 1) + (1 - 1) * (0 - 1)) + (0 * (0 - 1) + (1 - 0) * (0 - 0)) +
        (0 * (0 - 1) + (1 - 0) * (0 - 0))) /
      ↑4 =
    0

```
norm_num
```
Each treated unit contributes $1 \cdot (1 - 1) = 0$ and each control unit $1 \cdot (0 - 0) = 0$ , so the lower endpoint is $0 / 4 = 0$ . manskiUpper_data is the same two lines: there the treated units contribute $1 - 0 = 1$ and the control units $1 - 0 = 1$ , giving $4 / 4 = 1$ .
```
rw [identifiedSet_eq_Icc inRange_yEx, manskiLower_data, manskiUpper_data]
```
identifiedSet_data needs no work of its own: the sharpness theorem turns the identified set into an interval, and the two computations above name its endpoints. The result is Set.Icc 0 1, and rw closes the goal by reflexivity.
```
rw [identifiedSet_data]
exact Set.mem_Icc.mpr ⟨le_refl 0, by norm_num⟩
```
And 0 ∈ Set.Icc 0 1 is 0 ≤ 0 — le_refl — together with 0 ≤ 1, which norm_num supplies. The point is not the arithmetic but that the same identifiedSet appears in the statement about this data set and in the general theorem.

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,133 lines of library preamble — the code above is at the bottom of the editor.

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)

Under MTR the ATE is non-negative: an average of non-negative numbers is non-negative.

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

theorem tau_nonneg_of_MTR {P : Population n} (h : MTR P) : 0 ≤ P.tau := by
  sorry

Hint

Say it through mean_le_mean against the zero vector rather than by hand, so that the n = 0 case takes care of itself: 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 simpa [Population.effect]. Finish with simpa [mean] to evaluate mean (fun _ => 0).

Show solution

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

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.

Theorem. Suppose the observed outcomes lie in $[a, b]$ . Then the identified set of the average treatment effect under boundedness and monotone treatment response is exactly $[0, τ_{U}]$ .

Proof.

For the inclusion, a population satisfying MTR has every effect non-negative, so $τ \geq 0$ ; and it is still consistent and bounded, so $τ \leq τ_{U}$ by the bracketing proposition.

For sharpness, take $t \in [0, τ_{U}]$ and write $t = λ τ_{U}$ with $λ = t / τ_{U} \in [0, 1]$ ; if $τ_{U} = 0$ then $t = 0$ and $λ = 0$ serves. Now sweep between “no effect at all” and the worst-case upper bound: impute a control unit’s missing treated outcome at $(1 - λ) y_{i} + λ b$ and a treated unit’s missing control outcome at $(1 - λ) y_{i} + λ a$ . Each imputed value is a convex combination of the observed $y_{i}$ with an endpoint of $[a, b]$ , hence in $[a, b]$ . Each unit’s effect is $λ (y_{i} - a) \geq 0$ if treated and $λ (b - y_{i}) \geq 0$ if control, so MTR holds; and averaging those effects gives exactly $λ τ_{U} = t$ . At $λ = 0$ every unit has a zero effect; at $λ = 1$ the worst-case population is recovered.∎

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

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⟩
    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 Lean repeats the pattern of the Manski proof, which is the point of showing it twice; only the family being swept has changed.

```
refine Set.ext fun t => ⟨?_, ?_⟩
```
Sharpness again, so extensionality again: the goal becomes two implications at an arbitrary t.
```
rintro ⟨P, hcon, hb, hmtr, rfl⟩
```
The easy inclusion. rintro destructures membership in mtrIdentifiedSet — which is a five-fold existential — in one move, and the final rfl substitutes P.tau for t throughout, which is why the goal below mentions P.tau and not t.
Goal
```
P : Population n
hcon : ConsistentWith z y P
hb : Bounded a b P
hmtr : MTR P
⊢ P.tau ∈ Set.Icc 0 (manskiUpper z y a b)
```
```
exact ⟨tau_nonneg_of_MTR hmtr, tau_le_manskiUpper hcon hb⟩
```
Membership in Set.Icc is a pair of inequalities, and the two components are exactly the two sentences of the informal proof: MTR gives 0 ≤ P.tau, and the bracketing proposition gives the upper half.
```
obtain ⟨lam, h0, h1, hlam⟩ :
    ∃ lam : ℝ, 0 ≤ lam ∧ lam ≤ 1 ∧ lam * manskiUpper z y a b = t
```
The mixing weight, produced before the population that uses it. Inside, a case split rcases eq_or_lt_of_le (manskiUpper_nonneg hy) on whether the upper endpoint is zero: if it is, t = 0 is forced and lam = 0 works; otherwise lam = t / manskiUpper …, with div_nonneg and div_le_one for the two bounds and field_simp for the product. The degenerate branch exists solely because dividing by manskiUpper needs it to be non-zero.

refine ⟨imputePop z y (fun i => (1 - lam) * y i + lam * b) (fun i => (1 - lam) * y i + lam * a), imputePop_consistentWith z y _ _, ?_, ?_, ?_⟩

The witness, with consistency discharged as before. Note the imputed values now depend on i — they mix the observed outcome with an endpoint, rather than mixing the two endpoints as in the Manski proof. That is the whole difference between the two constructions. Three goals remain: bounded, MTR, and the value of the ATE.

Goal

case refine_2.refine_1
⊢ Bounded a b (imputePop z y (fun i => (1 - lam) * y i + lam * b) fun i => (1 - lam) * y i + lam * a)

case refine_2.refine_2
⊢ MTR (imputePop z y (fun i => (1 - lam) * y i + lam * b) fun i => (1 - lam) * y i + lam * a)

case refine_2.refine_3
⊢ (imputePop z y (fun i => (1 - lam) * y i + lam * b) fun i => (1 - lam) * y i + lam * a).tau = t

```
refine imputePop_bounded hy (fun i => ?_) (fun i => ?_)
```
Boundedness, reduced as before to the two imputed vectors being in range. The three mul_nonneg hypotheses hb1, hb2, hb3 that follow are $λ (b - a) \geq 0$ , $(1 - λ) (y_{i} - a) \geq 0$ and $(1 - λ) (b - y_{i}) \geq 0$ , and constructor <;> linarith assembles each of the four bounds from them.
```
simp only [imputePop_y1, imputePop_y0, Z_of_mem hi]
```
The MTR goal, treated branch, after intro i and by_cases hi : i ∈ z. Unfolding the two potential outcomes and resolving the indicator to 1 leaves an inequality between the imputed control outcome and the observed one.
Goal
```
hi : i ∈ z
⊢ 1 * ((1 - lam) * y i + lam * a) + (1 - 1) * y i ≤ 1 * y i + (1 - 1) * ((1 - lam) * y i + lam * b)
```
```
linarith [mul_nonneg h0 (sub_nonneg.mpr hy1)]
```
The hint is $λ (y_{i} - a) \geq 0$ , which is exactly the effect of the treated unit under this imputation; the control branch uses $λ (b - y_{i}) \geq 0$ in the same way. Non-negative effects at every unit is what MTR asks for.
```
rw [tau_imputePop, ← hlam, manskiUpper, ← mean_const_mul]
```
The last goal. tau_imputePop computes the ATE unit by unit; ← hlam replaces the target t by lam * manskiUpper …, which is the form that can be matched; manskiUpper unfolds that endpoint into a mean; and mean_const_mul right-to-left pushes the scalar lam inside it.
Goal
```
⊢ (mean fun i => Z z i * (y i - ((1 - lam) * y i + lam * a)) + (1 - Z z i) * ((1 - lam) * y i + lam * b - y i)) =
    mean fun i => lam * (Z z i * (y i - a) + (1 - Z z i) * (b - y i))
```
```
exact mean_congr fun i => by ring
```
Both sides are now means of explicit functions that agree at each unit, and ring checks the pointwise identity: the effect of unit i under the swept imputation is lam times its worst-case contribution.

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,203 lines of library preamble — the code above is at the bottom of the editor.

noncomputable def manskiLowerHat (P : Population n) (a b : ℝ) (z : Assignment n) : ℝ :=
  manskiLower z (Yobs P z) a b

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,209 lines of library preamble — the code above is at the bottom of the editor.

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.

```
⟨manskiLower_le_tau rfl hb, tau_le_manskiUpper rfl hb⟩
```
A term, not a tactic block, and the whole content is in the two rfls. The bracketing proposition wants a population consistent with the data; here the data are Yobs P z, the outcomes this very population produced under this very assignment, so consistency is the equality Yobs P z = Yobs P z and holds by reflexivity. The two components of the anonymous constructor are the two halves of the conjunction, and hb is the same boundedness assumption in both.

Taking expectations is then monotonicity and nothing else:

ExerciseBounds in expectation (core)

Under any design, the expectation of the estimated lower bound is still a lower bound on P.tau.

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

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

Hint

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.

Show solution

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

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.

Proposition. Let $D$ be any design and $n \geq 1$ . Then

E [{\hat{τ}}_{U}] - E [{\hat{τ}}_{L}] = b - a .

Proof.

By linearity, the left-hand side is $E [{\hat{τ}}_{U} - {\hat{τ}}_{L}]$ . For every assignment $z$ the width identity above gives ${\hat{τ}}_{U} (z) - {\hat{τ}}_{L} (z) = b - a$ , so the random variable inside the expectation is the constant $b - a$ , whose expectation is $b - a$ .∎

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

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 _

```
rw [← D.expect_sub]
```
Design.expect_sub states $E [f - g] = E [f] - E [g]$ ; used right-to-left it collects the two expectations into one. Linearity, and the only property of the design the proof uses.
Goal
```
⊢ (D.expect fun z => manskiUpperHat P a b z - manskiLowerHat P a b z) = b - a
```
```
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
```
Design.expect_congr replaces the statistic inside an expectation by any statistic equal to it pointwise. The pointwise equality supplied here is the width identity, instantiated at each assignment z and at the data Yobs P z that assignment produced. After this rewrite the integrand is a constant, and the design has vanished from the goal.
Goal
```
⊢ (D.expect fun x => b - a) = b - a
```
```
exact D.expect_const _
```
The expectation of a constant is that constant — because the design’s probabilities sum to one, which is the one axiom a Design carries.

D : Design n is universally quantified, and the only hypothesis is 0 < n — the same one every statement about a mean carries, since at $n = 0$ both estimated bounds are Lean’s $0 / 0 = 0$ . 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,234 lines of library preamble — the code above is at the bottom of the editor.

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⟩

```
rw [DiM_unbiased_completeRandomization hle P hpos hlt]
```
Unbiasedness, from chapter 8: under complete randomization with $0 < n_{1} < n$ the expectation of the difference in means is $τ$ . Rewriting with it replaces the estimator’s expectation in the goal by $τ$ itself, so what is left to show is that $τ$ lies between the two expected bounds.
```
exact ⟨expect_manskiLowerHat_le _ hb, le_expect_manskiUpperHat _ hb⟩
```
Which is the exercise above and its mirror image, as the two components of a Set.Icc membership. Two theorems from two different chapters meeting in one anonymous constructor is the whole point of the statement.

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,252 lines of library preamble — the code above is at the bottom of the editor.

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)

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.

Proposition. Let $R$ be the set of responders, and suppose $y$ agrees with the population’s observed outcome on $R$ (off $R$ it may be anything). If every potential outcome lies in $[a, b]$ then the responder-only bounds bracket $τ$ .

Proof.

Unit by unit again, and now four cases.

If $i$ responds and was treated, then $y_{i} = y_{1 i}$ and $y_{0 i} \leq b$ , so its effect is at least $y_{i} - b$ , the summand the definition assigns it. If $i$ responds and was a control, $y_{i} = y_{0 i}$ and $a \leq y_{1 i}$ , so its effect is at least $a - y_{i}$ , again the assigned summand.

If $i$ does not respond, neither of its potential outcomes is observed, and all that is known is $a \leq y_{1 i} \leq b$ and $a \leq y_{0 i} \leq b$ ; so its effect is at least $a - b$ , which is what the definition assigns to a non-responder — and this is the only place the crude interval $[a - b, b - a]$ appears. Averaging gives the lower bound; the upper one is the mirror image.∎

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

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

```
constructor
```
The conclusion is a conjunction of the two bracketing inequalities, so the proof splits into two halves at once. Everything below is the first half; the second is the same thirteen lines with the other two components of hb.
```
rw [attritionLower, Population.tau]
refine mean_le_mean fun i => ?_
```
The same opening as the Manski bracket: unfold both sides to means, then use monotonicity of the mean to reduce to one arbitrary unit. After obtain ⟨h1, _, _, h4⟩ := hb i and simp only [Population.effect] the goal compares the unit’s assigned summand with P.y1 i - P.y0 i.
Goal
```
⊢ Z R i * (Z z i * (y i - b) + (1 - Z z i) * (a - y i)) + (1 - Z R i) * (a - b) ≤ P.y1 i - P.y0 i
```
```
by_cases hiR : i ∈ R
```
The outer split, and the one the Manski proof did not need: did this unit respond? Note that it comes first. A non-responder’s summand does not look at the treatment indicator at all, so there is nothing to split further.
```
rw [Z_of_mem hiR]
```
The responder branch. Resolving the response indicator to 1 kills the (1 - Z R i) * (a - b) term and leaves precisely the Manski summand, which is the formal statement of “responders contribute exactly what they would have contributed with no attrition”.
Goal
```
hiR : i ∈ R
⊢ 1 * (Z z i * (y i - b) + (1 - Z z i) * (a - y i)) + (1 - 1) * (a - b) ≤ P.y1 i - P.y0 i
```
```
rw [Z_of_mem hi, ← hr i hiR, Yobs_of_mem hi]
```
Responder, treated. Three rewrites: the treatment indicator becomes 1; then ← hr i hiR replaces the observed number y i by Yobs P z i — note the direction, away from the data and back to the population, because the hypothesis only holds on R; and Yobs_of_mem hi evaluates that to P.y1 i. Now everything is in the population’s own vocabulary and linarith closes it from h4 : P.y0 i ≤ b.
Goal
```
hi : i ∈ z
⊢ 1 * (1 * (P.y1 i - b) + (1 - 1) * (a - P.y1 i)) + (1 - 1) * (a - b) ≤ P.y1 i - P.y0 i
```

rw [Z_of_not_mem hi, ← hr i hiR, Yobs_of_not_mem hi]

Responder, control. The same three moves with the indicator resolving to 0 and Yobs_of_not_mem giving P.y0 i; the closing linarith uses h1 : a ≤ P.y1 i.

Goal

hi : i ∉ z
⊢ 1 * (0 * (P.y0 i - b) + (1 - 0) * (a - P.y0 i)) + (1 - 1) * (a - b) ≤ P.y1 i - P.y0 i

```
rw [Z_of_not_mem hiR]
```
The non-responder branch, and no treatment split. The Manski part of the summand is multiplied by 0 and disappears; what is left is a - b, and linarith gets a - b ≤ P.y1 i - P.y0 i from h1 : a ≤ P.y1 i and h4 : P.y0 i ≤ b. The data vector y is never touched, which is exactly why the hypothesis could be weakened to R.
Goal
```
hiR : i ∉ R
⊢ 0 * (Z z i * (y i - b) + (1 - Z z i) * (a - y i)) + (1 - 0) * (a - b) ≤ P.y1 i - P.y0 i
```

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: with Finset.univ as the response set — everybody answers — the attrition bounds are the Manski bounds.

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

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

Hint

Work one unit at a time with refine mean_congr fun i => ?_; then Z_of_mem (Finset.mem_univ i) rewrites Z univ i to 1, and ring finishes the summand.

Show solution

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

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)

The mean is homogeneous: mean (fun i => c * v i) = c * mean v. Needed twice in mix_mem_identifiedSet, in the ← direction, to push a convex combination inside a mean.

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

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

Hint

Finset.mul_sum moves the constant into the sum (used right-to-left) and mul_div_assoc moves the division out; one simp only with both, plus mean, does it.

Show solution

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

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)

The lower bound really is below the upper bound whenever the data are in range. (The theorem needs InRange rather than a bare a ≤ b: with no units there is nothing to derive a ≤ b from.)

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

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

Hint

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 => ….

Show solution

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

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

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

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

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 ℝ`