PO.ID.Exact.Multiple­Instrument­IV

Z :

Ω → Fin K

k :

Fin K

def

supportMass μ Z k :

ℝ

given by

(μ {ω | Z ω = k}).toReal

Causalean.PO.ID.Exact.MultipleInstrumentIV.supportMass · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:77

def fromMeasureScore reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex

Given a measurable sample space, a finite support of size $K$ , a probability measure, a measurable instrument with that support, a real first-stage score at each support point, and the condition that this score is weakly increasing in support order, the ordered finite first-stage index has support masses equal to the instrument probabilities and the supplied score.

Definition (Lean source)

parameters

Ω :

Type*

MeasurableSpace Ω

K :

ℕ

μ :

IsProbabilityMeasure μ

Z :

Ω → Fin K

hZ :

Measurable Z

dhat :

Fin K → ℝ

hdhat_mono :

∀ {k l : Fin K}

k.val ≤ l.val

then

dhat k ≤ dhat l

def

fromMeasureScore μ Z hZ dhat hdhat_mono :

given by

clause 1

rho := supportMass μ Z

clause 2

dhat := dhat

clause 3

rho_nonneg := supportMass_nonneg μ Z

clause 4

rho_sum_one := supportMass_sum_eq_one μ Z hZ

clause 5

dhat_mono := hdhat_mono

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex.fromMeasureScore · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:115 · uses FiniteIndex

def meanIndex reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex

For an ordered finite first-stage index, the mean first-stage index is the support-mass-weighted average $\sum_k \rho_k\widehat d_k$ .

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

def

meanIndex I :

ℝ

given by

∑ k, I.rho k * I.dhat k

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex.meanIndex · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:136 · uses FiniteIndex

def centeredIndex reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex

For an ordered finite first-stage index and a support point, the centered first-stage index at that point is its first-stage score minus the support-mass-weighted mean score.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

k :

Fin K

def

centeredIndex I k :

ℝ

given by

I.dhat k - I.meanIndex

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex.centeredIndex · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:141 · uses FiniteIndex

def upperTail reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex

For a finite ordered support of size $K$ and an adjacent threshold, the upper-tail set contains exactly the support points at or above that threshold.

Definition (Lean source)

parameters

K :

ℕ

shared

j :

Adj K

def

upperTail j :

Finset (Fin K)

given by

Finset.univ.filter fun k => j.1.val ≤ k.val

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex.upperTail · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:147 · uses Adj

def tailCoeff reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex

For an ordered finite first-stage index and an adjacent threshold, the MTW tail coefficient is the sum, over the corresponding upper tail, of each support mass times its centered first-stage index.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

j :

Adj K

def

tailCoeff I j :

ℝ

given by

∑ k ∈ upperTail j, I.rho k * I.centeredIndex k

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex.tailCoeff · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:152 · uses Adj , FiniteIndex

theorem tailCoeff_nonneg reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex

For an adjacent threshold j with the support ordered by the first-stage index, the MTW tail coefficient B_j is nonnegative (def:po-estimand-mtw-tail-coefficients).

Formal statement

hypotheses

K :

ℕ

shared

I :

shared

j :

Adj K

conclusion

0 ≤ I.tailCoeff j

Proof (Lean source)

theorem tailCoeff_nonneg (j : Adj K) : 0 ≤ I.tailCoeff j := by classical let T := upperTail j let L : Finset (Fin K) := Finset.univ.filter fun l => l.val < j.1.val let A : ℝ := ∑ k ∈ T, I.rho k let B : ℝ := ∑ l ∈ L, I.rho l let ST : ℝ := ∑ k ∈ T, I.rho k * I.dhat k let SL : ℝ := ∑ l ∈ L, I.rho l * I.dhat l have hmass : B + A = 1 := by have h := Finset.sum_filter_not_add_sum_filter (s := univ) (p := fun k : Fin K => j.1.val ≤ k.val) (f := I.rho) simpa [A, B, T, L, upperTail, Nat.not_le] using h.trans I.rho_sum_one have hmean : I.meanIndex = SL + ST := by have h := Finset.sum_filter_not_add_sum_filter (s := univ) (p := fun k : Fin K => j.1.val ≤ k.val) (f := fun k => I.rho k * I.dhat k) simpa [ST, SL, T, L, upperTail, meanIndex, Nat.not_le] using h.symm have htail_basic : I.tailCoeff j = ST - A * I.meanIndex := by calc I.tailCoeff j = ∑ k ∈ T, (I.rho k * I.dhat k - I.rho k * I.meanIndex) := by simp [tailCoeff, centeredIndex, T, upperTail, mul_sub] _ = ST - ∑ k ∈ T, I.rho k * I.meanIndex := by rw [Finset.sum_sub_distrib] _ = ST - I.meanIndex * A := by simp [A, ST, Finset.mul_sum, mul_comm] _ = ST - A * I.meanIndex := by rw [mul_comm I.meanIndex A] have htail : I.tailCoeff j = B * ST - A * SL := by rw [htail_basic, hmean] have hB : B = 1 - A := by linarith rw [hB] ring have hfirst : (∑ k ∈ T, ∑ l ∈ L, I.rho k * I.rho l * I.dhat k) = B * ST := by simp [B, ST, Finset.mul_sum, mul_assoc, mul_comm, mul_left_comm] have hsecond : (∑ k ∈ T, ∑ l ∈ L, I.rho k * I.rho l * I.dhat l) = A * SL := by rw [Finset.sum_comm] simp [A, SL, Finset.mul_sum, Finset.sum_mul, mul_assoc, mul_comm, mul_left_comm] have hdouble : (∑ k ∈ T, ∑ l ∈ L, I.rho k * I.rho l * (I.dhat k - I.dhat l)) = B * ST - A * SL := by calc (∑ k ∈ T, ∑ l ∈ L, I.rho k * I.rho l * (I.dhat k - I.dhat l)) = (∑ k ∈ T, ∑ l ∈ L, I.rho k * I.rho l * I.dhat k) - (∑ k ∈ T, ∑ l ∈ L, I.rho k * I.rho l * I.dhat l) := by simp [mul_sub, Finset.sum_sub_distrib] _ = B * ST - A * SL := by rw [hfirst, hsecond] rw [htail, ← hdouble] apply Finset.sum_nonneg intro k hk apply Finset.sum_nonneg intro l hl have hkT : j.1.val ≤ k.val := by simpa [T, upperTail] using hk have hlL : l.val < j.1.val := by simpa [L] using hl have hle : l.val ≤ k.val := by omega have hdhat : 0 ≤ I.dhat k - I.dhat l := sub_nonneg.mpr (I.dhat_mono hle) exact mul_nonneg (mul_nonneg (I.rho_nonneg k) (I.rho_nonneg l)) hdhat

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex.tailCoeff_nonneg · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:175 · uses Adj , FiniteIndex , tailCoeff

theorem tailCoeff_eq_cov reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex

Covariance identity. For an adjacent threshold j, the MTW tail coefficient B_j equals the finite-support covariance between the first-stage index dhat(Z) and the upper-tail indicator 1_{Z ∈ T_j} under the instrument distribution ρ.

Formal statement

hypotheses

K :

ℕ

shared

I :

shared

j :

Adj K

conclusion

I.tailCoeff j

= ∑ k : Fin K, I.rho k * (I.dhat k - I.meanIndex) * ((if k ∈ upperTail j then (1 : ℝ) else 0) - ∑ l : Fin K, I.rho l * (if l ∈ upperTail j then (1 : ℝ) else 0))

Proof (Lean source)

theorem tailCoeff_eq_cov (j : Adj K) : I.tailCoeff j = ∑ k : Fin K, I.rho k * (I.dhat k - I.meanIndex) * ((if k ∈ upperTail j then (1 : ℝ) else 0) - ∑ l : Fin K, I.rho l * (if l ∈ upperTail j then (1 : ℝ) else 0)) := by -- The subtracted cross-term is (Σ_k ρ_k centeredIndex_k) * (Σ_l ρ_l ind_l) = 0. have hcross : ∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ l : Fin K, I.rho l * (if l ∈ upperTail j then (1 : ℝ) else 0)) = 0 := by have : (∑ k : Fin K, I.rho k * I.centeredIndex k) * (∑ l : Fin K, I.rho l * (if l ∈ upperTail j then (1 : ℝ) else 0)) = 0 := by rw [I.centered_weight_sum_zero]; ring calc ∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ l : Fin K, I.rho l * (if l ∈ upperTail j then (1 : ℝ) else 0)) = (∑ k : Fin K, I.rho k * I.centeredIndex k) * (∑ l : Fin K, I.rho l * (if l ∈ upperTail j then (1 : ℝ) else 0)) := by rw [Finset.sum_mul] _ = 0 := this -- Rewrite the whole RHS directly and cancel cross-term. -- Let C := Σ_l ρ_l * ind_l (a constant w.r.t. k). -- RHS = Σ_k ρ_k*(dhat_k - mean)*(ind_k - C) -- = Σ_k ρ_k*centeredIndex_k*ind_k - C * Σ_k ρ_k*centeredIndex_k -- = Σ_k ρ_k*centeredIndex_k*ind_k - C * 0 -- = Σ_{k∈T_j} ρ_k*centeredIndex_k = tailCoeff j. have key : ∑ k : Fin K, I.rho k * (I.dhat k - I.meanIndex) * ((if k ∈ upperTail j then (1 : ℝ) else 0) - ∑ l : Fin K, I.rho l * (if l ∈ upperTail j then (1 : ℝ) else 0)) = ∑ k : Fin K, I.rho k * I.centeredIndex k * (if k ∈ upperTail j then (1 : ℝ) else 0) := by -- unfold centeredIndex so ring can see everything simp only [centeredIndex] have hcross2 : (∑ k : Fin K, I.rho k * (I.dhat k - I.meanIndex)) * (∑ l : Fin K, I.rho l * (if l ∈ upperTail j then (1 : ℝ) else 0)) = 0 := by have : ∑ k : Fin K, I.rho k * (I.dhat k - I.meanIndex) = 0 := by have := I.centered_weight_sum_zero simp only [centeredIndex] at this; exact this rw [this]; ring calc ∑ k : Fin K, I.rho k * (I.dhat k - I.meanIndex) * ((if k ∈ upperTail j then (1 : ℝ) else 0) - ∑ l, I.rho l * (if l ∈ upperTail j then 1 else 0)) = (∑ k : Fin K, I.rho k * (I.dhat k - I.meanIndex) * (if k ∈ upperTail j then (1 : ℝ) else 0)) - (∑ k : Fin K, I.rho k * (I.dhat k - I.meanIndex)) * (∑ l : Fin K, I.rho l * (if l ∈ upperTail j then (1 : ℝ) else 0)) := by rw [Finset.sum_mul, ← Finset.sum_sub_distrib] congr 1; ext k; ring _ = ∑ k : Fin K, I.rho k * (I.dhat k - I.meanIndex) * (if k ∈ upperTail j then (1 : ℝ) else 0) := by rw [hcross2, sub_zero] rw [key] -- Now: Σ_k ρ_k*centeredIndex_k*indicator(k∈T_j) = Σ_{k∈T_j} ρ_k*centeredIndex_k = tailCoeff j simp only [tailCoeff, upperTail, Finset.sum_filter] apply Finset.sum_congr rfl intro k _hk simp only [mem_filter, Finset.mem_univ, true_and] split_ifs <;> ring

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex.tailCoeff_eq_cov · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:278 · uses Adj , FiniteIndex , meanIndex , tailCoeff , upperTail

