PO.ID.Exact.MultipleInstrumentIV
Multiple-instrument IV: Mogstad-Torgovitsky-Walters finite-support 2SLS response-type algebra and sign-alignment results.
FiniteIndex 16 core · 5 supporting This file develops the finite ordered-index algebra used in the Mogstad-Torgovitsky-Walters multiple-instrument characterization. ★ tailCoeff_nonneg★ tailCoeff_eq_cov
Multiple-Instrument IV Finite Index Algebra
This file develops the finite ordered-index algebra used in the Mogstad-Torgovitsky-Walters multiple-instrument characterization. It defines support masses, ordered first-stage indices, centered instruments, tail coefficients, and the finite matrix identities that underlie the signed decomposition.
abbrev Adj reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV
Adjacent threshold for the ordered support. The value j : Adj K represents the source-paper threshold between support positions j-1 and j in zero-based Lean indexing, i.e. source notation 2, ..., K.
structure FiniteIndex reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV
A finite ordered first-stage index for the saturated multiple-instrument characterization: instrument support masses that are nonnegative and sum to one, together with a first-stage index that is weakly increasing in the displayed support order.
Definition (Lean source)
parameters
K :
ℕ
fields
Instrument support mass `ρ_k`.
rho :
Fin K → ℝ
Ordered saturated first-stage index `dhat_k`.
dhat :
Fin K → ℝ
Support masses are nonnegative.
rho_nonneg :
∀ k, 0 ≤ rho k
Support masses sum to one.
rho_sum_one :
∑ k, rho k = 1
The displayed support order is weakly increasing in the first-stage index.
dhat_mono :
∀ {k l : Fin K}
if
k.val ≤ l.val
then
dhat k ≤ dhat l
def supportMass reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV
Measure-backed finite support mass P(Z = k) for a Fin K-valued instrument.
Definition (Lean source)
noncomputable def supportMass {Ω : Type*} [MeasurableSpace Ω] {K : ℕ}
(μ : Measure Ω) (Z : Ω → Fin K) (k : Fin K) : ℝ :=
(μ {ω | Z ω = k}).toReal
def fromMeasureScore reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex
Construct the ordered finite first-stage index from a probability-space instrument Z : Ω → Fin K and a finite support score dhat. The support masses are the actual measure masses P(Z = k); the only remaining first-stage input is the displayed-order monotonicity of the score.
Definition (Lean source)
noncomputable def FiniteIndex.fromMeasureScore {Ω : Type*} [MeasurableSpace Ω]
{K : ℕ} (μ : Measure Ω) [IsProbabilityMeasure μ]
(Z : Ω → Fin K) (hZ : Measurable Z)
(dhat : Fin K → ℝ)
(hdhat_mono : ∀ {k l : Fin K}, k.val ≤ l.val → dhat k ≤ dhat l) :
FiniteIndex K where
rho := supportMass μ Z
dhat := dhat
rho_nonneg := supportMass_nonneg μ Z
rho_sum_one := supportMass_sum_eq_one μ Z hZ
dhat_mono := hdhat_mono
def meanIndex reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex
Mean first-stage index dbar = Σ_k ρ_k dhat_k.
Definition (Lean source)
noncomputable def meanIndex : ℝ :=
∑ k, I.rho k * I.dhat k
def centeredIndex reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex
Centered first-stage index a_k = dhat_k - dbar.
Definition (Lean source)
noncomputable def centeredIndex (k : Fin K) : ℝ :=
I.dhat k - I.meanIndex
def upperTail reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex
Ordered upper tail T_j = {j, ..., K} for an adjacent threshold.
def tailCoeff reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.FiniteIndex
MTW tail coefficient B_j = Σ_{k ≥ j} ρ_k a_k.
theorem tailCoeff_nonneg reviewed
⚑ flagged
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
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
theorem tailCoeff_eq_cov reviewed
⚑ flagged
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
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
def firstStageGram reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV
Finite second-moment matrix E[q(Z)q(Z)ᵀ] for a score vector on finite instrument support.
structure MatrixFirstStage reviewed
⚑ flagged
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ᵏ)`.
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}
if
k.val ≤ l.val
then
def gram reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage
Finite second-moment matrix E[q(Z)q(Z)ᵀ].
Definition (Lean source)
def projectionCoeff reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage
Population first-stage projection coefficient (E[q(Z)q(Z)ᵀ])⁻¹ E[q(Z)D].
Definition (Lean source)
noncomputable def projectionCoeff (a : Fin L) : ℝ :=
∑ b : Fin L, (⅟S.gram) a b * S.firstStageMoment b
def fittedValue reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage
Fitted saturated first-stage value dhat_k = q(zᵏ)'Π.
def toFiniteIndex reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.MatrixFirstStage
The matrix first stage induces the ordered finite index consumed by the MTW tail-coefficient and response-type algebra.
Definition (Lean source)
noncomputable def toFiniteIndex : FiniteIndex K where
rho := S.rho
dhat := S.fittedValue
rho_nonneg := S.rho_nonneg
rho_sum_one := S.rho_sum_one
dhat_mono := by
intro k l hkl
simp only [fittedValue, projectionCoeff, gram]
exact S.fitted_mono hkl
5 supporting declarations (lemmas, instances)
-
supportMass_nonnegtheorem — Support masses obtained from a measure are nonnegative.hypothesesconclusion0 ≤ supportMass μ Z kProof (Lean source)
theorem supportMass_nonneg {Ω : Type*} [MeasurableSpace Ω] {K : ℕ} (μ : Measure Ω) (Z : Ω → Fin K) (k : Fin K) : 0 ≤ supportMass μ Z k := by exact ENNReal.toReal_nonneg -
supportMass_sum_eq_onetheorem — For a probability measure, the finite support masses induced by Z sum to one.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 -
centered_weight_sum_zerotheorem — Centering identity Σ_k ρ_k (dhat_k - dbar) = 0.conclusion∑ k, I.rho k * I.centeredIndex k = 0Proof (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] -
tail_sum_interchangetheorem — 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.hypothesesx :Adj K → ℝ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] -
instInvertibleGraminstance — The finite second-moment matrix is invertible by the matrix first-stage assumption.noncomputable instance instInvertibleGram : Invertible S.gram := by change Invertible (firstStageGram S.rho S.score) exact S.gram_invertible
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
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV
A response type is the binary vector g = (D(z^1), ..., D(z^K)).
Definition (Lean source)
def boolToReal reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV
Coerce a binary treatment indicator to the real values 0 and 1.
Definition (Lean source)
def boolToReal (b : Bool) : ℝ :=
if b then 1 else 0
def typeStep reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV
Adjacent response increment d_j - d_{j-1} for a response type.
Definition (Lean source)
def typeStep {K : ℕ} (g : ResponseType K) (j : Adj K) : ℝ :=
boolToReal (g (Adj.upper j)) - boolToReal (g (Adj.lower j))
structure ResponseTypeStats reviewed
⚑ flagged
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
def unnormTypeWeight reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats
Unnormalized MTW response-type weight λ_g = π_g Σ_j B_j (d_j - d_{j-1}).
Definition (Lean source)
noncomputable def unnormTypeWeight (g : ResponseType K) : ℝ :=
R.mass g * ∑ j : Adj K, I.tailCoeff j * typeStep g j
def typeWeightDenom reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats
First-stage denominator in response-type form, Σ_g λ_g.
Definition (Lean source)
noncomputable def typeWeightDenom : ℝ :=
∑ g : ResponseType K, R.unnormTypeWeight I g
def normalizedTypeWeight reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats
Normalized response-type weight ω_g = λ_g / Σ_g' λ_g'.
Definition (Lean source)
noncomputable def normalizedTypeWeight (g : ResponseType K) : ℝ :=
normalizedWeight (R.unnormTypeWeight I) g
def responseTypeEstimand reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats
Signed response-type weighted estimand Σ_g ω_g Δ_g.
Definition (Lean source)
noncomputable def responseTypeEstimand : ℝ :=
∑ g : ResponseType K, R.normalizedTypeWeight I g * R.effect g
def beta2SLSFiniteAlgebra reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats
Finite-algebra ratio after the MTW response-type partition: numerator Σ_g λ_g Δ_g, denominator Σ_g λ_g. The saturated finite-support population bridge below proves when the population 2SLS moment ratio reduces to this finite algebraic ratio.
Definition (Lean source)
noncomputable def beta2SLSFiniteAlgebra : ℝ :=
(∑ g : ResponseType K, R.unnormTypeWeight I g * R.effect g) /
R.typeWeightDenom I
structure PopulationBridge reviewed
⚑ flagged
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 → ℝ
def telescopedTypeStep reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Telescoped adjacent treatment response for support point k, i.e. Σ_{j≤k} (d_j - d_{j-1}) in zero-based Lean indexing.
Definition (Lean source)
noncomputable def telescopedTypeStep (g : ResponseType K) (k : Fin K) : ℝ :=
∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0
def outcomeAtSupport reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Response-type expansion of the potential outcome at support point k after consistency, exogeneity, and exclusion have replaced conditioning on Z = zᵏ by response-type averages.
Definition (Lean source)
noncomputable def outcomeAtSupport (P : PopulationBridge K) (k : Fin K) : ℝ :=
∑ g : ResponseType K,
P.stats.mass g *
(P.baseOutcome g + telescopedTypeStep g k * P.stats.effect g)
def treatmentAtSupport reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Response-type expansion of the potential treatment at support point k, written in the baseline-subtracted telescoped form used by the centered-index argument.
Definition (Lean source)
noncomputable def treatmentAtSupport (P : PopulationBridge K) (k : Fin K) : ℝ :=
∑ g : ResponseType K, P.stats.mass g * telescopedTypeStep g k
def reducedFormMoment reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Population reduced-form moment E[h(Z)Y] after the finite-support identification reductions.
Definition (Lean source)
noncomputable def reducedFormMoment (P : PopulationBridge K) (I : FiniteIndex K) : ℝ :=
∑ k : Fin K, I.rho k * I.centeredIndex k * P.outcomeAtSupport k
def firstStageMoment reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Population first-stage moment E[h(Z)D] after the same finite-support identification reductions.
Definition (Lean source)
noncomputable def firstStageMoment (P : PopulationBridge K) (I : FiniteIndex K) : ℝ :=
∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k
def beta2SLSPopulationBridge reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Population multiple-IV 2SLS ratio in the saturated finite-support bridge.
Definition (Lean source)
noncomputable def beta2SLSPopulationBridge (P : PopulationBridge K) (I : FiniteIndex K) : ℝ :=
P.reducedFormMoment I / P.firstStageMoment I
theorem beta2SLSPopulationBridge_eq_beta2SLSFiniteAlgebra reviewed
⚑ flagged
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
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]
def SignAligned reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats
MTW sign alignment: every positive-mass response type has a nonnegative tail-weighted step contrast.
Definition (Lean source)
def SignAligned : Prop :=
∀ g : ResponseType K, 0 < R.mass g →
0 ≤ ∑ j : Adj K, I.tailCoeff j * typeStep g j
structure ComponentwiseMonotoneRestriction reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats
Opaque response-type restriction interface.
Definition (Lean source)
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
theorem beta2SLSFiniteAlgebra_eq_responseTypeWeightedSum reviewed
⚑ flagged
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
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]
theorem beta2SLSFiniteAlgebra_eq_positiveResponseTypeAverage reviewed
⚑ flagged
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
hAlign :
R.SignAligned I
hden :
0 < R.typeWeightDenom I
conclusion
R.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I ∧
(∀ g : ResponseType K, 0 ≤ R.normalizedTypeWeight I g) ∧
(∑ 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
theorem exists_negativeNormalizedTypeWeight reviewed
⚑ flagged
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
0 < R.mass g ∧ 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
6 supporting declarations (lemmas, instances)
-
baselineMoment_eq_zerotheorem — The baseline outcome component vanishes because the first-stage index is centered.conclusion(∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g))= 0Proof (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 -
firstStageMoment_eq_typeWeightDenomtheorem — The finite-support first-stage moment is the response-type denominator. This is the denominator half of the MTW identification step.conclusionP.firstStageMoment I = P.stats.typeWeightDenom IProof (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)] -
reducedFormMoment_eq_typeWeightNumeratortheorem — The finite-support reduced-form moment is the response-type numerator. This is the numerator half of the MTW identification step.conclusionP.reducedFormMoment I= ∑ g : ResponseType K, P.stats.unnormTypeWeight I g * P.stats.effect gProof (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)] -
unnormTypeWeight_nonneg_of_signAlignedtheorem — Sign alignment and nonnegative type masses imply nonnegative unnormalized response-type weights.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] -
normalizedTypeWeight_nonneg_of_signAlignedtheorem — Normalized response-type weights are nonnegative when sign alignment holds and the denominator is positive (prop:po-estimand-mtw-positive-weights).hypothesesconclusion0 ≤ R.normalizedTypeWeight I gProof (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 -
normalizedTypeWeight_sum_eq_one_of_postheorem — Normalized response-type weights sum to one when the first-stage denominator is positive.hypotheseshden :0 < R.typeWeightDenom Iconclusion∑ g : ResponseType K, R.normalizedTypeWeight I g = 1Proof (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'
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
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Instrument cell {ω | Z ω = k}.
def observedReducedFormMoment reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Observed reduced-form moment E[h(Z)Y], where h(zᵏ) = dhat_k − Σ_l ρ_l dhat_l.
Definition (Lean source)
noncomputable def observedReducedFormMoment
(μ : Measure Ω) (Z : Ω → Fin K) (Y : Ω → ℝ) (I : FiniteIndex K) : ℝ :=
∫ ω, I.centeredIndex (Z ω) * Y ω ∂μ
def observedFirstStageMoment reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Observed first-stage moment E[h(Z)D], with binary treatment coerced to the real values 0 and 1.
Definition (Lean source)
noncomputable def observedFirstStageMoment
(μ : Measure Ω) (Z : Ω → Fin K) (D : Ω → Bool) (I : FiniteIndex K) : ℝ :=
∫ ω, I.centeredIndex (Z ω) * boolToReal (D ω) ∂μ
def observedBeta2SLS reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats.PopulationBridge
Source population 2SLS ratio E[h(Z)Y] / E[h(Z)D].
Definition (Lean source)
noncomputable def observedBeta2SLS
(μ : Measure Ω) (Z : Ω → Fin K) (D : Ω → Bool) (Y : Ω → ℝ)
(I : FiniteIndex K) : ℝ :=
observedReducedFormMoment μ Z Y I / observedFirstStageMoment μ Z D I
structure ObservedBridge reviewed
⚑ flagged
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
fields
The observed law is a probability measure, so the integrals below are
population expectations.
isProbability :
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
theorem observedBeta2SLS_eq_beta2SLSFiniteAlgebra reviewed
⚑ flagged
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
B :
ObservedBridge μ Z D Y I P
hZ :
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]
5 supporting declarations (lemmas, instances)
-
observedReducedFormMoment_eq_sum_eventCondExptheorem — Finite-support total-law rewrite of E[h(Z)Y] into instrument-cell conditional expectations.hypothesesconclusionobservedReducedFormMoment μ Z Y I= ∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * PO.eventCondExp μ (zEvent Z k) YProof (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 -
observedFirstStageMoment_eq_sum_eventCondExptheorem — Finite-support total-law rewrite of E[h(Z)D] into instrument-cell conditional expectations.hypothesesμ :Z :Ω → Fin KhZ :D :Ω → BoolI :hInt :Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μconclusionobservedFirstStageMoment μ 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 -
observedReducedFormMoment_eq_reducedFormMomenttheorem — The observed reduced-form moment equals the finite response-type reduced-form moment.hypothesesconclusionobservedReducedFormMoment μ Z Y I = P.reducedFormMoment IProof (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] -
observedFirstStageMoment_eq_firstStageMomenttheorem — The observed first-stage moment equals the finite response-type first-stage moment.hypothesesB :ObservedBridge μ Z D Y I PhZ :hInt :Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μconclusionobservedFirstStageMoment μ Z D I = P.firstStageMoment IProof (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 -
observedBeta2SLS_eq_beta2SLSPopulationBridgetheorem — Observed population 2SLS, written as E[h(Z)Y]/E[h(Z)D], equals the saturated finite-support population bridge ratio.hypothesesB :ObservedBridge μ Z D Y I PhZ :hYInt :Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μhDInt :Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μconclusionobservedBeta2SLS μ Z D Y I = P.beta2SLSPopulationBridge IProof (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]
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
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats
Signed adjacent reduced-form numerator in the finite response-type algebra: Σ_g λ_g Δ_g. This is the response-type counterpart of Σ_j B_j E[(Y(1)-Y(0)) Δ_jD].
Definition (Lean source)
noncomputable def signedAdjacentNumerator : ℝ :=
∑ g : ResponseType K, R.unnormTypeWeight I g * R.effect g
def signedAdjacentDenominator reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.ResponseTypeStats
Signed adjacent first-stage denominator in the finite response-type algebra: Σ_g λ_g, corresponding to Σ_j B_j E[Δ_jD].
Definition (Lean source)
noncomputable def signedAdjacentDenominator : ℝ :=
R.typeWeightDenom I
theorem beta2SLSFiniteAlgebra_eq_signedAdjacentRatio reviewed
⚑ flagged
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
_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
theorem beta2SLSPopulationBridge_eq_signedAdjacentRatio reviewed
⚑ flagged
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
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
theorem beta2SLSPopulationBridge_eq_responseTypeWeightedSum reviewed
⚑ flagged
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
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
theorem beta2SLSPopulationBridge_eq_positiveResponseTypeAverage reviewed
⚑ flagged
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
hAlign :
P.stats.SignAligned I
hden :
0 < P.stats.typeWeightDenom I
conclusion
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)
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
theorem observedBeta2SLS_eq_responseTypeWeightedSum reviewed
⚑ flagged
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
B :
ObservedBridge μ Z D Y I P
hZ :
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'
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).hypotheseshden :R.typeWeightDenom I ≠ 0conclusionR.beta2SLSFiniteAlgebra I = R.responseTypeEstimand IProof (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 -
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).hypotheseshAlign :R.SignAligned Ihden :0 < R.typeWeightDenom IconclusionR.beta2SLSFiniteAlgebra I = R.responseTypeEstimand I ∧(∀ g : ResponseType K, 0 ≤ R.normalizedTypeWeight I g) ∧(∑ 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
POBridge 27 core · 23 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
⚑ flagged
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
def zVar reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Instrument packaged as a POVar valued in Fin K.
def dVar reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Treatment packaged as a POVar valued in Bool.
def yVar reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Outcome packaged as a POVar valued in ℝ.
Definition (Lean source)
def yVar : POVar P ℝ := ⟨S.Y, S.hYreal⟩
def DofZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Potential treatment D(zᵏ) under fixing the instrument to support point k.
def YofD reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Potential outcome Y(d) under fixing the treatment to d.
Definition (Lean source)
def YofD (d : Bool) : P.Ω → ℝ := S.yVar.cfUnder S.dVar d
def factualZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Factual instrument Z.
Definition (Lean source)
def factualZ : P.Ω → Fin K := S.zVar.factual
def factualD reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Factual treatment D.
Definition (Lean source)
def factualD : P.Ω → Bool := S.dVar.factual
def factualY reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Factual outcome Y.
Definition (Lean source)
def factualY : P.Ω → ℝ := S.yVar.factual
def responseType reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Response type G(ω) = (D(z⁰)(ω), …, D(z^{K-1})(ω)), the vector of potential treatments across the instrument support.
Definition (Lean source)
def responseType : P.Ω → ResponseType K := fun ω k => S.DofZ k ω
def gEvent reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
The event {G = g} that a unit has response type g.
Definition (Lean source)
def zEvent reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
The instrument cell {Z = zᵏ}.
def YofDofZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Potential outcome under the treatment that instrument value zᵏ induces, Y(D(zᵏ)) = 1_{D(zᵏ)=1} Y(1) + 1_{D(zᵏ)=0} Y(0).
def dUnderZ reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Regimed variable D(zᵏ) (treatment under instrument set to zᵏ).
Definition (Lean source)
def yUnderD reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Regimed variable Y(d) (outcome under treatment set to d).
Definition (Lean source)
def yUnderD (d : Bool) : RegimedVar P ℝ :=
⟨S.yVar, Regime.single S.D (S.hDbool.symm d)⟩
def cfCell reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
The three-element counterfactual cell (D(zᵏ), Y(1), Y(0)) relevant to identifying the conditional means on {Z = zᵏ}. Coordinates: 0 ↦ D(zᵏ), 1 ↦ Y(1), 2 ↦ Y(0).
Definition (Lean source)
def cfCell (k : Fin K) : POCFBundle P :=
POCFBundle.cons (S.dUnderZ k) <|
POCFBundle.cons (S.yUnderD true) <|
POCFBundle.cons (S.yUnderD false) <|
POCFBundle.nil P
structure Assumptions reviewed
⚑ flagged
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
S :
fields
Consistency (SUTVA): observed `D`/`Y` equal the realized potential
treatment/outcome.
consistency :
P.Consistency
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.
instrumentIndep :
∀ k : Fin K, P.IndepCF (RegimedVar.ofFactual S.zVar) (S.cfCell k) P.μ
def mass reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Response-type mass π_g = P(G = g).
Definition (Lean source)
def mass (g : ResponseType K) : ℝ := (P.μ (S.gEvent g)).toReal
def effect reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Within-type conditional causal effect Δ_g = E[Y(1) - Y(0) | G = g].
Definition (Lean source)
def effect (g : ResponseType K) : ℝ :=
eventCondExp P.μ (S.gEvent g) (fun ω => S.YofD true ω - S.YofD false ω)
def z0 reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Reference support point z⁰ (requires 0 < K).
Definition (Lean source)
def baseOutcome reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Baseline response-type outcome E[Y(D(z⁰)) | G = g], the term the centered first-stage index cancels.
Definition (Lean source)
def baseOutcome (hK : 0 < K) (g : ResponseType K) : ℝ :=
eventCondExp P.μ (S.gEvent g) (S.YofDofZ (S.z0 hK))
def baseTreatment reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Baseline treatment mean E[D(z⁰)].
Definition (Lean source)
def baseTreatment (hK : 0 < K) : ℝ :=
∫ ω, boolToReal (S.DofZ (S.z0 hK) ω) ∂P.μ
def toStats reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Finite response-type statistics assembled from the PO system.
Definition (Lean source)
def toStats : ResponseTypeStats K where
mass := S.mass
effect := S.effect
mass_nonneg := S.mass_nonneg
mass_sum_one := S.mass_sum_one
def toPopulationBridge reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Saturated finite-support population bridge assembled from the PO system.
Definition (Lean source)
def toPopulationBridge (hK : 0 < K) : ResponseTypeStats.PopulationBridge K where
stats := S.toStats
baseOutcome := S.baseOutcome hK
def toFiniteIndex reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
Ordered finite index built from the instrument masses and a supplied saturated first-stage score.
Definition (Lean source)
def toFiniteIndex (dhat : Fin K → ℝ)
(hmono : ∀ {k l : Fin K}, k.val ≤ l.val → dhat k ≤ dhat l) :
FiniteIndex K :=
FiniteIndex.fromMeasureScore P.μ S.factualZ S.measurable_factualZ dhat hmono
def toObservedBridge reviewed
⚑ flagged
Causalean.PO.ID.Exact.MultipleInstrumentIV.POMultipleIVSystem
The observed bridge assembled from the PO system, with the two conditional-mean fields derived (not assumed) from consistency and instrument independence.
Definition (Lean source)
def toObservedBridge (hK : 0 < K) (hA : S.Assumptions)
(dhat : Fin K → ℝ)
(hmono : ∀ {k l : Fin K}, k.val ≤ l.val → 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.μ) :
ResponseTypeStats.PopulationBridge.ObservedBridge P.μ S.factualZ S.factualD
S.factualY (S.toFiniteIndex dhat hmono) (S.toPopulationBridge hK) where
isProbability := P.isProb
rho_eq_zMass := S.rho_eq_zMass dhat hmono
outcome_cell := fun k =>
S.outcome_cell_eq hK hA k (hZpos k) hY1 hY0
baseTreatment := S.baseTreatment hK
treatment_cell := fun k =>
S.treatment_cell_eq hK hA k (hZpos k)
theorem observedBeta2SLS_eq_responseTypeWeightedSum reviewed
⚑ flagged
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
IsFiniteMeasure P.μ
hK :
0 < K
hA :
S.Assumptions
dhat :
Fin K → ℝ
hmono :
∀ {k l : Fin K}
if
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.μ
hYInt :
Integrable (fun ω => (S.toFiniteIndex dhat hmono).centeredIndex (S.factualZ ω) * S.factualY ω) P.μ
hDInt :
Integrable (fun ω => (S.toFiniteIndex dhat hmono).centeredIndex (S.factualZ ω) * boolToReal (S.factualD ω)) P.μ
hden :
ResponseTypeStats.PopulationBridge.observedFirstStageMoment P.μ S.factualZ S.factualD (S.toFiniteIndex dhat hmono)
≠ 0
conclusion
ResponseTypeStats.PopulationBridge.observedBeta2SLS P.μ S.factualZ S.factualD S.factualY (S.toFiniteIndex dhat hmono)
= (S.toPopulationBridge hK).stats.responseTypeEstimand (S.toFiniteIndex dhat hmono)
Proof (Lean source)
theorem observedBeta2SLS_eq_responseTypeWeightedSum
[IsFiniteMeasure P.μ] (hK : 0 < K) (hA : S.Assumptions)
(dhat : Fin K → ℝ)
(hmono : ∀ {k l : Fin K}, k.val ≤ l.val → 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.μ)
(hYInt : Integrable
(fun ω => (S.toFiniteIndex dhat hmono).centeredIndex (S.factualZ ω) * S.factualY ω) P.μ)
(hDInt : Integrable
(fun ω => (S.toFiniteIndex dhat hmono).centeredIndex (S.factualZ ω)
* boolToReal (S.factualD ω)) P.μ)
(hden : ResponseTypeStats.PopulationBridge.observedFirstStageMoment
P.μ S.factualZ S.factualD (S.toFiniteIndex dhat hmono) ≠ 0) :
ResponseTypeStats.PopulationBridge.observedBeta2SLS
P.μ S.factualZ S.factualD S.factualY (S.toFiniteIndex dhat hmono)
= (S.toPopulationBridge hK).stats.responseTypeEstimand (S.toFiniteIndex dhat hmono) :=
(S.toObservedBridge hK hA dhat hmono hZpos hY1 hY0).observedBeta2SLS_eq_responseTypeWeightedSum
S.measurable_factualZ hYInt hDInt hden
23 supporting declarations (lemmas, instances)
-
measurable_DofZlemma — The potential treatment under any instrument support point is measurable.Proof (Lean source)
lemma measurable_DofZ (k : Fin K) : Measurable (S.DofZ k) := S.dVar.measurable_cfUnder S.zVar k -
measurable_YofDlemma — The potential outcome under either treatment arm is measurable.Proof (Lean source)
lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurable_factualZlemma — The factual instrument value is measurable.conclusionMeasurable S.factualZProof (Lean source)
lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — The factual treatment value is measurable.conclusionMeasurable S.factualDProof (Lean source)
lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The factual outcome value is measurable.conclusionMeasurable S.factualYProof (Lean source)
lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_responseTypelemma — The response-type map collecting all treatment responses is measurable.conclusionMeasurable S.responseTypeProof (Lean source)
lemma measurable_responseType : Measurable S.responseType := measurable_pi_lambda _ (fun k => S.measurable_DofZ k) -
measurableSet_gEventlemma — Each response-type cell is measurable.Proof (Lean source)
lemma measurableSet_gEvent (g : ResponseType K) : MeasurableSet (S.gEvent g) := S.measurable_responseType (measurableSet_singleton g) -
measurableSet_zEventlemma — Each instrument support cell is measurable.Proof (Lean source)
lemma measurableSet_zEvent (k : Fin K) : MeasurableSet (S.zEvent k) := S.zVar.measurableSet_event k (measurableSet_singleton k) -
measurable_YofDofZlemma — The outcome under the treatment induced by an instrument support point is measurable.Proof (Lean source)
lemma measurable_YofDofZ (k : Fin K) : Measurable (S.YofDofZ k) := by unfold YofDofZ exact Measurable.ite (S.measurable_DofZ k (MeasurableSet.singleton true)) (S.measurable_YofD true) (S.measurable_YofD false) -
DofZ_eq_factualD_on_zEventlemma — On {Z = zᵏ}, the counterfactual treatment D(zᵏ) equals the factual D.hypothesesconclusionS.DofZ k ω = S.factualD ωProof (Lean source)
lemma DofZ_eq_factualD_on_zEvent (hA : S.Assumptions) (k : Fin K) {ω : P.Ω} (hω : ω ∈ S.zEvent k) : S.DofZ k ω = S.factualD ω := POVar.cf_eq_factual_on_event hA.consistency S.dVar S.zVar k S.hZD.symm hω -
factualY_eq_YofD_factualDlemma — Factual Y equals Y(factualD) pointwise.hypotheseshA :S.Assumptionsω :P.ΩconclusionS.factualY ω = S.YofD (S.factualD ω) ωProof (Lean source)
lemma factualY_eq_YofD_factualD (hA : S.Assumptions) (ω : P.Ω) : S.factualY ω = S.YofD (S.factualD ω) ω := POVar.factual_eq_cfUnder_self_selected hA.consistency S.yVar S.dVar S.hDY.symm ω -
DofZ_eq_on_gEventlemma — On {G = g}, the potential treatment D(zᵏ) is the constant g k.Proof (Lean source)
lemma DofZ_eq_on_gEvent (g : ResponseType K) (k : Fin K) {ω : P.Ω} (hω : ω ∈ S.gEvent g) : S.DofZ k ω = g k := by have : S.responseType ω = g := hω calc S.DofZ k ω = S.responseType ω k := rfl _ = g k := by rw [this] -
treatmentDroptheorem — E[D | Z = zᵏ] = E[D(zᵏ)] (0/1-coded).hypothesesconclusioneventCondExp P.μ (S.zEvent k) (fun ω => boolToReal (S.factualD ω))= ∫ ω, boolToReal (S.DofZ k ω) ∂P.μProof (Lean source)
theorem treatmentDrop [IsFiniteMeasure P.μ] (hA : S.Assumptions) (k : Fin K) (hZk : P.μ (S.zEvent k) ≠ 0) : eventCondExp P.μ (S.zEvent k) (fun ω => boolToReal (S.factualD ω)) = ∫ ω, boolToReal (S.DofZ k ω) ∂P.μ := by let h_proj : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → ℝ := fun f => boolToReal ((f (0 : Fin 3)) : Bool) have hh_meas : Measurable h_proj := by -- Instance search no longer unfolds `cfCell` to see `n = 3`, so supply the -- coordinate measurable-space family at index type `Fin 3` directly. let _ : ∀ i : Fin 3, MeasurableSpace ((S.cfCell k).type i) := fun i => (S.cfCell k).inst i change Measurable fun f : ∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i => boolToReal ((f (0 : Fin 3)) : Bool) exact (by fun_prop : Measurable fun b : Bool => boolToReal b).comp (measurable_pi_apply (0 : Fin 3)) have hF_eq : ∀ ω ∈ S.zVar.event k, boolToReal (S.factualD ω) = h_proj ((S.cfCell k).jointValue ω) := by intro ω hω rw [← S.DofZ_eq_factualD_on_zEvent hA k hω] dsimp [h_proj] have hJV0 : ((S.cfCell k).jointValue ω (0 : Fin 3) : Bool) = S.DofZ k ω := rfl rw [hJV0] change eventCondExp P.μ (S.zVar.event k) (fun ω => boolToReal (S.factualD ω)) = ∫ ω, boolToReal (S.DofZ k ω) ∂P.μ rw [POSystem.eventCondExp_of_consistency_IndepCF (hA.instrumentIndep k) (a := S.zVar) hh_meas (measurableSet_singleton k) (ae_restrict_of_forall_mem (μ := P.μ) (S.measurableSet_zEvent k) hF_eq) hZk (measure_ne_top _ _)] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω dsimp [h_proj] have hJV0 : ((S.cfCell k).jointValue ω (0 : Fin 3) : Bool) = S.DofZ k ω := rfl rw [hJV0] -
outcomeDroptheorem — E[Y | Z = zᵏ] = E[Y(D(zᵏ))].hypothesesIsFiniteMeasure P.μhA :S.Assumptionsk :Fin KhZk :P.μ (S.zEvent k) ≠ 0hY1 :Integrable (S.YofD true) P.μhY0 :Integrable (S.YofD false) P.μconclusioneventCondExp P.μ (S.zEvent k) S.factualY = ∫ ω, S.YofDofZ k ω ∂P.μProof (Lean source)
theorem outcomeDrop [IsFiniteMeasure P.μ] (hA : S.Assumptions) (k : Fin K) (hZk : P.μ (S.zEvent k) ≠ 0) (hY1 : Integrable (S.YofD true) P.μ) (hY0 : Integrable (S.YofD false) P.μ) : eventCondExp P.μ (S.zEvent k) S.factualY = ∫ ω, S.YofDofZ k ω ∂P.μ := by have _hY1 : Integrable (S.YofD true) P.μ := hY1 have _hY0 : Integrable (S.YofD false) P.μ := hY0 let getD : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → Bool := fun f => ((f (0 : Fin 3)) : Bool) let getY1 : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → ℝ := fun f => ((f (1 : Fin 3)) : ℝ) let getY0 : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → ℝ := fun f => ((f (2 : Fin 3)) : ℝ) let h_proj : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → ℝ := fun f => cond (getD f) (getY1 f) (getY0 f) have hh_meas : Measurable h_proj := by -- Instance search no longer unfolds `cfCell` to see `n = 3`, so supply the -- coordinate measurable-space family at index type `Fin 3` directly. let _ : ∀ i : Fin 3, MeasurableSpace ((S.cfCell k).type i) := fun i => (S.cfCell k).inst i have hD_meas : Measurable getD := by dsimp [getD] exact measurable_pi_apply (0 : Fin 3) have hY1_meas : Measurable getY1 := by dsimp [getY1] exact measurable_pi_apply (1 : Fin 3) have hY0_meas : Measurable getY0 := by dsimp [getY0] exact measurable_pi_apply (2 : Fin 3) have hif : Measurable fun f => if getD f = true then getY1 f else getY0 f := by refine Measurable.ite ?_ ?_ ?_ · exact hD_meas (MeasurableSet.singleton true) · exact hY1_meas · exact hY0_meas simpa [h_proj, Bool.cond_eq_ite] using hif have hF_eq : ∀ ω ∈ S.zVar.event k, S.factualY ω = h_proj ((S.cfCell k).jointValue ω) := by intro ω hω rw [S.factualY_eq_YofD_factualD hA ω, ← S.DofZ_eq_factualD_on_zEvent hA k hω] dsimp [h_proj, getD, getY1, getY0] have hJV0 : ((S.cfCell k).jointValue ω (0 : Fin 3) : Bool) = S.DofZ k ω := rfl have hJV1 : ((S.cfCell k).jointValue ω (1 : Fin 3) : ℝ) = S.YofD true ω := rfl have hJV2 : ((S.cfCell k).jointValue ω (2 : Fin 3) : ℝ) = S.YofD false ω := rfl rw [hJV0, hJV1, hJV2] cases S.DofZ k ω <;> simp change eventCondExp P.μ (S.zVar.event k) S.factualY = ∫ ω, S.YofDofZ k ω ∂P.μ rw [POSystem.eventCondExp_of_consistency_IndepCF (hA.instrumentIndep k) (a := S.zVar) hh_meas (measurableSet_singleton k) (ae_restrict_of_forall_mem (μ := P.μ) (S.measurableSet_zEvent k) hF_eq) hZk (measure_ne_top _ _)] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω dsimp [h_proj, getD, getY1, getY0] have hJV0 : ((S.cfCell k).jointValue ω (0 : Fin 3) : Bool) = S.DofZ k ω := rfl have hJV1 : ((S.cfCell k).jointValue ω (1 : Fin 3) : ℝ) = S.YofD true ω := rfl have hJV2 : ((S.cfCell k).jointValue ω (2 : Fin 3) : ℝ) = S.YofD false ω := rfl rw [hJV0, hJV1, hJV2] unfold YofDofZ cases S.DofZ k ω <;> simp -
gEvent_pairwise_disjointlemma — The response-type events are pairwise disjoint. -
gEvent_iUnionlemma — The response-type events cover the sample space.conclusion(⋃ g : ResponseType K, S.gEvent g) = univProof (Lean source)
-
integral_partitionlemma — Total law over response types for an integrable integrand.hypothesesconclusion∫ ω, f ω ∂P.μ= ∑ g : ResponseType K, (P.μ (S.gEvent g)).toReal * eventCondExp P.μ (S.gEvent g) fProof (Lean source)
lemma integral_partition [IsFiniteMeasure P.μ] {f : P.Ω → ℝ} (hf : Integrable f P.μ) : ∫ ω, f ω ∂P.μ = ∑ g : ResponseType K, (P.μ (S.gEvent g)).toReal * eventCondExp P.μ (S.gEvent g) f := integral_eq_sum_measure_mul_eventCondExp P.μ S.gEvent S.measurableSet_gEvent S.gEvent_pairwise_disjoint S.gEvent_iUnion f hf -
mass_nonneglemma — Response-type masses are nonnegative because they are real-valued probabilities.Proof (Lean source)
lemma mass_nonneg (g : ResponseType K) : 0 ≤ S.mass g := ENNReal.toReal_nonneg -
mass_sum_onelemma — Response-type masses sum to one.conclusion∑ g : ResponseType K, S.mass g = 1Proof (Lean source)
lemma mass_sum_one : ∑ g : ResponseType K, S.mass g = 1 := by have hsum : (Finset.univ).sum (fun g : ResponseType K => (P.μ (S.responseType ⁻¹' ({g} : Set (ResponseType K)))).toReal) = (P.μ (S.responseType ⁻¹' (Set.univ : Set (ResponseType K)))).toReal := by simpa [Measure.real] using (MeasureTheory.sum_measureReal_preimage_singleton (μ := P.μ) (s := (Finset.univ : Finset (ResponseType K))) (f := S.responseType) (hf := by intro g _hg exact S.measurable_responseType (measurableSet_singleton g)) (h := by intro g _hg exact measure_ne_top _ _)) simpa [mass, gEvent, Set.preimage_univ, IsProbabilityMeasure.measure_univ] using hsum -
telescoped_eqlemma — The telescoped adjacent step at support point k collapses to the difference of endpoint treatments: Σ_{j≤k}(d_j - d_{j-1}) = g k - g 0.hypothesesconclusionResponseTypeStats.PopulationBridge.telescopedTypeStep g k= boolToReal (g k) - boolToReal (g (S.z0 hK))Proof (Lean source)
lemma telescoped_eq (hK : 0 < K) (g : ResponseType K) (k : Fin K) : ResponseTypeStats.PopulationBridge.telescopedTypeStep g k = boolToReal (g k) - boolToReal (g (S.z0 hK)) := by classical let a : ℕ → ℝ := fun n => if h : n < K then boolToReal (g ⟨n, h⟩) else 0 have htel : ∀ n : ℕ, (∑ r ∈ range n, (a (r + 1) - a r)) = a n - a 0 := by intro n induction n with | zero => simp | succ n ih => rw [Finset.sum_range_succ, ih] ring have hsum : (∑ j ∈ (Finset.univ.filter fun j : Adj K => j.1.val ≤ k.val), typeStep g j) = ∑ r ∈ range k.val, (a (r + 1) - a r) := by refine Finset.sum_nbij (fun j : Adj K => j.1.val - 1) ?_ ?_ ?_ ?_ · intro j hj have hjle : j.1.val ≤ k.val := by simpa using hj rw [Finset.mem_range] have hpos : 0 < j.1.val := j.2 omega · intro j1 hj1 j2 hj2 h apply Subtype.ext apply Fin.ext have hj1le : j1.1.val ≤ k.val := by simpa using hj1 have hj2le : j2.1.val ≤ k.val := by simpa using hj2 have hpos1 : 0 < j1.1.val := j1.2 have hpos2 : 0 < j2.1.val := j2.2 change j1.1.val - 1 = j2.1.val - 1 at h omega · intro r hr have hrlt : r < k.val := by simpa using hr refine ⟨⟨⟨r + 1, ?_⟩, ?_⟩, ?_, ?_⟩ · exact Nat.lt_of_le_of_lt (Nat.succ_le_of_lt hrlt) k.isLt · exact Nat.succ_pos r · refine Finset.mem_filter.mpr ⟨Finset.mem_univ _, ?_⟩ show r + 1 ≤ k.val omega · change r + 1 - 1 = r omega · intro j hj have hjle : j.1.val ≤ k.val := by simpa using hj have hsucc : j.1.val - 1 + 1 = j.1.val := Nat.sub_add_cancel (Nat.succ_le_of_lt j.2) have hpred_lt : j.1.val - 1 < K := Nat.lt_of_le_of_lt (Nat.sub_le _ _) j.1.isLt simp [typeStep, Adj.upper, Adj.lower, a, hpred_lt, hsucc] unfold ResponseTypeStats.PopulationBridge.telescopedTypeStep rw [Finset.sum_ite] simp only [Finset.sum_const_zero, add_zero] rw [hsum, htel] have hak : a k.val = boolToReal (g k) := by simp [a, k.isLt] have ha0 : a 0 = boolToReal (g (S.z0 hK)) := by simp [a, hK, z0] rw [hak, ha0] -
treatment_cell_eqtheorem — Treatment cell identity: E[D | Z = zᵏ] = baseTreatment + treatmentAtSupport k.hypothesesconclusioneventCondExp P.μ (S.zEvent k) (fun ω => boolToReal (S.factualD ω))= S.baseTreatment hK + (S.toPopulationBridge hK).treatmentAtSupport kProof (Lean source)
theorem treatment_cell_eq [IsFiniteMeasure P.μ] (hK : 0 < K) (hA : S.Assumptions) (k : Fin K) (hZk : P.μ (S.zEvent k) ≠ 0) : eventCondExp P.μ (S.zEvent k) (fun ω => boolToReal (S.factualD ω)) = S.baseTreatment hK + (S.toPopulationBridge hK).treatmentAtSupport k := by have hDint : ∀ q : Fin K, Integrable (fun ω => boolToReal (S.DofZ q ω)) P.μ := by intro q have hbdd : ∀ ω, |boolToReal (S.DofZ q ω)| ≤ (1 : ℝ) := by intro ω cases S.DofZ q ω <;> simp [boolToReal] exact (MeasureTheory.integrable_const (1 : ℝ)).mono' (((by fun_prop : Measurable fun b : Bool => boolToReal b).comp (S.measurable_DofZ q)).aestronglyMeasurable) (Filter.Eventually.of_forall hbdd) have hCell : ∀ (q : Fin K) (g : ResponseType K), S.mass g * eventCondExp P.μ (S.gEvent g) (fun ω => boolToReal (S.DofZ q ω)) = S.mass g * boolToReal (g q) := by intro q g calc S.mass g * eventCondExp P.μ (S.gEvent g) (fun ω => boolToReal (S.DofZ q ω)) = eventCondExp P.μ (S.gEvent g) (fun ω => boolToReal (S.DofZ q ω)) * S.mass g := by ring _ = ∫ ω in S.gEvent g, boolToReal (S.DofZ q ω) ∂P.μ := by rw [mass, eventCondExp_mul_measure_toReal _ _ (measure_ne_top _ _)] _ = ∫ ω in S.gEvent g, boolToReal (g q) ∂P.μ := by refine MeasureTheory.setIntegral_congr_fun (S.measurableSet_gEvent g) ?_ intro ω hω dsimp rw [S.DofZ_eq_on_gEvent g q hω] _ = boolToReal (g q) * S.mass g := by simp [mass, Measure.real, mul_comm] _ = S.mass g * boolToReal (g q) := by ring have hInt : ∫ ω, boolToReal (S.DofZ k ω) ∂P.μ = ∑ g : ResponseType K, S.mass g * boolToReal (g k) := by rw [S.integral_partition (hDint k)] refine Finset.sum_congr rfl ?_ intro g _ simpa [mass] using hCell k g have hBase : S.baseTreatment hK = ∑ g : ResponseType K, S.mass g * boolToReal (g (S.z0 hK)) := by unfold baseTreatment rw [S.integral_partition (hDint (S.z0 hK))] refine Finset.sum_congr rfl ?_ intro g _ simpa [mass] using hCell (S.z0 hK) g have hTreat : (S.toPopulationBridge hK).treatmentAtSupport k = ∑ g : ResponseType K, S.mass g * (boolToReal (g k) - boolToReal (g (S.z0 hK))) := by unfold ResponseTypeStats.PopulationBridge.treatmentAtSupport toPopulationBridge toStats refine Finset.sum_congr rfl ?_ intro g _ rw [S.telescoped_eq hK g k] rw [S.treatmentDrop hA k hZk, hInt, hBase, hTreat] rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl ?_ intro g _ ring -
outcome_cell_eqtheorem — Outcome cell identity: E[Y | Z = zᵏ] = outcomeAtSupport k.hypothesesIsFiniteMeasure P.μhK :0 < KhA :S.Assumptionsk :Fin KhZk :P.μ (S.zEvent k) ≠ 0hY1 :Integrable (S.YofD true) P.μhY0 :Integrable (S.YofD false) P.μconclusioneventCondExp P.μ (S.zEvent k) S.factualY = (S.toPopulationBridge hK).outcomeAtSupport kProof (Lean source)
theorem outcome_cell_eq [IsFiniteMeasure P.μ] (hK : 0 < K) (hA : S.Assumptions) (k : Fin K) (hZk : P.μ (S.zEvent k) ≠ 0) (hY1 : Integrable (S.YofD true) P.μ) (hY0 : Integrable (S.YofD false) P.μ) : eventCondExp P.μ (S.zEvent k) S.factualY = (S.toPopulationBridge hK).outcomeAtSupport k := by have hYDZ_bdd : ∀ q : Fin K, ∀ ω, |S.YofDofZ q ω| ≤ |S.YofD true ω| + |S.YofD false ω| := by intro q ω have h1 := abs_nonneg (S.YofD true ω) have h0 := abs_nonneg (S.YofD false ω) unfold YofDofZ cases S.DofZ q ω <;> simp [h1, h0] have hYDZ_int : ∀ q : Fin K, Integrable (S.YofDofZ q) P.μ := by intro q exact (hY1.norm.add hY0.norm).mono' (S.measurable_YofDofZ q).aestronglyMeasurable (Filter.Eventually.of_forall (hYDZ_bdd q)) have hCE : ∀ (q : Fin K) (g : ResponseType K), eventCondExp P.μ (S.gEvent g) (S.YofDofZ q) = eventCondExp P.μ (S.gEvent g) (S.YofD false) + boolToReal (g q) * S.effect g := by intro q g let c : ℝ := boolToReal (g q) have hcongr : eventCondExp P.μ (S.gEvent g) (S.YofDofZ q) = eventCondExp P.μ (S.gEvent g) (fun ω => S.YofD false ω + c * (S.YofD true ω - S.YofD false ω)) := by apply eventCondExp_congr_on P.μ (S.measurableSet_gEvent g) intro ω hω unfold YofDofZ rw [S.DofZ_eq_on_gEvent g q hω] dsimp [c] cases g q <;> simp [boolToReal] calc eventCondExp P.μ (S.gEvent g) (S.YofDofZ q) = eventCondExp P.μ (S.gEvent g) (fun ω => S.YofD false ω + c * (S.YofD true ω - S.YofD false ω)) := hcongr _ = eventCondExp P.μ (S.gEvent g) (S.YofD false) + eventCondExp P.μ (S.gEvent g) (fun ω => c * (S.YofD true ω - S.YofD false ω)) := by change eventCondExp P.μ (S.gEvent g) ((S.YofD false) + fun ω => c * (S.YofD true ω - S.YofD false ω)) = eventCondExp P.μ (S.gEvent g) (S.YofD false) + eventCondExp P.μ (S.gEvent g) (fun ω => c * (S.YofD true ω - S.YofD false ω)) rw [eventCondExp_add] · exact hY0.integrableOn · exact (hY1.integrableOn.sub hY0.integrableOn).const_mul c _ = eventCondExp P.μ (S.gEvent g) (S.YofD false) + c * eventCondExp P.μ (S.gEvent g) (fun ω => S.YofD true ω - S.YofD false ω) := by rw [eventCondExp_smul] _ = eventCondExp P.μ (S.gEvent g) (S.YofD false) + boolToReal (g q) * S.effect g := by rfl have hTerm : ∀ g : ResponseType K, eventCondExp P.μ (S.gEvent g) (S.YofDofZ k) = S.baseOutcome hK g + ResponseTypeStats.PopulationBridge.telescopedTypeStep g k * S.effect g := by intro g unfold baseOutcome rw [hCE k g, hCE (S.z0 hK) g, S.telescoped_eq hK g k] ring have hInt : ∫ ω, S.YofDofZ k ω ∂P.μ = ∑ g : ResponseType K, S.mass g * eventCondExp P.μ (S.gEvent g) (S.YofDofZ k) := by rw [S.integral_partition (hYDZ_int k)] refine Finset.sum_congr rfl ?_ intro g _ rfl rw [S.outcomeDrop hA k hZk hY1 hY0, hInt] unfold ResponseTypeStats.PopulationBridge.outcomeAtSupport toPopulationBridge toStats refine Finset.sum_congr rfl ?_ intro g _ rw [hTerm g] -
rho_eq_zMasslemma — The instrument masses ρ_k from toFiniteIndex are the probabilities of the observed instrument cells.hypothesesconclusion(S.toFiniteIndex dhat hmono).rho k= (P.μ (ResponseTypeStats.PopulationBridge.zEvent S.factualZ k)).toReal