def firstStageGram reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV

Given a finite instrument support of size $K$ , a score-vector dimension $L$ , a real mass assigned to each support point, and a real score vector at each support point, the first-stage Gram matrix has entry $(a,b)$ equal to the mass-weighted sum of the products of score coordinates $a$ and $b$ .

Definition (Lean source)

parameters

K L :

ℕ

rho :

Fin K → ℝ

score :

Fin K → Fin L → ℝ

def

firstStageGram rho score :

Matrix (Fin L) (Fin L) ℝ

given by

fun a b => ∑ k : Fin K, rho k * score k a * score k b

Causalean.PO.ID.Exact.MultipleInstrumentIV.firstStageGram · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:361

structure MatrixFirstStage reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV

Finite-support matrix first stage for the source population-2SLS definition. The score vector q, support masses rho, reduced-form first-stage moments firstStageMoment, and invertible Gram matrix determine the projection coefficient by the displayed matrix inverse. The resulting fitted values are required to be in the displayed weakly increasing order so they can feed the MTW tail-coefficient algebra.

Definition (Lean source)

parameters

K L :

ℕ

fields

Instrument support mass `ρ_k`.

rho :

Fin K → ℝ

Score vector `q(zᵏ)`.

score :

Fin K → Fin L → ℝ

Moment vector `E[q(Z)D]` in finite-support form.

firstStageMoment :

Fin L → ℝ

Support masses are nonnegative.

rho_nonneg :

∀ k, 0 ≤ rho k

Support masses sum to one.

rho_sum_one :

∑ k, rho k = 1

The finite second-moment matrix is invertible.

gram_invertible :

Invertible (firstStageGram rho score)

The matrix-inverse fitted first stage is weakly increasing in the displayed support order.

fitted_mono :

∀ {k l : Fin K}

k.val ≤ l.val

then

(∑ a : Fin L, (∑ b : Fin L, (⅟(firstStageGram rho score)) a b * firstStageMoment b) * score k a)

≤ (∑ a : Fin L, (∑ b : Fin L, (⅟(firstStageGram rho score)) a b * firstStageMoment b) * score l a)

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:370

def gram reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage

For a finite matrix first-stage specification, the Gram matrix is its mass-weighted second-moment matrix of instrument score vectors.

Definition (Lean source)

parameters

K :

ℕ

shared

L :

ℕ

shared

S :

shared

def

gram S :

Matrix (Fin L) (Fin L) ℝ

given by

firstStageGram S.rho S.score

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage.gram · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:408 · uses MatrixFirstStage

def projectionCoeff reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage

For a finite matrix first-stage specification and a score-coordinate index, the population first-stage projection coefficient at that coordinate is the corresponding entry of the inverse Gram matrix times the vector of first-stage moments.

Definition (Lean source)

parameters

K :

ℕ

shared

L :

ℕ

shared

S :

shared

a :

Fin L

def

projectionCoeff S a :

ℝ

given by

∑ b : Fin L, (⅟S.gram) a b * S.firstStageMoment b

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage.projectionCoeff · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:422 · uses MatrixFirstStage

def fittedValue reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage

For a finite matrix first-stage specification and an instrument support point, the fitted first-stage value is the inner product of that point's score vector and the population first-stage projection coefficients.

Definition (Lean source)

parameters

K :

ℕ

shared

L :

ℕ

shared

S :

shared

k :

Fin K

def

fittedValue S k :

ℝ

given by

∑ a : Fin L, S.projectionCoeff a * S.score k a

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage.fittedValue · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:428 · uses MatrixFirstStage

def toFiniteIndex reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage

For a finite matrix first-stage specification, the ordered finite first-stage index retains its support masses and uses its fitted first-stage values as the ordered score.

Definition (Lean source)

parameters

K :

ℕ

shared

L :

ℕ

shared

S :

shared

def

toFiniteIndex S :

given by

clause 1

rho := S.rho

clause 2

dhat := S.fittedValue

clause 3

rho_nonneg := S.rho_nonneg

clause 4

rho_sum_one := S.rho_sum_one

clause 5

dhat_mono := by intro k l hkl simp only [fittedValue, projectionCoeff, gram] exact S.fitted_mono hkl

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage.toFiniteIndex · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:434 · uses FiniteIndex , MatrixFirstStage

5 supporting declarations (lemmas, instances)

supportMass_nonneg theorem — Support masses obtained from a measure are nonnegative.

hypotheses

Ω :

Type*
MeasurableSpace Ω

K :

ℕ

μ :

Measure Ω

Z :

Ω → Fin K

k :

Fin K

conclusion

0 ≤ supportMass μ Z k

Proof (Lean source)

theorem supportMass_nonneg {Ω : Type*} [MeasurableSpace Ω] {K : ℕ} (μ : Measure Ω) (Z : Ω → Fin K) (k : Fin K) : 0 ≤ supportMass μ Z k := by exact ENNReal.toReal_nonneg

Causalean.PO.ID.Exact.MultipleInstrumentIV.supportMass_nonneg · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:85
supportMass_sum_eq_one theorem — For a probability measure, the finite support masses induced by Z sum to one.

hypotheses

Ω :

Type*
MeasurableSpace Ω

K :

ℕ

μ :

Measure Ω
IsProbabilityMeasure μ

Z :

Ω → Fin K

hZ :

Measurable Z

conclusion

∑ k : Fin K, supportMass μ Z k = 1

Proof (Lean source)

theorem supportMass_sum_eq_one {Ω : Type*} [MeasurableSpace Ω] {K : ℕ} (μ : Measure Ω) [IsProbabilityMeasure μ] (Z : Ω → Fin K) (hZ : Measurable Z) : ∑ k : Fin K, supportMass μ Z k = 1 := by have hsum : (Finset.univ).sum (fun k : Fin K => (μ (Z ⁻¹' ({k} : Set (Fin K)))).toReal) = (μ (Z ⁻¹' (Set.univ : Set (Fin K)))).toReal := by simpa [Measure.real] using (MeasureTheory.sum_measureReal_preimage_singleton (μ := μ) (s := (Finset.univ : Finset (Fin K))) (f := Z) (hf := by intro k _hk exact hZ (measurableSet_singleton k)) (h := by intro k _hk exact ne_of_lt <| lt_of_le_of_lt (measure_mono (Set.subset_univ _)) (by simp [IsProbabilityMeasure.measure_univ]))) have hpre : ∀ k : Fin K, ({ω | Z ω = k} : Set Ω) = Z ⁻¹' ({k} : Set (Fin K)) := fun _ => rfl simpa [supportMass, hpre, Set.preimage_univ] using hsum

Causalean.PO.ID.Exact.MultipleInstrumentIV.supportMass_sum_eq_one · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:91
centered_weight_sum_zero theorem — Centering identity Σ_k ρ_k (dhat_k - dbar) = 0.

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

conclusion

∑ k, I.rho k * I.centeredIndex k = 0

Proof (Lean source)

theorem centered_weight_sum_zero : ∑ k, I.rho k * I.centeredIndex k = 0 := by calc ∑ k, I.rho k * I.centeredIndex k = ∑ k, (I.rho k * I.dhat k - I.rho k * I.meanIndex) := by simp [centeredIndex, sub_eq_add_neg, mul_add] _ = ∑ k, I.rho k * I.dhat k - ∑ k, I.rho k * I.meanIndex := by rw [Finset.sum_sub_distrib] _ = I.meanIndex - I.meanIndex * ∑ k, I.rho k := by simp [meanIndex, Finset.sum_mul, mul_comm] _ = 0 := by simp [I.rho_sum_one]

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex.centered_weight_sum_zero · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:158
tail_sum_interchange theorem — Finite upper-tail interchange identity used by the signed decomposition. It is the algebraic form of moving from Σ_k ρ_k a_k Σ_{j≤k} x_j to Σ_j B_j x_j.

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

x :

Adj K → ℝ

conclusion

(∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ j : Adj K, if j.1.val ≤ k.val then x j else 0))
= ∑ j : Adj K, I.tailCoeff j * x j

Proof (Lean source)

theorem tail_sum_interchange (x : Adj K → ℝ) : (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ j : Adj K, if j.1.val ≤ k.val then x j else 0)) = ∑ j : Adj K, I.tailCoeff j * x j := by simp only [tailCoeff, upperTail] calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ j : Adj K, if j.1.val ≤ k.val then x j else 0)) = ∑ k : Fin K, ∑ j : Adj K, if j.1.val ≤ k.val then (I.rho k * I.centeredIndex k) * x j else 0 := by simp [Finset.mul_sum, mul_ite, mul_zero, mul_assoc] _ = ∑ j : Adj K, ∑ k : Fin K, if j.1.val ≤ k.val then (I.rho k * I.centeredIndex k) * x j else 0 := by rw [Finset.sum_comm] _ = ∑ j : Adj K, x j * ∑ k : Fin K, if j.1.val ≤ k.val then I.rho k * I.centeredIndex k else 0 := by apply Finset.sum_congr rfl intro j _hj rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k _hk by_cases h : j.1.val ≤ k.val · simp [h, mul_comm] · simp [h] _ = ∑ j : Adj K, (∑ k ∈ Finset.univ.filter fun k => j.1.val ≤ k.val, I.rho k * I.centeredIndex k) * x j := by simp [Finset.sum_filter, mul_comm]

Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex.tail_sum_interchange · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:244
instInvertibleGram instance — For a finite matrix first-stage specification, the assertion that its mass-weighted second-moment (Gram) matrix is invertible holds.

parameters

K :

ℕ
shared

L :

ℕ
shared

S :

MatrixFirstStage K L
shared

instance

instInvertibleGram S :
Invertible S.gram

given by

by change Invertible (firstStageGram S.rho S.score) exact S.gram_invertible

Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage.instInvertibleGram · Causalean/PO/ID/Exact/MultipleInstrumentIV/FiniteIndex.lean:413

ResponseTypes 22 core · 6 supporting This file formalizes the finite response-type algebra used in the Mogstad-Torgovitsky-Walters multiple-instrument IV decomposition. ★ beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra★ beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum★ beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage★ exists_negativeNormalizedTypeWeight

Multiple-Instrument IV Response Types

This file formalizes the finite response-type algebra used in the Mogstad-Torgovitsky-Walters multiple-instrument IV decomposition. The basic objects are ResponseType, typeStep, ResponseTypeStats, the unnormalized and normalized weights unnormTypeWeight and normalizedTypeWeight, and the finite ratio beta2SLSFiniteAlgebra.

The nested PopulationBridge structure gives a saturated finite-support bridge from support-point outcome and treatment expansions to the response-type ratio. Theorems firstStageMoment_eq_typeWeightDenom, reducedFormMoment_eq_typeWeightNumerator, and beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra prove the algebraic identification step. The sign-alignment results normalizedTypeWeight_nonneg_of_signAligned, normalizedTypeWeight_sum_eq_one_of_pos, and beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage explain when the ratio is a convex response-type average, while exists_negativeNormalizedTypeWeight gives a concrete two-support-point counterexample with a negative normalized weight.

The ComponentwiseMonotoneRestriction structure is intentionally documented as an opaque interface, not a faithful formalization of MTW partial monotonicity.

abbrev ResponseType reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV

For a finite instrument support of size $K$ , a response type is a binary treatment response specified for every instrument support point.

Definition (Lean source)

parameters

K :

ℕ

def

ResponseType K :

Type

given by

Fin K → Bool

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseType · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:57

def boolToReal reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV

For a binary treatment indicator, the real-valued treatment indicator equals one for treatment and zero otherwise.

Definition (Lean source)

parameters

b :

Bool

def

boolToReal b :

ℝ

given by

if b then 1 else 0

Causalean.PO.ID.Exact.MultipleInstrumentIV.boolToReal · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:60

def typeStep reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV

For a finite instrument support of size $K$ , a response type, and an adjacent threshold, the adjacent treatment-response increment is the real-valued treatment response at the upper support point minus that at the preceding point.

Definition (Lean source)

parameters

K :

ℕ

g :

j :

Adj K

def

typeStep g j :

ℝ

given by

boolToReal (g (Adj.upper j)) - boolToReal (g (Adj.lower j))

Causalean.PO.ID.Exact.MultipleInstrumentIV.typeStep · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:64 · uses Adj , ResponseType

structure ResponseTypeStats reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV

Finite response-type statistics. For a finite family of latent response types, this records the probability mass of each type and the type-specific average causal effect Δ_g, subject to every mass being nonnegative and the masses summing to one, so together they form a probability vector over response types.

Definition (Lean source)

parameters

K :

ℕ

fields

Response-type mass `π_g = P(G = g)`.

mass :

ResponseType K → ℝ

Response-type causal effect `Δ_g`. Zero-mass conventions are handled at the finite-algebra layer by multiplying by `mass`.

effect :

ResponseType K → ℝ

Response-type masses are nonnegative.

mass_nonneg :

∀ g, 0 ≤ mass g

Response-type masses sum to one.

mass_sum_one :

∑ g, mass g = 1

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:68

def unnormTypeWeight reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

For an ordered finite first-stage index, finite response-type statistics, and a response type, the unnormalized MTW response-type weight is that type's mass times the sum of each tail coefficient times its adjacent treatment-response increment.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

R :

shared

g :

def

unnormTypeWeight I R g :

ℝ

given by

R.mass g * ∑ j : Adj K, I.tailCoeff j * typeStep g j

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.unnormTypeWeight · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:88 · uses FiniteIndex , ResponseType , ResponseTypeStats

def typeWeightDenom reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

For an ordered finite first-stage index and finite response-type statistics, the response-type weight denominator is the sum of the unnormalized weights over all response types.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

R :

shared

def

typeWeightDenom I R :

ℝ

given by

∑ g : ResponseType K, R.unnormTypeWeight I g

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.typeWeightDenom · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:92 · uses FiniteIndex , ResponseTypeStats

def normalizedTypeWeight reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

For an ordered finite first-stage index, finite response-type statistics, and a response type, the normalized response-type weight is that type's unnormalized weight divided by the sum of all unnormalized weights.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

R :

shared

g :

def

normalizedTypeWeight I R g :

ℝ

given by

normalizedWeight (R.unnormTypeWeight I) g

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.normalizedTypeWeight · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:96 · uses FiniteIndex , ResponseType , ResponseTypeStats

def responseTypeEstimand reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

For an ordered finite first-stage index and finite response-type statistics, the response-type estimand is the sum of each within-type causal effect weighted by its normalized response-type weight.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

R :

shared

def

responseTypeEstimand I R :

ℝ

given by

∑ g : ResponseType K, R.normalizedTypeWeight I g * R.effect g

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.responseTypeEstimand · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:100 · uses FiniteIndex , ResponseTypeStats

def beta2SLSFiniteAlgebra reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

For an ordered finite first-stage index and finite response-type statistics, the finite-algebra 2SLS estimand is the unnormalized response-type-weighted sum of causal effects divided by the sum of unnormalized response-type weights.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

R :

shared

def

beta2SLSFiniteAlgebra I R :

ℝ

given by

(∑ g : ResponseType K, R.unnormTypeWeight I g * R.effect g) / R.typeWeightDenom I

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.beta2SLSFiniteAlgebra · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:104 · uses FiniteIndex , ResponseTypeStats

structure PopulationBridge reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

Saturated finite-support population bridge for the MTW identification step. Bundles a finite response-type statistics record supplying the type masses and type-specific effects together with a response-type-specific baseline outcome mean, the term the centered first-stage index cancels, leaving the telescoped adjacent treatment increments used by the finite algebra.

Definition (Lean source)

parameters

K :

ℕ

fields

Response-type masses and type-specific treatment effects.

stats :

Response-type-specific baseline outcome mean, the term subtracted by the centered-index argument in the signed decomposition proof.

baseOutcome :

ResponseType K → ℝ

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:111

def telescopedTypeStep reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

For a finite instrument support of size $K$ , a response type, and a support point, the telescoped adjacent treatment response is the sum of that type's adjacent treatment-response increments from the first support point through that point.

Definition (Lean source)

parameters

K :

ℕ

shared

g :

k :

Fin K

def

telescopedTypeStep g k :

ℝ

given by

∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.telescopedTypeStep · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:127 · uses ResponseType

def outcomeAtSupport reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

For a finite instrument support of size $K$ , a saturated finite-support population bridge, and a support point, the response-type outcome expansion is the baseline outcome plus the response-type-mass-weighted sum of within-type effects times telescoped treatment responses.

Definition (Lean source)

parameters

K :

ℕ

shared

P :

k :

Fin K

def

outcomeAtSupport P k :

ℝ

given by

∑ g : ResponseType K, P.stats.mass g * (P.baseOutcome g + telescopedTypeStep g k * P.stats.effect g)

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.outcomeAtSupport · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:131 · uses PopulationBridge

def treatmentAtSupport reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

For a finite instrument support of size $K$ , a saturated finite-support population bridge, and a support point, the response-type treatment expansion is the response-type-mass-weighted sum of telescoped treatment responses at that point.

Definition (Lean source)

parameters

K :

ℕ

shared

P :

k :

Fin K

def

treatmentAtSupport P k :

ℝ

given by

∑ g : ResponseType K, P.stats.mass g * telescopedTypeStep g k

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.treatmentAtSupport · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:137 · uses PopulationBridge

def reducedFormMoment reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

For a finite instrument support of size $K$ , a saturated finite-support population bridge, and an ordered finite first-stage index, the population reduced-form moment is the support-mass-weighted sum of centered first-stage indices times response-type outcome expansions.

Definition (Lean source)

parameters

K :

ℕ

shared

P :

I :

def

reducedFormMoment P I :

ℝ

given by

∑ k : Fin K, I.rho k * I.centeredIndex k * P.outcomeAtSupport k

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.reducedFormMoment · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:141 · uses FiniteIndex , PopulationBridge

def firstStageMoment reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

For a finite instrument support of size $K$ , a saturated finite-support population bridge, and an ordered finite first-stage index, the population first-stage moment is the support-mass-weighted sum of centered first-stage indices times response-type treatment expansions.

Definition (Lean source)

parameters

K :

ℕ

shared

P :

I :

def

firstStageMoment P I :

ℝ

given by

∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.firstStageMoment · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:145 · uses FiniteIndex , PopulationBridge

def beta2SLSPopulationBridge reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

For a finite instrument support of size $K$ , a saturated finite-support population bridge, and an ordered finite first-stage index, the population multiple-IV 2SLS ratio is its reduced-form moment divided by its first-stage moment.

Definition (Lean source)

parameters

K :

ℕ

shared

P :

I :

def

beta2SLSPopulationBridge P I :

ℝ

given by

P.reducedFormMoment I / P.firstStageMoment I

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.beta2SLSPopulationBridge · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:149 · uses FiniteIndex , PopulationBridge

theorem beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

Saturated finite-support MTW identification. The population 2SLS ratio E[h(Z)Y] / E[h(Z)D], after consistency, exogeneity, exclusion, and telescoping, is exactly the finite response-type ratio.

Formal statement

hypotheses

K :

ℕ

shared

I :

shared

P :

shared

conclusion

P.beta2SLSPopulationBridge I = P.stats.beta2SLSFiniteAlgebra I

Proof (Lean source)

theorem beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra : P.beta2SLSPopulationBridge I = P.stats.beta2SLSFiniteAlgebra I := by unfold beta2SLSPopulationBridge ResponseTypeStats.beta2SLSFiniteAlgebra rw [P.reducedFormMoment_eq_typeWeightNumerator I, P.firstStageMoment_eq_typeWeightDenom I]

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra

· Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:277 · uses FiniteIndex , PopulationBridge , beta2SLSPopulationBridge , beta2SLSFiniteAlgebra

def SignAligned reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

For an ordered finite first-stage index and finite response-type statistics, sign alignment means that every response type with strictly positive mass has a nonnegative tail-coefficient-weighted sum of adjacent treatment-response increments.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

R :

shared

g :

0 < R.mass g

def

SignAligned I R :

Prop

given by

0 ≤ ∑ j : Adj K, I.tailCoeff j * typeStep g j

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.SignAligned · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:288 · uses FiniteIndex , ResponseTypeStats

structure ComponentwiseMonotoneRestriction reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

Opaque response-type restriction interface.

Definition (Lean source)

parameters

K :

ℕ

shared

fields

Response types admitted by the restriction. This predicate is unconstrained; nothing in Lean forces it to correspond to any geometric or probabilistic monotonicity condition.

allowed :

ResponseType K → Prop

Allowed response types have nonnegative adjacent steps in the displayed support order. This is an axiom field, not a derived fact.

step_nonneg_of_allowed :

∀ g : ResponseType K

allowed g

then

∀ j : Adj K, 0 ≤ typeStep g j

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.ComponentwiseMonotoneRestriction · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:293

theorem beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

Response-type form of the finite MTW ratio (prop:po-estimand-mtw-response-type-form). Provided the first-stage type-weight denominator is nonzero, the finite-algebra 2SLS estimand equals the response-type-weighted sum of within-type causal effects.

Formal statement

hypotheses

K :

ℕ

shared

I :

shared

R :

shared

hden :

R.typeWeightDenom I ≠ 0

conclusion

R.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I

Proof (Lean source)

theorem beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum (hden : R.typeWeightDenom I ≠ 0) : R.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I := by have _ : R.typeWeightDenom I ≠ 0 := hden unfold beta2SLSFiniteAlgebra responseTypeEstimand normalizedTypeWeight calc (∑ g : ResponseType K, R.unnormTypeWeight I g * R.effect g) / R.typeWeightDenom I = ∑ g : ResponseType K, (R.unnormTypeWeight I g * R.effect g) / R.typeWeightDenom I := by rw [Finset.sum_div] _ = ∑ g : ResponseType K, R.unnormTypeWeight I g / R.typeWeightDenom I * R.effect g := by apply Finset.sum_congr rfl intro g _hg rw [div_mul_eq_mul_div]

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:358 · uses FiniteIndex , ResponseTypeStats , beta2SLSFiniteAlgebra , responseTypeEstimand , typeWeightDenom

theorem beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

Positive-weight response-type characterization. When the response types are sign-aligned with the instrument order and the first-stage type-weight denominator is strictly positive, the finite-algebra 2SLS estimand equals the response-type estimand, every normalized response-type weight is nonnegative, and the weights sum to one.

Formal statement

hypotheses

K :

ℕ

shared

I :

shared

R :

shared

hAlign :

R.SignAligned I

hden :

0 < R.typeWeightDenom I

conclusion

conclusion 1

R.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I

conclusion 2

g :

0 ≤ R.normalizedTypeWeight I g

conclusion 3

∑ g : ResponseType K, R.normalizedTypeWeight I g = 1

Proof (Lean source)

theorem beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage (hAlign : R.SignAligned I) (hden : 0 < R.typeWeightDenom I) : R.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I ∧ (∀ g : ResponseType K, 0 ≤ R.normalizedTypeWeight I g) ∧ (∑ g : ResponseType K, R.normalizedTypeWeight I g = 1) := by constructor · exact R.beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum I hden.ne' constructor · intro g exact R.normalizedTypeWeight_nonneg_of_signAligned I hAlign hden g · exact R.normalizedTypeWeight_sum_eq_one_of_pos I hden

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:377 · uses FiniteIndex , ResponseType , ResponseTypeStats , SignAligned , beta2SLSFiniteAlgebra , normalizedTypeWeight , responseTypeEstimand , typeWeightDenom

theorem exists_negativeNormalizedTypeWeight reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV

Negative-weights theorem. There exists a finite-support instrument index, a response-type population, and a response type such that, with two support points and a 3/4-defier population, that type has positive mass yet a negative normalized response-type weight (equal to −1/2).

Formal statement

conclusion

∃ (I : FiniteIndex 2) (R : ResponseTypeStats 2) (g : ResponseType 2),

conclusion 1

0 < R.mass g

conclusion 2

R.normalizedTypeWeight I g < 0

Proof (Lean source)

theorem exists_negativeNormalizedTypeWeight : ∃ (I : FiniteIndex 2) (R : ResponseTypeStats 2) (g : ResponseType 2), 0 < R.mass g ∧ R.normalizedTypeWeight I g < 0 := by refine ⟨exIndex, exStats, gComplier, ?_, ?_⟩ · -- mass of complier type = 1/4 > 0 rw [exStats_mass, exMass_complier]; norm_num · -- normalized weight = (3/64) / (-3/32) = -1/2 < 0 rw [ResponseTypeStats.normalizedTypeWeight, normalizedWeight] change exStats.unnormTypeWeight exIndex gComplier / (∑ k, exStats.unnormTypeWeight exIndex k) < 0 rw [← ResponseTypeStats.typeWeightDenom, exStats_unnorm_complier, exStats_denom] norm_num

Causalean.PO.ID.Exact.MultipleInstrumentIV.exists_negativeNormalizedTypeWeight · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:582 · uses FiniteIndex , ResponseType , ResponseTypeStats , normalizedTypeWeight

6 supporting declarations (lemmas, instances)

baselineMoment_eq_zero theorem — The baseline outcome component vanishes because the first-stage index is centered.

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

P :

PopulationBridge K
shared

conclusion

(∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g))
= 0

Proof (Lean source)

theorem baselineMoment_eq_zero : (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g)) = 0 := by calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g)) = (∑ k : Fin K, I.rho k * I.centeredIndex k) * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g) := by rw [Finset.sum_mul] _ = 0 := by rw [I.centered_weight_sum_zero] simp

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.baselineMoment_eq_zero · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:153
firstStageMoment_eq_typeWeightDenom theorem — The finite-support first-stage moment is the response-type denominator. This is the denominator half of the MTW identification step.

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

P :

PopulationBridge K
shared

conclusion

P.firstStageMoment I = P.stats.typeWeightDenom I

Proof (Lean source)

theorem firstStageMoment_eq_typeWeightDenom : P.firstStageMoment I = P.stats.typeWeightDenom I := by classical unfold firstStageMoment treatmentAtSupport telescopedTypeStep ResponseTypeStats.typeWeightDenom ResponseTypeStats.unnormTypeWeight calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0))) = ∑ k : Fin K, ∑ g : ResponseType K, I.rho k * I.centeredIndex k * (P.stats.mass g * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0)) := by apply Finset.sum_congr rfl intro k _hk rw [Finset.mul_sum] _ = ∑ g : ResponseType K, ∑ k : Fin K, I.rho k * I.centeredIndex k * (P.stats.mass g * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0)) := by rw [Finset.sum_comm] _ = ∑ g : ResponseType K, P.stats.mass g * (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0)) := by apply Finset.sum_congr rfl intro g _hg rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k _hk ring _ = ∑ g : ResponseType K, P.stats.mass g * (∑ j : Adj K, I.tailCoeff j * typeStep g j) := by apply Finset.sum_congr rfl intro g _hg rw [I.tail_sum_interchange (fun j => typeStep g j)]

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.firstStageMoment_eq_typeWeightDenom · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:170
reducedFormMoment_eq_typeWeightNumerator theorem — The finite-support reduced-form moment is the response-type numerator. This is the numerator half of the MTW identification step.

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

P :

PopulationBridge K
shared

conclusion

P.reducedFormMoment I
= ∑ g : ResponseType K, P.stats.unnormTypeWeight I g * P.stats.effect g

Proof (Lean source)

theorem reducedFormMoment_eq_typeWeightNumerator : P.reducedFormMoment I = ∑ g : ResponseType K, P.stats.unnormTypeWeight I g * P.stats.effect g := by classical unfold reducedFormMoment outcomeAtSupport telescopedTypeStep ResponseTypeStats.unnormTypeWeight calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * (P.baseOutcome g + (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g))) = (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g)) + ∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * ((∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g)) := by simp only [mul_add, Finset.sum_add_distrib] _ = ∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * ((∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g)) := by rw [P.baselineMoment_eq_zero I] simp _ = ∑ k : Fin K, ∑ g : ResponseType K, I.rho k * I.centeredIndex k * (P.stats.mass g * ((∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g)) := by apply Finset.sum_congr rfl intro k _hk rw [Finset.mul_sum] _ = ∑ g : ResponseType K, ∑ k : Fin K, I.rho k * I.centeredIndex k * (P.stats.mass g * ((∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g)) := by rw [Finset.sum_comm] _ = ∑ g : ResponseType K, P.stats.mass g * (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0)) * P.stats.effect g := by apply Finset.sum_congr rfl intro g _hg simp [Finset.mul_sum, mul_assoc, mul_comm, mul_left_comm] _ = ∑ g : ResponseType K, (P.stats.mass g * (∑ j : Adj K, I.tailCoeff j * typeStep g j)) * P.stats.effect g := by apply Finset.sum_congr rfl intro g _hg rw [I.tail_sum_interchange (fun j => typeStep g j)]

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.reducedFormMoment_eq_typeWeightNumerator · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:212
unnormTypeWeight_nonneg_of_signAligned theorem — Sign alignment and nonnegative type masses imply nonnegative unnormalized response-type weights.

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

R :

ResponseTypeStats K
shared

hAlign :

R.SignAligned I

g :

ResponseType K

conclusion

0 ≤ R.unnormTypeWeight I g

Proof (Lean source)

theorem unnormTypeWeight_nonneg_of_signAligned (hAlign : R.SignAligned I) (g : ResponseType K) : 0 ≤ R.unnormTypeWeight I g := by unfold unnormTypeWeight by_cases hpos : 0 < R.mass g · exact mul_nonneg (R.mass_nonneg g) (hAlign g hpos) · have hle : R.mass g ≤ 0 := le_of_not_gt hpos have hmass : R.mass g = 0 := le_antisymm hle (R.mass_nonneg g) simp [hmass]

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.unnormTypeWeight_nonneg_of_signAligned · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:329
normalizedTypeWeight_nonneg_of_signAligned theorem — Normalized response-type weights are nonnegative when sign alignment holds and the denominator is positive (prop:po-estimand-mtw-positive-weights).

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

R :

ResponseTypeStats K
shared

hAlign :

R.SignAligned I

hden :

0 < R.typeWeightDenom I

g :

ResponseType K

conclusion

0 ≤ R.normalizedTypeWeight I g

Proof (Lean source)

theorem normalizedTypeWeight_nonneg_of_signAligned (hAlign : R.SignAligned I) (hden : 0 < R.typeWeightDenom I) (g : ResponseType K) : 0 ≤ R.normalizedTypeWeight I g := by exact normalizedWeight_nonneg (R.unnormTypeWeight I) (R.unnormTypeWeight_nonneg_of_signAligned I hAlign) hden g

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.normalizedTypeWeight_nonneg_of_signAligned · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:341
normalizedTypeWeight_sum_eq_one_of_pos theorem — Normalized response-type weights sum to one when the first-stage denominator is positive.

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

R :

ResponseTypeStats K
shared

hden :

0 < R.typeWeightDenom I

conclusion

∑ g : ResponseType K, R.normalizedTypeWeight I g = 1

Proof (Lean source)

theorem normalizedTypeWeight_sum_eq_one_of_pos (hden : 0 < R.typeWeightDenom I) : ∑ g : ResponseType K, R.normalizedTypeWeight I g = 1 := by exact sum_normalizedWeight_eq_one (R.unnormTypeWeight I) hden.ne'

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.normalizedTypeWeight_sum_eq_one_of_pos · Causalean/PO/ID/Exact/MultipleInstrumentIV/ResponseTypes.lean:350

Population 6 core · 5 supporting This file connects the observed population two-stage least squares moment ratio for a finite instrument to the response-type finite algebra. ★ observedBeta2SLS_eq_beta2SLSFiniteAlgebra

Multiple-Instrument IV Population Bridge

This file connects the observed population two-stage least squares moment ratio for a finite instrument to the response-type finite algebra. It defines the observed moments observedReducedFormMoment, observedFirstStageMoment, and observedBeta2SLS; rewrites the first two as finite sums over instrument cells; and packages the assumptions needed for the measure-backed bridge in ObservedBridge.

The main results are ObservedBridge.observedReducedFormMoment_eq_reducedFormMoment, ObservedBridge.observedFirstStageMoment_eq_firstStageMoment, ObservedBridge.observedBeta2SLS_eq_beta2SLSPopulationBridge, and the end-to-end theorem ObservedBridge.observedBeta2SLS_eq_beta2SLSFiniteAlgebra. They show that the observable population ratio E[h(Z)Y] / E[h(Z)D] agrees with the saturated response-type algebra once the observed conditional means are linked to the finite response-type bridge.

def zEvent reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

For a sample space, a finite instrument support of size $K$ , an instrument on that sample space, and a support point, the instrument cell is the set of units whose instrument equals that point.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

K :

ℕ

shared

Z :

Ω → Fin K

k :

Fin K

def

zEvent Z k :

Set Ω

given by

Z ⁻¹' ({k} : Set (Fin K))

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.zEvent · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:43

def observedReducedFormMoment reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

Given a measurable sample space, a finite instrument support of size $K$ , a measure, an instrument, a real outcome, and an ordered finite first-stage index, the observed reduced-form moment is the integral of the centered first-stage index evaluated at the instrument times the outcome.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

K :

ℕ

shared

μ :

Z :

Ω → Fin K

Y :

Ω → ℝ

I :

def

observedReducedFormMoment μ Z Y I :

ℝ

given by

∫ ω, I.centeredIndex (Z ω) * Y ω ∂μ

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.observedReducedFormMoment · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:47 · uses FiniteIndex

def observedFirstStageMoment reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

Given a measurable sample space, a finite instrument support of size $K$ , a measure, an instrument, a binary treatment, and an ordered finite first-stage index, the observed first-stage moment is the integral of the centered first-stage index evaluated at the instrument times the zero-one treatment indicator.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

K :

ℕ

shared

μ :

Z :

Ω → Fin K

D :

Ω → Bool

I :

def

observedFirstStageMoment μ Z D I :

ℝ

given by

∫ ω, I.centeredIndex (Z ω) * boolToReal (D ω) ∂μ

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.observedFirstStageMoment · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:52 · uses FiniteIndex

def observedBeta2SLS reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

Given a measurable sample space, a finite instrument support of size $K$ , a measure, an instrument, a binary treatment, a real outcome, and an ordered finite first-stage index, the observed population 2SLS ratio is the observed reduced-form moment divided by the observed first-stage moment.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

K :

ℕ

shared

μ :

Z :

Ω → Fin K

D :

Ω → Bool

Y :

Ω → ℝ

I :

def

observedBeta2SLS μ Z D Y I :

ℝ

given by

observedReducedFormMoment μ Z Y I / observedFirstStageMoment μ Z D I

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.observedBeta2SLS · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:57 · uses FiniteIndex

structure ObservedBridge reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

Bridge from an observed finite-instrument population to the response-type algebra. Given an instrument, a binary treatment, an outcome, a finite index, and a saturated response-type population P, this bundles the underlying law being a probability measure, the finite-index masses reproducing the probabilities of the observed instrument cells, the observed conditional mean of the outcome on each instrument cell equaling the response-type expansion P.outcomeAtSupport, a baseline treatment mean common across cells after exogeneity, and the observed conditional mean of the treatment on each instrument cell equaling that common baseline plus the response-type expansion P.treatmentAtSupport.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

K :

ℕ

shared

μ :

Z :

Ω → Fin K

D :

Ω → Bool

Y :

Ω → ℝ

I :

P :

fields

The observed law is a probability measure, so the integrals below are population expectations.

isProbability :

IsProbabilityMeasure μ

The finite support masses in `I` are the probabilities of the observed instrument cells.

rho_eq_zMass :

∀ k : Fin K, I.rho k = (μ (zEvent Z k)).toReal

Conditional outcome bridge after consistency, exogeneity, and exclusion: for each instrument cell Z = zᵏ, the observed conditional mean E[Y | Z = zᵏ] equals the response-type expansion `P.outcomeAtSupport k`. This is a *field* of the algebraic bridge, but it is no longer only an external hypothesis: `MultipleInstrumentIV/POBridge.lean` (`toObservedBridge`) *derives* it from a `POMultipleIVSystem` under consistency + instrument independence, discharging Gap G5 of the faithfulness audit (`doc/basic_concepts/po/estimand_characterization/audit/mtw.md`). Callers may either supply it directly or obtain the whole bridge from the PO system.

outcome_cell :

∀ k : Fin K, PO.eventCondExp μ (zEvent Z k) Y = P.outcomeAtSupport k

Baseline treatment mean, common across support cells after exogeneity. The centered first-stage score cancels this term in the first-stage moment.

baseTreatment :

ℝ

Conditional treatment bridge after consistency and exogeneity, stated in baseline-subtracted form: the adjacent telescoping term is the deviation from the baseline support point, not the raw treatment mean. Like `outcome_cell`, this field is *derived* (not merely assumed) from a `POMultipleIVSystem` under consistency + instrument independence in `MultipleInstrumentIV/POBridge.lean` (`toObservedBridge`), discharging Gap G5 of the faithfulness audit.

treatment_cell :

∀ k : Fin K,

PO.eventCondExp μ (zEvent Z k) (fun ω => boolToReal (D ω))

= baseTreatment + P.treatmentAtSupport k

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.ObservedBridge · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:132 · uses FiniteIndex , PopulationBridge

theorem observedBeta2SLS_eq_beta2SLSFiniteAlgebra reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.ObservedBridge

End-to-end bridge to the finite response-type algebra. Given a bridge B linking the observed data to the response-type population, provided the instrument is measurable, the centered-instrument-weighted outcome is integrable, and the centered-instrument-weighted treatment is integrable, the observed population 2SLS ratio E[h(Z)Y] / E[h(Z)D] equals the finite response-type algebra estimand beta2SLSFiniteAlgebra.

Formal statement

hypotheses

Ω :

Type u_1

shared

K :

ℕ

shared

μ :

shared

Z :

Ω → Fin K

shared

D :

Ω → Bool

shared

Y :

Ω → ℝ

shared

I :

shared

P :

shared

B :

ObservedBridge μ Z D Y I P

IsFiniteMeasure μ

hZ :

Measurable Z

hYInt :

Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ

hDInt :

Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ

conclusion

observedBeta2SLS μ Z D Y I = P.stats.beta2SLSFiniteAlgebra I

Proof (Lean source)

theorem observedBeta2SLS_eq_beta2SLSFiniteAlgebra (B : ObservedBridge μ Z D Y I P) [IsFiniteMeasure μ] (hZ : Measurable Z) (hYInt : Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ) (hDInt : Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ) : observedBeta2SLS μ Z D Y I = P.stats.beta2SLSFiniteAlgebra I := by rw [B.observedBeta2SLS_eq_beta2SLSPopulationBridge hZ hYInt hDInt, P.beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra I]

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.ObservedBridge.observedBeta2SLS_eq_beta2SLSFiniteAlgebra

· Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:251 · uses FiniteIndex , centeredIndex , PopulationBridge , ObservedBridge , observedBeta2SLS , beta2SLSFiniteAlgebra , boolToReal

5 supporting declarations (lemmas, instances)

observedReducedFormMoment_eq_sum_eventCondExp theorem — Finite-support total-law rewrite of E[h(Z)Y] into instrument-cell conditional expectations.

hypotheses

Ω :

Type u_1
shared

K :

ℕ
shared

μ :

Measure Ω
IsFiniteMeasure μ

Z :

Ω → Fin K

hZ :

Measurable Z

Y :

Ω → ℝ

I :

FiniteIndex K

hInt :

Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ

conclusion

observedReducedFormMoment μ Z Y I
= ∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * PO.eventCondExp μ (zEvent Z k) Y

Proof (Lean source)

theorem observedReducedFormMoment_eq_sum_eventCondExp (μ : Measure Ω) [IsFiniteMeasure μ] (Z : Ω → Fin K) (hZ : Measurable Z) (Y : Ω → ℝ) (I : FiniteIndex K) (hInt : Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ) : observedReducedFormMoment μ Z Y I = ∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * PO.eventCondExp μ (zEvent Z k) Y := by unfold observedReducedFormMoment rw [PO.integral_eq_sum_measure_mul_eventCondExp (μ := μ) (A := zEvent Z) (hmeas := zEvent_measurable Z hZ) (hdisj := zEvent_pairwise_disjoint Z) (hcov := zEvent_iUnion Z) (f := fun ω => I.centeredIndex (Z ω) * Y ω) hInt] refine Finset.sum_congr rfl ?_ intro k _hk rw [eventCondExp_centered_mul_eq μ Z hZ Y I k] ring

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.observedReducedFormMoment_eq_sum_eventCondExp · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:97
observedFirstStageMoment_eq_sum_eventCondExp theorem — Finite-support total-law rewrite of E[h(Z)D] into instrument-cell conditional expectations.

hypotheses

Ω :

Type u_1
shared

K :

ℕ
shared

μ :

Measure Ω
IsFiniteMeasure μ

Z :

Ω → Fin K

hZ :

Measurable Z

D :

Ω → Bool

I :

FiniteIndex K

hInt :

Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ

conclusion

observedFirstStageMoment μ Z D I
= ∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * PO.eventCondExp μ (zEvent Z k) (fun ω => boolToReal (D ω))

Proof (Lean source)

theorem observedFirstStageMoment_eq_sum_eventCondExp (μ : Measure Ω) [IsFiniteMeasure μ] (Z : Ω → Fin K) (hZ : Measurable Z) (D : Ω → Bool) (I : FiniteIndex K) (hInt : Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ) : observedFirstStageMoment μ Z D I = ∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * PO.eventCondExp μ (zEvent Z k) (fun ω => boolToReal (D ω)) := by exact observedReducedFormMoment_eq_sum_eventCondExp (μ := μ) (Z := Z) hZ (Y := fun ω => boolToReal (D ω)) I hInt

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.observedFirstStageMoment_eq_sum_eventCondExp · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:119
observedReducedFormMoment_eq_reducedFormMoment theorem — The observed reduced-form moment equals the finite response-type reduced-form moment.

hypotheses

Ω :

Type u_1
shared

K :

ℕ
shared

μ :

Measure Ω
shared

Z :

Ω → Fin K
shared

D :

Ω → Bool
shared

Y :

Ω → ℝ
shared

I :

FiniteIndex K
shared

P :

PopulationBridge K
shared

B :

ObservedBridge μ Z D Y I P

IsFiniteMeasure μ

hZ :

Measurable Z

hInt :

Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ

conclusion

observedReducedFormMoment μ Z Y I = P.reducedFormMoment I

Proof (Lean source)

theorem observedReducedFormMoment_eq_reducedFormMoment (B : ObservedBridge μ Z D Y I P) [IsFiniteMeasure μ] (hZ : Measurable Z) (hInt : Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ) : observedReducedFormMoment μ Z Y I = P.reducedFormMoment I := by rw [observedReducedFormMoment_eq_sum_eventCondExp μ Z hZ Y I hInt] unfold reducedFormMoment refine Finset.sum_congr rfl ?_ intro k _hk rw [← B.rho_eq_zMass k, B.outcome_cell k]

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.ObservedBridge.observedReducedFormMoment_eq_reducedFormMoment · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:189
observedFirstStageMoment_eq_firstStageMoment theorem — The observed first-stage moment equals the finite response-type first-stage moment.

hypotheses

Ω :

Type u_1
shared

K :

ℕ
shared

μ :

Measure Ω
shared

Z :

Ω → Fin K
shared

D :

Ω → Bool
shared

Y :

Ω → ℝ
shared

I :

FiniteIndex K
shared

P :

PopulationBridge K
shared

B :

ObservedBridge μ Z D Y I P

IsFiniteMeasure μ

hZ :

Measurable Z

hInt :

Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ

conclusion

observedFirstStageMoment μ Z D I = P.firstStageMoment I

Proof (Lean source)

theorem observedFirstStageMoment_eq_firstStageMoment (B : ObservedBridge μ Z D Y I P) [IsFiniteMeasure μ] (hZ : Measurable Z) (hInt : Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ) : observedFirstStageMoment μ Z D I = P.firstStageMoment I := by rw [observedFirstStageMoment_eq_sum_eventCondExp μ Z hZ D I hInt] unfold firstStageMoment calc (∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * PO.eventCondExp μ (zEvent Z k) (fun ω => boolToReal (D ω))) = ∑ k : Fin K, I.rho k * I.centeredIndex k * (B.baseTreatment + P.treatmentAtSupport k) := by refine Finset.sum_congr rfl ?_ intro k _hk rw [← B.rho_eq_zMass k, B.treatment_cell k] _ = (∑ k : Fin K, I.rho k * I.centeredIndex k) * B.baseTreatment + ∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k := by calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (B.baseTreatment + P.treatmentAtSupport k)) = ∑ k : Fin K, (I.rho k * I.centeredIndex k * B.baseTreatment + I.rho k * I.centeredIndex k * P.treatmentAtSupport k) := by refine Finset.sum_congr rfl ?_ intro k _hk ring _ = (∑ k : Fin K, I.rho k * I.centeredIndex k * B.baseTreatment) + ∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k := by rw [Finset.sum_add_distrib] _ = (∑ k : Fin K, I.rho k * I.centeredIndex k) * B.baseTreatment + ∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k := by rw [Finset.sum_mul] _ = ∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k := by rw [I.centered_weight_sum_zero] simp

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.ObservedBridge.observedFirstStageMoment_eq_firstStageMoment · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:201
observedBeta2SLS_eq_beta2SLSPopulationBridge theorem — Observed population 2SLS, written as E[h(Z)Y]/E[h(Z)D], equals the saturated finite-support population bridge ratio.

hypotheses

Ω :

Type u_1
shared

K :

ℕ
shared

μ :

Measure Ω
shared

Z :

Ω → Fin K
shared

D :

Ω → Bool
shared

Y :

Ω → ℝ
shared

I :

FiniteIndex K
shared

P :

PopulationBridge K
shared

B :

ObservedBridge μ Z D Y I P

IsFiniteMeasure μ

hZ :

Measurable Z

hYInt :

Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ

hDInt :

Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ

conclusion

observedBeta2SLS μ Z D Y I = P.beta2SLSPopulationBridge I

Proof (Lean source)

theorem observedBeta2SLS_eq_beta2SLSPopulationBridge (B : ObservedBridge μ Z D Y I P) [IsFiniteMeasure μ] (hZ : Measurable Z) (hYInt : Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ) (hDInt : Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ) : observedBeta2SLS μ Z D Y I = P.beta2SLSPopulationBridge I := by unfold observedBeta2SLS beta2SLSPopulationBridge rw [B.observedReducedFormMoment_eq_reducedFormMoment hZ hYInt, B.observedFirstStageMoment_eq_firstStageMoment hZ hDInt]

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.ObservedBridge.observedBeta2SLS_eq_beta2SLSPopulationBridge · Causalean/PO/ID/Exact/MultipleInstrumentIV/Population.lean:240

Main 7 core · 2 supporting This file provides the public finite-support facade for the Mogstad-Torgovitsky-Walters multiple-instrument characterization. ★ beta2SLSFiniteAlgebra_eq_signedAdjacentRatio★ beta2SLSPopulationBridge_eq_signedAdjacentRatio★ beta2SLSPopulationBridge_eq_responseTypeWeightedSum★ beta2SLSPopulationBridge_eq_positiveResponseTypeAverage★ observedBeta2SLS_eq_responseTypeWeightedSum

Multiple-Instrument IV Main Facade

This file provides the public finite-support facade for the Mogstad-Torgovitsky-Walters multiple-instrument characterization. It exposes the signed adjacent ratio, the response-type weighted-sum form, positivity under sign alignment, and the corresponding population bridge statements.

def signedAdjacentNumerator reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

For an ordered finite first-stage index and finite response-type statistics, the signed adjacent reduced-form numerator is the sum of each within-type causal effect multiplied by its unnormalized response-type weight.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

R :

shared

def

signedAdjacentNumerator I R :

ℝ

given by

∑ g : ResponseType K, R.unnormTypeWeight I g * R.effect g

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.signedAdjacentNumerator · Causalean/PO/ID/Exact/MultipleInstrumentIV/Main.lean:36 · uses FiniteIndex , ResponseTypeStats

def signedAdjacentDenominator reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

For an ordered finite first-stage index and finite response-type statistics, the signed adjacent first-stage denominator is the sum of all unnormalized response-type weights.

Definition (Lean source)

parameters

K :

ℕ

shared

I :

shared

R :

shared

def

signedAdjacentDenominator I R :

ℝ

given by

R.typeWeightDenom I

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.signedAdjacentDenominator · Causalean/PO/ID/Exact/MultipleInstrumentIV/Main.lean:40 · uses FiniteIndex , ResponseTypeStats

theorem beta2SLSFiniteAlgebra_eq_signedAdjacentRatio reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats

Finite response-type ratio as signed adjacent ratio. Provided the signed adjacent first-stage denominator is nonzero, the finite-algebra MTW estimand beta2SLSFiniteAlgebra equals the signed adjacent numerator Σ_g λ_g Δ_g divided by the signed adjacent denominator Σ_g λ_g.

Formal statement

hypotheses

K :

ℕ

shared

I :

shared

R :

shared

_hden :

R.signedAdjacentDenominator I ≠ 0

conclusion

R.beta2SLSFiniteAlgebra I = R.signedAdjacentNumerator I / R.signedAdjacentDenominator I

Proof (Lean source)

theorem beta2SLSFiniteAlgebra_eq_signedAdjacentRatio (_hden : R.signedAdjacentDenominator I ≠ 0) : R.beta2SLSFiniteAlgebra I = R.signedAdjacentNumerator I / R.signedAdjacentDenominator I := by rfl

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.beta2SLSFiniteAlgebra_eq_signedAdjacentRatio · Causalean/PO/ID/Exact/MultipleInstrumentIV/Main.lean:44 · uses FiniteIndex , ResponseTypeStats , beta2SLSFiniteAlgebra , signedAdjacentDenominator , signedAdjacentNumerator

theorem beta2SLSPopulationBridge_eq_signedAdjacentRatio reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

Signed adjacent ratio form (population bridge). Provided the signed adjacent first-stage denominator is nonzero, the population- bridge 2SLS estimand equals the signed adjacent numerator divided by the signed adjacent denominator.

Formal statement

hypotheses

K :

ℕ

shared

I :

shared

P :

shared

hden :

P.stats.signedAdjacentDenominator I ≠ 0

conclusion

P.beta2SLSPopulationBridge I

= P.stats.signedAdjacentNumerator I / P.stats.signedAdjacentDenominator I

Proof (Lean source)

theorem beta2SLSPopulationBridge_eq_signedAdjacentRatio (hden : P.stats.signedAdjacentDenominator I ≠ 0) : P.beta2SLSPopulationBridge I = P.stats.signedAdjacentNumerator I / P.stats.signedAdjacentDenominator I := by rw [P.beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra I] exact P.stats.beta2SLSFiniteAlgebra_eq_signedAdjacentRatio I hden

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.beta2SLSPopulationBridge_eq_signedAdjacentRatio

· Causalean/PO/ID/Exact/MultipleInstrumentIV/Main.lean:82 · uses FiniteIndex , PopulationBridge , beta2SLSPopulationBridge , signedAdjacentDenominator , signedAdjacentNumerator

theorem beta2SLSPopulationBridge_eq_responseTypeWeightedSum reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

Response-type weighted-sum form (population bridge). Provided the first-stage type-weight denominator is nonzero, the population- bridge 2SLS estimand equals the response-type-weighted sum Σ_g ω_g Δ_g of within-type causal effects.

Formal statement

hypotheses

K :

ℕ

shared

I :

shared

P :

shared

hden :

P.stats.typeWeightDenom I ≠ 0

conclusion

P.beta2SLSPopulationBridge I = P.stats.responseTypeEstimand I

Proof (Lean source)

theorem beta2SLSPopulationBridge_eq_responseTypeWeightedSum (hden : P.stats.typeWeightDenom I ≠ 0) : P.beta2SLSPopulationBridge I = P.stats.responseTypeEstimand I := by rw [P.beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra I] exact P.stats.beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum I hden

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.beta2SLSPopulationBridge_eq_responseTypeWeightedSum

· Causalean/PO/ID/Exact/MultipleInstrumentIV/Main.lean:93 · uses FiniteIndex , PopulationBridge , beta2SLSPopulationBridge , responseTypeEstimand , typeWeightDenom

theorem beta2SLSPopulationBridge_eq_positiveResponseTypeAverage reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge

Positive response-type average (population bridge). When the response types are sign-aligned with the instrument order and the first-stage type-weight denominator is strictly positive, the population-bridge 2SLS estimand beta2SLSPopulationBridge equals the response-type estimand, its normalized response-type weights are all nonnegative, and those weights sum to one.

Formal statement

hypotheses

K :

ℕ

shared

I :

shared

P :

shared

hAlign :

P.stats.SignAligned I

hden :

0 < P.stats.typeWeightDenom I

conclusion

conclusion 1

P.beta2SLSPopulationBridge I = P.stats.responseTypeEstimand I

conclusion 2

g :

0 ≤ P.stats.normalizedTypeWeight I g

conclusion 3

∑ g : ResponseType K, P.stats.normalizedTypeWeight I g = 1

Proof (Lean source)

theorem beta2SLSPopulationBridge_eq_positiveResponseTypeAverage (hAlign : P.stats.SignAligned I) (hden : 0 < P.stats.typeWeightDenom I) : P.beta2SLSPopulationBridge I = P.stats.responseTypeEstimand I ∧ (∀ g : ResponseType K, 0 ≤ P.stats.normalizedTypeWeight I g) ∧ (∑ g : ResponseType K, P.stats.normalizedTypeWeight I g = 1) := by rw [P.beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra I] exact P.stats.beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage I hAlign hden

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.beta2SLSPopulationBridge_eq_positiveResponseTypeAverage

· Causalean/PO/ID/Exact/MultipleInstrumentIV/Main.lean:103 · uses FiniteIndex , ResponseType , PopulationBridge , beta2SLSPopulationBridge , SignAligned , normalizedTypeWeight , responseTypeEstimand , typeWeightDenom

theorem observedBeta2SLS_eq_responseTypeWeightedSum reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.ObservedBridge

End-to-end corollary (prop:po-estimand-mtw-response-type-form, observed level). Given a bridge B linking the data-generating instrument, treatment, and outcome to the response-type population, provided the instrument is measurable, the centered-instrument-weighted outcome is integrable, the centered-instrument-weighted treatment is integrable, and the observed first-stage moment observedFirstStageMoment μ Z D I is nonzero, the observed population 2SLS ratio equals the response-type weighted sum of within-type causal effects.

Formal statement

hypotheses

Ω :

Type u_1

shared

K :

ℕ

shared

μ :

shared

Z :

Ω → Fin K

shared

D :

Ω → Bool

shared

Y :

Ω → ℝ

shared

I :

shared

P :

shared

B :

ObservedBridge μ Z D Y I P

IsFiniteMeasure μ

hZ :

Measurable Z

hYInt :

Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ

hDInt :

Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ

hden :

observedFirstStageMoment μ Z D I ≠ 0

conclusion

observedBeta2SLS μ Z D Y I = P.stats.responseTypeEstimand I

Proof (Lean source)

theorem observedBeta2SLS_eq_responseTypeWeightedSum (B : ObservedBridge μ Z D Y I P) [IsFiniteMeasure μ] (hZ : Measurable Z) (hYInt : Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ) (hDInt : Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ) (hden : observedFirstStageMoment μ Z D I ≠ 0) : observedBeta2SLS μ Z D Y I = P.stats.responseTypeEstimand I := by -- Step 1: observed → finite algebra have h1 : observedBeta2SLS μ Z D Y I = P.stats.beta2SLSFiniteAlgebra I := B.observedBeta2SLS_eq_beta2SLSFiniteAlgebra hZ hYInt hDInt -- Step 2: the observed denominator equals typeWeightDenom have hden' : P.stats.typeWeightDenom I ≠ 0 := by rwa [← P.firstStageMoment_eq_typeWeightDenom I, ← B.observedFirstStageMoment_eq_firstStageMoment hZ hDInt] -- Step 3: finite algebra → response-type weighted sum rw [h1] exact P.stats.beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum I hden'

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge.ObservedBridge.observedBeta2SLS_eq_responseTypeWeightedSum

· Causalean/PO/ID/Exact/MultipleInstrumentIV/Main.lean:129 · uses FiniteIndex , centeredIndex , PopulationBridge , ObservedBridge , observedBeta2SLS , observedFirstStageMoment , responseTypeEstimand , boolToReal

2 supporting declarations (lemmas, instances)

beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum' theorem — Response-type weighted-sum form of the finite MTW algebra (prop:po-estimand-mtw-response-type-form, finite algebra layer).

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

R :

ResponseTypeStats K
shared

hden :

R.typeWeightDenom I ≠ 0

conclusion

R.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I

Proof (Lean source)

theorem beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum' (hden : R.typeWeightDenom I ≠ 0) : R.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I := by exact R.beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum I hden

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum' · Causalean/PO/ID/Exact/MultipleInstrumentIV/Main.lean:58
beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage' theorem — Positive response-type average under MTW sign alignment and a positive finite first-stage denominator (prop:po-estimand-mtw-positive-weights, finite algebra layer).

hypotheses

K :

ℕ
shared

I :

FiniteIndex K
shared

R :

ResponseTypeStats K
shared

hAlign :

R.SignAligned I

hden :

0 < R.typeWeightDenom I

conclusion

conclusion 1
R.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I
conclusion 2

g :

ResponseType K

0 ≤ R.normalizedTypeWeight I g
conclusion 3
∑ g : ResponseType K, R.normalizedTypeWeight I g = 1

Proof (Lean source)

theorem beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage' (hAlign : R.SignAligned I) (hden : 0 < R.typeWeightDenom I) : R.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I ∧ (∀ g : ResponseType K, 0 ≤ R.normalizedTypeWeight I g) ∧ (∑ g : ResponseType K, R.normalizedTypeWeight I g = 1) := by exact R.beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage I hAlign hden

Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage' · Causalean/PO/ID/Exact/MultipleInstrumentIV/Main.lean:65

POBridge 27 core · 24 supporting This file grounds the MTW multiple-instrument finite algebra in a potential-outcome system. ★ POMultipleIVSystem★ observedBeta2SLS_eq_responseTypeWeightedSum

Multiple-Instrument IV Potential-Outcome Bridge

This file grounds the MTW multiple-instrument finite algebra in a potential-outcome system. The structure POMultipleIVSystem records a finite instrument, binary treatment, and real outcome; responseType, mass, effect, toStats, and toPopulationBridge turn its counterfactual response types into the finite response-type algebra.

The bridge lemmas treatmentDrop and outcomeDrop derive instrument-cell conditional means from consistency and instrument independence. The definitions toObservedBridge and theorem observedBeta2SLS_eq_responseTypeWeightedSum assemble those derived cell identities into the observed MTW 2SLS characterization.

structure POMultipleIVSystem reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV

Multiple-instrument IV potential-outcome subsystem. Inside a potential-outcome system, this bundles a node serving as the instrument, taking values in a finite support of size K, a node serving as the binary treatment, and a node serving as the real-valued outcome, subject to the instrument, treatment, and outcome being pairwise distinct nodes. This is the Fin K generalization of PO.POIVSystem.

Definition (Lean source)

parameters

P :

K :

ℕ

fields

Instrument node.

Z :

P.V

Treatment node.

D :

P.V

Outcome node.

Y :

P.V

The instrument value space is a `Fin K` support.

hZfin :

P.X Z ≃ᵐ Fin K

The treatment is binary.

hDbool :

P.X D ≃ᵐ Bool

The outcome is real.

hYreal :

P.X Y ≃ᵐ ℝ

The instrument and treatment are distinct nodes.

hZD :

Z ≠ D

The treatment and outcome are distinct nodes.

hDY :

D ≠ Y

The instrument and outcome are distinct nodes.

hZY :

Z ≠ Y

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:61 · uses POSystem

def zVar reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , and a multiple-instrument IV subsystem, the instrument variable is that subsystem's instrument represented as a potential-outcome variable with the stated finite support.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

def

zVar S :

POVar P (Fin K)

given by

⟨S.Z, S.hZfin⟩

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.zVar · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:91 · uses POMultipleIVSystem , POSystem , POVar

def dVar reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , and a multiple-instrument IV subsystem, the treatment variable is that subsystem's binary treatment represented as a potential-outcome variable.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

def

dVar S :

POVar P Bool

given by

⟨S.D, S.hDbool⟩

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.dVar · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:94 · uses POMultipleIVSystem , POSystem , POVar

def yVar reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , and a multiple-instrument IV subsystem, the outcome variable is that subsystem's real-valued outcome represented as a potential-outcome variable.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

def

yVar S :

POVar P ℝ

given by

⟨S.Y, S.hYreal⟩

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.yVar · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:97 · uses POMultipleIVSystem , POSystem , POVar

def DofZ reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and an instrument support point, the potential treatment maps each unit to its binary treatment were the instrument fixed at that point.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

k :

Fin K

def

DofZ S k :

P.Ω → Bool

given by

S.dVar.cfUnder S.zVar k

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.DofZ · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:100 · uses POMultipleIVSystem , POSystem

def YofD reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and a binary treatment value, the potential outcome maps each unit to its real outcome were treatment fixed at that value.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

d :

Bool

def

YofD S d :

P.Ω → ℝ

given by

S.yVar.cfUnder S.dVar d

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.YofD · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:103 · uses POMultipleIVSystem , POSystem

def factualZ reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , and a multiple-instrument IV subsystem, the factual instrument maps each unit to its observed instrument value.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

def

factualZ S :

P.Ω → Fin K

given by

S.zVar.factual

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.factualZ · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:106 · uses POMultipleIVSystem , POSystem

def factualD reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , and a multiple-instrument IV subsystem, the factual treatment maps each unit to its observed binary treatment.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

def

factualD S :

P.Ω → Bool

given by

S.dVar.factual

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.factualD · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:109 · uses POMultipleIVSystem , POSystem

def factualY reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , and a multiple-instrument IV subsystem, the factual outcome maps each unit to its observed real-valued outcome.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

def

factualY S :

P.Ω → ℝ

given by

S.yVar.factual

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.factualY · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:112 · uses POMultipleIVSystem , POSystem

def responseType reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , and a multiple-instrument IV subsystem, the response-type map assigns each unit the binary vector of its potential treatments at every instrument support point.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

def

responseType S :

P.Ω → ResponseType K

given by

fun ω k => S.DofZ k ω

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.responseType · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:115 · uses POMultipleIVSystem , ResponseType , POSystem

def gEvent reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and a response type, the response-type event is the set of units whose vector of potential treatments equals that response type.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

g :

def

gEvent S g :

Set P.Ω

given by

S.responseType ⁻¹' {g}

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.gEvent · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:118 · uses POMultipleIVSystem , ResponseType , POSystem

def zEvent reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and an instrument support point, the instrument cell is the set of units whose factual instrument equals that point.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

k :

Fin K

def

zEvent S k :

Set P.Ω

given by

S.zVar.event k

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.zEvent · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:121 · uses POMultipleIVSystem , POSystem

def YofDofZ reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and an instrument support point, the potential outcome under the induced treatment gives each unit's treated potential outcome if that instrument point induces treatment and its untreated potential outcome otherwise.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

k :

Fin K

def

YofDofZ S k :

P.Ω → ℝ

given by

fun ω => if S.DofZ k ω then S.YofD true ω else S.YofD false ω

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.YofDofZ · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:124 · uses POMultipleIVSystem , POSystem

def dUnderZ reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and an instrument support point, the regimed treatment variable represents treatment under an intervention fixing the instrument at that point.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

k :

Fin K

def

dUnderZ S k :

RegimedVar P Bool

given by

⟨S.dVar, Regime.single S.Z (S.hZfin.symm k)⟩

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.dUnderZ · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:136 · uses POMultipleIVSystem , POSystem , RegimedVar

def yUnderD reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and a binary treatment value, the regimed outcome variable represents outcome under an intervention fixing treatment at that value.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

d :

Bool

def

yUnderD S d :

RegimedVar P ℝ

given by

⟨S.yVar, Regime.single S.D (S.hDbool.symm d)⟩

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.yUnderD · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:140 · uses POMultipleIVSystem , POSystem , RegimedVar

def cfCell reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and an instrument support point, the counterfactual cell bundles the potential treatment at that point with the treated and untreated potential outcomes.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

k :

Fin K

def

cfCell S k :

POCFBundle P

given by

POCFBundle.cons (S.dUnderZ k) <| POCFBundle.cons (S.yUnderD true) <| POCFBundle.cons (S.yUnderD false) <| POCFBundle.nil P

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.cfCell · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:144 · uses POMultipleIVSystem , POCFBundle , POSystem

structure Assumptions reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

Classical multi-instrument IV assumption bundle (ass:po-estimand-mtw-iv-validity). For a multiple-instrument potential-outcome subsystem, this packages the observed treatment and outcome equaling the potential treatment and outcome realized under the actual instrument value (SUTVA), and at each instrument support point, the instrument being independent of the counterfactual triple consisting of the potential treatment under that instrument value together with the two treatment-arm potential outcomes (IV exogeneity).

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

assumes

consistency :

P.Consistency

Consistency (SUTVA): observed D/Y equal the realized potential treatment/outcome.

instrumentIndep :

∀ k : Fin K, P.IndepCF (RegimedVar.ofFactual S.zVar) (S.cfCell k) P.μ

Instrument independence (IV exogeneity): for each support point, the instrument is independent of the counterfactual cell (D(zᵏ), Y(1), Y(0)). This is implied by (and weaker than) full joint independence of Z from all potential outcomes; it is exactly what the cell-conditional-mean derivations below consume.

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.Assumptions · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:197 · uses POMultipleIVSystem , POSystem

def mass reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and a response type, the response-type mass is the probability that a unit has that response type.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

g :

def

mass S g :

ℝ

given by

(P.μ (S.gEvent g)).toReal

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.mass · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:374 · uses POMultipleIVSystem , ResponseType , POSystem

def effect reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, and a response type, the within-type causal effect is the conditional expectation of the treated-minus-untreated potential outcome among units of that type.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

g :

def

effect S g :

ℝ

given by

eventCondExp P.μ (S.gEvent g) (fun ω => S.YofD true ω - S.YofD false ω)

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.effect · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:377 · uses POMultipleIVSystem , ResponseType , POSystem

def z0 reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support size $K$ , a multiple-instrument IV subsystem, and the condition $K>0$ , the reference support point is the first point of the support.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

_S :

hK :

0 < K

def

z0 _S hK :

Fin K

given by

⟨0, hK⟩

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.z0 · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:381 · uses POMultipleIVSystem , POSystem

def baseOutcome reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support size $K$ , a multiple-instrument IV subsystem, the condition $K>0$ , and a response type, the baseline response-type outcome is the conditional expectation, within that type, of the potential outcome under treatment induced by the first instrument support point.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

hK :

0 < K

g :

def

baseOutcome S hK g :

ℝ

given by

eventCondExp P.μ (S.gEvent g) (S.YofDofZ (S.z0 hK))

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.baseOutcome · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:384 · uses POMultipleIVSystem , ResponseType , POSystem

def baseTreatment reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support size $K$ , a multiple-instrument IV subsystem, and the condition $K>0$ , the baseline treatment mean is the expectation of treatment induced by the first instrument support point.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

hK :

0 < K

def

baseTreatment S hK :

ℝ

given by

∫ ω, boolToReal (S.DofZ (S.z0 hK) ω) ∂P.μ

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.baseTreatment · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:388 · uses POMultipleIVSystem , POSystem

def toStats reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , and a multiple-instrument IV subsystem, the finite response-type statistics consist of the subsystem's response-type masses and within-type causal effects.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

def

toStats S :

given by

clause 1

mass := S.mass

clause 2

effect := S.effect

clause 3

mass_nonneg := S.mass_nonneg

clause 4

mass_sum_one := S.mass_sum_one

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.toStats · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:414 · uses POMultipleIVSystem , ResponseTypeStats , POSystem

def toPopulationBridge reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support size $K$ , a multiple-instrument IV subsystem, and the condition $K>0$ , the saturated finite-support population bridge is assembled from its response-type statistics and baseline quantities.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

hK :

0 < K

def

toPopulationBridge S hK :

ResponseTypeStats.PopulationBridge K

given by

clause 1

stats := S.toStats

clause 2

baseOutcome := S.baseOutcome hK

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.toPopulationBridge · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:421 · uses POMultipleIVSystem , PopulationBridge , POSystem

def toFiniteIndex reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support of size $K$ , a multiple-instrument IV subsystem, a real first-stage score at each support point, and the condition that this score is weakly increasing in support order, the ordered finite first-stage index has the subsystem's instrument probabilities and the supplied score.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

dhat :

Fin K → ℝ

hmono :

∀ {k l : Fin K}

k.val ≤ l.val

then

dhat k ≤ dhat l

def

toFiniteIndex S dhat hmono :

given by

FiniteIndex.fromMeasureScore P.μ S.factualZ S.measurable_factualZ dhat hmono

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.toFiniteIndex · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:426 · uses FiniteIndex , POMultipleIVSystem , POSystem

def toObservedBridge reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

For a potential-outcome system, a finite instrument support size $K$ , a multiple-instrument IV subsystem, the condition $K>0$ , its IV assumptions, a real first-stage score, weak monotonicity of that score in support order, positive probability for every instrument cell, and integrable treated and untreated potential outcomes, the observed population bridge links factual variables to the finite response-type representation.

Definition (Lean source)

parameters

P :

shared

K :

ℕ

shared

S :

shared

hK :

0 < K

hA :

S.Assumptions

dhat :

Fin K → ℝ

hmono :

∀ {k l : Fin K}

k.val ≤ l.val

then

dhat k ≤ dhat l

hZpos :

∀ k : Fin K, P.μ (S.zEvent k) ≠ 0

hY1 :

Integrable (S.YofD true) P.μ

hY0 :

Integrable (S.YofD false) P.μ

def

toObservedBridge S hK hA dhat hmono hZpos hY1 hY0 :

ResponseTypeStats.PopulationBridge.ObservedBridge P.μ S.factualZ S.factualD S.factualY (S.toFiniteIndex dhat hmono) (S.toPopulationBridge hK)

given by

clause 1

isProbability := P.isProb

clause 2

rho_eq_zMass := S.rho_eq_zMass dhat hmono

clause 3

outcome_cell := fun k => S.outcome_cell_eq hK hA k (hZpos k) hY1 hY0

clause 4

baseTreatment := S.baseTreatment hK

clause 5

treatment_cell := fun k => S.treatment_cell_eq hK hA k (hZpos k)

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem.toObservedBridge · Causalean/PO/ID/Exact/MultipleInstrumentIV/POBridge.lean:636 · uses POMultipleIVSystem , Assumptions , YofD , factualD , factualY , factualZ , toFiniteIndex , toPopulationBridge , zEvent , ObservedBridge , POSystem

theorem observedBeta2SLS_eq_responseTypeWeightedSum reviewed

Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem

Potential-outcome multiple-IV 2SLS characterization (prop:po-estimand-mtw-response-type-form, PO level). Consider a finite instrument support of positive size K together with weights dhat that are weakly increasing in the support order, under the potential-outcome identifying assumption bundle. If every instrument-support cell has positive probability, the potential outcome under treatment and under control are integrable, the centered-instrument-weighted outcome and treatment are integrable, and the observed first-stage moment is nonzero, then the observed population 2SLS ratio E[h(Z)Y] / E[h(Z)D] equals the response-type weighted sum Σ_g ω_g Δ_g of within-type conditional causal effects Δ_g = E[Y(1) - Y(0) | G = g].

Formal statement

hypotheses

P :

shared

K :

ℕ

shared

S :